Separating Functional and Parallel Correctness Using Nondeterministic Sequential Specifications

Writing correct explicitly-parallel programs can be very challenging. While the functional correctness of a program can often be understood largely sequentially, a software engineer must simultaneously reason about the non-deterministic parallel interleavings of the program's threads of execution. This complication is similarly a challenge to automated verification efforts. Thus, the authors argue that it is desirable to decompose a program's correctness into its sequential functional correctness and the correctness of its parallelization. They propose achieving this decomposition by specifying the parallel correctness of a program with a non-deterministic but sequential version of the program.