Armada: Automated Verification of Concurrent Code with Sound Semantic Extensibility

Reference. Armada: Automated Verification of Concurrent Code with Sound Semantic Extensibility

Jacob R. Lorch, Yixuan Chen, Manos Kapritsos, Haojun Ma, Bryan Parno, Shaz Qadeer, Upamanyu Sharma, James R. Wilcox, Xueyuan Zhao · TOPLAS · 2022 · concurrency · PDF · DOI · pldb

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.

Cite

Cite as @lorch-2022-armada (helia, typst) · \cite{lorch-2022-armada} (LaTeX)

BibTeX

bibtex · 1 line

@article{lorch-2022-armada, title={Armada: Automated Verification of Concurrent Code with Sound Semantic Extensibility}, volume={44}, ISSN={1558-4593}, url={http://dx.doi.org/10.1145/3502491}, DOI={10.1145/3502491}, number={2}, journal={ACM Transactions on Programming Languages and Systems}, publisher={Association for Computing Machinery (ACM)}, author={Lorch, Jacob R. and Chen, Yixuan and Kapritsos, Manos and Ma, Haojun and Parno, Bryan and Qadeer, Shaz and Sharma, Upamanyu and Wilcox, James R. and Zhao, Xueyuan}, year={2022}, month=May, pages={1–39} }

hayagriva YAML (typst)

yaml · 25 lines

lorch-2022-armada:
  type: article
  title: 'Armada: Automated Verification of Concurrent Code with Sound Semantic Extensibility'
  author:
  - Lorch, Jacob R.
  - Chen, Yixuan
  - Kapritsos, Manos
  - Ma, Haojun
  - Parno, Bryan
  - Qadeer, Shaz
  - Sharma, Upamanyu
  - Wilcox, James R.
  - Zhao, Xueyuan
  date: 2022-05
  page-range: 1-39
  url: http://dx.doi.org/10.1145/3502491
  serial-number:
    doi: 10.1145/3502491
    issn: 1558-4593
  parent:
    type: periodical
    title: ACM Transactions on Programming Languages and Systems
    publisher: Association for Computing Machinery (ACM)
    issue: 2
    volume: 44

Download: lorch-2022-armada.bib · lorch-2022-armada.yml

Cited by (2)

Verus: A Practical Foundation for Systems Verification lattuada-2024-verusSOSP · 2024

DOI

Galápagos: Developing Verified Low Level Cryptography on Heterogeneous Hardwares zhou-2023-galapagosCCS · 2023

DOI

Cites 46 works (2 here)

With notes (2)

Armada: low-effort verification of high-performance concurrent programs lorch-2020-armadaPLDI · 2020

PDF · DOI · pldb

Iris from the ground up: A modular foundation for higher-order concurrent separation logic jung_etal_iris_ground_up_2018JFP · 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.

PDF · DOI · pldb

External (44)

Market share of the x86 architecture (2021)
CSim2: compositional top-down verification of concurrent systems using rely-guarantee (2021)
Verifying concurrent, crash-safe systems with Perennial (2019)
LFDS 7.11 queue implementation (2019)
Private communication (Shaz Qadeer) (2019)
Certified concurrent abstraction layers (2018)
Layered Concurrent Programs (2018)
Go with the flow: Compositional abstractions for concurrent data structures (2018)
Verifying concurrent software using movers in CSPEC (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)
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)
Hyperproperties (2010)
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)
Relaxed memory models: an operational approach (2009)
VCC: A Practical System for Verifying Concurrent C (2009)
Deny-Guarantee Reasoning (2009)
A calculus of atomic actions (2009)
A Better x86 Memory Model: x86-TSO (2009)
Z3: An Efficient SMT Solver (2008)
Resources, concurrency, and local reasoning (2007)
Formal Verification of a C Compiler Front-End (2006)
Boogie: A modular reusable verifier for object-oriented programs (2005)
Exploiting purity for atomicity (2004)
Reduction in TLA (1998)
Points-to analysis in almost linear time (1996)
Simple, fast, and practical non-blocking and blocking concurrent queue algorithms (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)
Verifying properties of parallel programs: an axiomatic approach (1976)
Reduction: a method of proving properties of parallel programs (1975)