Testing is the most widely-used methodology for software
validation. However, due to the nondeterministic
interleavings of threads, traditional testing for concurrent
programs is not as effective as for sequential programs.
To attack the nondeterminism problem, software
model checking techniques have been used to systematically
enumerate all possible thread schedules of a
test program. But such systematic and exhaustive exploration
is typically too time-consuming for many test programs.
We believe that the programmer’s help to guide
the model checker towards interesting executions is critical
to circumvent this problem.
We propose a testing technique and a supporting tool
called CONCURRIT, which provides a model checker
that can be guided programmatically within test code.
While writing a test, the programmer specifies a particular
thread interleaving scenario in mind using an embedded
domain-specific language (DSL), and CONCURRIT
explores all and only the executions realizing the
intended scenario. During the exploration, the programmer
is also able to observe the execution (e.g., assert invariants)
and constrain the future decisions of the model
checker, all within the test code.We believe that providing
the programmer the ability to observe and control
the exploration of executions will lead to more effective
and efficient testing for concurrent programs.