DETERMIN: Inferring Likely Deterministic Specifications of Multithreaded Programs

TitleDETERMIN: Inferring Likely Deterministic Specifications of Multithreaded Programs
Publication TypeConference Paper
Year of Publication2010
AuthorsBurnim, J., & Sen K.
Conference Name32nd International Conference on Software Engineering (ICSE'10)
Date Published05/2010
Conference LocationCape Town, South Africa

The trend towards multicore processors and graphic processing
units is increasing the need for software that can take advantage of parallelism. Writing correct parallel programs using threads, however, has proven to be quite challenging due to nondeterminism.
The threads of a parallel application may be interleaved nondeter-
ministically during execution, which can lead to nondeterministic
results—some interleavings may produce the correct result while
others may not. We have previously proposed an assertion frame-
work for specifying that regions of a parallel program behave de-
terministically despite nondeterministic thread interleaving. The
framework allows programmers to write assertions involving pairs
of program states arising from different parallel schedules.
We propose an algorithm to dynamically infer likely deterministic specifications for parallel programs given a set of inputs and schedules. We have implemented our specification inference algorithm for Java and have applied it to a number of previously examined Java benchmarks. We were able to automatically infer specifications largely equivalent to or stronger than our manual assertions from our previous work.
We believe that the inference of deterministic specifications can
aid in understanding and documenting the deterministic behavior
of parallel programs. Moreover, an unexpected deterministic spec-
ification can indicate to a programmer the presence of erroneous or
unintended behavior.

detinfer-1.pdf217.43 KB