December, 19th: Verification of Concurrent Programs under Relaxed Memory Models (in English)

Roland Meyer - Juniorprofessor of Theoretical Computer Science, Head of the Concurrency Theory Group (University of Kaiserslautern). Previously, he was a CNRS postdoc in LIAFA, University Paris 7, from March 2009 to June 2010. He worked in the Transregional Research Center AVACS at the University of Oldenburg. In February 2009, he obtained his PhD from the University of Oldenburg, where he was a PhD student in the graduate school TrustSoft. From October 2001 to September 2005, I studied Computer Science and Mathematics in Oldenburg. His research interests are expressiveness, computer-aided verification, and formal languages of concurrent systems. Focus on infinite-state models, in particular reconfigurable networks and relaxed memory models.

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.

Please feel free to email your questions to sdat@ispras.ru or by twitter @sdat_seminar.