Memoised Garbage Collection for Software Model Checking

Viet Yen Nguyen; Theo C. Ruys

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

Memoised Garbage Collection for Software Model Checking

Viet Yen Nguyen, Theo C. Ruys

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

4 Citations (Scopus)

18 Downloads (Pure)

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.

Original language	English
Title of host publication	Tools and Algorithms for the Construction and Analysis of Systems
Subtitle of host publication	15th International Conference, TACAS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009, Proceedings
Editors	Stefan Kowalewski, Anna Philippou
Place of Publication	Berlin, Heidelberg
Publisher	Springer
Pages	201-214
Number of pages	14
ISBN (Electronic)	978-3-642-00768-2
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, United Kingdom Duration: 22 Mar 2009 → 29 Mar 2009 Conference number: 15

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	5505
ISSN (Print)	0302-9743

Name	Theoretical Computer Science and General Issues
Publisher	Springer
ISSN (Print)	2512-2010
ISSN (Electronic)	2512-2029

Conference

Conference	15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2009
Abbreviated title	TACAS
Country/Territory	United Kingdom
City	York
Period	22/03/09 → 29/03/09

Keywords

FMT-MC: MODEL CHECKING
n/a OA procedure

Access to Document

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

ArticleAccepted author version, 202 KB

Cite this

Nguyen, V. Y., & Ruys, T. C. (2009). Memoised Garbage Collection for Software Model Checking. In S. Kowalewski, & A. Philippou (Eds.), Tools and Algorithms for the Construction and Analysis of Systems: 15th International Conference, TACAS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009, Proceedings (pp. 201-214). (Lecture Notes in Computer Science; Vol. 5505), (Theoretical Computer Science and General Issues). Springer. https://doi.org/10.1007/978-3-642-00768-2_20

Nguyen, Viet Yen ; Ruys, Theo C. / Memoised Garbage Collection for Software Model Checking. Tools and Algorithms for the Construction and Analysis of Systems: 15th International Conference, TACAS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009, Proceedings. editor / Stefan Kowalewski ; Anna Philippou. Berlin, Heidelberg : Springer, 2009. pp. 201-214 (Lecture Notes in Computer Science). (Theoretical Computer Science and General Issues).

@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 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.",

keywords = "FMT-MC: MODEL CHECKING, n/a OA procedure",

author = "Nguyen, \{Viet Yen\} and Ruys, \{Theo C.\}",

year = "2009",

month = mar,

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

language = "English",

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

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "201--214",

editor = "Stefan Kowalewski and Anna Philippou",

booktitle = "Tools and Algorithms for the Construction and Analysis of Systems",

address = "Germany",

note = "15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2009, TACAS ; Conference date: 22-03-2009 Through 29-03-2009",

}

Nguyen, VY & Ruys, TC 2009, Memoised Garbage Collection for Software Model Checking. in S Kowalewski & A Philippou (eds), Tools and Algorithms for the Construction and Analysis of Systems: 15th International Conference, TACAS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009, Proceedings. Lecture Notes in Computer Science, vol. 5505, Theoretical Computer Science and General Issues, Springer, Berlin, Heidelberg, pp. 201-214, 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2009, York, United Kingdom, 22/03/09. https://doi.org/10.1007/978-3-642-00768-2_20

Memoised Garbage Collection for Software Model Checking. / Nguyen, Viet Yen; Ruys, Theo C.
Tools and Algorithms for the Construction and Analysis of Systems: 15th International Conference, TACAS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009, Proceedings. ed. / Stefan Kowalewski; Anna Philippou. Berlin, Heidelberg: Springer, 2009. p. 201-214 (Lecture Notes in Computer Science; Vol. 5505), (Theoretical Computer Science and General Issues).

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, Viet Yen

AU - Ruys, Theo C.

N1 - Conference code: 15

PY - 2009/3

Y1 - 2009/3

N2 - 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.

AB - 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.

KW - FMT-MC: MODEL CHECKING

KW - n/a OA procedure

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 - Tools and Algorithms for the Construction and Analysis of Systems

A2 - Kowalewski, Stefan

A2 - Philippou, Anna

PB - Springer

CY - Berlin, Heidelberg

T2 - 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2009

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, Tools and Algorithms for the Construction and Analysis of Systems: 15th International Conference, TACAS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009, Proceedings. Berlin, Heidelberg: Springer. 2009. p. 201-214. (Lecture Notes in Computer Science). (Theoretical Computer Science and General Issues). doi: 10.1007/978-3-642-00768-2_20

Memoised Garbage Collection for Software Model Checking

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this