Toward Formal Verification of a Lock-Free Distributed Double Buffer Cache

Training deep learning models on synthetic data is increasingly important in neuroimaging, yet on-the-fly generation introduces severe throughput bottlenecks. Wirehead is a distributed caching system that decouples data generation from model training using a MongoDB-backed double buffer, achieving near-linear scaling with additional generators. While Wirehead has demonstrated a 15.7x throughput increase with 16 generators in practice, its correctness properties, including freedom from deadlocks, data corruption, and zombie processes, have not been formally established. This thesis presents Wirehead’s design and evolution from a three-component architecture to a streamlined distributed double buffer, then investigates the formal verification of this algorithm using the Rocq proof assistant. We model the relevant MongoDB operations as pure Rocq functions, translate the core algorithm into a nondeterministic state machine, and present proofs of six properties: three safety (swap mutual exclusion, read consistency, and post-swap data integrity) and three liveness (swap completion, lock acquisition, and progress). Five are fully machine-checked; the progress theorem depends on two Admitted lemmas involving a pigeonhole counting argument. This effort contributes to the broader goal of building trustworthy infrastructure for scientific computing.