Decoupling Lock-Free Data Structures from Memory Reclamation for Static Analysis
Verification of concurrent data structures is one of the most challenging tasks in software verification. The topic has received considerable attention over the course of the last decade. Nevertheless, human-driven techniques remain cumbersome and notoriously difficult while automated approaches suffer from limited applicability. The main obstacle for automation is the complexity of concurrent data structures. This is particularly true in the absence of garbage collection. The intricacy of lock-free memory management paired with the complexity of concurrent data structures makes automated verification prohibitive.
In this work we present a method for verifying concurrent data structures and their memory management separately. We suggest two simpler verification tasks that imply the correctness of the data structure. The first task establishes an over-approximation of the reclamation behavior of the memory management. The second task exploits this over-approximation to verify the data structure without the need to consider the implementation of the memory management itself. To make the resulting verification tasks tractable for automated techniques, we establish a second result. We show that a verification tool needs to consider only executions where a single memory location is reused. We implemented our approach and were able to verify linearizability of Michael&Scott’s queue and the DGLM queue for both hazard pointers and epoch-based reclamation. To the best of our knowledge, we are the first to verify such implementations fully automatically.
Wed 16 JanDisplayed time zone: Belfast change
10:35 - 12:03
|A True Positives Theorem for a Static Race Detector|
Nikos Gorogiannis , Peter W. O'Hearn Facebook and University College London, Ilya Sergey Yale-NUS College and National University of SingaporeLink to publication DOI Pre-print Media Attached File Attached
|Decoupling Lock-Free Data Structures from Memory Reclamation for Static Analysis|
Research PapersLink to publication DOI Pre-print Media Attached File Attached
|Pretend Synchrony: Synchronous Verification of Asynchronous Distributed Programs|
Klaus v. Gleissenthall University of California at San Diego, USA, Rami Gökhan Kıcı University of California at San Diego, USA, Alexander Bakst , Deian Stefan University of California San Diego, Ranjit Jhala University of California, San DiegoLink to publication DOI Media Attached
|Weak-Consistency Specification via Visibility Relaxation|
Research PapersLink to publication DOI Media Attached File Attached