Abstract
Virtual machine based software model checkers like jpf and MoonWalker spend up to half of their verification time on garbage collection. This is no surprise as after nearly each transition the heap has to be cleaned from garbage. To improve this, this paper presents the Memoised Garbage Collection (MGC) algorithm, which exploits the (typical) locality of transitions to incrementally perform garbage collection. MGC tracks the depths of objects efficiently and only purges objects whose depths have become infinite, hence unreachable. MGC was experimentally evaluated via an implementation in our model checker MoonWalker and benchmarks using the parallel Java Grande Forum benchmark suite. By using MGC, a performance increase up to 78% was measured over the traditional Mark&Sweep implementation.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Aan de Brugh, N.H.M.: Software Model Checking for Mono. Master’s thesis, University of Twente, Enschede, The Netherlands (August 2006)
Aan de Brugh, N.H.M., Ruys, T.C., Nguyen, V.Y.: MoonWalker: Verification of .NET Programs. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 170–173. Springer, Heidelberg (2009)
Cherkassky, B.V., Goldberg, A.V., Silverstein, C.: Buckets, Heaps, Lists, and Monotone Priority Queues. In: Saks, M. (ed.) SODA 1997: Proceedings of the eighth annual ACM-SIAM symposium on Discrete algorithms, Philadelphia, PA, USA, pp. 83–92. Society for Industrial and Applied Mathematics (1997)
Corbett, J.C., Dwyer, M.B., Hatcliff, J., Bandera, R.: A Source-Level Interface for Model Checking Java Programs. In: ICSE 2000, pp. 762–765 (2000)
Dijkstra, E.: A Note on Two Problems in Connexion with Graphs. In: Numerische Mathematik, vol. 1, pp. 269–271 (1959)
Elmas, T., Qadeer, S., Tasiran, S.: Goldilocks: Efficiently Computing the Happens-Before Relation Using Locksets. In: Havelund, K., Núñez, M., Roşu, G., Wolff, B. (eds.) FATES 2006 and RV 2006. LNCS, vol. 4262, pp. 193–208. Springer, Heidelberg (2006)
Flanagan, C., Godefroid, P.: Dynamic Partial-Order Reduction for Model Checking Software. In: Palsberg, J., Abadi, M. (eds.) POPL 2005, pp. 110–121. ACM, New York (2005)
Grieskamp, W., Tillmann, N., Schulte, W.: XRT- Exploring Runtime for. NET Architecture and Applications. In: Cook, B., Stoller, S., Visser, W. (eds.) Proceedings of the Workshop on Software Model Checking, SoftMC 2005. Electr. Notes Theor. Comput. Sci., vol. 144, pp. 3–26 (2006)
Havelund, K.: Java PathFinder, A Translator from Java to Promela. In: Dams, D.R., Gerth, R., Leue, S., Massink, M. (eds.) SPIN 1999. LNCS, vol. 1680, p. 152. Springer, Heidelberg (1999)
Holzmann, G.J.: The Spin Model Checker – Primer and Reference Manual. Addison-Wesley, Boston (2004)
Iosif, R.: Exploiting Heap Symmetries in Explicit-State Model Checking of Software. In: ASE 2001, pp. 254–261. IEEE Computer Society, Los Alamitos (2001)
Iosif, R.: Symmetry Reductions for Model Checking of Concurrent Dynamic Software. STTT 6(4), 302–319 (2004)
Iosif, R., Sisto, R.: Using Garbage Collection in Model Checking. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885, pp. 20–33. Springer, Heidelberg (2000)
Jones, R., Lins, R.: Garbage Collection. John Wiley & Sons, Chichester (1996)
Lerda, F., Visser, W.: Addressing Dynamic Issues of Program Model Checking. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 80–102. Springer, Heidelberg (2001)
McCarthy, J.: Recursive Functions of Symbolic Expressions and Their Computation by Machine, Part I. Communications of the ACM 3(4), 184–195 (1960)
Musuvathi, M., Dill, D.L.: An Incremental Heap Canonicalization Algorithm. In: Godefroid, P. (ed.) SPIN 2005. LNCS, vol. 3639, pp. 28–42. Springer, Heidelberg (2005)
Nguyen, V.Y.: Optimising Techniques for Model Checkers. Master’s thesis, University of Twente, Enschede, The Netherlands (December 2007)
Ramalingam, G., Reps, T.W.: An Incremental Algorithm for a Generalization of the Shortest-Path Problem. Journal Algorithms 21(2), 267–305 (1996)
Robby, Dwyer, M.B., Hatcliff, J.: Domain-specific Model Checking Using The Bogor Framework. In: ASE 2006, pp. 369–370. IEEE Computer Society, Los Alamitos (2006)
Ruys, T.C., Aan de Brugh, N.H.M.: MMC: the Mono Model Checker. Electr. Notes Theor. Comput. Sci. 190(1), 149–160 (2007); Proc. of Bytecode 2007
Smith, L.A., Bull, J.M., Obdrzálek, J.: A Parallel Java Grande Benchmark Suite. In: ACM/IEEE Conference on Supercomputing (SC 2001). ACM, New York (2001)
Visser, W., Havelund, K., Brat, G.P., Park, S.: Model Checking Programs. In: ASE 2000, pp. 3–12. IEEE Computer Society, Los Alamitos (2000)
The Java Grande Forum Benchmark Suite, http://www.epcc.ed.ac.uk/research/activities/java-grande/
Java PathFinder, http://javapathfinder.sourceforge.net/
MoonWalker, http://www.cs.utwente.nl/~ruys/moonwalker/
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Nguyen, V.Y., Ruys, T.C. (2009). Memoised Garbage Collection for Software Model Checking. In: Kowalewski, S., Philippou, A. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2009. Lecture Notes in Computer Science, vol 5505. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-00768-2_20
Download citation
DOI: https://doi.org/10.1007/978-3-642-00768-2_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-00767-5
Online ISBN: 978-3-642-00768-2
eBook Packages: Computer ScienceComputer Science (R0)