Reference. Armada: low-effort verification of high-performance concurrent programs
Cite
Cited by (4)
TäKōFormal: Enabling Robust Software for Programmable Memory Hierarchies srinivasan-2026-takoformal
Grove: A Separation-Logic Library for Verifying Distributed Systems sharmaGroveSeparationLogicLibrary2023
Grove is a concurrent separation logic library for verifying distributed systems. Grove is the first to handle time-based leases, including their interaction with reconfiguration, crash recovery, thread-level concurrency, and unreliable networks. This paper uses Grove to verify several distributed system components written in Go, including vKV, a realistic distributed multi-threaded key-value store. vKV supports reconfiguration, primary/backup replication, and crash recovery, and uses leases to execute read-only requests on any replica. vKV achieves high performance (67–73% of Redis on a single core), scales with more cores and more backup replicas (achieving about 2× the throughput when going from 1 to 3 servers), and can safely execute reads while reconfiguring.
Armada: Automated Verification of Concurrent Code with Sound Semantic Extensibility lorch-2022-armada
Safely writing high-performance concurrent programs is notoriously difficult. To aid developers, we introduce Armada, a language and tool designed to formally verify such programs with relatively little effort. Via a C-like language and a small-step, state-machine-based semantics, Armadagives developers the flexibility to choose arbitrary memory layout and synchronization primitives so that they are never constrained in their pursuit of performance. To reduce developer effort, Armadaleverages SMT-powered automation and a library of powerful reasoning techniques, including rely-guarantee, TSO elimination, reduction, and pointer analysis. All of these techniques are proven sound, and Armadacan be soundly extended with additional strategies over time. Using Armada, we verify five concurrent case studies and show that we can achieve performance equivalent to that of unverified code.
Sift: Using Refinement-guided Automation to Verify Complex Distributed Systems maSiftUsingRefinementguided
Distributed systems are hard to design and implement correctly. Recent work has tried to use formal verification techniques to provide rigorous correctness guarantees. These works present a hard choice, though. One must either opt for the power of refinement-based approaches like IronFleet and Verdi, at the cost of large amounts of manual effort; or choose the more automated approach of I4, IC3PO, SWISS and DistAI which give up the ability to prove refinement and the power and scalability that come with it.
Cites 41 works (1 here)
With notes (1)
Iris from the ground up: A modular foundation for higher-order concurrent separation logic jung_etal_iris_ground_up_2018
Iris is a framework for higher-order concurrent separation logic, which has been implemented in the Coq proof assistant and deployed very effectively in a wide variety of verification projects. Iris was designed with the express goal of simplifying and consolidating the foundations of modern separation logics, but it has evolved over time, and the design and semantic foundations of Iris itself have yet to be fully written down and explained together properly in one place. Here, we attempt to fill this gap, presenting a reasonably complete picture of the latest version of Iris (version 3.1), from first principles and in one coherent narrative.
External (40)
- Verifying concurrent, crash-safe systems with Perennial (2019)
- LibLFDS: LFDS 7.11 queue implementation (2019)
- Private communication (Shaz Qadeer) (2019)
- Verifying concurrent software using movers in CSPEC (2018)
- Certified concurrent abstraction layers (2018)
- Layered Concurrent Programs (2018)
- Nickel: a framework for design and verification of information flow control systems (2018)
- A promising semantics for relaxed-memory concurrency (2017)
- Safety and liveness of MCS lock—layer by layer (2017)
- The Essence of Higher-Order Concurrent Separation Logic (2017)
- Go with the flow: compositional abstractions for concurrent data structures (2017)
- CertiKOS: an extensible architecture for building certified concurrent OS kernels (2016)
- Deep Specifications and Certified Abstraction Layers (2015)
- Automated and modular refinement reasoning for concurrent programs (2015)
- TaDA: A Logic for Time and Data Abstraction (2014)
- Views: compositional reasoning for concurrent programs (2013)
- A rely-guarantee-based simulation for verifying concurrent program transformations (2012)
- Relaxed-memory concurrency and verified compilation (2011)
- Dafny: An Automatic Program Verifier for Functional Correctness (2010)
- Reasoning about the Implementation of Concurrency Abstractions on x86-TSO (2010)
- From total store order to sequential consistency: a practical reduction theorem (2010)
- Hyperproperties (2010)
- Deny-guarantee reasoning (2009)
- A calculus of atomic actions (2009)
- A better x86 memory model: x86-TSO (2009)
- Relaxed memory models: an operational approach (2009)
- Z3: An Efficient SMT Solver (2008)
- Resources, concurrency, and local reasoning (2007)
- Boogie: a modular reusable verifier for object-oriented programs (2006)
- Formal verification of a C compiler front-end (2006)
- Exploiting purity for atomicity (2004)
- Reduction in TLA (1998)
- Simple, fast, and practical non-blocking and blocking concurrent queue algorithms (1996)
- Points-to analysis in almost linear time (1996)
- Noninterference, transitivity, and channel-control security policies (1992)
- The existence of refinement mappings (1991)
- Algorithms for scalable synchronization on shared-memory multiprocessors (1991)
- Weak ordering—a new definition (1990)
- Tentative steps toward a development method for interfering programs (1983)
- Reduction: a method of proving properties of parallel programs (1975)