Edward Aftandilian and Samuel Guyer. PLDI 2009.
May 18, 2009
The key idea in this paper is to piggyback on the GC to perform (data structure) invariant checks that would either be impossible or prohibitively expensive to check using standard assertions. For example, assert-dead check allows the developer to check that the object can be reclaimed, which would be essentially impossible without performing a GC. As another example, the assert-unshared check, which verifies that an object has at most one incoming pointer, would be difficult and expensive to perform manually. The assertion checking does not happen immediately but rather at the next GC and, we guess, during all subsequent GCs. This choice allows the checking to essentially be batched up.
The paper presents an interesting idea and allows run-time checking that is difficult to accomplish otherwise. However, the main weakness is that the GC assertions provide fairly weak guarantees: the assertion holds at some indeterminate time in the future, which is a counterintuitive "assert" statement. Moreover, the kinds of GC assertions are a few kinds and do not support general assertions. Additionally, it would have been nice to have a sense of what the overhead would have been like without using the "bit stealing" tricks.
Discussion
We had some debate about whether once an assert is encountered is the assertion checking done only on the next GC or all future GCs. With assert-dead, it's clear that it is only relevant on the next GC, but assert-unshared might make more sense if it was checked on all future GCs.
Devin thought a "dominance" ownership check where all paths to an object x must go through its owner o would be useful. This was intial ownership check presented in the paper but was discarded as being too strict. Instead, they do an existential check where there must exist a path to an object x through its owner o. The cited problem with iterators could potentially be addressed by considering references from stack variables as not contributing to ownership.
We discussed ideas about giving better guarantees. Perhaps it would be possible to use write barriers to log the changes between when the assert was made and the GC time. Then, the algorithm would need to reconstruct the state of memory from the log to perform the invariant check on the memory state at that point in the execution. Devin mentioned a possible paper related to this idea: Bond et al., Tracking Bad Apples: Reporting the Origin of Null and Undefined Value Errors, OOPSLA 2007. Jeremy wondered whether some his blame tracking work might be applicable, though state changes would be a challenge.
Devin brought up an alternative semantics for assertions: does the assertion hold "most of the time"? An example is that the steady-state of data structure has no sharing (which you want to check with assert-unshared), but there are intermediate states that violate this invariant. The hypothesis is that most GCs will happen during the steady state.
We also had a digression into a short discussion about separation logic and shape analysis.