2025/04/21 by Roy Margalit, Margalit, Roy, Michalis Kokologiannakis +5
Computer Science · Engineering · #FOS: Computer and information sciences #Fault Detection and Control Systems #Neural Networks and Applications #Programming Languages (cs.PL)
paper · pdf · doi:10.48550/arxiv.2504.15036
openalex publication_date 2025/04/21 · openalex created_date 2025/10/18 · openalex updated_date 2026/08/01
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.