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 nondeterministic parallel interleavings of the program’s threads of execution. This complication is similarly a challenge to automated veriﬁcation efforts.
Thus, we argue that it is desirable to decompose a program’s correctness into its sequential functional correctness and the correctness of its parallelization. We propose achieving this decomposition by specifying the parallel correctness of a program with a nondeterministic but sequential version of the program. In particular, if a software engineer annotates the intended algorithmic nondeterminism in a program, then the program can act
as its own speciﬁcation in verifying the correctness of its
parallelism. We can interpret the annotated program as
sequential but nondeterministic, and then verify the correctness of the parallelism by showing that it introduces no additional nondeterminism.