Paper Info
Title
Quantitative Reasoning for Proving Lock-Freedom
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 lock-freedom 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 elimination-back off schemes and hazard-pointers.
Year
DOI
Venue
2013
10.1109/LICS.2013.18
Logic in Computer Science
Keywords
Field
DocType
concurrency theory,formal verification,inference mechanisms,program control structures,shared memory systems,temporal logic,theorem proving,CSL,Treiber nonblocking stack,affine token,concurrent separation logic,elimination-backoff scheme,hazard-pointer,local verification,lock-freedom,memory safety verification,modern program logic,modular verification,program loop iteration,quantitative proof technique,quantitative reasoning,safety properties,shared-memory data structure,temporal logic,temporal rely-guarantee requirement,total-correctness proof,Concurrency,Liveness,Lock-Freedom,Non-Blocking Data Structures,Quantitative Analysis,Separation Logic
Discrete mathematics,Separation logic,Programming language,Concurrency,Computer science,Automated theorem proving,Correctness,Theoretical computer science,Mathematical proof,Temporal logic,Formal verification,Qualitative reasoning
Conference
ISSN
ISBN
Citations 
1043-6871
978-1-4799-0413-6
13
PageRank 
References 
Authors
0.58
27
3
Name
Order
Citations
PageRank
Jan Hoffmannand120316.61
Michael Marmar2130.58
Zhong Shao389768.80