Modern multiprocessor platforms typically employ a memory model which
is weaker than sequential consistency. This means that we cannot use
the naive interleaving semantics when reasoning about the behavior of
concurrent programs running on multiprocessors with shared memory,
at least not in the most general case. In this presentation, I will illustrate
problems that arise for concurrent programs on shared memory models, and
in addition overview a couple of approaches to model checking them.
A large part of the presentation will present CheckFence, a tool by
Burckhardt and Alur that employs bounded model checking, but I will also
indicate other possible strategies. The paper by BurckHardt and Alur is
available at http://research.microsoft.com/~sburckha/