Abstract
We present a case study in using the PVS interactive theorem prover to formally model and verify properties of a tricolour garbage collection algorithm. We model the algorithm using state transition systems and verify safety and liveness properties in linear temporal logic. We set up two systems, each of which models the algorithm itself, object allocation, and the behaviour of user programs. The models differ in how concretely they model the heap. We verify the properties of the more abstract system, and then, once a refinement relation is exhibited between the systems, we show the more concrete system to have corresponding properties.
We discuss the linear temporal logic framework we set up, commenting in particular on how we handle fairness and how we use a ‘leads-to-via’ predicate to reason about the propagation of properties that are stable in specified regions of system state spaces. We also describe strategies (tactics) we wrote to improve the quality of interaction and increase the degree of automation.
This work was supported by the UK Engineering and Physical Sciences Research Council under grant GR/J85509 and, while the author was a Visiting Fellow in the Computer Science Laboratory of SRI International in Menlo Park, California USA, by the US National Science Foundation under contract CCR-9509931.
Preview
Unable to display preview. Download preview PDF.
References
Rajeev Alur and Thomas A. Henzinger, editors. Computer Aided Verification: 8th International Conference, volume 1102 of Lecture Notes in Computer Science. Springer, July 1996.
Mordechai Ben-Ari. Algorithms for on-the-fly garbage collection. ACM Transactions on Programming Languages and Systems, 6(3):333–344, July 1984.
Glenn Bruns. Distributed Systems Analysis with CCS. Prentice Hall Europe, 1997.
K. Mani Chandy and Jayadev Misra. Parallel Program Design: A Foundation. Addison Wesley, 1988.
Ching-Tsun Chou. Predicates, temporal logic, and simulations. In Jeffrey J. Joyce and Carl-Johan H. Seger, editors, Higher Order Logic Theorem Proving and Its Applications: 6th International Workshop, HUG '93., volume 780 of Lecture Notes in Computer Science, pages 310–323. Springer-Verlag, August 1993.
Edsger W. Dijkstra, Leslie Lamport, A. J. Martin, C. S. Scholten, and E. F. M. Steffens. On-the-fly garbage collection: An exercise in cooperation. Communications of the ACM, 21(11):966–975, November 1978.
Dov M. Gabbay. Labelled deductive systems, volume 1 of Oxford Logic Guides. Oxford University Press (Imprint: Clarendon Press), 1996.
Georges Gonthier. Verifying the safety of a practical concurrent garbage collector. In Alur and Henzinger [1].
Klaus Havelund. Mechanical verification of a garbage collector. Available from http://www.cs.auc.dk/~havelund/, May 1996.
Klaus Havelund and Natarajan Shankar. A mechanized refinement proof for a garbage collector. Available from http://www.cs.auc.dk/~havelund/, December 1996.
Richard Jones and Rafael Lins. Garbage Collection: Algorithms for Automatic Dynamic memory Management. John Wiley & Sons, 1996.
Leslie Lamport. The temporal logic of actions. ACM Transactions on Programming Languages and Systems, 16(3):872–923, May 1994.
Zohar Manna and Amir Pnueli. Completing the temporal picture. Theoretical Computer Science, 83:97–130, 1991.
Zohar Manna and Amir Pnueli. Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, 1991.
Stephan Merz. Yet another encoding of TLA in Isabelle. Available from http://www4.informatik.tu-muenchen.de/~merz/isabelle/. The encoding described by this note accompanies the Isabelle98 release.
Susan Owicki and Leslie Lamport. Proving liveness properties of concurrent programs. ACM Transactions on Programming Languages and Systems, 4(3):455–495, July 1982.
S. Owre, J.M. Rushby, and N. Shankar. PVS: A prototype verification system. In D. Kapur, editor, 11th Conference on Automated Deduction, volume 607 of Lecture Notes in Artificial Intelligence, pages 748–752. Springer-Verlag, 1992. See http://www.csl.sri.com/pvs.html for up-to-date information on PVS.
David M. Russinoff. A mechanically verified garbage collector. Formal Aspects of Computing, 6:359–390, 1994.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Jackson, P.B. (1998). Verifying a garbage collection algorithm. In: Grundy, J., Newey, M. (eds) Theorem Proving in Higher Order Logics. TPHOLs 1998. Lecture Notes in Computer Science, vol 1479. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0055139
Download citation
DOI: https://doi.org/10.1007/BFb0055139
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64987-8
Online ISBN: 978-3-540-49801-8
eBook Packages: Springer Book Archive