Abstract
Verifying program transformations usually requires proving that the resulting program (the target) refines or is equivalent to the original one (the source). However, the refinement relation between individual sequential threads cannot be preserved in general with the presence of parallel compositions, due to instruction reordering and the different granularities of atomic operations at the source and the target. On the other hand, the refinement relation defined based on fully abstract semantics of concurrent programs assumes arbitrary parallel environments, which is too strong and cannot be satisfied by many well-known transformations.
In this article, we propose a Rely-Guarantee-based Simulation (RGSim) to verify concurrent program transformations. The relation is parametrized with constraints of the environments that the source and the target programs may compose with. It considers the interference between threads and their environments, thus is less permissive than relations over sequential programs. It is compositional with respect to parallel compositions as long as the constraints are satisfied. Also, RGSim does not require semantics preservation under all environments, and can incorporate the assumptions about environments made by specific program transformations in the form of rely/guarantee conditions. We use RGSim to reason about optimizations and prove atomicity of concurrent objects. We also propose a general garbage collector verification framework based on RGSim, and verify the Boehm et al. concurrent mark-sweep GC.
- Martín Abadi and Leslie Lamport. 1991. The existence of refinement mappings. Theor. Comput. Sci. 82, 2, 253--284. Google ScholarDigital Library
- Martín Abadi and Gordon Plotkin. 2009. A model of cooperative threads. In Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’09). ACM Press, New York, 29--40. Google ScholarDigital Library
- Katherine Barabash, Ori Ben-Yitzhak, Irit Goft, Elliot K. Kolodner, Victor Leikehman, Yoav Ossia, Avi Owshanko, and Erez Petrank. 2005. A parallel, incremental, mostly concurrent garbage collector for servers. ACM Trans. Program. Lang. Syst. 27, 6, 1097--1146. Google ScholarDigital Library
- Nick Benton. 2004. Simple relational correctness proofs for static analyses and program transformations. In Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’04). ACM Press, New York, 14--25. Google ScholarDigital Library
- Nick Benton and Chung-Kil Hur. 2009. Biorthogonality, step-indexing and compiler correctness. In Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming (ICFP’09). ACM Press, New York, 97--108. Google ScholarDigital Library
- Hans-Juergen Boehm. 2005. Threads cannot be implemented as a library. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’05). ACM Press, New York, 261--268. Google ScholarDigital Library
- Hans-Juergen Boehm and Sarita V. Adve. 2008. Foundations of the C++ concurrency memory model. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’08). ACM Press, New York, 68--78. Google ScholarDigital Library
- Hans-Juergen Boehm, Alan J. Demers, and Scott Shenker. 1991. Mostly parallel garbage collection. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’91). ACM Press, New York, 157--164. Google ScholarDigital Library
- Stephen D. Brookes. 1996. Full abstraction for a shared-variable parallel language. Inf. Comput. 127, 2, 145--163.Google ScholarCross Ref
- Sebastian Burckhardt, Madanlal Musuvathi, and Vasu Singh. 2010. Verifying local transformations on relaxed memory models. In Proceedings of the 19th Joint European Conference on Theory and Practice of Software and the International Conference on Compiler Construction (CC’10/ETAPS’10). Springer, 104--123. Google ScholarDigital Library
- Coq Development Team. 2010. The Coq proof assistant reference manual. The Coq release v8.3. http://coq.inria.fr/V8.3/refman/Google Scholar
- David Dice, Ori Shalev, and Nir Shavit. 2006. Transactional locking ii. In Proceedings of the 20th International Conference on Distributed Computing (DISC’06). Springer, 194--208. Google ScholarDigital Library
- Tayfun Elmas, Shaz Qadeer, Ali Sezgin, Omer Subasi, and Serdar Tasiran. 2010. Simplifying linearizability proofs with reduction and abstraction. In Proceedings of the 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’10). Springer, 296--311. Google ScholarDigital Library
- Xinyu Feng. 2009. Local rely-guarantee reasoning. In Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’09). ACM Press, New York, 315--327. Google ScholarDigital Library
- Ivana Filipović, Peter O’Hearn, Noam Rinetzky, and Hongseok Yang. 2010. Abstraction for concurrent objects. Theor. Comput. Sci. 411, 51--52, 4379--4398. Google ScholarDigital Library
- David S. Gladstein and Mitchell Wand. 1996. Compiler correctness for concurrent languages. In Proceedings of the 1st International Conference on Coordination Languages and Models (COORDINATION’96). Lecture Notes in Computer Science, vol. 1061, Springer, 231--248. Google ScholarDigital Library
- Maurice Herlihy and Nir Shavit. 2008. The Art of Multiprocessor Programming. Morgan Kaufmann, San Fransisco. Google ScholarDigital Library
- Charles A. R. Hoare. 1972. Proof of correctness of data representations. Acta Inf. 1, 4, 271--281. Google ScholarDigital Library
- Chung-Kil Hur and Derek Dreyer. 2011. A Kripke logical relation between ML and assembly. In Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’11). ACM Press, New York, 133--146. Google ScholarDigital Library
- Cliff B. Jones. 1983. Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst. 5, 4, 596--619. Google ScholarDigital Library
- Kalpesh Kapoor, Kamal Lodaya, and Uday Reddy. 2011. Fine-grained concurrency with separation logic. J. Philos. Logic 40, 5, 583--632.Google ScholarCross Ref
- Xavier Leroy. 2009. A formally verified compiler back-end. J. Autom. Reason. 43, 4, 363--446. Google ScholarDigital Library
- Hongjin Liang, Xinyu Feng, and Ming Fu. 2012. A rely-guarantee-based simulation for verifying concurrent program transformations. In Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’12). ACM Press, New York, 455--468. Google ScholarDigital Library
- Andreas Lochbihler. 2010. Verifying a compiler for java threads. In Proceedings of the 19th European Conference on Programming Languages and Systems (ESOP’10). Springer, 427--447. Google ScholarDigital Library
- Andrew McCreight, Zhong Shao, Chunxiao Lin, and Long Li. 2007. A general framework for certifying garbage collectors and their mutators. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’07). ACM Press, New York, 468--479. Google ScholarDigital Library
- Matthew Parkinson, Richard Bornat, and Cristiano Calcagno. 2006. Variables as resource in hoare logics. In Proceedings of the 21st Annual IEEE Symposium on Logic in Computer Science (LICS’06). IEEE Computer Society, 137--146. Google ScholarDigital Library
- Dusko Pavlovic, Peter Pepper, and Douglas R. Smith. 2010. Formal derivation of concurrent garbage collectors. In Proceedings of the 10th International Conference on Mathematics of Program Construction (MPC’10). 353--376. Google ScholarDigital Library
- John C. Reynolds. 2002. Separation logic: A logic for shared mutable data structures. In Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science (LICS’02). IEEE Computer Society, 55--74. Google ScholarDigital Library
- Jaroslav Ševčík, Viktor Vafeiadis, Francesco Zappa Nardelli, Suresh Jagannathan, and Peter Sewell. 2011. Relaxed-memory concurrency and verified compilation. In Proceedings of the 38th ACM SIGPLANSIGACT Symposium on Principles of Programming Languages (POPL’11). ACM Press, New York, 43--54. Google ScholarDigital Library
- R. Kent Treiber. 1986. System programming: Coping with parallelism. Tech. rep. RJ 5118, IBM Almaden Research Center.Google Scholar
- Aaron Turon and Mitchell Wand. 2011. A separation logic for refining concurrent objects. In Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’11). ACM Press, New York, 247--258. Google ScholarDigital Library
- Viktor Vafeiadis. 2008. Modular fine-grained concurrency verification. Tech. rep. UCAM-CL-TR-726, University of Cambridge, Computer Laboratory.Google Scholar
- Viktor Vafeiadis and Matthew J. Parkinson. 2007. A marriage of rely/guarantee and separation logic. In Proceedings of the 18th International Conference on Concurrency Theory (CONCUR’07). Springer, 256--271. Google ScholarDigital Library
- Martin T. Vechev, Eran Yahav, and David F. Bacon. 2006. Correctness-preserving derivation of concurrent garbage collection algorithms. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’06). ACM Press, New York, 341--353. Google ScholarDigital Library
- Mitchell Wand. 1995. Compiler correctness for parallel languages. In Proceedings of the 7th International Conference on Functional Programming Languages and Computer Architecture (FPCA’95). ACM Press, New York, 120--134. Google ScholarDigital Library
- Hongseok Yang. 2007. Relational separation logic. Theor. Comput. Sci. 375, 1--3, 308--334. Google ScholarDigital Library
Index Terms
- Rely-Guarantee-Based Simulation for Compositional Verification of Concurrent Program Transformations
Recommendations
Local rely-guarantee reasoning
POPL '09: Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languagesRely-Guarantee reasoning is a well-known method for verification of shared-variable concurrent programs. However, it is difficult for users to define rely/guarantee conditions, which specify threads' behaviors over the whole program state. Recent ...
A rely-guarantee-based simulation for verifying concurrent program transformations
POPL '12Verifying program transformations usually requires proving that the resulting program (the target) refines or is equivalent to the original one (the source). However, the refinement relation between individual sequential threads cannot be preserved in ...
A rely-guarantee-based simulation for verifying concurrent program transformations
POPL '12: Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languagesVerifying program transformations usually requires proving that the resulting program (the target) refines or is equivalent to the original one (the source). However, the refinement relation between individual sequential threads cannot be preserved in ...
Comments