Inferring Fences in a Concurrent Program Using SC proof of Correctness

TL;DR

This paper presents a method to infer minimal fence instructions needed for concurrent programs to maintain correctness when executed on relaxed memory models, based on SC proof of correctness.

Contribution

It shows that SC proofs can identify essential instruction orderings, simplifying fence insertion for correct execution on relaxed memory models.

Findings

SC proof of correctness identifies sufficient instruction orderings.

Only these orderings need fences to ensure correctness.

Reduces unnecessary fence insertions for relaxed memory models.

Abstract

Most proof systems for concurrent programs assume the underlying memory model to be sequentially consistent (SC), an assumption which does not hold for modern multicore processors. These processors, for performance reasons, implement relaxed memory models. As a result of this relaxation a program, proved correct on the SC memory model, might execute incorrectly. To ensure its correctness under relaxation, fence instructions are inserted in the code. In this paper we show that the SC proof of correctness of an algorithm, carried out in the proof system of [Sou84], identifies per-thread instruction orderings sufficient for this SC proof. Further, to correctly execute this algorithm on an underlying relaxed memory model it is sufficient to respect only these orderings by inserting fence instructions.