On December 4, 2012, Jun.-Prof. Dr. Roland Meyer will give a talk about "Robustness Checking Against TSO: Attacks and Defence" in the context of the SFB 901 colloquium.
Abstract:
Programmers often assume concurrent programs run on sequentially consistent (SC) processors that execute the actions of each thread in program order. This assumption, however, does not hold for modern processors. For performance reasons, recent hardware only implements relaxed memory models where actions may be executed out-of-program-order. Programs that run on relaxed memories may show undesirable behavior that is impossible under SC. With the trend towards multicore machines, bugs due to relaxed memory models become a serious problem in mainstream programming that calls for a solution.
This talk provides 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 reachability and the robustness problems. Given a concurrent program and a configuration, reachability checks whether the program admits a run that leads to this configuration. Robustness checks whether the behavior 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.