NDetermin: Inferring Nondeterministic Sequential Specifications for Parallelism Correctness
CALIFORNIA UNIV BERKELEY DEPT OF ELECTRICAL ENGINEERING AND COMPUTER SCIENCE
Pagination or Media Count:
A key reason for the great difficulty of writing, testing, and verifying parallel programs is the need to reason simultaneously about not only the sequential correctness of each part of a program in isolation but also about all possible nondeterministic interleavings of the programs parallel threads. Thus, there has been much interest in techniques for separately testing or verifying the correctness of a programs use of parallelism, allowing the programs functional correctness to be tested or verified in a sequential way. Nondeterministic Sequential NDSeq specifications have been proposed as a means for achieving this decomposition in testing debugging, and verifying a programs parallelism correctness and its sequential functional correctness. An NDSeq specification for a parallel program is a sequential version of the program, with no parallel threads but with some limited, controlled nondeterminism. A programs use of parallelism is correct if, for every execution of the parallel program, there exists an execution of the NDSeq specification producing the same result. Functional correctness can then be checked on this NDSeq specification, without any interleaving of parallel threads. While NDSeq specifications have been used successfully to check parallelism correctness, manually writing NDSeq specifications for programs can be a challenging and time-consuming process. Thus, in this work, we propose a technique for automatically inferring a likely NDSeq specification for a parallel program. Given a few representative executions of a parallel program, our technique combines dynamic data flow analysis and Minimum-Cost Boolean Satisfiability MinCostSAT solving to infer a likely NDSeq specification for the programs parallelism. We have implemented our technique for Java in a prototype tool called NDETERMIN. For a number of benchmarks, our tool infers equivalent or stronger NDSeq specifications than those previously written manually.
- Computer Programming and Software