Phalanx: Parallel Checking of Expressive Heap Assertions

Martin Vechev, Eran Yahav, Greta Yorsh, Bard Bloom

In Proc. International Symposium on Memory Management, 2010 (ISMM'10)
Full version published as IBM Technical Report, May 2009

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.
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: PDF; PS; Slides

Click here to access the technical report: TR-PDF; TR-PS