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.
NDetermin: Inferring Nondeterministic Sequential Specifications for Parallelism Correctness
Researchers may make free and open use of the UC Berkeley Library’s digitized public domain materials. However, some materials in our online collections may be protected by U.S. copyright law (Title 17, U.S.C.). Use or reproduction of materials protected by copyright beyond that allowed by fair use (Title 17, U.S.C. § 107) requires permission from the copyright owners. The use or reproduction of some materials may also be restricted by terms of University of California gift or purchase agreements, privacy and publicity rights, or trademark law. Responsibility for determining rights status and permissibility of any use or reproduction rests exclusively with the researcher. To learn more or make inquiries, please see our permissions policies (https://www.lib.berkeley.edu/about/permissions-policies).