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

Displayed time zone: Tijuana, Baja California change

15:50 - 17:30
Memory and ConcurrencyResearch Papers at Bunker Hill
Chair(s): Azadeh Farzan University of Toronto
15:50
25m
Talk
Effective Stateless Model Checking for C/C++ Concurrency
Research Papers
Michalis Kokologiannakis National Technical University of Athens, Greece, Ori Lahav Tel Aviv University, Israel, Konstantinos (Kostis) Sagonas , Viktor Vafeiadis MPI-SWS, Germany
16:15
25m
Talk
Transactions in Relaxed Memory Architectures
Research Papers
Brijesh Dongol Brunel University London, Radha Jagadeesan DePaul University, James Riely DePaul University
Link to publication DOI Pre-print Media Attached
16:40
25m
Talk
Simplifying ARM Concurrency: Multicopy-Atomic Axiomatic and Operational Models for ARMv8
Research Papers
Christopher Pulte University of Cambridge, Shaked Flur University of Cambridge, Will Deacon ARM Ltd., Jon French University of Cambridge, Susmit Sarkar University of St. Andrews, Peter Sewell University of Cambridge
17:05
25m
Talk
Progress of Concurrent Objects with Partial Methods
Research Papers
Hongjin Liang University of Science and Technology of China, Xinyu Feng University of Science and Technology of China