Paper Info
Title
Armada: low-effort verification of high-performance concurrent programs
Abstract
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, Armada gives developers the flexibility to choose arbitrary memory layout and synchronization primitives so they are never constrained in their pursuit of performance. To reduce developer effort, Armada leverages SMT-powered automation and a library of powerful reasoning techniques, including rely-guarantee, TSO elimination, reduction, and alias analysis. All these techniques are proven sound, and Armada can be soundly extended with additional strategies over time. Using Armada, we verify four concurrent case studies and show that we can achieve performance equivalent to that of unverified code.
Year
DOI
Venue
2020
10.1145/3385412.3385971
PLDI '20: 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation London UK June, 2020
Keywords
DocType
ISBN
refinement, weak memory models, x86-TSO
Conference
978-1-4503-7613-6
Citations 
PageRank 
References 
0
0.34
0
Authors
8
Name
Order
Citations
PageRank
Jacob R. Lorch12226260.39
Yixuan Chen201.01
Manos Kapritsos328614.50
Bryan Parno452.47
Shaz Qadeer53257239.11
Upamanyu Sharma600.34
James R. Wilcox710.68
Xueyuan Zhao892.92