
Evènement pour le groupe Modélisation et Verification
Date  20091105 11:0012:15 
Titre  On the Verification Problem for Weak Memory Models 
Résumé  We address the verification problem of finitestate concurrent programs running under weak memory models. These models capture the reordering of program (read and write) operations done by modern multiprocessor architectures for performance. The verification problem we study is crucial for the correctness of concurrency libraries and other performancecritical system services employing lockfree synchronization, as well as for the correctness of compiler backends that generate code targeted to run on such architectures.
We consider in this work combinations of three wellknown program order relaxations. We consider first the "write to read" relaxation, which corresponds to the TSO (Total Store Ordering) model. This relaxation is used in most hardware architectures available today. Then, we consider models obtained by adding either (1) the "write to write" relaxation (leading to a model which is essentially PSO), or (2) the "read to read/write" relaxation, or (3) both of them (as it is done in the RMO model for instance).
We define abstract operational models for these weak memory models based
on state machines with (potentially unbounded) FIFO buffers, and we
investigate the decidability of their reachability and their repeated
reachability problems.
We prove that the reachability problem is decidable for the TSO model, as well as for its extension with "write to write" relaxation (PSO). Furthermore, we prove that the reachability problem becomes undecidable when the "read to read/write" relaxation is added to either of these two memory models, and we give a condition under which this addition preserves the decidability of the reachability problem. As for the repeated reachability problem, we prove that it is undecidable already for the TSO model.
(Joint work with Ahmed Bouajjani, Sebastian Burckhardt, and Madanlal Musuvathi) 
Lieu  Salle 076, LaBRI, Rezdechaussée 
Orateur  MohamedFaouzi Atig 
Email  atig@liafa.jussieu.fr 
Url  LIAFA 
Aucun document lié à cet événement. RetourRetour à l'index
 