Am 4. Dezember 2012 hält Jun.-Prof. Dr. Roland Meyer von der Universität Kaiserslautern einen Vortrag mit dem Titel „Robustness Checking against TSO: Attacks and Defence". Der Vortrag gehört zum aktuell laufenden Informatikkolloquium in diesem Semester.
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.
Das Kolloquium findet um 18.00 Uhr im Hörsaal O2 statt. Bei Rückfragen wenden Sie sich bitte an Frau Bewermeyer, Institut für Informatik, Telefon: 05251/60-6695, E-Mail: m.bewermeyer@upb.de
Alle Interessierten sind herzlich willkommen!
