This program is tentative and subject to change.
Dynamic race detection is a highly effective runtime verification technique for identifying data races by instrumenting and monitoring concurrent program runs. However, standard dynamic race detection is incompatible with practical weak memory models; the added instrumentation introduces extra synchronization, which masks weakly consistent behaviors and inherently misses certain data races. In response, we propose to dynamically verify program robustness-a property ensuring that a program exhibits only strongly consistent behaviors. Building on an existing static decision procedures, we develop an algorithm for dynamic robustness verification under a C11-style memory model. The algorithm is based on "location clocks", a variant of vector clocks used in standard race detection. It allows effective and easy-to-apply defense against weak memory on a per-program basis, which can be combined with race detection that assumes strong consistency. We implement our algorithm in a tool, called RSAN, and evaluate it across various settings. To our knowledge, this work is the first to propose and develop dynamic verification of robustness against weak memory models.
This program is tentative and subject to change.
Wed 18 JunDisplayed time zone: Seoul change
16:00 - 17:20 | High Performance ComputingPLDI Research Papers at Grand Ball Room 2 Chair(s): Charith Mendis University of Illinois at Urbana-Champaign | ||
16:00 20mTalk | Task-Based Tensor Computations on Modern GPUs PLDI Research Papers Rohan Yadav Stanford University, Michael Garland NVIDIA, Alex Aiken Stanford University, Michael Bauer NVIDIA DOI | ||
16:20 20mTalk | Lightweight and Locality-Aware Composition of Black-Box Subroutines PLDI Research Papers Manya Bansal Massachusetts Institute of Technology, Dillon Sharlet Google, Jonathan Ragan-Kelley Massachusetts Institute of Technology, Saman Amarasinghe Massachusetts Institute of Technology DOI | ||
16:40 20mTalk | Modular Construction and Optimization of the UZP Sparse Format for SpMV on CPUs PLDI Research Papers Alonso Rodriguez Universidade da Coruña, Santoshkumar T. Tongli Colorado State University, Emily Tucker Colorado State University, Louis-Noël Pouchet Colorado State University, Gabriel Rodríguez Universidade da Coruña, Juan Tourino Universidade da Coruña DOI | ||
17:00 20mTalk | Dynamic Robustness Verification against Weak Memory PLDI Research Papers Roy Margalit Tel Aviv University, Michalis Kokologiannakis ETH Zurich, Shachar Itzhaky Technion, Ori Lahav Tel Aviv University DOI |