Thread Modularity on the Next Level

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.