Roland Meyer

Date: 16:30, Friday, January 31, 2014
Speaker: Roland Meyer
Venue: IST Austria

Friday 16:30

Sequential Consistency (SC) is the intuitive shared memory model where
operations happen atomically and in the order in which they were issued.
Programmers often assume their code runs on SC hardware, an assumption that is
no longer valid for modern multiprocessors. For performance reasons, recent
hardware only implements relaxed memory models that admit out-of-program-order
and non-store atomic executions. Programs that work correctly under SC may show
undesirable effects when run on relaxed memory models. With the trend towards
multicore machines, bugs due to relaxed memory models become a serious problem
in mainstream programming.

In this talk, we provide an overview of recent results on the verification of
concurrent programs that run on relaxed memory models. We concentrate on the
Total Store Ordering model that is implemented in x86 processors, and discuss
the problems of reachability and robustness. Given a concurrent program and a
configuration, reachability checks whether the program admits an execution
leading to this configuration. Robustness is to decide whether the behaviour of
a given program on a relaxed memory model coincides with the expected SC
semantics. Both problems have been shown to be decidable, but with very
different complexity.

Posted in RiSE Seminar