Thu 8 Nov 2018 10:30 - 10:52 at Studio 1 - Weak Memory and Refactoring Chair(s): Richard Jones

We present a framework for efficient application of stateless model checking (SMC) to concurrent programs running under the release-acquire (RA) fragment of the C11 memory model. Our approach is based on exploring the possible program orders, which define the order in which instructions of a thread are executed, and read-from relations, which define how reads obtain their values from writes. This is in contrast to previous approaches, which in addition explore the possible coherence orders, i.e., orderings between conflicting writes. Since unexpected test results such as program crashes or assertion violations depend only on the read-from relation, we avoid a potentially large source of redundancy. Our framework is based on a novel technique for determining whether a particular read-from relation is feasible under the RA semantics. We define an SMC algorithm which is provably optimal in the sense that it explores each program order and read-from relation exactly once. This optimality result is strictly stronger than previous analogous optimality results, which also take coherence order into account. We have implemented our framework in the tool TRACER . Experiments show that TRACER can be significantly faster than state-of-the-art tools that can handle the RA semantics.

Thu 8 Nov

Displayed time zone: Guadalajara, Mexico City, Monterrey change

10:30 - 12:00
Weak Memory and RefactoringOOPSLA at Studio 1
Chair(s): Richard Jones University of Kent
10:30
22m
Talk
Optimal Stateless Model Checking under the Release-Acquire Semantics
OOPSLA
Parosh Aziz Abdulla Uppsala University, Sweden, Mohamed Faouzi Atig Uppsala University, Bengt Jonsson Uppsala University, Tuan Phong Ngo Uppsala University
10:52
22m
Talk
Towards Understanding the Costs of Avoiding Out-of-Thin-Air Results
OOPSLA
Peizhao Ou University of California, Irvine, Brian Demsky University of California, Irvine
11:15
22m
Talk
Persistence Semantics for Weak Memory
OOPSLA
Azalea Raad MPI-SWS, Germany, Viktor Vafeiadis MPI-SWS, Germany
11:37
22m
Talk
Identifying Refactoring Opportunities for Replacing Type Code with Subclass and State
OOPSLA
Jyothi Vedurada IIT Madras, V Krishna Nandivada IIT Madras