Back to Search
Start Over
The anchor verifier for blocking and non-blocking concurrent software
- Source :
- Proceedings of the ACM on Programming Languages. 4:1-29
- Publication Year :
- 2020
- Publisher :
- Association for Computing Machinery (ACM), 2020.
-
Abstract
- Verifying the correctness of concurrent software with subtle synchronization is notoriously challenging. We present the Anchor verifier, which is based on a new formalism for specifying synchronization disciplines that describes both (1) what memory accesses are permitted, and (2) how each permitted access commutes with concurrent operations of other threads (to facilitate reduction proofs). Anchor supports the verification of both lock-based blocking and cas-based non-blocking algorithms. Experiments on a variety concurrent data structures and algorithms show that Anchor significantly reduces the burden of concurrent verification.
Details
- ISSN :
- 24751421
- Volume :
- 4
- Database :
- OpenAIRE
- Journal :
- Proceedings of the ACM on Programming Languages
- Accession number :
- edsair.doi...........157a9a5a22eacfa0ccd8604d48411a1c