Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
114 changes: 105 additions & 9 deletions dag/gunbc/runner/runner_host_file_converge.dag
Original file line number Diff line number Diff line change
Expand Up @@ -30,6 +30,13 @@ import gunbc.fleet_known_hosts_anchor { FleetSshExecutionContext, SshTarget }
import gunbc.fleet_reach_endpoint { fleet_probe_endpoint_for }
import gunbc.file_access { FileTreeScope }
import gunbc.typed_argv_exec { typed_argv_exec_over_fleet_ssh, TypedArgvExecOutcome, TypedArgvExecConverged, TypedArgvExecRefused }
import extdeps.exec.command { argv_words }
import extdeps.tools.stat { stat_file_type_command }
import gunbc.host_effect { FleetSsh }
import gunbc.live_deploy.member_observe {
EntryPresence, EntryPresent, EntryAbsent, EntryPresenceIndeterminate,
ObservationArm, OverTransport, entry_presence,
}
import gunbc.typed_remote_file_write {
RemoteFileMode,
RemoteFileModeOwnerReadWriteWorldRead,
Expand Down Expand Up @@ -374,17 +381,74 @@ type RunnerHostFileStanding
| HostFileAbsent
| HostFileUnobservable { reason: String }

// `test -e` answers 0 or 1 and nothing else on its own; any other exit means the test did not run.
fn classify_host_file_presence(exit_code: Int, stderr: String) -> RunnerHostFileStanding? {
// THE PROBE READS METADATA; IT DOES NOT ANSWER PRESENCE. This was `test -e`, whose exit 1 was read
// here as HostFileAbsent -- and GNU `test -e` is stat(path) == 0, so ENOENT, EACCES on an ancestor
// directory, ELOOP, ENOTDIR and EIO all answer 1 with an empty stderr. "The file is not there" and
// "I could not look" arrived as one value, and they license opposite actions: the absent arm walks
// into the write-admission and comparison path for a file this module exists to keep root-owned and
// non-injectable. `extdeps.tools.stat` `stat.File.FileType` states that defect as the whole reason
// it exists and reports the GNU file-type word on success, saying only that the metadata read
// FAILED otherwise -- so the read has two honest outcomes here and absence is not one of them.
type RunnerHostFileMetadataReading
= HostFileMetadataRead { file_type: String }
| HostFileMetadataUnread { cause: String }

// A COMPLETED READ THAT PRINTED NOTHING IS NOT A TYPE. Exit success is a fact about the CALL, never
// about whether the output carrying the answer arrived, so an empty `%F` is unread rather than a
// nameless kind -- the same separation gunbc.fabric.fabric_cell_acquire draws over this operation.
fn classify_host_file_metadata(exit_code: Int, stdout: String, stderr: String) -> RunnerHostFileMetadataReading {
if exit_code == 0 {
none
} else if exit_code == 1 {
Present { value: HostFileAbsent }
let w = trim(s: stdout)
if w == "" {
HostFileMetadataUnread { cause: "the metadata read exited successfully and printed no file type, so the path kind is unanswered" }
} else {
HostFileMetadataRead { file_type: w }
}
} else {
Present { value: HostFileUnobservable { reason: join(["presence test exit=", to_string(exit_code), " ", trim(s: stderr)], "") } }
HostFileMetadataUnread { cause: join(["stat could not read the path's metadata; exit=", to_string(exit_code), " ", trim(s: stderr)], "") }
}
}

// THE THREE OUTCOMES THE PROBE OWES, WITH ABSENCE ESTABLISHED BY THE PARENT AND NEVER BY THE PROBE'S
// SILENCE. The read decides presence; when it failed, what the containing directory already said
// about this entry decides whether nothing is there or nobody could look. The parent standing is
// gunbc.live_deploy.member_observe `entry_presence`, the landed authority for that rule over a
// transport, consumed rather than restated (DESIGN section 3).
type RunnerHostFilePathStanding
= HostFilePathPresent { file_type: String }
| HostFilePathAbsent
| HostFilePathUnreadable { cause: String }

fn classify_host_file_path(reading: RunnerHostFileMetadataReading, parent: EntryPresence) -> RunnerHostFilePathStanding {
match reading {
HostFileMetadataRead { file_type: t } => HostFilePathPresent { file_type: t }
HostFileMetadataUnread { cause: c } =>
match parent {
EntryAbsent => HostFilePathAbsent
EntryPresent =>
HostFilePathUnreadable { cause: join(["the containing directory holds this entry and ", c], "") }
EntryPresenceIndeterminate { cause: pc } =>
HostFilePathUnreadable { cause: join([c, "; and the containing directory could not establish absence: ", pc], "") }
}
}
}

// THE SETTLED ARM, AT THE STANDING'S OWN GRAIN. A path that was read continues into the byte
// comparison and is not settled here, so this answers `none` for it; absence and unreadability are
// settled, and they land on DIFFERENT standings -- which is the whole repair, because `test -e`
// sent both to HostFileAbsent and HostFileAbsent plans a write.
fn runner_host_file_settled_standing(st: RunnerHostFilePathStanding) -> RunnerHostFileStanding? {
match st {
HostFilePathPresent { file_type: _ } => none
HostFilePathAbsent => Present { value: HostFileAbsent }
HostFilePathUnreadable { cause: c } => Present { value: HostFileUnobservable { reason: c } }
}
}

fn runner_host_file_metadata_probe_argv(path: String) -> List<String> {
argv_words(command: stat_file_type_command(path: path))
}

// WHO CAN CHANGE A FILE IS PART OF WHAT THE FILE IS, when root evaluates it. A byte-exact needrestart
// snippet that the CI user owns, or that sits in a directory the CI user can write, is a root-code
// injection point that merely happens to hold the right bytes today. So every path the file depends on
Expand Down Expand Up @@ -762,6 +826,33 @@ fn runner_host_file_standing_of_report(report: RemoteFileComparisonReport) -> Ru
}
}

// THE PARENT IS ENUMERATED ONLY WHEN THE READ FAILED, because that is the only outcome whose
// meaning the parent decides. `entry_presence` is a remote leg -- `ls -1 -A --` of the parent over
// the same transport, recursing up the ancestor chain when a listing refuses -- so asking it beside
// a read that already answered buys a standing the classifier discards (DESIGN section 2, and
// section 6's bare minimum cost). Both of the classifier's parent-dependent outcomes stay inhabited
// by production, because this arm is the only route that can reach them (DESIGN section 3c).
fn observe_runner_host_file_path(
subject: RunnerHostFileSubject,
context: FleetSshExecutionContext,
path: String,
reading: RunnerHostFileMetadataReading,
) -> RunnerHostFilePathStanding
uses net: Network
{
match reading {
HostFileMetadataRead { file_type: t } => HostFilePathPresent { file_type: t }
HostFileMetadataUnread { cause: _ } =>
classify_host_file_path(
reading: reading,
parent: entry_presence(
arm: OverTransport { transport: FleetSsh { target: subject.target, context: context } },
path: path,
),
)
}
}

// THE PLAN'S "IDENTICAL" AND THE APPLY'S "CONVERGED" ARE ONE JUDGMENT OVER ONE LEG. The comparison is
// typed_remote_file_write's own far-side `cmp -s -` with the declared bytes on stdin, classified by
// its own exit vocabulary, so an observation cannot call a file converged that the write's read-back
Expand All @@ -773,10 +864,15 @@ fn observe_runner_host_file_content(
) -> RunnerHostFileStanding
uses net: Network
{
match typed_argv_exec_over_fleet_ssh(target: subject.target, context: context, argv: ["test", "-e", file.path as String]) {
match typed_argv_exec_over_fleet_ssh(target: subject.target, context: context, argv: runner_host_file_metadata_probe_argv(path: file.path as String)) {
TypedArgvExecRefused { reason: why } => HostFileUnobservable { reason: why }
TypedArgvExecConverged { result: presence } =>
match classify_host_file_presence(exit_code: presence.exit_code, stderr: presence.stderr) {
TypedArgvExecConverged { result: metadata } =>
match runner_host_file_settled_standing(st: observe_runner_host_file_path(
subject: subject,
context: context,
path: file.path as String,
reading: classify_host_file_metadata(exit_code: metadata.exit_code, stdout: metadata.stdout, stderr: metadata.stderr),
)) {
Present { value: settled } => settled
Absent =>
match runner_host_file_write_admission(file: file) {
Expand Down
130 changes: 120 additions & 10 deletions dag/test/claim/runner/runner_host_file_converge_witness_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -51,6 +51,9 @@ import gunbc.typed_remote_file_write {
}
import extdeps.external_authority { CitedToAuthority, ExternalAuthority }
import extdeps.uri { Uri, File }
import extdeps.exec.command { argv_words }
import extdeps.tools.stat { stat_file_type_command }
import gunbc.live_deploy.member_observe { EntryPresence, EntryPresent, EntryAbsent, EntryPresenceIndeterminate }
import gunbc.runner_host_file_converge {
RunnerHostFileDesired,
RunnerHostFilesDesired,
Expand All @@ -67,7 +70,17 @@ import gunbc.runner_host_file_converge {
HostFileDiffers,
HostFileAbsent,
HostFileUnobservable,
classify_host_file_presence,
RunnerHostFileMetadataReading,
HostFileMetadataRead,
HostFileMetadataUnread,
classify_host_file_metadata,
RunnerHostFilePathStanding,
HostFilePathPresent,
HostFilePathAbsent,
HostFilePathUnreadable,
classify_host_file_path,
runner_host_file_settled_standing,
runner_host_file_metadata_probe_argv,
RunnerHostFileStanding,
RunnerHostPathMetadata,
PathsRootOnly,
Expand Down Expand Up @@ -337,20 +350,117 @@ fn standing_is_unobservable(standing: RunnerHostFileStanding) -> Bool {
}
}

test fn presence_zero_continues_one_is_absent_other_is_unobservable() -> Bool {
let continues = match classify_host_file_presence(exit_code: 0, stderr: "") {
Absent => true
Present { value: _ } => false
fn path_is_present(st: RunnerHostFilePathStanding) -> Bool {
match st { HostFilePathPresent { file_type: _ } => true HostFilePathAbsent => false HostFilePathUnreadable { cause: _ } => false }
}

fn path_is_absent(st: RunnerHostFilePathStanding) -> Bool {
match st { HostFilePathAbsent => true HostFilePathPresent { file_type: _ } => false HostFilePathUnreadable { cause: _ } => false }
}

fn path_is_unreadable(st: RunnerHostFilePathStanding) -> Bool {
match st { HostFilePathUnreadable { cause: _ } => true HostFilePathPresent { file_type: _ } => false HostFilePathAbsent => false }
}

// A metadata read that FAILED is the outcome `test -e` could not distinguish from an absence: both
// were exit 1 with an empty stderr. Here the same failed read reaches three different standings
// depending on what the containing directory established, and the middle row is the discriminating
// one: the parent HOLDS the entry, so the read failed for a reason that is not absence -- EACCES on
// an ancestor, ELOOP, ENOTDIR, EIO -- and it must reach unreadable. A classifier that collapsed the
// failed read back to absence reds on that row alone; one that merely separated exit 0 from exit 1
// would pass every row here, which is why the unread cause is held constant across all three.
test fn a_metadata_read_that_failed_is_absent_only_when_the_parent_lacks_the_entry() -> Bool {
let unread = HostFileMetadataUnread { cause: "stat could not read the path's metadata; exit=1 " }
path_is_absent(st: classify_host_file_path(reading: unread, parent: EntryAbsent))
&& path_is_unreadable(st: classify_host_file_path(reading: unread, parent: EntryPresent))
&& path_is_unreadable(st: classify_host_file_path(
reading: unread,
parent: EntryPresenceIndeterminate { cause: "listing /etc/needrestart/conf.d failed" },
))
}

fn settled_is_unobservable(st: RunnerHostFilePathStanding) -> Bool {
match runner_host_file_settled_standing(st: st) {
Absent => false
Present { value: s } => standing_is_unobservable(standing: s) && !standing_is_absent(standing: s)
}
let absent = match classify_host_file_presence(exit_code: 1, stderr: "") {
Present { value: st } => standing_is_absent(standing: st)
}

fn settled_is_absent(st: RunnerHostFilePathStanding) -> Bool {
match runner_host_file_settled_standing(st: st) {
Absent => false
Present { value: s } => standing_is_absent(standing: s)
}
}

fn settles_nothing(st: RunnerHostFilePathStanding) -> Bool {
match runner_host_file_settled_standing(st: st) {
Absent => true
Present { value: _ } => false
}
let unobservable = match classify_host_file_presence(exit_code: 2, stderr: "test: extra argument") {
Present { value: st } => standing_is_unobservable(standing: st)
}

// THE BRIEF'S OWN SENTENCE, AT THE STANDING GRAIN: a metadata read that did not happen must reach
// HostFileUnobservable carrying the failure and must NEVER reach HostFileAbsent. Under `test -e`
// both of these rows were exit 1 and both became HostFileAbsent, which is the arm that plans a
// write into a file this module exists to keep root-owned; a classifier that collapses them again
// reds here. The present arm settles nothing because it continues into the byte comparison.
test fn an_unread_path_reaches_unobservable_and_never_absent() -> Bool {
let unread = HostFileMetadataUnread { cause: "stat could not read the path's metadata; exit=1 " }
settled_is_unobservable(st: classify_host_file_path(reading: unread, parent: EntryPresent))
&& settled_is_absent(st: classify_host_file_path(reading: unread, parent: EntryAbsent))
&& settles_nothing(st: classify_host_file_path(
reading: HostFileMetadataRead { file_type: "regular file" },
parent: EntryPresent,
))
}

// The read decides presence; the parent decides nothing when the read answered. An indeterminate
// parent beside a successful read is still present, so the join cannot turn a read file unreadable.
test fn a_metadata_read_that_answered_is_present_whatever_the_parent_said() -> Bool {
let read = HostFileMetadataRead { file_type: "regular file" }
path_is_present(st: classify_host_file_path(reading: read, parent: EntryPresent))
&& path_is_present(st: classify_host_file_path(reading: read, parent: EntryAbsent))
&& path_is_present(st: classify_host_file_path(
reading: read,
parent: EntryPresenceIndeterminate { cause: "listing refused" },
))
}

// Exit success is a fact about the CALL. A `stat` that exited zero and printed nothing answered no
// question, so it is unread -- and unread beside a parent that holds the entry is unreadable, never
// a nameless kind and never an absence.
fn reading_is_unread(r: RunnerHostFileMetadataReading) -> Bool {
match r { HostFileMetadataUnread { cause: _ } => true HostFileMetadataRead { file_type: _ } => false }
}

test fn a_stat_that_exited_zero_and_printed_nothing_is_unread() -> Bool {
reading_is_unread(r: classify_host_file_metadata(exit_code: 0, stdout: " \n", stderr: ""))
&& reading_is_unread(r: classify_host_file_metadata(exit_code: 1, stdout: "", stderr: ""))
&& !reading_is_unread(r: classify_host_file_metadata(exit_code: 0, stdout: "regular file\n", stderr: ""))
&& match classify_host_file_metadata(exit_code: 0, stdout: " directory \n", stderr: "") {
HostFileMetadataRead { file_type: t } => t == "directory"
HostFileMetadataUnread { cause: _ } => false
}
}

// INHABITANCE (DESIGN section 3): the words observe_runner_host_file_content actually sends are the
// ones extdeps.tools.stat derives from its cited GNU authority, over the production path of a
// production desired file -- not a boolean test, and not a literal spelled here. The remote leg
// itself is not executed hermetically (gunbc.rung_drop runner_host_file_apply_route_hermetic), so
// this is the deepest live route to the new probe: the same function the observer calls, over the
// same path the population produces. It reds if the probe is respelled as any boolean test.
test fn the_production_probe_sends_the_cited_stat_metadata_words() -> Bool {
match teardown_desired() {
Absent => false
Present { value: f } => {
let path = f.path as String
let sent = runner_host_file_metadata_probe_argv(path: path)
sent == argv_words(command: stat_file_type_command(path: path))
&& sent == ["/usr/bin/stat", "-c", "%F", "--", path]
&& !any(sent, w => w == "test" || w == "-e")
}
}
continues && absent && unobservable
}

// Every directory from the write scope down to the file's own, in order, and nothing above /etc.
Expand Down