The project is part of http://javapathfineder.org, and it is the JPF HJ project.

The goal of this aspect of the research is to modify the Java Pathfinder tool (JPF) to efficiently model check Habanero Java programs (HJ). It is hoped to learn from studying ways to efficiently model check HJ programs that the results are able to generalize to other mid-level parallel languages.

Relevant work in model checking mid-level concurrency languages such as HJ:

• X10X Model Checking a New Programming Language with an Old Model Checker
• Delay Bounded Scheduling

Other resources relevant to this aspect of the research:

• The Java Pathfinder model checker
• Habanero Java download and install instructions.
• Other details on Habanero Java

Habanero Java (HJ) is a mid-level concurrency language developed at RICE University that is similar in spirit to the X10 language from IBM. HJ hopes to produce portable parallel programming abstractions for future multi-core technologies. Currently, HJ adds new keywords to the Java language for asynchronous task creation, mutual exclusion in asynchronous tasks, barriers, and phasers. A simple HJ example that creates asynchronous tasks is shown below:

// Start of Task T1 (main program)
sum1 = 0; sum2 = 0; // Assume that sum1 & sum2 are fields (not local vars) 
finish {
   // Compute sum1 (lower half) and sum2 (upper half) in parallel 
   async for(int i=0; i<X.length/2 ; i++)sum1+=X[i]; //TaskT2 
   async for(int i=X.length/2 ; i<X.length ; i++)sum2+=X[i]; //TaskT
}
 
//Task T1 waits for Tasks T2 and T3 to complete 
int sum = sum1 + sum2; // Continuation of Task T1

The goal of this project is to modify and extend JPF to be able to verify HJ programs for deadlock and user provided assertion violations. ://ieeexplore.ieee.org/xpl/articleDetails.jsp?reload=true&arnumber=6200092&contentType=Conference+Publications Prior work] that extends JPF for the X10 language uses the X10 runtime libraries directly in JPF but requires modifications to JPF, the X10 runtime libraries, X10 language compiler, and other static analysis methods. This approach, rather than use the HJ runtime libraries, is to simulate the HJ runtime directly in JPF either through a specialized verification version of the runtime or arbitrary state transformations on the JPF state. A successful project would be able to take simple compiled HJ programs that only use async, finish, isolated, and next keywords as input to JPF and successfully show correctness or provide a counterexample that either deadlocks or violates a user provided assertion.

Back to top