search
Table of Contents
Achieving higher performance and lower energy consumption in computing systems requires the judi- cious use of parallel programming methods. Unfortunately, the inevitable use of heterogeneous hardware CPU/GPU platforms and multiple parallel programming models brings fundamental challenges to the ability to design reliable software/hardware systems. Recent advances in languages for parallel program- ming help simplify the programmer model but do not solve how the programmer is to show these programs correct.
Both static and dynamic analysis methods are needed to adequately address the correctness challenges of parallel programming. These analysis approaches are inherently different in terms of the problem sizes they can handle, the level of precision they provide, and the level of program representations (e.g., higher level primitives versus transition systems) they deal with. Yet, keeping the tools for static and dynamic analysis separate is highly wasteful in many ways. For example, dynamic analysis ignores static infor- mation which can inform where verification can be dispensed with and where additional verification is needed. Similarly, dynamic analysis is forced to present results in low-level semantically unintelligible ways by ignoring static information rather than in terms of the programmers conceptual high-level model.
The PIs will study ways to further static analysis in response to new concurrency primitives that are needed to adequately address the challenges of parallel programming. They will develop a formal state- transition (operational) semantic description of subsets of modern parallel programming languages, taking Rice’s Habenaro Java (HJ) as the main case study. They will validate subsets of these semantics by creating executable semantics in frameworks such as PLT Redex, the Coq proof assistant, and the Java Pathfinder software model checker (JPF). Based on the rigorous semantics, they will formally verify guarantees using the Coq proof assistant that can be achieved through static analysis by the HJ compiler. They will also em- ploy the JPF framework to conduct unit-level formal verification of critical concurrent datatypes and APIs using software model-checking. They will create a verification-assisting version of the HJ compiler, and devise ways to efficiently convey the guarantees achieved and those that are unmet by this compiler for consumption by dynamic tools based on active testing approaches that employ formal schedule-bounding methods. They will modify existing parallel language runtimes to enable them to be controlled in accor- dance with the intended active formal testing strategies, and to effect schedule-bounding. These active testing methods will be deployed on larger-scale HJ programs with multiple concurrent datatypes and complex task-creation loops on real multicore platforms, thus helping with efficient bug-hunting in the final deployment runtime. The PIs’ extensive past collaborations will help achieve these results, impact science, practice, and pedagogy.
Intellectual Merit: (1) Scientific aspects of static analysis for hybrid concurrency, including formal se- mantic description of higher level languages that can express parallelism, verification of static correctness guarantees specific against the semantics of each language construct; (2) Understanding of how modern parallel language runtimes can be controlled to implement active formal testing based on schedule bound- ing; (3) Improvements to the overall ability to close the loop between programming intentions and program execution effects. Scientific solutions that positively impact large-scale parallel programming productivity.
Broader Impact: (1) General know-how to benefit future static and dynamic analysis tool developers and parallel language compiler developers in terms of simple but powerful features that they can incorporate into their tool to benefit an associated tool; (2) Concrete case studies that serve as a valuable community resource for comparative study and experiments; (3) Direct tie into pedagogy, and the generation of cur- ricular material (validated examples, courseware) validated in three universities, addressing several open challenges in teaching parallel programming at the undergraduate and graduate levels.
Keywords: Formal methods; parallelism and concurrency; multicore computing; static and dynamic anal- ysis; partial order reduction; schedule-bounding methods; symbolic execution; programming languages.
NSF award number CCF-1302524 with PI Ganesh Gopalakrishnan and PI Vivek Sarkar.
Collaborator Webpages
Research Projects
Here is an ongoing annotated bibliography discussing related work to the various research projects in the lab.
Selected Publications
- Eric Noonan. Slice-N-Dice Algorithm Implementation in JPF, Brigham Young University, 2014.
- P. Anderson, N. Vrvilo, E. Mercer, and V. Sarkar. “JPF Verification of Habanero Java Programs using Gradual Permission Regions”, in Proceedings of JPF Workshop, UT, November 2014.
- B. Hillery, E. Mercer, N. Rungta and S. Person. Towards a Lazier Symbolic PathFinder, in Proceedings of JPF Workshop, CA, November 2013.
- E. Noonan, E. Mercer and N. Rungta. Vector-Clock Based Partial Order Reduction for JPF, in Proceedings of JPF Workshop, CA, November 2013.
- P. Anderson, B. Chase and E. Mercer. JPF Verification of Habanero Java Programs, in Proceedings of JPF Workshop, CA, November 2013.
- J. Shirako, N. Vrvilo, E. Mercer, and V. Sarkar, Design, Verification, and Applications of a New Read- Write Lock Algorithm, in 24th ACM Symposium on Parallelism in Algorithms and Architectures, Pittsburgh, USA 2012, pages 48-57.
