Title :
Quantitative Reasoning for Proving Lock-Freedom
Author :
Hoffmann, J. ; Marmar, Michael ; 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 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-backoff schemes and hazard-pointers.
Keywords :
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; Cognition; Data structures; Educational institutions; Interference; Safety; Synchronization; Upper bound; Concurrency; Liveness; Lock-Freedom; Non-Blocking Data Structures; Quantitative Analysis; Separation Logic;
Conference_Titel :
Logic in Computer Science (LICS), 2013 28th Annual IEEE/ACM Symposium on
Conference_Location :
New Orleans, LA
Print_ISBN :
978-1-4799-0413-6
DOI :
10.1109/LICS.2013.18