P1780R2
Modular Relaxed Dependencies: A new approach to the Out-Of-Thin-Air Problem

1. Changelog

1.1. Revision 0 (Cologne June 2019)

• Original paper.

1.2. Revision 1 (Belfast October 2019)

• Draft wording to incorporate an algorithm which calculates semantic dependency.

1.3. Revision 2 (Kona November 2022)

• Draft wording which introduces semantic dependency as implementation defined.

2. Recap: The out-of-thin-air problem

From its introduction in 2011, the C++ concurrency model has faced a great deal of scrutiny, leading to various refinements of the standard. [P0668R5] Revising the C++ Memory Model, describes changes needed to incorporate the fixes of [RC11], the latest revision of the existing C++ concurrency design, solving most known problems.

This process of scrutiny and refinement has produced a mature model, but it has also uncovered major problems. The out-of-thin-air problem, discussed most recently in [P1217R1] allows unintuitive and unobservable behaviours and makes reasoning formally about the correctness of concurrent code impossible. The thin air problem does not yet have a convenient solution: existing solutions -- like the Promising Semantics [Promising] -- discard the mature concurrency model of the standard and start afresh with a different paradigm. Implementing such a change would require a wide-ranging rewrite of the standard.

The out-of-thin-air problem arises from an under-specification of which program dependencies ought to order memory accesses. The trouble is neatly explained by example.

// Thread 1
r1 = x.load(memory_order::relaxed);
y.store(1, memory_order::relaxed);

// Thread 2
r2 = y.load(memory_order::relaxed);
x.store(1, memory_order::relaxed);

In the example above, called Load Buffering (LB), C++ allows the execution where r1 and r2 have value 1 at the end of execution. This outcome must be allowed to permit efficient compilation of relaxed accesses to plain loads and stores on the Power and ARM architectures, where the corresponding behaviour is allowed.

// Thread 1
r1 = x.load(memory_order::relaxed);
y.store(r1, memory_order::relaxed);

// Thread 2
r2 = y.load(memory_order::relaxed);
x.store(r1, memory_order::relaxed);

In the example above, taken from [P1217R1], there are now data dependencies from load to store and no explicit write of any value. Surprisingly, the outcome 42 is allowed by the C++ standard -- we say that the value 42 is conjured from thin-air.

// Thread 1
r1 = x.load(memory_order::relaxed);
if(r1 == 42) {
  y.store(42, memory_order::relaxed);
}

// Thread 2
r2 = y.load(memory_order::relaxed);
if(r2 == 42) {
  x.store(42, memory_order::relaxed);
}

A similar behaviour can be exhibited using control dependencies, as above. The thin-air outcomes of LB+datas and LB+ctrls are the result of a design choice that aims to permit compiler optimisation: some optimisations remove syntactic dependencies, so if C++ bestows ordering to no dependencies, the compiler is free to remove what it likes.

// Thread 1
r1 = x.load(memory_order::relaxed);
if(r1 == 42) {
  y.store(42, memory_order::relaxed);
} else {
  y.store(42, memory_order::relaxed);
}

// Thread 2
r2 = y.load(memory_order::relaxed);
if(r2 == 42) {
  x.store(42, memory_order::relaxed);
}

In Thread 1 above, a compiler may spot that, whatever value is read, the write will be made regardless, optimising to the program below, and allowing both threads to read 42:

// Thread 1
r1 = x.load(memory_order::relaxed);
y.store(42, memory_order::relaxed);

As it stands, the standard allows both threads to read 42 and hence it permits the optimisation, but it also allows the thin-air outcomes in LB+datas and LB+ctrls. [P1217R1] explains that these outcomes cannot occur in practice and must be forbidden to enable reasoning and formal verification.

3. Our Solution

[P0422R0] highlights a series of litmus tests, borrowed from Java, that constrain the ideal behaviour of an improved semantics (e.g. JCTC4, JCTC13 and JCTC6 above). The paper makes the observation that the thin-air execution of each test features a cycle in (rf ∪ sdep) where sdep, semantic dependency, is an as yet undefined relation that captures only the real dependencies that the compiler will leave in place. If only we forbid cycles in (rf ∪ sdep), then the model would have the behaviour we desire.

[P1217R1] highlights a simple way to guarantee a lack of thin-air behaviour: forbid the reordering of relaxed loads with following stores. This is equivalent to forbidding cycles in (rf ∪ sb), and is sufficient to avoid cycles in (rf ∪ sdep). This approach is controversial because it may have a substantial overhead, especially on GPUs.

We have worked as academics on building a definition for sdep which can be calculated over an input program. We have found two such approaches, one presented in an earlier version of this paper, and in academic literature as [MRD], and another in the academic literature which uses a different approach to build sdep [PWT]. These models are complex and by no means industrially verified, but it leads us to agree with [P0422R0] and propose a standard wording change which incorporates an idea of sdep. In further work, we adapted established concurrent reasoning techiques (Hoare triples with Owicki-Gries global invariants) to work above the C++ model with sdep, establishing that this approach once again enables one to prove C++ code correct [owicki-gries].

The standard describes the three stages of working out the concurrent behaviour of a program:

1. Generate a list of pre-executions from the source of a program, each corresponding to an arbitrary choice of read values.

2. Pair each pre-execution with reads-from and modification order relations that capture the dynamic memory behaviour of the program, and filter, keeping those that are consistent with the rules of the memory model.

3. Finally, check for races: race free programs have the consistent executions calculated in step 2, racy programs have undefined behaviour.

We augment this scheme by parameterising sdep in step 1, and by providing a technical note on constraints which a good C++ implementation should put on sdep—for example, forbidding the out-of-thin-air execution by always including sdep edges in JCTC4.

This approach is distinct from [Promising] and other suggested academic models, because nearly all of the existing wording on memory consitency can be preserved. It also is certainly compatible with existing implementations, as constraints to place on the "shape" of sdep would be provided in a technical note, which can be written with taste for current implementations of C++.

4. Conclusion

We have found several possible solutions in academic literature to the thin-air problem, but none look like they can be plucked and placed into the standard without considerable re-writes of the existing memory model text. We consider this to be undesirable, and propose a fix as was originally suggested in [P0422R0], but with the added knowledge that sdep can be calculated and used for reasoning. This aproach has several benefits:

• continued support of ld;st re-ordering,

• reasoning about programs with RFUB behaviour,

• no additional implementation cost on major architectures,

• extension rather than re-creation of the existing standard,

• the extensionis compatible with the latest refinements to the standard, not just with the C++11 wording,

• potential route to redefining memory_order::consume using semantic dependency.

5. Proposed Standard Change

[...]

[...]

[...]

// Thread 1:
r1 = y.load(memory_order::relaxed);
x.store(r1, memory_order::relaxed);
// Thread 2:
r2 = x.load(memory_order::relaxed);
y.store(r2, memory_order::relaxed);

// Thread 1:
r1 = x.load(memory_order::relaxed);
if (r1 == 42) y.store(42, memory_order::relaxed);
// Thread 2:
r2 = y.load(memory_order::relaxed);
if (r2 == 42) x.store(42, memory_order::relaxed);

[...]