kirancodes.me
To Proof Maintenance & Beyond!

What can the GC compute efficiently?: a language for heap assertions at GC time

Christoph Reichenbach, Neil Immerman, Yannis Smaragdakis, Edward Aftandilian, Samuel Z. Guyer

Abstract

We present the DeAL language for heap assertions that are efficiently evaluated during garbage collection time. DeAL is a rich, declarative, logic-based language whose programs are guaranteed to be executable with good whole-heap locality, i.e., within a single traversal over every live object on the heap and a finite neighborhood around each object. As a result, evaluating DeAL programs incurs negligible cost: for simple assertion checking at each garbage collection, the end-to-end execution slowdown is below 2%. DeAL is integrated into Java as a VM extension and we demonstrate its efficiency and expressiveness with several applications and properties from the past literature.

Related papers