Authors

Jan Hoffmann
Michael Marmar
Zhong Shao

Abstract

This article describes a novel quantitative proof technique for the modular and local verification of lock-freedom. In contrast to proofs based on temporal rely-guarantee requirements, this new quantitative reasoning method can be directly integrated in modern program logics that are designed for the verification of safety properties. Using a single formalism for verifying memory safety and lock-freedom allows a combined correctness proof that verifies both properties simultaneously.

This article presents one possible formalization of this quantitative proof technique by developing a variant of concurrent separation logic (CSL) for total correctness. To enable quantitative reasoning, CSL is extended with a predicate for affine tokens to account for, and provide an upper bound on the number of loop iterations in a program. Lock-freedom is then reduced to total-correctness proofs. Quantitative reasoning is demonstrated in detail, both informally and formally, by verifying the lockfreedom of Treiber's non-blocking stack. Furthermore, it is shown how the technique is used to verify the lock-freedom of more advanced shared-memory data structures that use eliminationbackoff schemes and hazard-pointers.

Published

In Proc. 28th Annual IEEE Symposium on Logic In Computer Science (LICS'13), New Orleans, USA, pages 124-133, June 2013. ©2013 IEEE.

• Conference Paper [PDF]
• Extended Technical Report[PDF]