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.


Linearizability examples

Specifications: stack, queue, set.

TreiberTreiber's stack
Treiber_extTreiber's stack (extended version)
DCAS_stackDCAS-based stack
DCAS_stack_extDCAS-based stack (extended version)
2lock_queueMichael and Scott two-lock queue
2lock_queue_extMichael and Scott two-lock queue (extended version)
MSqueueMichael and Scott non-blocking queue
MSqueue_extMichael and Scott non-blocking queue (extended version)
DGLMqueueDoherty et al. non-blocking queue
DGLMqueue_extDoherty et al. non-blocking queue (extended version)
CG_setCoarse-grain set
CG_set_lfcCoarse-grain set + lock-free contains
CG_set_ndCoarse-grain set + no memory dispose
LC_setLock-coupling set (a.k.a., pessimistic set)
LC_set_lfcLock-coupling set + lock-free contains
LC_set_ndLock-coupling set + no memory dispose
Vaf_DCAS_setDCAS-based set with repointing delete
Vechev_DCAS_setVechev and Yahav DCAS-based set

Lock-freedom examples

CounterCAS-based counter
TwoCounterDouble CAS-based counter
TreiberTreiber's stack
DCAS_stackDCAS-based stack
HSYHendler et al. elimination stack
MSqueueMichael and Scott non-blocking queue
DGLMqueueDoherty et al. non-blocking queue

Related tools

Valid XHTML 1.0 Strict