Function set_forwarded_source 

pub fn set_forwarded_source(socket: OwnedFd, sink: ForwardedRecordSink)

Registers the receiving end of the socket an in-guest Tool sends its records on (send_forwarded_record) and the sink that writes them to the run’s log.

THE ORDER RULE, one for every backend whose Tool runs in the guest. Each record carries its sending thread (tagged_forwarded_message). Before it handles any guest request the coordinator takes the records waiting on the socket into a queue per sending thread (drain_forwarded_at_request at the top of the request handler). A thread’s queued records are written into the log:

• when that thread’s own request arrives, if it is the thread the scheduler last committed an ordinary turn to, or, before any turn, the thread whose request arrives first (the root; every other thread is created during some turn). That thread’s request is the event that ends the turn the schedule gave it, so the request arrives at a point the schedule fixes, and its records land where a single-process (ptrace) run writes them, ahead of everything handling that request writes. (A thread still in background IO from an earlier BACKGROUND turn may run at the same time; its records wait for its own COMMIT, by the next rule. Coordinator lines its continuation writes below INFO verbosity, such as TRACE, are not ordered by this rule; the INFO DETLOG and COMMIT lines that verification compares are.)
• otherwise immediately before the scheduler commits that thread’s next turn (write_forwarded_for, at both kinds of COMMIT): a thread that runs without holding the turn (a forked child doing its setup, a thread in background IO) sends its records while other threads’ turns are being handled, so only its own next COMMIT is a point the schedule fixes;
• and, for any still queued when the run ends, then, thread by thread in thread-id order.

If a second thread sends a request before the first turn, there is more than one root (a preload constructor that forked before the runtime was installed, say), and which root’s records come first would be the host’s choice. The coordinator then writes FORWARDING_AMBIGUOUS_ORDER_NOTICE, so verification refuses to compare the records rather than compare a host-timed order.

A send on a message socket queues the record on the receiver before it returns, so a guest thread’s records sent before a request are queued by the time that request is handled, and so before the turn it leads to is committed. Writing every thread’s records at any request’s arrival instead put a record wherever the host happened to deliver it: a forked child’s records, sent while its parent’s next request was being handled, landed before or after the scheduler’s records for that request depending on timing.

The records are TAKEN off the socket continuously, by a receiver task that queues each one for its thread as soon as it arrives, so a guest never blocks on a full socket buffer waiting for a request the coordinator would drain at: a single writev of 1024 buffers sends 1024 records before its thread’s next request. Taking a record only queues it; where it is written is still decided by the rule above. (A message without a sender tag is written as it is taken, which verification refuses to compare anyway: see ForwardedOrder::untagged.) The receiver is a task on the coordinator’s tokio runtime, started at the first request (start_forwarded_receiver), not a thread of its own: inside Hermit’s PID namespace a coordinator thread takes an ID from the same allocator as the guest’s tasks, and one more thread shifted every guest ID by one (the root became DetPid 4).