Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Dynamic Robustness Verification Against Weak Memory (Extended Version)

Roy Margalit, Michalis Kokologiannakis, Shachar Itzhaky, Ori Lahav

TL;DR

This work tackles the observer effect in dynamic data-race detection under weak memory by introducing dynamic robustness verification against weak memory models, specifically RC20/C11. It develops Location Clocks (LCs) to track per-location views and integrates a robustness verifier with a race detector, yielding a practical tool (RSAN) built on TSan. The approach provides a sound and complete dynamic method for detecting non-robust behaviors, supports RMWs and RC20 semantics, and demonstrates scalability on real-world code with meaningful overhead reductions compared to exhaustive static techniques. RSAN enables developers to identify and repair weak-memory-induced robustness violations with targeted fences or access-strengthening, improving portability and performance without requiring deep expertise in weak memory semantics.

Abstract

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.

Dynamic Robustness Verification Against Weak Memory (Extended Version)

TL;DR

This work tackles the observer effect in dynamic data-race detection under weak memory by introducing dynamic robustness verification against weak memory models, specifically RC20/C11. It develops Location Clocks (LCs) to track per-location views and integrates a robustness verifier with a race detector, yielding a practical tool (RSAN) built on TSan. The approach provides a sound and complete dynamic method for detecting non-robust behaviors, supports RMWs and RC20 semantics, and demonstrates scalability on real-world code with meaningful overhead reductions compared to exhaustive static techniques. RSAN enables developers to identify and repair weak-memory-induced robustness violations with targeted fences or access-strengthening, improving portability and performance without requiring deep expertise in weak memory semantics.

Abstract

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.

Paper Structure

This paper contains 54 sections, 4 theorems, 28 equations, 8 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. The Release/Acquire Memory Model
  4. Domains
  5. Events
  6. Execution Graphs
  7. Derived Relations
  8. From Programs to Execution Graphs
  9. Consistency
  10. Robustness
  11. Robustness Verification
  12. Non-Robustness Witnesses
  13. Bounded Instrumentation
  14. Robustness Verification
  15. Location-Clock-Based Robustness Analysis
  16. ...and 39 more sections

Key Result

theorem 1

A program ${P}$ is robust iff running ${P}$ under $\textnormal{SC}$ with the instrumentation given in fig:bm:transitions never reaches a state in which thread ${\tau}$ is about to access some location ${x} \in \mathrm{T}_\textnormal{SC}\xspace({\tau}) \setminus \mathrm{T}_\textnormal{HB}\xspace({\ta

Figures (8)

  • Figure 1: Examples of consistency and robustness.
  • Figure 2: Maintaining BMs when thread ${\tau}$ accesses location ${x}$
  • Figure 3: BM-instrumentation maintenance for a run of \ref{['prog:sb']}
  • Figure 4: Maintaining LCs when thread ${\tau}$ accesses location ${x}$, where $t = {\mathbb{{}{W}}_\textnormal{HB}\xspace}({x})({x}) +1= {\mathbb{{}{W}}_\textnormal{SC}\xspace}({x})({x}) +1$
  • Figure 5: LC-instrumentation maintenance for a run of \ref{['prog:sb']}
  • ...and 3 more figures

Theorems & Definitions (7)

  • definition 1
  • theorem 1
  • theorem 2
  • proof : Proof (sketch)
  • theorem 3: WR & WW-races
  • proof
  • theorem 4: RW-races