Memoised Garbage Collection for Software Model Checking

V.Y. Nguyen; T.C. Ruys

doi:10.1007/978-3-642-00768-2_20

Memoised Garbage Collection for Software Model Checking

V.Y. Nguyen, T.C. Ruys

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

4 Citations (Scopus)

Abstract

Virtual machine based software model checkers like JPF and MoonWalker spend up to half of their veri��?cation 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 eﬃciently and only purges objects whose depths have become in��?nite, 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.

Original language	Undefined
Title of host publication	Proceedings of the 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2009)
Editors	S. Kowalewski, A. Philippou
Place of Publication	Berlin
Publisher	Springer
Pages	201-214
Number of pages	14
ISBN (Print)	978-3-642-00767-5
DOIs	https://doi.org/10.1007/978-3-642-00768-2_20
Publication status	Published - Mar 2009
Event	15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2009) - York, UK Duration: 22 Mar 2009 → 29 Mar 2009

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Verlag
Volume	5505

Conference

Conference	15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2009)
Period	22/03/09 → 29/03/09
Other	22-29 March 2009

Keywords

IR-67808
EWI-15713
FMT-MC: MODEL CHECKING
METIS-263923

Access to Document

10.1007/978-3-642-00768-2_20

http://eprints.eemcs.utwente.nl/secure2/15713/01/nguyen-ruys-tacas-2009-final-draft.pdf

Cite this

Nguyen, V. Y., & Ruys, T. C. (2009). Memoised Garbage Collection for Software Model Checking. In S. Kowalewski, & A. Philippou (Eds.), Proceedings of the 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2009) (pp. 201-214). [10.1007/978-3-642-00768-2_20] (Lecture Notes in Computer Science; Vol. 5505). Springer. https://doi.org/10.1007/978-3-642-00768-2_20

@inproceedings{4f79310ffc9642bd9aea63f828f80294,

title = "Memoised Garbage Collection for Software Model Checking",

abstract = "Virtual machine based software model checkers like JPF and MoonWalker spend up to half of their veri��?cation 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 eﬃciently and only purges objects whose depths have become in��?nite, 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.",

keywords = "IR-67808, EWI-15713, FMT-MC: MODEL CHECKING, METIS-263923",

author = "V.Y. Nguyen and T.C. Ruys",

note = "10.1007/978-3-642-00768-2_20 ; null ; Conference date: 22-03-2009 Through 29-03-2009",

year = "2009",

month = mar,

doi = "10.1007/978-3-642-00768-2_20",

language = "Undefined",

isbn = "978-3-642-00767-5",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "201--214",

editor = "S. Kowalewski and A. Philippou",

booktitle = "Proceedings of the 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2009)",

}

Nguyen, VY & Ruys, TC 2009, Memoised Garbage Collection for Software Model Checking. in S Kowalewski & A Philippou (eds), Proceedings of the 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2009)., 10.1007/978-3-642-00768-2_20, Lecture Notes in Computer Science, vol. 5505, Springer, Berlin, pp. 201-214, 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2009), 22/03/09. https://doi.org/10.1007/978-3-642-00768-2_20

Memoised Garbage Collection for Software Model Checking. / Nguyen, V.Y.; Ruys, T.C.

Proceedings of the 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2009). ed. / S. Kowalewski; A. Philippou. Berlin : Springer, 2009. p. 201-214 10.1007/978-3-642-00768-2_20 (Lecture Notes in Computer Science; Vol. 5505).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Memoised Garbage Collection for Software Model Checking

AU - Nguyen, V.Y.

AU - Ruys, T.C.

N1 - 10.1007/978-3-642-00768-2_20

PY - 2009/3

Y1 - 2009/3

N2 - Virtual machine based software model checkers like JPF and MoonWalker spend up to half of their veri��?cation 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 eﬃciently and only purges objects whose depths have become in��?nite, 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.

AB - Virtual machine based software model checkers like JPF and MoonWalker spend up to half of their veri��?cation 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 eﬃciently and only purges objects whose depths have become in��?nite, 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.

KW - IR-67808

KW - EWI-15713

KW - FMT-MC: MODEL CHECKING

KW - METIS-263923

U2 - 10.1007/978-3-642-00768-2_20

DO - 10.1007/978-3-642-00768-2_20

M3 - Conference contribution

SN - 978-3-642-00767-5

T3 - Lecture Notes in Computer Science

SP - 201

EP - 214

BT - Proceedings of the 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2009)

A2 - Kowalewski, S.

A2 - Philippou, A.

PB - Springer

CY - Berlin

Y2 - 22 March 2009 through 29 March 2009

ER -

Nguyen VY, Ruys TC. Memoised Garbage Collection for Software Model Checking. In Kowalewski S, Philippou A, editors, Proceedings of the 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2009). Berlin: Springer. 2009. p. 201-214. 10.1007/978-3-642-00768-2_20. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-642-00768-2_20