xv6 §9, "Sleep and Wakeup". "Scheduling and locks help conceal the actions of one thread from another, but we also need abstractions that help threads intentionally interact."
Phase 9 lets threads, and therefore vCPUs, wait without burning CPU, and be woken by an event. Three things follow from that: an idle guest costs almost nothing, virtio devices can signal instead of being polled, and guests can be stopped and restarted cleanly. It starts from Phase 8's scheduler. It leaves Phase 10 an event-driven virtio path and a Glint↔guest channel.
Provisional slices. Each is refined, with its quoted sentence, when the phase starts.
Slices
9.1 Sleep and wakeup. A thread can sleep on a condition, giving up its lock and its CPU in one atomic step, and another thread or an interrupt handler can wake it. It needs Phase 8's scheduler (8.1–8.4) to take the sleeping thread off the run queue and put it back, which is why it opens this phase. Its specs reproduce the lost-wakeup race (the event arrives just before the sleeper is asleep) that MOS4 §2.3.4 / MOS5 §2.4.4 describes, and show it cannot happen. That proof by spec is Demonstrability. Its passage is xv6 §9.2 ("Code: Sleep and wakeup").
9.2 Sleep locks. Locks that put the waiting thread to sleep through 9.1, rather than spinning like 7.2's, are used for locks held a long time. They were deferred from Phase 7 because they need 9.1, and they come right after it. Its passage is xv6 §7.8 ("Sleep locks"). They join 7.3's lock order like any other lock, so there is still one ordering rule, which is Parsimony.
9.3 Idle guests sleep. When a guest's vCPU runs the idle instruction (WFI on Arm, HLT on x86), Glint traps it. Because a vCPU is a thread (8.5), Glint puts that thread to sleep with 9.1 until an interrupt is pending for it. That trap is what makes an idle guest nearly free. It comes after 9.1 and 9.2 because it is the first user of sleep outside Glint itself. Host CPU use dropping to nearly zero for an idle Linux guest is the phase's main Demonstrability evidence.
9.4 Virtqueue notifications. Each emulated device gets a backend thread, created here, that sleeps (9.1) until a guest notifies it of new buffers in a virtqueue (5.4–5.6). On completion it injects an interrupt into the guest (6.4a/6.4b). Phase 5's polling path retires. It comes after 9.3 because both directions of waking (guest wakes device, device wakes guest) now exist. Hailperin §4.4.1's bounded buffer is the model for a virtqueue. Replacing polling with one notification path is Parsimony, improvement by subtraction.
9.5 A channel between Glint and a guest. virtio-vsock, a virtio device that carries socket-like byte streams between a guest and its host, gives Glint and a guest a channel. It is built on 9.4's backend threads. This is the analogue of xv6 §9.3's pipes, and MOS4 §2.3.8 / MOS5 §2.4.8 covers message passing. It comes after 9.4 because it is just another device on that path. Phase 10's driver domain (10.7) uses it first. A plain byte stream, with no shared memory, keeps Glint and the guest Loosely Coupled.
9.6 Guest lifecycle. When a guest makes the PSCI call SYSTEM_OFF or
SYSTEM_RESET, or Glint kills it, all of its resources are released: vCPU
threads (8.5), backend threads (9.4), memory (3.1, 3.5) and devices. This is
the analogue of xv6 §9.4 ("Code: Wait, exit, and kill"). It comes last
because only now does a guest own everything it must give back. A spec
counting free pages before a guest starts and after it ends, and finding
them equal, serves Demonstrability.
Phase demo: an idle Linux guest uses almost no host CPU, and a vsock echo round-trips between Glint and Linux.
References
- xv6 §9: "we also need abstractions that help threads intentionally interact"; §9.3 "Code: Pipes"; §9.4 "Code: Wait, exit, and kill".
- Hailperin §4.4.1 "Bounded Buffers" (a virtqueue is one shared by Glint and a guest); §4.5 "Condition Variables"; §10.2 "Messaging Systems" (for Glint↔guest channels).
- Tanenbaum: MOS4 §2.3.4 / MOS5 §2.4.4 "Sleep and Wakeup" [the producer-consumer problem and the lost-wakeup race]; MOS4 §2.3.8 / MOS5 §2.4.8 "Message Passing" [send and receive].
- Rationale: both xv6 and Tanenbaum use the name sleep and wakeup, and Tanenbaum's lost-wakeup race is the bug Glint's virtqueue notification slices must be tested against. Hailperin's bounded buffer is the closest model of a virtqueue.