Description


parachute logo In the Parachute project (“Safely Descend from Static to Dynamic Analysis” — collaboration between Rice University, Brigham Young University and the University of Utah), the focus is to design dynamic analysis methods that work congruous to the needs of modern high productivity parallel programming languages. We will develop our work around the Rice Habanero Java (HJ) language as a target for our active tester (HAT). The HJ compiler will be modified to generate information for downstream dynamic analysis tools. HJ also has known safe subsets which guarantee various properties. As elaborated in the HJ paper, programming in async language construct for example guarantees deadlock freedom by avoiding waiting/synchronization, while programming in isolated construct guarantees race freedom by enforcing mutual exclusion, and so on. We will modify the HJ compiler to inform the Habanero Active Tester to capitalize on these known subsets and avoid or minimize dynamic checks.

The other aspect of HAT is to adjust its operations to match proposed HJ runtimes. HJ runtime has a diverse set of scheduling mechanisms. Some of which are preemptive and some of which are cooperating. Those that are cooperative lead to difficulties in enforcing some behaviors and those that are preemptive may lead to deadlocks and liveness issues. Our tool should be able to explore all of these scenarios and be able to reason about them.

The challenges faced for hybrid runtimes verification is that they require both SA and DA but there is still a lot of scope for improving their cooperation. They require rigorous operational semantics specifications. They require simulation of the packaged SA, DA and OpSem (Operational Semantics) to draw conclusions about methodologies effectiveness. More over, HJ has inadequate dynamic verification tools support to aid reason about its programs. HJ has no OpSem specifications, regardless of how heavily they are discussed in published work. This introduces confusions for both tools developers and users of HJ alike. As a result, a concise OpSem is crucially needed to address ambiguity(ies).

Downloads

Publications

Projects and Reports

Habanero-Java Verification Runtime (HJ-VRT)

  • Understanding HJ and Srcs of the Cooperative runtime - Mar 2014: This report explains our experience learning Habanero Java, teaching two interns how to use it in developing a GUI app that does its computation using HJ different concurrency constructs, our experience running HJ applications on Raspberry Pi in preparation for Parallelism class, our understanding of HJ Cooperative runtime based on its source code provided by Rice University, and initial plans about how we are working towards a verification cooperative runtime based on HJ Coop Runtime.

Habanero Java Applciations

Related Work

Members