PHALANX: Parallel Checking of Expressive Heap Assertions

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.

By: Greta Yorsh; Eran Yahav; Martin Vechev; Bard Bloom

Published in: RC24822 in 2009


This Research Report is available. This report has been submitted for publication outside of IBM and will probably be copyrighted if accepted for publication. It has been issued as a Research Report for early dissemination of its contents. In view of the transfer of copyright to the outside publisher, its distribution outside of IBM prior to publication should be limited to peer communications and specific requests. After outside publication, requests should be filled only by reprints or legally obtained copies of the article (e.g., payment of royalties). I have read and understand this notice and am a member of the scientific community outside or inside of IBM seeking a single copy only.


Questions about this service can be mailed to .