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:

Other resources relevant to this aspect of the research:

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
}

int sum = sum1 + sum2; // Continuation of Task T1