Wed 10 Jan 2018 15:50 - 16:15 at Bunker Hill - Memory and Concurrency Chair(s): Azadeh Farzan

We present a stateless model checking algorithm for verifying concurrent programs running under RC11, a repaired version of the C/C++11 weak memory model without dependency cycles. Unlike previous approaches, which enumerate thread interleavings up to some partial order reduction improvements, our approach works directly on execution graphs and (in the absence of RMW instructions) avoids redundant exploration by construction. We have implemented a model checker, called RCMC, based on this approach and apply it to a number of challenging concurrent programs. Our experiments confirm that our tool leads to much faster verification times than other model checking tools.

Wed 10 Jan
Times are displayed in time zone: (GMT-07:00) Tijuana, Baja California change

15:50 - 17:30: Research Papers - Memory and Concurrency at Bunker Hill
Chair(s): Azadeh FarzanUniversity of Toronto
POPL-2018-papers15:50 - 16:15
Michalis KokologiannakisNational Technical University of Athens, Greece, Ori LahavTel Aviv University, Israel, Konstantinos (Kostis) Sagonas, Viktor VafeiadisMPI-SWS, Germany
POPL-2018-papers16:15 - 16:40
Brijesh DongolBrunel University London, Radha JagadeesanDePaul University, James RielyDePaul University
Link to publication DOI Pre-print Media Attached
POPL-2018-papers16:40 - 17:05
Christopher PulteUniversity of Cambridge, Shaked FlurUniversity of Cambridge, Will DeaconARM Ltd., Jon FrenchUniversity of Cambridge, Susmit SarkarUniversity of St. Andrews, Peter SewellUniversity of Cambridge
POPL-2018-papers17:05 - 17:30
Hongjin LiangUniversity of Science and Technology of China, Xinyu FengUniversity of Science and Technology of China