Languages

Modular Verification of Linearizability with Non-Fixed Linearization Points

 Authors

 
Abstract
 
Locating linearization points (LPs) is an intuitive approach for proving linearizability, but it is difficult to apply the idea in Hoare-style logic for formal program verification, especially for verifying algorithms whose LPs cannot be statically located in the code. In this paper, we propose a program logic with a lightweight instrumentation mechanism which can verify algorithms with non-fixed LPs, including the most challenging ones that use the helping mechanism to achieve lock-freedom (as in HSY elimination-based stack), or have LPs depending on unpredictable future executions (as in the lazy set algorithm), or involve both features. We also develop a thread-local simulation as the meta-theory of our logic, and show it implies contextual refinement, which is equivalent to linearizability. Using our logic we have successfully verified various classic algorithms, some of which are used in the java.util.concurrent package.
 
Published
 
In Proc. 34th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'13), Seattle, WA, pages 459 - 470, June 2013. ©2013 ACM.