LSV Seminar
The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.
The seminar is open to public and does not require any form of registration.
Past Seminars
Counter-Example Guided Fence Insertion under TSO
- Date
- Tuesday, January 31 2012 at 11:00AM
- Place
- Salle de Conférence (Pavillon des Jardins)
- Speaker
- Mohamed Faouzi Atig (Uppsala University, Sweden)
We consider the reachability problem for concurrent finite-state programs running under the classical TSO memory model. This model allows "write to read" relaxation corresponding to the addition of an unbounded store buffer between each processor and the main memory. We show that the reachability problem for a program under TSO is decidable. Then, we propose a counter-example guided fence insertion procedure. The procedure is augmented by a placement constraint that allows the user to choose places inside the program where fences may be inserted. For a given placement constraint, we automatically infer all minimal sets of fences that ensure correctness. We have implemented a prototype and run it successfully on all standard benchmarks together with several challenging examples that are beyond the applicability of existing methods.
[This talk will be based on: (1) POPL'10 paper with Ahmed Bouajjani, Burckhardt and Madanlal Musuvathi, and (2) TACAS'12 paper with Parosh Abdulla, Yu-Fang Chen, Carl Leonardsson and Ahmed Rezine]