Hagit Attiya, Ganesan Ramalingam, and Noam Rinetzky
Serializability is a commonly used correctness condition in concurrent programming. When a concurrent module is serializable, certain other properties of the module can be verified by considering only its sequential executions. In many cases, concurrent modules guarantee serializability by using standard locking protocols, such as tree locking or two-phase locking. Unfortunately, according to the existing literature, verifying that a concurrent module adheres to these protocols requires considering concurrent interleavings. In this paper, we show that adherence to a large class of locking protocols (including tree locking and two-phase locking) can be verified by considering only sequential executions. The main consequence of our results is that in many cases, the (manual or automatic) verification of serializability can itself be done using sequential reasoning. We have implemented a shape analysis that uses sequential reasoning to verify that a concurrent heap-manipulating module adheres to the tree (hand-over-hand) locking protocol. Our analyzer also verifies other aspects of partial correctness such as memory safety, structural (shape) properties, and sortedness, as well as termination. We have used our analyzer to verify concurrent list and tree modules implementations that use an unbounded heap an allow for an unbounded number of threads. Our preliminary experimental results show that the sequential reduction greatly reduces the cost of the analysis. We note that, for the best of our knowledge, our analyzer is the first to be able to automatically analyze an implementation of concurrent tree which uses fine-grained locking.
In Principles of Programming Languages (POPL)
Publisher Association for Computing Machinery, Inc.
Copyright © 2007 by the Association for Computing Machinery, Inc. Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, to republish, to post on servers, or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from Publications Dept, ACM Inc., fax +1 (212) 869-0481, or email@example.com. The definitive version of this paper can be found at ACM’s Digital Library --http://www.acm.org/dl/.