NDSeq: Runtime Checking for Nondeterministic Sequential Specifications of Parallel Correctness
The authors propose to specify the correctness of a program's parallelism using a sequential version of the program with controlled non-determinism. Such a non-deterministic sequential specification allows the correctness of parallel interference to be verified independently of the program's functional correctness, and the functional correctness of a program to be understood and verified on a sequential version of the program, one with controlled non-determinism but no interleaving of parallel threads. They identify a number of common patterns for writing non-deterministic sequential specifications. They apply these patterns to specify the parallelism correctness for a variety of parallel Java benchmarks, even in cases when the functional correctness is far too complex to feasibly specify.