SHF: Small: Specifying and Verifying Essential Deterministic Behavior of Concurrent Programs

University Of California-Berkeley, Berkeley CA

Investigators

Abstract

Parallel multi-threaded programs are more difficult to write than their sequential counterparts because while writing parallel programs programmers must consider all possible behaviors due to thread interleavings, in addition to the algorithmic correctness of the program. A widespread belief is that the only way to make multi-threaded programming accessible to a large number of programmers is to come up with programming paradigms and associated tools that explicitly separate reasoning about functional correctness from reasoning about additional behaviors arising due to parallelism. This project investigates strategies for separating the parallelization correctness aspect of a program from its functional correctness. First, for most parallel programs it is desired that the non-determinism introduced by the thread scheduler in a parallel program does not change the intended output of the program. This project will develop an assertion framework for specifying that regions of a parallel program behave deterministically despite non-deterministic thread interleaving. The second strategy is based on the observation that a natural step in the development of a parallel program is to first extend the sequential algorithm with a controlled amount of non-determinism, followed by the actual parallelization, when additional non-determinism is introduced by thread interleavings. This project will investigate the use of non-deterministic sequential programs as a specification mechanism, such that for each execution of a parallel program there exists an equivalent execution of the corresponding non-deterministic sequential program. Such non-deterministic sequential programs decouple parallelization correctness from functional correctness.