Fence Synthesis under the C11 Memory Model

TL;DR

This paper introduces FenSying, the first optimal fence synthesis method for C11 programs, and a near-optimal alternative, fFenSying, both designed to restore correctness with minimal performance impact.

Contribution

It presents the first optimal fence synthesis technique for C11 programs and proposes a near-optimal, efficient alternative, with proofs and empirical evaluation.

Findings

FenSying is proven optimal for fence synthesis.

fFenSying is a sound, near-optimal alternative.

Empirical results show fFenSying's effectiveness and efficiency.

Abstract

The C/C++11 (C11) standard offers a spectrum of ordering guarantees on memory access operations. The combinations of such orderings pose a challenge in developing correct and efficient weak memory programs. A common solution to preclude those program outcomes that violate the correctness specification is using C11 synchronization-fences, which establish ordering on program events. The challenge is in choosing a combination of fences that (i) restores the correctness of the input program, with (ii) as little impact on efficiency as possible (i.e., the smallest set of weakest fences). This problem is the optimal fence synthesis problem and is NP-hard for straight-line programs. In this work, we propose the first fence synthesis technique for C11 programs called FenSying and show its optimality. We additionally propose a near-optimal efficient alternative called fFenSying. We prove the optimality of FenSying and the soundness of fFenSying and present an implementation of both techniques. Finally, we contrast the performance of the two techniques and empirically demonstrate fFenSyings effectiveness.