Separating Functional and Parallel Correctness using Nondeterministic Sequential Specifications

TitleSeparating Functional and Parallel Correctness using Nondeterministic Sequential Specifications
Publication TypeConference Paper
Year of Publication2010
AuthorsBurnim, J., Necula G., & Sen K.
Conference Name2nd USENIX Workshop on Hot Topics in Parallelism (HotPar '10)
Date Published06/2010
Conference LocationBerkeley, CA

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 verification 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 specification 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.

Paper.pdf223.8 KB