Phalanx: Parallel Checking of Expressive Heap Assertions
Martin Vechev, Eran Yahav, Greta Yorsh, Bard Bloom
In Proc. International Symposium on Memory Management, 2010
Unrestricted use of heap pointers makes software systems
particularly difficult to understand. Incidental and accidental
pointer aliasing result in unexpected side effects of seemingly
unrelated operations, and are a major source of system
failures. Such failures are hard to test or debug with existing
tools, especially for concurrent programs.
Full version published as IBM Technical Report, May 2009
We present PHALANX — a practical framework for dynamically
checking expressive heap properties such as ownership,
sharing and reachability. PHALANX uses novel parallel
algorithms to efficiently check heap properties utilizing
the available cores in the system.
To debug her program, a programmer can annotate it
with expressive heap assertions in JML, which use heap
primitives provided by PHALANX. The framework combines
a modified version of the JML compiler with a specialized
runtime to efficiently evaluate these assertions using parallel
algorithms. The PHALANX runtime has been implemented
on top of a production virtual machine.
We applied PHALANX to real world applications in various
scenarios, and found expressive heap assertions to be
extremely valuable in debugging and program understanding.
Further, our experimental results indicate that evaluating
heap queries using parallel algorithms can lead to significant
performance improvements, often resulting in linear
speedups as the number of cores increases.
Click here to access the paper:
Click here to access the technical report: