Module host_input_change 

Name a host file that changed during one verification run.

Each run of hermit run --verify records the host identity of every file the guest opens, in order, with the open that found it (see detcore_model::host_input). A file that a run opens several times shows a PATTERN of identities: each open finds an identity it has found at that path before, or a new one. A file the guest itself creates, rewrites or replaces changes at the same opens in both runs, even though its host inode numbers and times differ between them. So the two runs’ patterns agree unless something outside the guest changed a file underneath one run: that run finds a new identity at an open where the other run found a known one.

Only one kind of change is named: the file was REPLACED, so the open found a different host inode (dev, ino). Hermit mints deterministic inodes in the order it first sees host inodes, so a replacement gives that run one more inode and shifts every later deterministic inode number, whatever the guest does with the file. A change of size or time alone is not named.

A pattern difference is evidence of a host change only if the runs had not diverged yet. A guest that behaves differently in the two runs can, for example, replace a file in one run only, and then the patterns differ too, but that behaviour shows in the compared log before the open. So the difference names the cause of a divergence only when the comparison compared everything (one strict enough for bitwise parity) and the open that found it is recorded, in BOTH runs’ logs, before the first divergent record (explains_divergence): up to that record both runs did the same things, so the guest did not cause the difference.

Positions are records in the log, not times. On a backend whose log is not one stream in time order, such as SaBRe, which appends the records its guest forwards after the coordinator’s own, each part is still in time order, and the comparator reports the first difference in the earliest part. An open in a later part than that difference is therefore refused, and an open before it in the same part did happen before it.

Nor is a change named when the guest itself rebound that path, or a directory above it, in either run: renamed to or from it, linked or unlinked it, or created something there. Those operations can replace the file without the compared log showing any difference (a rename onto a name that already names the same file succeeds and changes nothing), so a replacement there may be the guest’s own.

Nothing else is concluded. The walk stops at the first open whose path, thread or syscall differs between the runs and at the first difference that is not a replacement, an incomplete log names nothing, an open whose finish record a log does not show exactly once is not placed, and paths below /proc, /sys and /dev are skipped: those are kernel objects whose metadata is not file content and which Hermit virtualizes separately. So are the records of files the kernel opened for an exec (HostInputRecord::exec), which have no open in the log to place.

Structs

HostInputs

One run’s host-input log.

PatternDifference

A pattern difference between the runs: in run, the open that thread dtid made as its syscall number syscall found path changed from before to after, while the other run found a known identity there.

Functions

explains_divergence

Whether a pattern difference explains a divergence: the comparison was one strict enough for bitwise parity (complete_comparison), and the open that found the difference (placed by open_position in each run’s log) is recorded before the first divergent record in both logs (first_divergent_positions, the comparator’s positions of that record), so the two runs had done the same things up to that open. Without every position nothing is attributed.

find_pattern_difference

The first open, in order, at which exactly one run found an identity it had not found at that path before while the other run found one it had, when that identity is a different host inode.

open_position

Where an open sits in a run’s log (contents): the position, as the comparator counts records (detcore::logdiff::log_record_events), of the record on which thread dtid finished its syscall number syscall, an open. None when the log does not show that record exactly once: a log without it says nothing, and a thread number and syscall count can repeat (a thread that execs from a non-leader thread takes the leader’s number and keeps its own count), so a repeated one is ambiguous; also None for a log the comparator could not read either.

open_position_for_path

Fallback placement by path and syscall number, for backends whose per-thread syscall numbering restarts across process images (DBT), so (dtid, syscall) names more than one finished open in the log. The open that found a new identity is the last finished open of path with that syscall number; without a match nothing is placed.

read_host_inputs

Read one run’s log. A missing or empty file is an incomplete log.