Séminaire des équipes de recherche
Verification of Concurrent Programs Targeting the x86-TSO Weak Memory Model
- Date : 10/06/2013
- Lieu : rocquencourt, bâtiment 07
- Intervenant(s) : Arthur Charguéraud
- Organisateur(s) : Gallium
Pretty much every computer sold today is multi-core. Taking advantage of more than one core to speed up a program is a nontrivial problem in general. Nevertheless, it has been shown that many algorithms can be relatively easily parallelized on shared memory architecture by using appropriate dynamic load balancing algorithms as well as a small number of classic concurrent data structures. These components involve a fairly small amount of code, however this code is extremely error-prone and very hard to debug. These components are therefore an ideal target for program verification. In this talk, I will recall the simple weak memory model associated with Intel and AMD's x86 hardware, and explain how to build on top of this model a logic for reasoning about concurrent programs. I will present concrete code examples taken from a realistic scheduling library, show how they can be verified by hand, and discuss the possibility of mechanizing and automating the proofs.