NDetermin: Inferring Nondeterministic Sequential Specifications for Parallelism Correctness
Abstract
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 program's parallel threads. Thus, there has been much interest in techniques for separately testing or verifying the correctness of a program's use of parallelism, allowing the program's 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 program's 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 program's 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 program's 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.
Document Details
- Document Type
- Technical Report
- Publication Date
- Dec 16, 2011
- Accession Number
- ADA555872
Entities
People
- George Necula
- Jacob Burnim
- Koushik Sen
- Tayfun Elmas
Organizations
- University of California, Berkeley