Lock-freedom is a liveness property satisfied by most non-blocking concurrent algorithms. It ensures that at any point at least one thread is making progress towards termination; so the system as a whole makes progress.

As a global property, lock-freedom is typically shown by global proofs or complex iterated arguments. We show that this complexity is not needed in practice. By introducing simple loop depth counters into the programs, we can reduce proving lock-freedom to checking simple local properties on those counters. We have implemented the approach in Cave and report on our findings.


Supplementary material

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
Imprint | Data protection