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.

Provided by: Association for Computing Machinery Topic: Software Date Added: Jun 2011 Format: PDF

Find By Topic