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

So-called “out-of-thin-air” (OOTA) results are an open problem with many existing programming language memory models including Java, C, and C++. OOTA behaviors are problematic in that they break both formal and informal modular reasoning about program behavior. Defining memory model semantics that are easily understood, allow existing optimizations, and that forbid OOTA results remains an open problem. This paper explores two simple solutions to this problem that forbid OOTA results by restricting compiler optimizations. One solution is targeted towards C/C++-like memory models in which racing operations are explicitly labeled as atomic operations and a second solution is targeted towards Java-like languages in which all memory operations may create OOTA executions. Our solutions provide a per-candidate execution criteria that makes it possible to examine a single execution and determine whether the memory model permits the execution. We implement and evaluated both solutions in the LLVM compiler framework. Our results suggest that OOTA behaviors can be eliminated from language memory models with minimal runtime overhead.

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