SPLASH 2020
Sun 15 - Sat 21 November 2020 Online Conference
Fri 20 Nov 2020 08:00 - 08:20 at SPLASH-I - F-1A Chair(s): Diomidis Spinellis, John Wickerson
Fri 20 Nov 2020 20:00 - 20:20 at SPLASH-I - F-1A Chair(s): Tongping Liu, Azalea Raad

Modern memory consistency models are complex, and it is difficult to reason about the relaxed behaviors that current systems allow. Programming languages, such as C and OpenCL, offer a memory model interface that developers can use to safely write concurrent applications. This abstraction provides functional portability across any platform that implements the interface, regardless of differences in the underlying systems. This powerful abstraction hinges on the ability of the system to correctly implement the interface. Many techniques for memory consistency model validation use empirical testing, which has been effective at uncovering undocumented behaviors and even finding bugs in trusted compilation schemes. Memory model testing consists of small concurrent unit tests called ``litmus tests''. In these tests, certain observations, \emph{including potential bugs}, are exceedingly rare, as they may only be triggered by precise interleaving of system steps in a complex processor, which is probabilistic in nature. Thus, each test must be run many times in order to provide a high level of confidence in its coverage.

In this work, we rigorously investigate empirical memory model testing. In particular, we propose methodologies for navigating complex stressing routines and analyzing large numbers of testing observations. Using these insights, we can more efficiently tune stressing parameters, which can lead to higher confidence results at a faster rate. We emphasize the need for such approaches by performing a meta-study of prior work, which reveals results with low reproducibility and inefficient use of testing time.

Our investigation is presented alongside empirical data. We believe that OpenCL targeting GPUs is a pragmatic choice in this domain as there exists a variety of different platforms to test, from large HPC servers to power-efficient edge devices. The tests presented in the work span 3 GPUs from 3 different vendors. We show that our methodologies are applicable across the GPUs, despite significant variances in the results. Concretely, our results show: lossless speedups of more than $5\times$ in tuning using data peeking; a definition of portable stressing parameters which loses only 12% efficiency when generalized across our domain; a priority order of litmus tests for tuning. We stress test a conformance test suite for the OpenCL 2.0 memory model and discover a bug in Intel's compiler. Our methods are evaluated on the other two GPUs using mutation testing. We end with recommendations for official memory model conformance tests.

Fri 20 Nov

Displayed time zone: Central Time (US & Canada) change

07:00 - 08:20
F-1AOOPSLA at SPLASH-I +12h
Chair(s): Diomidis Spinellis Athens University of Economics and Business, John Wickerson Imperial College London
07:00
20m
Talk
DiffStream: Differential Output Testing for Stream Processing Programs
OOPSLA
Konstantinos Kallas University of Pennsylvania, Filip Niksic Google, Caleb Stanford University of Pennsylvania, Rajeev Alur University of Pennsylvania
Link to publication DOI Media Attached
07:20
20m
Talk
Pomsets with Preconditions: A Simple Model of Relaxed Memory
OOPSLA
Radha Jagadeesan DePaul University, Alan Jeffrey Mozilla Research, James Riely DePaul University
Link to publication DOI Pre-print Media Attached
07:40
20m
Talk
StreamQL: A Query Language for Processing Streaming Time Series
OOPSLA
Lingkun Kong Rice University, Konstantinos Mamouras Rice University
Link to publication DOI Media Attached
08:00
20m
Talk
Foundations of Empirical Memory Consistency Testing
OOPSLA
Jake Kirkham Princeton University, Tyler Sorensen University of California at Santa Cruz, Esin Tureci Princeton University, Margaret Martonosi Princeton University
Link to publication DOI Media Attached
19:00 - 20:20
F-1AOOPSLA at SPLASH-I
Chair(s): Tongping Liu University of Massachusetts at Amherst, Azalea Raad Imperial College London
19:00
20m
Talk
DiffStream: Differential Output Testing for Stream Processing Programs
OOPSLA
Konstantinos Kallas University of Pennsylvania, Filip Niksic Google, Caleb Stanford University of Pennsylvania, Rajeev Alur University of Pennsylvania
Link to publication DOI Media Attached
19:20
20m
Talk
Pomsets with Preconditions: A Simple Model of Relaxed Memory
OOPSLA
Radha Jagadeesan DePaul University, Alan Jeffrey Mozilla Research, James Riely DePaul University
Link to publication DOI Pre-print Media Attached
19:40
20m
Talk
StreamQL: A Query Language for Processing Streaming Time Series
OOPSLA
Lingkun Kong Rice University, Konstantinos Mamouras Rice University
Link to publication DOI Media Attached
20:00
20m
Talk
Foundations of Empirical Memory Consistency Testing
OOPSLA
Jake Kirkham Princeton University, Tyler Sorensen University of California at Santa Cruz, Esin Tureci Princeton University, Margaret Martonosi Princeton University
Link to publication DOI Media Attached