Skip to main content

Assertional reasoning about data races in relaxed memory models

Beverly A. Sanders, KyungHee Kim

Publisher page dblp BibTeX

Abstract

We describe the ideas behind a method to use assertional reasoning to statically show that all sequentially consistent executions of a concurrent program are free from data races.

DOI 10.1145/1345206.1345249

Related papers

Relaxed separation logic: a program logic for C11 concurrency OOPSLA 2013
Modular data-race-freedom guarantees in the promising semantics PLDI 2021
RustBelt meets relaxed memory POPL 2020
Relaxed memory models: an operational approach POPL 2009
Automated Robustness Verification of Concurrent Data Structure Libraries against Relaxed Memory Models OOPSLA 2024
RaceFree: an efficient multi-threading model for determinism PPoPP 2013
Repairing and mechanising the JavaScript relaxed memory model PLDI 2020
Relaxed Memory Concurrency Re-executed POPL 2025