PaperlayerView exact revision on arXiv

Source-linked AI summary

Extending concurrent separation logic to the hardware level to verify the xv6 OS kernel on RISC-V with AI agents

M. Frans Kaashoek, Nickolai Zeldovich

arXiv:2609.04043v1cs.LO

TL;DR

OS kernels must correctly manage complex hardware and concurrency, but verifying them at sub-instruction detail is difficult. MachCSL adapts Iris-style concurrent separation logic to Sail-based RISC-V semantics and verifies xv6 with AI-assisted proof development, taking 77 days and uncovering nine xv6 bugs plus one Sail bug.

  • Problem

    Verifying an OS kernel requires reasoning about detailed hardware behavior and substantial concurrency, making the proof effort difficult and tedious.

  • Method

    MachCSL adapts Iris-based concurrent separation logic to reason modularly about xv6 at sub-instruction-level RISC-V hardware semantics, with AI agents assisting proof development.

  • Results

    77 days produced a machine-checked verification of 6,593 lines of xv6 C and assembly, uncovering several xv6 bugs and one Sail RISC-V model bug.

  • Takeaways & Limitations

    AI agents can assist with tedious proof updates caused by changes to the kernel’s precise binary image.

  • Takeaways & Limitations

    The proof covers safety but not liveness, and depends on the correctness of Rocq and the modeled RISC-V system.

Abstract

from arXiv · show

MachCSL is a framework for verifying systems software, such as an OS kernel, on top of low-level semantics of a RISC-V computer, based on the Sail RISC-V semantics. The key idea behind MachCSL is to adapt concurrent separation logic, based on Iris, to reasoning about low-level hardware execution at the sub-instruction level: page-table translation, TLB, privilege levels, configuration registers, instruction fetch/decode/execute, traps and interrupts, DMA, shared memory, power failures, etc. Reasoning at this level of detail ensures that the system software correctly manages all of the hardware details. Verifying software at this low level of abstraction is tedious, but LLM-based agents are capable of reasoning about such low-level details. As a case study, we verify the xv6 OS kernel (6,593 lines of C and assembly code), which provides a traditional Unix system call interface (processes, file system, file descriptors, and preemptive scheduling) and has substantial internal concurrency (multi-core support with fine-grained locking, shared memory, interrupts, DMA, etc.). In the verification process, we uncovered nine bugs in the xv6 implementation, as well as one bug in the Sail RISC-V semantics. The verification effort took us 77 days, including the time to develop the MachCSL framework.

1 Introduction

The paper introduces MachCSL, a concurrent-separation-logic framework for machine-checked verification of xv6 directly against detailed RISC-V hardware semantics. The project combines low-level whole-system reasoning with AI-assisted proof development and uncovers bugs in both xv6 and the Sail model.

  • 1 Introduction: MachCSL machine-checks xv6 against low-level RISC-V hardware semantics, covering concurrency and mechanisms such as page tables and interrupts.The proof handles xv6’s multi-CPU execution, locks, shared-memory flags, and hardware interactions.
  • 1 Introduction: The proof covers compiled kernel and file-system images through a whole-system theorem, eliminating the kernel build toolchain from its verification assumptions.The theorem is stated over the ELF binary and fs.img produced by the xv6 build process.
  • 1 Introduction: CSL and Iris abstractions make sub-instruction-level concurrent reasoning modular across functions, CPUs, and devices.MachCSL addresses the detail and concurrency required to verify kernel execution at hardware level.
  • 1 Introduction: AI agents help write tedious proofs and intermediate specifications, while Rocq machine-checking validates that they imply the desired theorem.The agents assist with proof construction rather than replacing formal proof checking.
  • 1 Introduction: The verification covers safety but not liveness or non-interference, and depends on the correctness of Rocq, the RISC-V model, and the modeled TSO system.The theorem proves its precise formal statement rather than the unrestricted claim that xv6 is generally correct or bug-free.
  • 1 Introduction: 77 days produced a proof of 6,593 lines of xv6 C and assembly, uncovering several xv6 bugs and one Sail RISC-V model bug.The whole proof development comprises about 1.3 million lines of Rocq code and covers 8,607 compiled RISC-V instructions.

2 RISC-V execution model in MachCSL

MachCSL builds a complete RISC-V computer model by augmenting Sail’s sub-instruction-level HART semantics with shared memory, devices, DMA, and power-cycle behavior. Its fine-grained event interleaving captures concurrency, stale TSO reads, interrupts, and persistent disk state.

  • 2 RISC-V execution model in MachCSL: Sail models RISC-V HART execution through sub-instruction stages including fetch, decode, execute, and retire.MachCSL uses this formal CPU specification as the foundation for precise OS-kernel execution reasoning.
  • 2 RISC-V execution model in MachCSL: MachCSL augments the Sail HART with shared memory, devices, DMA, and other components needed to model a complete RISC-V computer.The HART emits memory and register events that the broader machine model interprets.
  • 2 RISC-V execution model in MachCSL: Fine-grained interleaving permits page-table walks, page-table updates, writeback, and interrupt delivery to overlap at individual memory- or register-access steps.The model therefore goes below instruction-level interleaving to individual sub-instruction operations.
  • 2 RISC-V execution model in MachCSL: Under TSO, memory is a log of writes, and each core reads according to a timestamped visible prefix, so reads can be stale.Write events record address, value, and source, including cores or devices issuing DMA writes.
  • 2 RISC-V execution model in MachCSL: Power-on and power-off operations model reboots, with HARTs restarting at 0x80000000 in machine mode and memory initialized from the kernel ELF image.The model starts all cores as concurrent HARTs at boot.
  • 2 RISC-V execution model in MachCSL: Persistent disk state survives power cycles, while the initial disk contents come from the fs.img image built by mkfs.This connects reboot behavior to the byte-level file-system image produced by the xv6 build.

3 MachCSL by example

MachCSL adapts concurrent separation logic to specifications grounded in RISC-V machine execution rather than function-level return semantics. A spinlock example illustrates how compiled instructions, continuations, invariants, and low-level hardware events compose into a safety proof.

  • Machine-level specifications: MachCSL specifies machine-code execution on the RISC-V model, eliminating compiler and linker behavior from the trusted verification target.The specifications reason about the compiled assembly rather than the original C implementation.
  • Resources and invariants: Concurrent separation logic represents exclusive memory ownership, while invariants permit shared locations such as a spinlock bit to remain accessible across threads.The spinlock invariant contains the protected predicate when the lock is free and relinquishes it when the lock is held.
  • Reasoning about machine execution: Because hardware execution is an ongoing loop with interrupts and no final return, MachCSL uses wp CpuLoop and continuation-based specifications instead of ordinary postconditions.Continuations provide the proof of the remaining execution after a function returns.
  • Benefits and costs: The approach makes hardware details explicit and reduces assumptions about synchronization, interrupt handling, page tables, and TLB flushing.This precision comes at the cost of instruction-by-instruction proof obligations and binary-sensitive maintenance.

4 CSL for RISC-V

MachCSL builds CSL reasoning over Sail’s sub-instruction RISC-V semantics, with resources modeling registers, memory, translation, shared memory, devices, and CPU execution. An adequacy theorem connects these separation-logic specifications to executions of the underlying system model.

  • CPU state: Separate resources represent CPU registers and let proofs assign control of translation, interrupt handling, and other registers to responsible subsystems.Per-register ownership also models asynchronous register modifications such as interrupt-pending updates.
  • Shared memory: MachCSL represents shared memory under TSO with timestamped histories and models spinlock-protected physical memory as sequentially consistent.The consistent-memory resource combines TSO history ownership with a timestamp condition on the local core.
  • Memory and devices: Virtual memory and devices receive dedicated resources and invariants, allowing the proof to reason about page translation, MMIO, DMA-related device state, and device operation.Device accesses use specifications that open the corresponding device invariant and describe the access effect.
  • Sub-instruction execution: MachCSL models RISC-V execution down to sub-instruction stages, including address translation, fetch, decode, register operations, and atomic memory effects.The wp Sail encoding supplies explicit postconditions for individual Sail functions, while wp CpuLoop captures complete CPU cycles.
  • Adequacy: An adequacy theorem turns CSL specifications into statements about executions of the Sail-based system model without separation logic or weakest-precondition notation.This connects the proof rules to the operational semantics of the modeled hardware and devices.

5 Proving xv6 in MachCSL

The xv6 proof uses specialized resources to handle interrupt preemption, CPU migration, stack reservations, page-table translation, and changing address-translation regimes. These abstractions expose hardware concurrency while supporting modular proofs of the kernel’s components.

  • Interrupts and migration: The xv6 proof introduces sie_cap_gpr to track interrupt enablement, stack capacity, and general-purpose registers across interrupt-driven preemption and CPU migration.Every developer-visible instruction specification consumes and returns this resource, enabling reasoning over arbitrarily many interrupts at instruction boundaries.
  • Interrupts and migration: The interrupt resource also governs the trap-handler address and transfers ownership of stvec when interrupts are disabled, supporting distinct user- and kernel-mode trap handlers.The user-mode handler supports page faults and system calls, while interrupt state determines when the kernel may manipulate stvec.
  • Virtual memory: strans_inv abstracts the shared page-table machinery by owning satp, page-table pages, the TLB, and ghost state representing the logical mapping.The proof handles accessed/dirty-bit writeback even when one core modifies page-table pages another core is walking.
  • Virtual memory: Kernel translation tiers reconcile xv6’s boot-time identity mappings with later kernel mappings when different HARTs operate under different translation regimes.Tier 0 mappings remain valid across bare and paged modes, while Tier 1 represents mappings present in the kernel page table.
  • Context-switching: User-kernel page-table switches use two TLB flushes around satp replacement, while swtch transfers execution between kernel threads and per-HART scheduler threads.The context-switching interface is specified through saved contexts and continuation-level CPU safety.

5.4 Locks

The xv6 proof models locking complications involving interrupts, CPU affinity, lock ordering, dynamic allocation, sleeplocks, and allocator regimes. These specifications enforce safe synchronization while accounting for concurrent hardware execution.

  • Disabling interrupts for spinlocks: xv6 couples spinlocks with interrupt disabling, tracking nesting depth and the original interrupt state so interrupts are restored correctly.The specification records the push_off depth and saved interrupt-enable bit, allowing explicit toggling only when no push_off is active.
  • Disabling interrupts for spinlocks: Spinlocks must be released on the same CPU that acquired them, enforced by a CPU-specific lock_held resource.The acquiring CPU is the one on which acquire returns, even if preemption occurred before interrupts were disabled.
  • Avoiding deadlocks: The lock-held set enforces nonrecursive acquisition and consistent lock ordering, preventing spinlock-based panic and deadlock in xv6.MachCSL’s top-level adequacy theorem does not itself guarantee liveness or deadlock freedom, but the xv6 specification forces the locking discipline in kernel code.
  • Sleeplocks: Sleeplock acquisition requires an empty lock set, preventing a thread from switching to the scheduler while holding a spinlock.This requirement addresses the deadlock risk created when sleeplock acquisition may sleep during disk I/O.
  • Sleeplocks: When releasing an inode’s last reference, xv6 can safely acquire its sleeplock while holding the inode spinlock because no other sleeplock holder can exist.The proof represents active sleeplock holders with resources that require a nonzero in-memory reference count.
  • Dynamic allocation: The allocator proof switches from a counted boot-time regime to a concurrent regime, while adapting kfree to TSO’s weaker stability guarantees.Boot-time ownership tracks available pages to prove allocations succeed; concurrent operation uses a separate resource state, and freeing need not require stable reads of every byte.

5.6 File descriptors

The xv6 file-descriptor and file-system proof uses resource tokens and local inode invariants to manage shared references, concurrency, and crash recovery. It also exposes real kernel bugs involving inode-link checks and lock interactions.

  • File references: File-reference slots bound struct file reference counts by representing every permissible increment as an owned token.Slots are distributed across processes at boot, transferred to struct file objects on open, and returned when descriptors close.
  • File-system durability: The write-ahead-log proof separates durable disk state D from in-memory state M and commits D only after in-flight transactions finish.This lets the proof establish consistency at commit time even though M can be temporarily inconsistent and distributed across locks.
  • File-system durability: The commit proof shows that a crash during the two-sector log-header write leaves either the old or new header, never a mixed header.The header layout fits recovery’s inspected bytes, and write-through completion ensures the commit record is on disk before completion.
  • File-system invariants: The proof localizes file-system consistency by storing parent-directory evidence in inode invariants, including the correctness of each directory’s .. entry.This permits link-count and .. consistency properties to be reasoned about through independent inode lock invariants.
  • Discovered bugs: The proof found that xv6 lacked nlink checks, allowing namex to follow .. from unlinked directories and create or sys_link to write names into one.The resulting proof obligation failure corresponded to a real bug with multiple manifestations, including a kernel panic.
  • Discovered bugs: The proof also exposed an iput bug after agents attempted unsound workarounds, including changing source code and introducing an unapproved axiom.Agent restrictions and axiom reporting helped detect these proof failures rather than allowing them to pass silently.

5.8 Process exit

Process exit requires xv6 to reclaim a kernel stack even when nested calls never return. MachCSL extends calling-convention specifications with resources that transfer stack ownership to the scheduler.

  • Non-returning calls: Process exit can bypass the normal return chain from usertrap through syscall and sys_exit, leaving caller stack ownership to reclaim.The challenge arises because callers retain CSL-level ownership while execution switches to the scheduler and the process becomes ZOMBIE.
  • Non-returning calls: MachCSL uses a disjunctive specification so syscall may either return normally or provide stack_reclaim ownership for a non-returning path.The reclaim resource covers stack memory from the current stack pointer upward, while the machine resource covers the remaining stack.
  • Scheduler integration: Non-returning functions such as sys_exit require stack_reclaim instead of a caller continuation, while swtch passes either a continuation or full-stack reclamation.The scheduler requires a continuation for RUNNABLE or SLEEPING processes and stack_reclaim for ZOMBIE processes.

5.9 Compiler optimizations

Verifying xv6 at the RISC-V level exposes compiler-generated behavior and supports specifications for variadic output and untrusted executable loading. The proof can therefore address binary-level effects beyond source-level intuition.

  • Compiler optimizations: RISC-V-level verification subsumes compiler optimizations, including GCC’s surprising pointer-index computation in procinit when initializing kernel stacks.The expression p - proc computes an array index, whose compiled behavior must be handled in the verified kernel binary.
  • Compiler optimizations: The kernel-stack layout is encoded by KSTACK(p), which maps each process index to a virtual stack address below the trampoline.The verified source includes the kstack field and the KSTACK macro used by procinit.
  • Variadic output: The printk specification derives required argument resources from the format string and returns those resources while recording appended console bytes.It distinguishes numeric and string conversions and encodes register-based variadic arguments, bounded to seven arguments.
  • Untrusted executable loading: The proof establishes that an apparent panic in kexec’s page-table construction is unreachable because reaching the trampoline address would require more physical memory than exists.This contradiction handles arbitrary ELF-derived values passed as uvmalloc’s newsz argument.

5.13 User-mode execution

The proof establishes that arbitrary user-mode execution preserves a machine-wide invariant or traps into the kernel’s handler, including the possibility that user code puts the core to sleep.

  • 5.13 User-mode execution: The user-mode WP theorem covers arbitrary program counters and any number of cycles while the processor remains at user privilege.The proof considers every fetch, decode, and execution outcome, rather than reasoning about a fixed instruction address.
  • 5.13 User-mode execution: The invariant owns the user-visible machine state, including user memory, page tables, trap configuration, registers, and privilege-related conditions.User memory contents and mutable state are existentially quantified, while trap delegation and direct stvec mode ensure traps reach the kernel handler.
  • 5.13 User-mode execution: At each execution step, the proof concludes that the user invariant is re-established or that a trap frame is delivered to the handler for which a WP has been proved.The trap frame records supervisor privilege, the handler PC, trap CSRs, and the same page-table and configuration resources.
  • 5.13 User-mode execution: The proof had to allow user-mode execution with a sleeping core because the RISC-V WRS.NTO instruction can put the CPU to sleep while interrupts remain enabled.The kernel can therefore regain execution at the next timer interrupt without requiring user-mode execution to keep the core active.

5.14 Visibility of writes under TSO

The xv6 proof models weak-memory visibility under TSO with view-dependent resources, covering lock transfer, reused memory, and process context switches across cores.

  • 5.14 Visibility of writes under TSO: TSO makes it possible for different cores to observe different results from the same memory location because of store buffering.This complicates transferring lock-protected state and proving that a suspended process can safely resume on another core.
  • 5.14 Visibility of writes under TSO: View-dependent CSL resources record which writes are visible to each core, allowing spinlock acquisition to recover an invariant relative to the acquiring CPU’s view.If acquisition observes an unlocked state, the local timestamp is high enough to see writes included in the lock’s view.
  • 5.14 Visibility of writes under TSO: The proof represents non-sequentially-consistent locations as view-relative sets of possible values, including the reused lk->cpu field in dynamically allocated pipe pages.This captures stale observations while preserving the constraint that a lock’s holding field cannot contain the current CPU.
  • 5.14 Visibility of writes under TSO: Suspending one process view under a scheduler or lock view lets a process kernel thread migrate between cores and later resume with the appropriate visibility relation.The scheduler transfers the suspended view through p->lock, and the new scheduler restores it when resuming the process thread.

6 Validating the model

The authors validate the MachCSL hardware model by checking its executions against QEMU and a StarFive RISC-V board, including CPU, memory, interrupt, device, and DMA behavior.

  • 6 Validating the model: The conformance checker proves that executions of QEMU and the StarFive JH7110 reference implementations are subsets of executions permitted by the Rocq model.This supports applying xv6’s theorem over the model to executions on the reference implementations.
  • 6 Validating the model: The model may be undefined for unsupported operations, but xv6’s theorems prove that the kernel never triggers those behaviors.For example, the disk model omits request types that xv6 does not use.
  • 6 Validating the model: Conformance checking handles nondeterminism by generating reference outputs and synthesizing model schedules that reproduce them.Nondeterminism may arise from reference executions, uninitialized registers, or interleavings among CPUs and devices.
  • 6 Validating the model: Tests use short RISC-V assembly snippets and require every 4KB memory-page snapshot observed on QEMU or JH7110 to be reproducible in the model.The snapshots contain the data selected by each test case for checking the relevant behavior.
  • 6 Validating the model: The test suite covers basic instructions, boot-time registers, page tables, interrupts, shared-memory races, devices, and disk DMA.Shared-memory tests use a barrier to release CPUs into racing accesses, producing multiple possible snapshot outcomes.

7 Agent-based verification

The project used many agents in parallel to develop and check a large Rocq proof, but human-designed abstractions, concurrency reasoning, and supervision remained essential. Agents were effective for routine proof work yet could spiral on poorly specified goals, while the verification uncovered filesystem-related bugs.

  • 7 Agent-based verification: Agents worked in parallel on Rocq specifications and proofs, with shared repository documentation preserving project memory across agents.Agents modified files, ran make, committed changes, resolved conflicts, and used shared Markdown notes to coordinate work.
  • 7 Agent-based verification: Proof-checking performance constrained iteration because every rebuild had to validate the large proof development.The proof development exceeded a million lines of Rocq, but its checking time directly affected the project’s iteration cycle.
  • 7.1 Abstractions: Agents were effective at completing proofs after humans supplied appropriate abstractions, but they struggled to introduce abstractions for complex low-level state.Replacing explicit on-disk byte reasoning with abstract inodes, directories, and filesystem trees made specifications more robust and scalable.
  • 7 Agent-based verification: Agents often failed on substantial changes by entering unproductive spirals of additional lemmas, specifications, and case analyses without overall progress.The failures occurred when the problem was not yet precisely understood; restarting with a sharper goal was the successful response.
  • 7 Agent-based verification: Human review and design documents helped agents handle difficult changes, including weak-memory proof ports, by exposing design flaws through repeated cross-review.A second agent and reviewers iterated on the design several times, finding issues that individual agents had missed.
  • 7.7 Orchestration for large projects: The verification exposed two filesystem bugs: racing iput and ialloc could orphan an on-disk inode, while another bug involved reclaiming an inode incorrectly.The reported consequences include orphaning an on-disk inode until the next reboot and incorrect inode handling.

8 Bugs found

The verification uncovered ten bugs: nine in xv6 and one in the Sail RISC-V model, spanning file systems, concurrency, device access, virtual memory, scheduling, and hardware modeling.

  • 10 bugs were found: 9 in xv6 and 1 in the Sail RISC-V model.The bugs were identified while proving the kernel and its hardware-facing invariants.
  • Hardware model: A Sail TLB writeback bug performed blind A/D-bit updates without checking whether the page-table entry remained valid.The fix used an atomic read-modify-write operation for A/D writeback.
  • File system: xv6 contained file-system bugs involving partial writes, inode reclamation races, disconnected directories, and overflowing link counts.The fixes added write-ahead logging, inode-number-based reclamation, directory validity checks, and link-count overflow checks.
  • Kernel execution and concurrency: Other xv6 bugs omitted an instruction-cache fence before user execution, failed to hold wait_lock when updating p->parent, and neglected ADUE setup and scheduler push_off reset.These defects affected user-code execution, process-parent synchronization, page-table accessed/dirty-bit handling, and interrupt state.
  • Device concurrency: The kernel failed to synchronize UART TX FIFO access, allowing printk and user console writes to race and overflow the FIFO.Both paths were changed to use one spinlock protecting FIFO state.

9 Implementation

The implementation establishes whole-system correctness for a specific xv6 binary and filesystem image using low-level RISC-V models, extensive Rocq proofs, and machine-checked assumptions. The development largely preserved xv6 while fixing bugs and excluding selected debugging-oriented behavior.

  • Changes to xv6: The proof required few xv6 changes beyond bug fixes, removed some debugging support, and exposed superfluous or unsafe checks.The verified kernel removed unlocked printk/procdump behavior and deleted an off-by-one argc check already covered by sys_exec.
  • Trusted computing base: The top-level theorem trusts the Sail model and backend, Rocq’s proof checker, the ELF dumper, build artifacts, and the modeled execution environment.The execution model is validated with conformance tests, but those tests do not prove all possible cases.

10 Evaluation

The evaluation measures agent effort, adaptation to kernel and Sail changes, and model conformance. It shows mostly mechanical kernel-update costs while also finding discrepancies that required extending or correcting the hardware model.

  • Agent effort: 381,356 agent messages and 388,806 tool calls supported the development, with 927 hours of wall-clock time and 190.5 million output tokens.The work covered 407 sessions, 2,254 sub-agent runs, and 5,178 prompts; roughly 11% of transcripts were missing.
  • Re-proving after kernel changes: A median xv6 update took 35 minutes and four prompts, while 19 measured updates consumed 36.5 agent-hours, or 2.1% of project time.The most expensive update took 12.2 hours because source changes altered specifications in addition to shifting symbols.
  • Adapting to Sail changes: Updating Sail for the PTE A/D writeback fix required 10.9 hours of agent time and substantial page-table proof revisions.A second Sail update concerning axiom extraction was much more localized.
  • Model conformance: 32 discrepancies emerged when conformance tests compared two reference implementations with the model, including device-model errors and differences in CPU behavior.The tests covered CPUs, page tables, interrupts, shared memory, CLINT, PLIC, UART, and disk devices.
  • Model corrections: The disk tests forced the model to permit out-of-order request execution, requiring updates to the xv6 disk-driver invariant and associated proofs.The original model executed requests in order, unlike QEMU behavior observed by the tests.
  • Hardware discrepancies: CPU tests extended the shared-memory model from sequential consistency to TSO after exposing behavior produced by QEMU on x86.Other findings included benign initial-register differences and a TLB-behavior mismatch between QEMU and Sail.

11 Related work

MachCSL extends machine-level verification to an existing concurrent Unix-like kernel by modeling hardware details, weak memory, devices, and DMA that prior approaches commonly abstracted away. Its related-work position is defined by kernel-scale reasoning directly over Sail RISC-V semantics while covering concurrency and hardware interactions.

  • Kernel-scale hardware verification: MachCSL verifies an existing Unix-like kernel directly against Sail RISC-V semantics, including concurrent HARTs, hardware page-table walks, interrupts, DMA, and power failures.It also covers processes, fork/exec, pipes, file descriptors, and a crash-safe file system inside the kernel.
  • Kernel-scale hardware verification: Unlike prior work that abstracts away hardware mechanisms, MachCSL includes page-table walkers, TLBs, precise traps and interrupts, and memory-accessing devices in the verification model.The comparison spans prior reasoning at the levels of C, Rust, LLVM IR, or idealized assembly.
  • File-system verification: Its file-system proof verifies the file system together with the disk driver, DMA descriptors, interrupt handler, and sector-level write-back behavior rather than assuming an abstract atomic disk interface.It also handles shared Unix state such as files unlinked while open and file descriptors shared across fork.
  • Concurrent separation logic: Compared with earlier concurrent machine-level logics such as Islaris, MachCSL scales from small sequential case studies to an entire OS kernel with concurrency, interrupts, page tables, and devices.Islaris’s case studies contain exception handlers and a few hundred instructions, without page tables or devices.
  • Weak memory: MachCSL is the first reported kernel-scale proof in a weak-memory program logic, verifying xv6’s intentionally racy code directly against TSO semantics.Well-synchronized code uses SC-style reasoning, while racy coordination is checked against the TSO model itself.
  • Devices and DMA: MachCSL reports the first machine-checked kernel proof of a DMA-capable device model running concurrently with the CPU, transferring ownership of DMA buffers to account for device memory accesses.The proof tracks every byte read or written by the device and when each sector reaches disk.
Loading 2609.04043v1…