Peter Gammie
Antony L. Hosking
ABSTRACT
We report on a machine-checked verification of safety for a state-of-the-art, on-the-fly, concurrent, mark-sweep garbage collector that is designed for multi-core architectures with weak memory consistency. The proof explicitly incorporates the relaxed memory semantics of x86 multiprocessors. To our knowledge, this is the first fully machine-checked proof of safety for such a garbage collector. We couch the proof in a framework that system implementers will find appealing, with the fundamental components of the system specified in a simple and intuitive programming language. The abstract model is detailed enough for its correspondence with an assembly language implementation to be straightforward.
- S. Abraham and J. Patel. Parallel garbage collection on a virtual memory system. In International Conference on Parallel Processing, pages 243–246, University Park, Pennsylvania, Aug. 1987.Google Scholar
- J. Alglave, D. Kroening, V. Nimal, and M. Tautschnig. Software verification for weak memory via program transformation. In European Symposium on Programming, volume 7792 of Lecture Notes in Computer Science, pages 512–532, Rome, Italy, Mar. 2013. Springer. doi: 10.1007/978-3-642-37036-6_28. Google ScholarDigital Library
- E. Cohen and B. Schirmer. From total store order to sequential consistency: A practical reduction theorem. In International Conference on Interactive Theorem Proving, volume 6172 of Lecture Notes in Computer Science, pages 403–418, Edinburgh, Scotland, July 2010. Google ScholarDigital Library
- Springer. doi: 10.1007/978-3-642-14052-5_28.Google Scholar
- S. Das, D. L. Dill, and S. Park. Experience with predicate abstraction. In International Conference on Computer Aided Verification, volume 1633 of Lecture Notes in Computer Science, pages 160–171, Trento, Italy, July 1999. Springer. doi: 10.1007/3-540-48683-6_16. Google ScholarDigital Library
- W. P. de Roever, F. S. de Boer, U. Hannemann, J. Hooman, Y. Lakhnech, M. Poel, and J. Zwiers. Concurrency Verification: Introduction to Compositional and Noncompositional Methods, volume 54 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2001. Google ScholarDigital Library
- E. W. Dijkstra, L. Lamport, A. J. Martin, C. S. Scholten, and E. F. M. Steffens. On-the-fly garbage collection: An exercise in cooperation. Commun. ACM, 21(11):966–975, Nov. 1978. doi: 10.1145/359642. Google ScholarDigital Library
- 359655.Google Scholar
- D. Doligez and G. Gonthier. Portable, unobtrusive garbage collection for multiprocessor systems. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 70–83, Portland, Oregon, Jan. 1994. doi: 10.1145/174675.174673. Google ScholarDigital Library
- D. Doligez and X. Leroy. A concurrent generational garbage collector for a multi-threaded implementation of ML. In ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, pages 113–123, Charleston, South Carolina, Jan. 1993. Google ScholarDigital Library
- doi: 10.1145/ 158511.158611.Google Scholar
- M. Felleisen and R. Hieb. The revised report on the syntactic theories of sequential control and state. Theoretical Computer Science, 103(2): 235–271, Sept. 1992. doi: 10.1016/0304-3975(92)90014-7. Google ScholarDigital Library
- X. Feng. Local rely-guarantee reasoning. In ACM SIGPLAN Symposium on Principles of Programming Languages, pages 315–327, Savannah, Georgia, Jan. 2009. doi: 10.1145/1480881.1480922. Google ScholarDigital Library
- G. Gonthier. Verifying the safety of a practical concurrent garbage collector. In International Conference on Computer Aided Verification, volume 1102 of Lecture Notes in Computer Science, pages 462–465, New Brunswick, New Jerseu, July–Aug. 1996. Springer. doi: 10.1007/ 3-540-61474-5_103. Google ScholarDigital Library
- D. Gries. An exercise in proving parallel programs correct. Commun. ACM, 20(12):921–930, Dec. 1977. doi: 10.1145/359897.359903. Google ScholarDigital Library
- C. Hawblitzel and E. Petrank. Automated verification of practical garbage collectors. In ACM SIGPLAN Symposium on Principles of Programming Languages, pages 441–453, Savannah, GA, Jan. 2009. Google ScholarDigital Library
- doi: 10.1145/1480881.1480935.Google Scholar
- S. Jagannathan, V. Laporte, G. Petri, D. Pichardie, and J. Vitek. Atomicity refinement for verified compilation. ACM Trans. Prog. Lang. Syst., 36(2):6:1–30, Apr. 2014. doi: 10.1145/2601339. Google ScholarDigital Library
- R. Jones, A. Hosking, and E. Moss. The Garbage Collection Handbook: The Art of Automatic Memory Management. CRC Applied Algorithms and Data Structures. Chapman & Hall, Aug. 2012. Google ScholarDigital Library
- G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, T. Sewell, H. Tuch, and S. Winwood. seL4: Formal verification of an OS kernel. In ACM SIGOPS Symposium on Operating Systems Principles, pages 207– 220, Big Sky Resort, Montana, Oct. 2009. doi: 10.1145/1629575. Google ScholarDigital Library
- 1629596.Google Scholar
- H. T. Kung and S. W. Song. An efficient parallel garbage collection system and its correctness proof. In Symposium on Foundations of Computer Science, pages 120–131, Providence, Rhode Island, Oct. 1977. IEEE. doi: 10.1109/SFCS.1977.5. Google ScholarDigital Library
- L. Lamport. Garbage collection with multiple processes: an exercise in parallelism. In International Conference on Parallel Processing, pages 50–54, 1976.Google Scholar
- L. Lamport. Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, 2002. Google ScholarDigital Library
- L. Lamport. Who builds a house without drawing blueprints? Commun. ACM, 58(4):38–41, Apr. 2015. doi: 10.1145/2736348. Google ScholarDigital Library
- C. Lin, Y. Chen, and B. Hua. Verification of an incremental garbage collector in Hoare-style logic. International Journal of Software and Informatics, 3(1):67–88, Mar. 2009.Google Scholar
- J. McCarthy. Recursive functions of symbolic expressions and their computation by machine, Part I. Commun. ACM, 3(4):184–195, Apr. 1960. doi: 10.1145/367177.367199. Google ScholarDigital Library
- A. McCreight, Z. Shao, C. Lin, and L. Li. A general framework for certifying garbage collectors and their mutators. In ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 468–479, San Diego, California, June 2007. doi: 10.1145/ 1250734.1250788. Google ScholarDigital Library
- A. McCreight, T. Chevalier, and A. Tolmach. A certified framework for compiling and executing garbage-collected languages. In ACM SIGPLAN International Conference on Functional Programming, pages 273–284, Baltimore, Maryland, Sept. 2010. doi: 10.1145/1863543. Google ScholarDigital Library
- 1863584.Google Scholar
- R. Milner. Communication and Concurrency. Prentice-Hall, Englewood Cliffs, New Jersey, 1989. Google ScholarDigital Library
- S. Owens. Reasoning about the implementation of concurrency abstractions on x86-TSO. In European Conference on Object-Oriented Programming, volume 6183 of Lecture Notes in Computer Science, pages 478–503, Maribor, Slovenia, June 2010. Springer. doi: 10.1007/ 978-3-642-14107-2_23. Google ScholarDigital Library
- S. Park and D. L. Dill. An executable specification and verifier for relaxed memory order. IEEE Transactions on Computers, 48(2):227– 235, 1999. doi: 10.1109/12.752664. Google ScholarDigital Library
- D. Pavlovic, P. Pepper, and D. R. Smith. Formal derivation of concurrent garbage collectors. In International Conference on Mathematics of Program Construction, volume 6120, pages 353–376, Québec City, Canada, June 2010. Springer. doi: 10.1007/978-3-642-13321-3_ 20. Google ScholarDigital Library
- A. M. Pitts. Operational semantics and program equivalence. In International Summer School on Applied Semantics, Advanced Lectures, volume 2395 of Lecture Notes in Computer Science, pages 378–412. Springer, Caminha, Portugal, Sept. 2000. doi: 10.1007/ 3-540-45699-6_8. Google ScholarDigital Library
- F. Pizlo, L. Ziarek, P. Maj, A. L. Hosking, E. Blanton, and J. Vitek. Schism: Fragmentation-tolerant real-time garbage collection. In ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 146–159, Toronto, Canada, June 2010. doi: 10.1145/ 1806596.1806615. Google ScholarDigital Library
- T. Ridge. Verifying distributed systems: the operational approach. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 429–440, Savannah, Georgia, Jan. 2009. doi: 10. 1145/1480881.1480934. Google ScholarDigital Library
- T. Ridge. A rely-guarantee proof system for x86-TSO. In International Conference on Verified Software: Theories, Tools, Experiments, volume 6217 of Lecture Notes in Computer Science, pages 55–70, Edinburgh, Scotland, Aug. 2010. Springer. doi: 10.1007/978-3-642-15057-9_ 4. Google ScholarDigital Library
- S. Sarkar, P. Sewell, J. Alglave, L. Maranget, and D. Williams. Understanding POWER multiprocessors. In ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 175–186, San Jose, California, June 2011. doi: 10.1145/1993498.1993520. Google ScholarDigital Library
- J. Sevcík, V. Vafeiadis, F. Zappa Nardelli, S. Jagannathan, and P. Sewell. CompCertTSO: A verified compiler for relaxed-memory concurrency. J. ACM, 60(3):22, 2013. doi: 10.1145/2487241.2487248. Google ScholarDigital Library
- P. Sewell, S. Sarkar, S. Owens, F. Z. Nardelli, and M. O. Myreen. x86-TSO: a rigorous and usable programmer’s model for x86 multiprocessors. Commun. ACM, 53(7):89–97, July 2010. doi: 10.1145/ 1785414.1785443. Google ScholarDigital Library
- N. Torp-Smith, L. Birkedal, and J. C. Reynolds. Local reasoning about a copying garbage collector. ACM Trans. Prog. Lang. Syst., 30(4), July 2008. doi: 10.1145/1377492.1377499. Google ScholarDigital Library
- A. Turon, V. Vafeiadis, and D. Dreyer. GPS: Navigating weak memory with ghosts, protocols, and separation. In ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, pages 691–707, Portland, Oregon, Oct. 2014. doi: 10. 1145/2660193.2660243. Google ScholarDigital Library
- M. T. Vechev, D. F. Bacon, P. Cheng, and D. Grove. Derivation and evaluation of concurrent collectors. In ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 341–353, Ottawa, Canada, June 2007. doi: 10.1145/1133981.1134022.Google Scholar
- M. Wenzel. Shared-memory multiprocessing for interactive theorem proving. In International Conference on Interactive Theorem Proving, volume 7998 of Lecture Notes in Computer Science, pages 418–434, Rennes, France, July 2013. Springer. doi: 10.1007/ 978-3-642-39634-2_30. Google ScholarDigital Library
- G. Winskel. The Formal Semantics of Programming Languages. MIT Press, Cambridge, Massachusetts, 1993. Google ScholarCross Ref
- T. Yuasa. Real-time garbage collection on general-purpose machines. Journal of Systems and Software, 11(3):181–198, Mar. 1990. doi: 10. 1016/0164-1212(90)90084-Y. Introduction Contributions The Verified Collector Abstractions and Invariants The Collector Marking Relaxed Memory: x86-TSO Formal Verification in Isabelle/HOL Model Formal Abstractions and Invariants Concluding Remarks Google ScholarDigital Library
Index Terms
- Relaxing safely: verified on-the-fly garbage collection for x86-TSO
Recommendations
Relaxing safely: verified on-the-fly garbage collection for x86-TSO
PLDI '15We report on a machine-checked verification of safety for a state-of-the-art, on-the-fly, concurrent, mark-sweep garbage collector that is designed for multi-core architectures with weak memory consistency. The proof explicitly incorporates the relaxed ...
Age-based garbage collection
Modern generational garbage collectors look for garbage among the young objects, because they have high mortality; however, these objects include the very youngest objects, which clearly are still live. We introduce new garbage collection algorithms, ...
A Simpler Reduction Theorem for x86-TSO
VSTTE 2015: Revised Selected Papers of the 7th International Conference on Verified Software: Theories, Tools, and Experiments - Volume 9593The memory model of x86-TSO allows code to run in weakly synchronous fashion, resulting in a smaller memory bottleneck but also possibly causing inconsistent memory effects. Cohen and Schirmer [5] described an efficient software discipline which ...
Comments