Model Checking Task Parallel Programs Using Gradual Permissions (N)

Habanero is a task parallel programming model that provides correctness guarantees to the programmer. Even so, programs may contain data races that lead to non-determinism, which complicates debugging and verification. This paper presents a sound algorithm based on permission regions to prove data race and deadlock freedom in Habanero programs. Permission regions are user annotations to indicate the use of shared variables over spans of code. The verification algorithm restricts scheduling to permission region boundaries and isolation to reduce verification cost. The effectiveness of the algorithm is shown in benchmarks with an implementation in the Java Pathfinder (JPF) model checker. The implementation uses a verification specific library for Habanero that is tested using JPF for correctness. The results show significant reductions in cost, where cost is controlled with the size of the permission regions, at the risk of rejecting programs that are actually free of any data race or deadlock.