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 NovDisplayed 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 20mTalk | 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 20mTalk | Pomsets with Preconditions: A Simple Model of Relaxed Memory OOPSLA Link to publication DOI Pre-print Media Attached | ||
07:40 20mTalk | StreamQL: A Query Language for Processing Streaming Time Series OOPSLA Link to publication DOI Media Attached | ||
08:00 20mTalk | 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 20mTalk | 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 20mTalk | Pomsets with Preconditions: A Simple Model of Relaxed Memory OOPSLA Link to publication DOI Pre-print Media Attached | ||
19:40 20mTalk | StreamQL: A Query Language for Processing Streaming Time Series OOPSLA Link to publication DOI Media Attached | ||
20:00 20mTalk | 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 |