H. Attiya
ABSTRACT
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 .
- D. Amit, N. Rinetzky, T. Reps, M. Sagiv, and E. Yahav. Comparison under abstraction for verifying linearizability. In CAV, 2007. Google Scholar
Digital Library
- H. Attiya, G. Ramalingam, and N. Rinetzky. Sequential verification of serializability. Technical report. http://www.dcs.qmul.ac.uk/~maon/pubs/seqser.pdf.Google Scholar
- J. Berdine, A. Chawdhary, B. Cook, D. Distefano, and P. O'Hearn. Variance analyses from invariance analyses. In POPL, 2007. Google ScholarDigital Library
- J. Berdine, T. Lev-Ami, R. Manevich, G. Ramalingam, and M. Sagiv. Thread quantification for concurrent shape analysis. In CAV, 2008. Google ScholarDigital Library
- P. A. Bernstein, V. Hadzilacos, and N. Goodman. Concurrency Control and Recovery in Database Systems. Addison-Wesley, 1987. Google ScholarDigital Library
- A. R. Bradley, Z. Manna, and H. B. Sipma. The polyranking principle. In ICALP, 2005. Google ScholarDigital Library
- V. K. Chaudhri and V. Hadzilacos. Safe locking policies for dynamic databases. In PODS, 1995. Google ScholarDigital Library
- S. Cherem, T. M. Chilimbi, and S. Gulwani. Inferring locks for atomic sections. In PLDI, 2008. Google ScholarDigital Library
- E. M. Clarke, Jr., O. Grumberg, and D. A. Peled. Model checking. MIT Press, Cambridge, MA, USA, 1999. Google ScholarDigital Library
- B. Cook, A. Podelski, and A. Rybalchenko. Termination proofs for systems code. In PLDI, 2006. Google ScholarDigital Library
- T. Elmas, S. Qadeer, and S. Tasiran. A calculus of atomic actions. In POPL, 2009. Google ScholarDigital Library
- F. Fich, M. Herlihy, and N. Shavit. On the space complexity of randomized synchronization. JACM, 45(5), 1998. Google ScholarDigital Library
- C. Flanagan and S. Qadeer. A type and effect system for atomicity. In PLDI, 2003. Google ScholarDigital Library
- M. P. Herlihy and J. M. Wing. Linearizability: a correctness condition for concurrent objects. TOPLAS, 12(3), 1990. Google ScholarDigital Library
- Z. M. Kedem and A. Silberschatz. A characterization of database graphs admitting a simple locking protocol. Acta Informatica, 16, 1981.Google Scholar
- C. S. Lee, N. D. Jones, and A. M. Ben-Amram. The size-change principle for program termination. In POPL, 2001. Google ScholarDigital Library
- T. Lev-Ami, T. Reps, M. Sagiv, and R. Wilhelm. Putting static analysis to work for verification: A case study. In ISSTA, 2000. Google ScholarDigital Library
- T. Lev-Ami and M. Sagiv. TVLA: A framework for Kleene based static analysis. In SAS. Springer, 2000.Google Scholar
- R. J. Lipton. Reduction: a method of proving properties of parallel programs. CACM, 18(12), 1975. Google ScholarDigital Library
- A. Loginov, T. W. Reps, and M. Sagiv. Automated verification of the deutsch-schorr-waite tree-traversal algorithm. In SAS, 2006. Google ScholarDigital Library
- R. Manevich, T. Lev-Ami, G. Ramalingam, M. Sagiv, and J. Berdine. Heap decomposition for concurrent shape analysis. In SAS, 2008. Google ScholarDigital Library
- A. Miné. The octagon abstract domain. HOSC, 19(1), 2006. Google ScholarDigital Library
- C. H. Papadimitriou. The serializability of concurrent database updates. J. ACM, 26(4), 1979. Google ScholarDigital Library
- M. Segalov, T. Lev-Ami, R. Manevich, G. Ramalingam, and M. Sagiv. Abstract transformers for thread correlation analysis. In APLAS, 2009. Google ScholarDigital Library
- S. D. Stoller and E. Cohen. Optimistic synchronization-based state-space reduction. FMSD, 28(3), 2006. Google ScholarDigital Library
- R. H. Thomas. A majority consensus approach to concurrency control for multiple copy databases. ACM Trans. Database Syst., 4(2), 1979. Google ScholarDigital Library
- V. Vafeiadis. Shape-value abstraction for verifying linearizability. In VMCAI, 2009. Google ScholarDigital Library
- G. Weikum and G. Vossen. Transactional Information Systems: Theory, Algorithms, and the Practice of Concurrency Control. Morgan Kaufmann, 2001. Google ScholarDigital Library
Index Terms
- Sequential verification of serializability
Recommendations
Sequential verification of serializability
POPL '10Serializability 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 ...
Automatic fine-grain locking using shape properties
OOPSLA '11We present a technique for automatically adding fine-grain locking to an abstract data type that is implemented using a dynamic forest -i.e., the data structures may be mutated, even to the point of violating forestness temporarily during the execution ...
Automatic fine-grain locking using shape properties
OOPSLA '11: Proceedings of the 2011 ACM international conference on Object oriented programming systems languages and applicationsWe present a technique for automatically adding fine-grain locking to an abstract data type that is implemented using a dynamic forest -i.e., the data structures may be mutated, even to the point of violating forestness temporarily during the execution ...
Comments