Partial-Coherence Abstractions for Relaxed Memory Models
The authors present an approach for automatic verification and fence inference in concurrent programs running under relaxed memory models. Verification under relaxed memory models is a hard problem. Given a finite state program and a safety specification, verifying that the program satisfies the specification under a sufficiently relaxed memory model is undecidable. For stronger models, the problem is decidable but has non-primitive recursive complexity. In this paper, they focus on models that have store-buffer based semantics, e.g., SPARC TSO and PSO.