NDetermin: Inferring Nondeterministic Sequential Specifications for Parallelism Correctness

Jacob Burnim, Tayfun Elmas, George Necula and Koushik Sen

EECS Department
University of California, Berkeley
Technical Report No. UCB/EECS-2011-143
December 16, 2011

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2011/EECS-2011-143.pdf

A key reason for the great difficulty of writing, testing, and verifying parallel programs is the need to reason simultaneously about not only the sequential correctness of each part of a program in isolation, but also about all possible nondeterministic interleavings of the program's parallel threads. Thus, there has been much interest in techniques for separately testing or verifying the correctness of a program's use of parallelism, allowing the program's functional correctness to be tested or verified in a sequential way.

Nondeterministic Sequential (NDSeq) specifications have been proposed as a means for achieving this decomposition in testing, debugging, and verifying a program's parallelism correctness and its sequential functional correctness. An NDSeq specification for a parallel program is a sequential version of the program, with no parallel threads but with some limited, controlled nondeterminism. A program's use of parallelism is correct if, for every execution of the parallel program, there exists an execution of the NDSeq specification producing the same result. Functional correctness can then be checked on this NDSeq specification, without any interleaving of parallel threads.

While NDSeq specifications have been used successfully to check parallelism correctness, manually writing NDSeq specifications for programs can be a challenging and time-consuming process. Thus, in this work, we propose a technique for automatically inferring a likely NDSeq specification for a parallel program. Given a few representative executions of a parallel program, our technique combines dynamic data flow analysis and Minimum-Cost Boolean Satisfiability (MinCostSAT) solving to infer a likely NDSeq specification for the program's parallelism. We have implemented our technique for Java in a prototype tool called NDetermin. For a number of benchmarks, our tool infers equivalent or stronger NDSeq specifications than those previously written manually.


BibTeX citation:

@techreport{Burnim:EECS-2011-143,
    Author = {Burnim, Jacob and Elmas, Tayfun and Necula, George and Sen, Koushik},
    Title = {NDetermin: Inferring Nondeterministic Sequential Specifications for Parallelism Correctness},
    Institution = {EECS Department, University of California, Berkeley},
    Year = {2011},
    Month = {Dec},
    URL = {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2011/EECS-2011-143.html},
    Number = {UCB/EECS-2011-143},
    Abstract = {  A key reason for the great difficulty of writing, testing, and
  verifying parallel programs is the need to reason simultaneously
  about not only the sequential correctness of each part of a program
  in isolation, but also about all possible nondeterministic
  interleavings of the program's parallel threads.  Thus, there has
  been much interest in techniques for separately testing or verifying
  the correctness of a program's use of parallelism, allowing the
  program's functional correctness to be tested or verified in a
  sequential way.

  Nondeterministic Sequential (NDSeq) specifications have been
  proposed as a means for achieving this decomposition in testing,
  debugging, and verifying a program's parallelism correctness and its
  sequential functional correctness.  An NDSeq specification for a
  parallel program is a sequential version of the program, with no
  parallel threads but with some limited, controlled nondeterminism.
  A program's use of parallelism is correct if, for every execution of
  the parallel program, there exists an execution of the NDSeq
  specification producing the same result.  Functional correctness can
  then be checked on this NDSeq specification, without any
  interleaving of parallel threads.

  While NDSeq specifications have been used successfully to check
  parallelism correctness, manually writing NDSeq specifications for
  programs can be a challenging and time-consuming process.  Thus, in
  this work, we propose a technique for automatically inferring a
  likely NDSeq specification for a parallel program.  Given a few
  representative executions of a parallel program, our technique
  combines dynamic data flow analysis and Minimum-Cost Boolean
  Satisfiability (MinCostSAT) solving to infer a likely NDSeq
  specification for the program's parallelism.  We have implemented
  our technique for Java in a prototype tool called NDetermin.  For a
  number of benchmarks, our tool infers equivalent or stronger NDSeq
  specifications than those previously written manually.}
}

EndNote citation:

%0 Report
%A Burnim, Jacob
%A Elmas, Tayfun
%A Necula, George
%A Sen, Koushik
%T NDetermin: Inferring Nondeterministic Sequential Specifications for Parallelism Correctness
%I EECS Department, University of California, Berkeley
%D 2011
%8 December 16
%@ UCB/EECS-2011-143
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2011/EECS-2011-143.html
%F Burnim:EECS-2011-143