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.
Paper
-
Proving Lock-Freedom Easily and Automatically.
Xiao Jia, Wei Li, Viktor Vafeiadis.
In CPP 2015. ACM (January 2015)
[PDF]
Supplementary material
- Download the Coq proofs: [ZIP file]
- Download the Cave implementation: [ZIP file]
- Slides presented at CPP'15: [PDF]
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 |