Détails sur le séminaire

Auditorium (Builbing IMAG)
29 septembre 2016 - 09h30
Thread Modularity on the Next Level
par Andreas Podelski de University of Freiburg

Abstract: A thread-modular proof for the correctness of a concurrent program is based on an inductive and interference-free annotation of each thread. It is well-known that the corresponding proof system is not complete (unless one adds auxiliary variables). We introduce a hierarchy of proof systems where each level k corresponds to a new notion of thread modular- ity (level 1 corresponds to the original notion). Each level is strictly more expressive than the previous. The hierarchy can be used to prove interesting programs. We give the to our knowledge first proof of the MACH shootdown algorithm for TLB consistency. The algorithm is correct for an arbitrary number of CPUs. This is joint work with Jochen Hoenicke and Rupak Majumdar.


Contact | Plan du site | Site réalisé avec SPIP 4.2.8 + AHUNTSIC [CC License]

info visites 3969928