Login
Phase 7: Locking
Login

xv6 §7, "Locking". "Finally, a device interrupt handler that modifies the same data as some interruptible code could damage the data if the interrupt occurs just as the interrupted code is also modifying the data."

Phase 6 brought interrupts. Phase 7 brings the other source of concurrency, more than one CPU, and then protects Glint's shared data against both. It starts from Phase 6's interrupt handlers and single-vCPU guest. It leaves Phase 8 locks it can rely on when it starts switching between threads. Sleep locks, which need a scheduler to sleep on, wait until Phase 9 (9.2).

Where the two architectures differ substantially, a slice is split into an aarch64 check-in (a) followed by an x86_64 one (b), and both land within the phase.

Provisional slices. Each is refined, with its quoted sentence, when the phase starts.

Slices

7.1a Secondary CPUs on Arm. Glint asks the firmware to start each other CPU through the PSCI call CPU_ON, gives each one its own stack and interrupt setup (6.1a), and parks it idle. Locks only matter once something can run alongside, so this comes first in the phase. xv6 §7 names multiprocessor hardware as the first source of interleaving. A boot log listing every CPU as started and idle is the evidence, which serves Demonstrability.

7.1b Secondary CPUs on x86. On x86 the boot CPU starts the others with the INIT-SIPI sequence through its local APIC (6.1b), and each runs the same idle loop as 7.1a. It is split from 7.1a because the start-up protocols share no code, and it follows 7.1a under the plan's aarch64-first rule. Keeping the two start-up paths apart keeps each small, which is Parsimony.

7.2 Spinlocks. A spinlock is built on the CPU's atomic instructions and masks interrupts on its own CPU while held. That protects shared data against both other CPUs (7.1) and interrupt handlers (6.1a–6.4b), the two dangers the phase's opening passage describes. It comes right after 7.1 because only then can the spinning half be tested for real. Its passages are xv6 §7.2 ("Code: Locks") and §7.5 ("Locks and interrupts"), with MOS4/5 §8.1.3 on spinning. One small lock used everywhere, rather than a lock per situation, is Parsimony.

7.3 Lock order and a checker. Glint records a global order for the locks of 7.2, and in debug builds every acquisition is checked against that order. The order follows Hailperin §4.7.2's rule: "imposing a linear order in which resources need to be locked". It comes after 7.2 because there must be locks to order. Its passage is xv6 §7.4 ("Deadlock and lock ordering"). The checker turns a design rule into something specs can catch being broken, which is Demonstrability.

7.4 Memory ordering. Explicit barriers (instructions that stop the CPU or compiler from reordering memory accesses across them) go into 7.2's lock code. They also go into the shared structures Glint already has, starting with the virtqueues that Phase 5 introduced (5.4–5.6). It comes after 7.2 because the barriers belong where the locks are, and before Phase 8 because multiple threads will soon touch those queues. Its passage is xv6 §7.6 ("Instruction and memory ordering"). Stating each ordering assumption beside the code that relies on it serves Clarity.

7.5 Zephyr's locks. The shim's k_spinlock and k_mutex, which started in 6.9 as interrupt-masking stand-ins, now map onto 7.2's spinlocks. They sit in 7.3's order, so Zephyr drivers and Glint obey one lock order. It comes last because it needs both the real locks and the checker. Zephyr code gains real locking without a line of it changing, which is Loose Coupling: the shim stays the only place where Zephyr's API meets Glint's.

Phase demo: the lock-order checker catches a deliberately inverted pair in specs, and a stress run on 4 QEMU CPUs passes.

References