Another notable work is the CHESS project [1]}
of Microsoft. This includes a DPOR-based model
checker [2]} to reproduce “Heisenbugs”
(rare race conditions).
They also directly
modeling multi-threaded programs, rather than explicitly supporting
the common POSIX synchronization operations for mutex, semaphore
and condition variable.
They also limit the number of thread context
switches in a trace, but they do so using a best-first search heuristic
to emphasize regions of code with likely race conditions. That work
is extended in GAMBIT [3]}, which
employs different priority functions for preemption-bounded search.
