Cave is an automated verification tool for proving memory safety and
linearizability (that is, atomicity and functional correctness) of
concurrent data structures. The tool consists of a program analyser
implementing the RGSep action inference algorithm using the shape-value abstract
domain, as well as a procedure for searching for linearisation point
assignments.
There is also a prototype extension of Cave for verifying lock-freedom of concurrent algorithms. For more information, see here.
Cave is written in OCaml and is released under a BSD-style license.
- Download the source code (latest release: 2.1, released: 2015-03-19)
- Download the binary distribution for Win32 (version 2.1)
- Browse the source code documentation (generated by ocamldoc)
Publications
-
Proving lock-freedom easily and automatically.
X. Jia, W. Li, and V. Vafeiadis. In CPP 2015.
This paper describes a simple technique sufficient to verify lock-freedom of concurrent stack and queue algorithms, and implements it within Cave. -
Aspect-oriented linearizability proofs.
S. Chakraborty, T.A. Henzinger, A. Sezgin, and V. Vafeiadis. LMCS, vol. 11(1:20), 2015
This paper proposes an alternative proof method for verifying linearizability of concurrent queue algorithms, such as the Herlihy-Wing queue, whose linearization points are non-local. It extends the Cave implementation to support this proof method. -
Automatically proving linearizability.
V. Vafeiadis. In CAV 2010.
This paper describes the procedure used by Cave to verify linearizability which does not require linearization points to be annotated. -
RGSep action inference.
V. Vafeiadis. In VMCAI 2010.
This paper describes the action inference algorithm, which forms the core of Cave's program analyser for proving memory safety. -
Shape-value abstraction for verifying linearizability.
V. Vafeiadis. In VMCAI 2009.
This paper describes shape-value abstraction, an abstraction able to represent the fact that two data structures store the same (or related) abstract values. This abstraction is crucial for finding a abstraction map that is sufficiently strong to prove linearizability.
Linearizability examples
Specifications: stack, queue, set.
| Name | Description |
|---|---|
| Treiber | Treiber's stack |
| Treiber_ext | Treiber's stack (extended version) |
| DCAS_stack | DCAS-based stack |
| DCAS_stack_ext | DCAS-based stack (extended version) |
| 2lock_queue | Michael and Scott two-lock queue |
| 2lock_queue_ext | Michael and Scott two-lock queue (extended version) |
| MSqueue | Michael and Scott non-blocking queue |
| MSqueue_ext | Michael and Scott non-blocking queue (extended version) |
| DGLMqueue | Doherty et al. non-blocking queue |
| DGLMqueue_ext | Doherty et al. non-blocking queue (extended version) |
| CG_set | Coarse-grain set |
| CG_set_lfc | Coarse-grain set + lock-free contains |
| CG_set_nd | Coarse-grain set + no memory dispose |
| LC_set | Lock-coupling set (a.k.a., pessimistic set) |
| LC_set_lfc | Lock-coupling set + lock-free contains |
| LC_set_nd | Lock-coupling set + no memory dispose |
| Vaf_DCAS_set | DCAS-based set with repointing delete |
| Vechev_DCAS_set | Vechev and Yahav DCAS-based set |
Lock-freedom examples
| Name | Description |
|---|---|
| Counter | CAS-based counter |
| TwoCounter | Double CAS-based counter |
| Treiber | Treiber's stack |
| DCAS_stack | DCAS-based stack |
| HSY | Hendler et al. elimination stack |
| MSqueue | Michael and Scott non-blocking queue |
| DGLMqueue | Doherty et al. non-blocking queue |
Related tools
- TVLA is a generic static analyser for 3-valued logic domains and has been used to prove properties of concurrent algorithms, including linearizability if the linearization points are specified by the used.
- SmallfootRG is a RGSep-based memory safety checker by Calcagno, Parkinson and Vafeiadis. It has been superseeded by Cave and is now obsolete.