POPL 2017
Sun 15 - Sat 21 January 2017
Thu 19 Jan 2017 15:35 - 16:00 at Amphitheater 44 - Concurrency 2 Chair(s): Nobuko Yoshida

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 modularity (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.

Thu 19 Jan
Times are displayed in time zone: (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

14:20 - 16:00: POPL - Concurrency 2 at Amphitheater 44
Chair(s): Nobuko YoshidaImperial College London, UK
POPL-2017-papers14:20 - 14:45
Shaked FlurUniversity of Cambridge, Susmit SarkarUniversity of St. Andrews, UK, Christopher PulteUniversity of Cambridge, Kyndylan NienhuisUniversity of Cambridge, Luc MarangetINRIA Rocquencourt, Kathryn E. GrayUniversity of Cambridge, Ali SezginUniversity of Cambridge, Mark BattyUniversity of Kent, Peter SewellUniversity of Cambridge
POPL-2017-papers14:45 - 15:10
Christopher LidburyImperial College London, Alastair DonaldsonImperial College London
POPL-2017-papers15:10 - 15:35
Lucas BrutschyETH Zurich, Dimitar DimitrovETH Zurich, Switzerland, Peter MüllerETH Zurich, Martin VechevETH Zurich
POPL-2017-papers15:35 - 16:00
Jochen HoenickeUniversität Freiburg, Rupak MajumdarMPI-SWS, Andreas PodelskiUniversity of Freiburg, Germany