2009 | OriginalPaper | Buchkapitel
Memoised Garbage Collection for Software Model Checking
verfasst von : Viet Yen Nguyen, Theo C. Ruys
Erschienen in: Tools and Algorithms for the Construction and Analysis of Systems
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.