February 14, 2017
This article was contributed by Jade Alglave,
Paul E. McKenney, Alan Stern, Luc Maranget, and Andrea Parri
Introduction
This article describes the weak model in terms of its differences from
the strong model.
Note that this weak model is not based on any sort of operational
model, but was instead constructed from the
strong model
by removing the following things that didn't seem to be important
or mature enough for the Linux kernel:
- Locking.
- C11 Release Sequences.
- Preserved Program Order.
- Cumulativity.
- Coherence Point and RCU.
This is followed by the inevitable
answers to the quick quizzes.
The
strong model
includes an early prototype of locking, but this prototype is under
development and is likely to change dramatically before being finalized.
Therefore, locking will not be included into the weak model until after
all the strong-model kinks have been worked out:
1 @@ -20,7 +20,6 @@
2 *)
3
4 include "cos-opt.cat"
5 -include "lock.cat"
6
7 let com = rf | co | fr
8 let coherence-order = po-loc | com
9 @@ -29,26 +28,16 @@
10 empty rmw & (fre;coe) as atomic
11
12
13 -let rf = rf | next-crit
14 -let rfe = rf & ext
15 -
16 -let exec-order-fence = rmb | acq-po | lk-po
17 -let propagation-fence = strong-fence | wmb | po-relass | po-ul
18 +let exec-order-fence = rmb | acq-po
19 +let propagation-fence = strong-fence | wmb | po-relass
20 let ordering-fence = propagation-fence | exec-order-fence
Release sequences are an interesting part of the C11 memory model, but
we don't know of any Linux-kernel use cases, so the weak model omits them.
The following unified diff from the strong to the weak model implements
this omission:
1 -(* Determine the release sequences *)
2 -let rel-seq = [ReleaseAssign] ; coi? ; (rf ; rmw)*
3 -let po-rel-seq = po ; rel-seq
The difference is illustrated by the following litmus test:
Weak Model Litmus Test #1
1 C C-relseq.litmus
2
3 {
4 }
5
6 P0(int *x, int *y)
7 {
8 WRITE_ONCE(*x, 1);
9 smp_store_release(y, 1);
10 WRITE_ONCE(*y, 2);
11 }
12
13 P1(int *y)
14 {
15 r1 = xchg_relaxed(y, 3);
16 }
17
18 P2(int *x, int *y)
19 {
20 r2 = READ_ONCE(*y);
21 smp_rmb();
22 r3 = READ_ONCE(*x);
23 }
24
25 exists (1:r1=2 /\ 2:r2=3 /\ 2:r3=0)
The strong model forbids this outcome:
Outcome for Weak Model Litmus Test #1 (strong model)
1 Test C-relseq Allowed
2 States 16
3 1:r1=0; 2:r2=0; 2:r3=0;
4 1:r1=0; 2:r2=0; 2:r3=1;
5 1:r1=0; 2:r2=1; 2:r3=1;
6 1:r1=0; 2:r2=2; 2:r3=1;
7 1:r1=0; 2:r2=3; 2:r3=0;
8 1:r1=0; 2:r2=3; 2:r3=1;
9 1:r1=1; 2:r2=0; 2:r3=0;
10 1:r1=1; 2:r2=0; 2:r3=1;
11 1:r1=1; 2:r2=1; 2:r3=1;
12 1:r1=1; 2:r2=2; 2:r3=1;
13 1:r1=1; 2:r2=3; 2:r3=1;
14 1:r1=2; 2:r2=0; 2:r3=0;
15 1:r1=2; 2:r2=0; 2:r3=1;
16 1:r1=2; 2:r2=1; 2:r3=1;
17 1:r1=2; 2:r2=2; 2:r3=1;
18 1:r1=2; 2:r2=3; 2:r3=1;
19 No
20 Witnesses
21 Positive: 0 Negative: 16
22 Condition exists (1:r1=2 /\ 2:r2=3 /\ 2:r3=0)
23 Observation C-relseq Never 0 16
24 Hash=e91cd6a4ee3993b84e2c28cb21588172
But the weak model allows it, as required:
Outcome for Weak Model Litmus Test #1
1 Test C-relseq Allowed
2 States 21
3 1:r1=0; 2:r2=0; 2:r3=0;
4 1:r1=0; 2:r2=0; 2:r3=1;
5 1:r1=0; 2:r2=1; 2:r3=1;
6 1:r1=0; 2:r2=2; 2:r3=0;
7 1:r1=0; 2:r2=2; 2:r3=1;
8 1:r1=0; 2:r2=3; 2:r3=0;
9 1:r1=0; 2:r2=3; 2:r3=1;
10 1:r1=1; 2:r2=0; 2:r3=0;
11 1:r1=1; 2:r2=0; 2:r3=1;
12 1:r1=1; 2:r2=1; 2:r3=1;
13 1:r1=1; 2:r2=2; 2:r3=0;
14 1:r1=1; 2:r2=2; 2:r3=1;
15 1:r1=1; 2:r2=3; 2:r3=0;
16 1:r1=1; 2:r2=3; 2:r3=1;
17 1:r1=2; 2:r2=0; 2:r3=0;
18 1:r1=2; 2:r2=0; 2:r3=1;
19 1:r1=2; 2:r2=1; 2:r3=1;
20 1:r1=2; 2:r2=2; 2:r3=0;
21 1:r1=2; 2:r2=2; 2:r3=1;
22 1:r1=2; 2:r2=3; 2:r3=0;
23 1:r1=2; 2:r2=3; 2:r3=1;
24 Ok
25 Witnesses
26 Positive: 1 Negative: 20
27 Condition exists (1:r1=2 /\ 2:r2=3 /\ 2:r3=0)
28 Observation C-relseq Sometimes 1 20
29 Hash=e91cd6a4ee3993b84e2c28cb21588172
An additional adjustment will be required later in the model to account
for the fact that po-rel-seq is no longer defined.
This will be covered
in a later section.
The weak model weakens preserved program order (ppo)
by eliminating the po-loc,
addrpo, rd-rdw, detour,
and rdw constraints, as shown in this diff:
1 -(* On Alpha, rd-dep-fence makes addr, dep-rfi, and rdw strong *)
2 +(* On Alpha, rd-dep-fence makes addr and dep-rfi strong *)
3 let dep = addr | data
4 let dep-rfi = dep ; rfi
5 let rd-addr-dep-rfi = (addr | dep-rfi)+ & rd-dep-fence
6 -let rdw = po-loc & (fre ; rfe)
7 -let rd-rdw = rdw & rd-dep-fence
8 let po-loc-ww = po-loc & (W*W)
9 let detour = (po-loc & (coe ; rfe)) \ (po-loc-ww ; po-loc)
10 -let addrpo = addr ; po
11
12 (* The set of writes that are bounded by the end of the thread
13 or by a fence before the next write to the same address *)
14 @@ -65,45 +54,31 @@
15 let ncoe = nco & ext
16
17 let strong-ppo = rd-addr-dep-rfi | ordering-fence |
18 - ((dep | ctrl | addrpo) & (R*W))
19 -let Alpha-strong-ppo = strong-ppo | rd-rdw | detour |
20 - (po-loc & ((M\OW\OR)*W))
21 + ((dep | ctrl) & (R*W))
22 +let Alpha-strong-ppo = strong-ppo
23 let ARM-strong-ppo = strong-ppo | addr | dep-rfi
24 -let ppo = Alpha-strong-ppo | ARM-strong-ppo | rdw
25 +let ppo = Alpha-strong-ppo | ARM-strong-ppo
The effect of the omission of rd-rdw is illustrated by this
litmus test:
Weak Model Litmus Test #2
1 C C-rdw
2
3 {
4 int *x = &u;
5 int *y = &u;
6 }
7
8 P0(int **x, int **y, int *z)
9 {
10 WRITE_ONCE(*z, 1);
11 smp_mb();
12 WRITE_ONCE(*y, x);
13 }
14
15 P1(int **x, int **y)
16 {
17 int *r1;
18 int r2;
19 int *r3;
20 int r4;
21
22 r1 = lockless_dereference(*y);
23 r2 = READ_ONCE(*r1);
24 r3 = lockless_dereference(*x);
25 r4 = READ_ONCE(*r3);
26 }
27
28 P2(int **x, int *z)
29 {
30 WRITE_ONCE(*x, z);
31 }
32
33 exists (1:r1=x /\ 1:r2=u /\ 1:r3=z /\ 1:r4=0)
The strong model forbids this outcome:
Outcome for Weak Model Litmus Test #2 (strong model)
1 Test C-rdw Allowed
2 States 7
3 1:r1=u; 1:r2=0; 1:r3=u; 1:r4=0;
4 1:r1=u; 1:r2=0; 1:r3=z; 1:r4=0;
5 1:r1=u; 1:r2=0; 1:r3=z; 1:r4=1;
6 1:r1=x; 1:r2=u; 1:r3=u; 1:r4=0;
7 1:r1=x; 1:r2=u; 1:r3=z; 1:r4=1;
8 1:r1=x; 1:r2=z; 1:r3=z; 1:r4=0;
9 1:r1=x; 1:r2=z; 1:r3=z; 1:r4=1;
10 No
11 Witnesses
12 Positive: 0 Negative: 7
13 Condition exists (1:r1=x /\ 1:r2=u /\ 1:r3=z /\ 1:r4=0)
14 Observation C-rdw Never 0 7
15 Hash=f043c902021117322a4e168a27c60da9
But the weak model allows it, as required:
Outcome for Weak Model Litmus Test #2
1 Test C-rdw Allowed
2 States 8
3 1:r1=u; 1:r2=0; 1:r3=u; 1:r4=0;
4 1:r1=u; 1:r2=0; 1:r3=z; 1:r4=0;
5 1:r1=u; 1:r2=0; 1:r3=z; 1:r4=1;
6 1:r1=x; 1:r2=u; 1:r3=u; 1:r4=0;
7 1:r1=x; 1:r2=u; 1:r3=z; 1:r4=0;
8 1:r1=x; 1:r2=u; 1:r3=z; 1:r4=1;
9 1:r1=x; 1:r2=z; 1:r3=z; 1:r4=0;
10 1:r1=x; 1:r2=z; 1:r3=z; 1:r4=1;
11 Ok
12 Witnesses
13 Positive: 1 Negative: 7
14 Condition exists (1:r1=x /\ 1:r2=u /\ 1:r3=z /\ 1:r4=0)
15 Observation C-rdw Sometimes 1 7
16 Hash=f043c902021117322a4e168a27c60da9
The effect of the omission of po-loc is illustrated by this
litmus test:
Weak Model Litmus Test #3
1 C C-po-loc
2
3 {
4 }
5
6 P0(int *x, int *y)
7 {
8 int r0;
9 int r1;
10
11 r0 = READ_ONCE(*y);
12 smp_rmb();
13 r1 = READ_ONCE(*x);
14 WRITE_ONCE(*x, 1);
15 }
16
17 P1(int *x, int *y)
18 {
19 int r2;
20
21 r2 = READ_ONCE(*x);
22 WRITE_ONCE(*y, r2);
23 }
24
25 exists (0:r0=1)
The strong model forbids this outcome:
Outcome for Weak Model Litmus Test #3 (strong model)
1 Test C-po-loc Allowed
2 States 1
3 0:r0=0;
4 No
5 Witnesses
6 Positive: 0 Negative: 3
7 Condition exists (0:r0=1)
8 Observation C-po-loc Never 0 3
9 Hash=a11fb621142d409791210d12be417e35
But the weak model allows it, as required:
Outcome for Weak Model Litmus Test #3
1 Test C-po-loc Allowed
2 States 2
3 0:r0=0;
4 0:r0=1;
5 Ok
6 Witnesses
7 Positive: 1 Negative: 3
8 Condition exists (0:r0=1)
9 Observation C-po-loc Sometimes 1 3
10 Hash=a11fb621142d409791210d12be417e35
The effect of the omission of addrpo is illustrated by this
litmus test:
Weak Model Litmus Test #4
1 C C-addrpo
2
3 {
4 int u = 0;
5 int v = 1;
6 int *x = u;
7 }
8
9 P0(int **x, int *y)
10 {
11 int *r0;
12 int r1;
13
14 r0 = lockless_dereference(*x);
15 r1 = READ_ONCE(*r0);
16 WRITE_ONCE(*y, 1);
17 }
18
19 P1(int **x, int *y, int *v)
20 {
21 int r2;
22
23 r2 = READ_ONCE(*y);
24 if (r2 != 0)
25 WRITE_ONCE(*x, v);
26 }
27
28 exists (0:r1=1)
The strong model forbids this outcome:
Outcome for Weak Model Litmus Test #4 (strong model)
1 Test C-addrpo Allowed
2 States 1
3 0:r1=0;
4 No
5 Witnesses
6 Positive: 0 Negative: 2
7 Condition exists (0:r1=1)
8 Observation C-addrpo Never 0 2
9 Hash=9d214f4ecf25f0dc4aec431700fe56ea
But the weak model allows it, as required:
Outcome for Weak Model Litmus Test #4
1 Test C-addrpo Allowed
2 States 2
3 0:r1=0;
4 0:r1=1;
5 Ok
6 Witnesses
7 Positive: 1 Negative: 2
8 Condition exists (0:r1=1)
9 Observation C-addrpo Sometimes 1 2
10 Hash=9d214f4ecf25f0dc4aec431700fe56ea
The omission of rdw and detour are more subtle and
are difficult to illustrate with C code, which is one reason we felt
confident about omitting them from the weak model.
The weak model requires less hardware support for cumulativity than does
the strong model:
1 let rfe-ppo = strong-ppo | (ARM-strong-ppo ; ppo* ; Alpha-strong-ppo)
2 -let po-relass-acq-hb = (po ; (rfe & (ReleaseAssign*Acquire)) ; rfe-ppo) |
3 - (po-ul ; next-crit ; lk-po)
4
5 -(* Release paired with Acquire is both A- and B-cumulative *)
6 -let AB-cum-hb = strong-fence | po-relass-acq-hb
7 -let A-cum-hb = AB-cum-hb | po-relass | po-rel-seq
8 -let B-cum-hb = AB-cum-hb | wmb
9 +(* strong-fence and release/assign are A-cumulative; wmb is not. *)
10 +let propbase = wmb | (rfe? ; strong-fence) | (rfe? ; po-relass)
11
12 +let short-obs = ((ncoe|fre) ; propbase+ ; rfe) & int
13 let hb0 = (ppo* ; Alpha-strong-ppo) | (rfe ; rfe-ppo)
14 -let propbase0 = propagation-fence | (rfe? ; A-cum-hb)
15 -
16 -let rec B-cum-propbase = (B-cum-hb ; hb* ) |
17 - (rfe? ; AB-cum-hb ; hb* )
18 - and propbase = propbase0 | B-cum-propbase
19 - and short-obs = ((ncoe|fre) ; propbase+ ; rfe) & int
20 - and obs = short-obs |
21 - ((hb* ; (ncoe|fre) ; propbase* ; B-cum-propbase ; rfe) & int)
22 - and hb = hb0 | (obs ; rfe-ppo)
23 +let hb = hb0 | (short-obs ; rfe-ppo)
24
25 acyclic hb as happens-before
26 -irreflexive (short-obs ; Alpha-strong-ppo) as observation
In particular, the weak model does not provide B-cumulativity for
smp_wmb() or for release-acquire sequences.
However, it does provide A-cumulativity for strong barriers and for
write-release operations.
As can be seen above, this has the advantage of greatly simplifying
the hb relation.
The effect of the omission of B-cumulativity for smp_wmb()
is illustrated by this litmus test:
Weak Model Litmus Test #5
1 C C-wmb-is-B-cumulative.litmus
2
3 {
4 }
5
6 P0(int *x, int *y)
7 {
8 WRITE_ONCE(*x, 1);
9 smp_wmb();
10 WRITE_ONCE(*y, 1);
11 }
12
13 P1(int *y, int *z)
14 {
15 r1 = READ_ONCE(*y);
16 WRITE_ONCE(*z, r1);
17 }
18
19 P2(int *x, int *z)
20 {
21 r2 = READ_ONCE(*z);
22 smp_rmb();
23 r3 = READ_ONCE(*x);
24 }
25
26 exists (1:r1=1 /\ 2:r2=1 /\ 2:r3=0)
The strong model forbids this outcome:
Outcome for Weak Model Litmus Test #5 (strong model)
1 Test C-wmb-is-B-cumulative Allowed
2 States 5
3 1:r1=0; 2:r2=0; 2:r3=0;
4 1:r1=0; 2:r2=0; 2:r3=1;
5 1:r1=1; 2:r2=0; 2:r3=0;
6 1:r1=1; 2:r2=0; 2:r3=1;
7 1:r1=1; 2:r2=1; 2:r3=1;
8 No
9 Witnesses
10 Positive: 0 Negative: 7
11 Condition exists (1:r1=1 /\ 2:r2=1 /\ 2:r3=0)
12 Observation C-wmb-is-B-cumulative Never 0 7
13 Hash=50e5fc4aa803470487c5d3d26abf5b04
But the weak model allows it, as required:
Outcome for Weak Model Litmus Test #5
1 Test C-wmb-is-B-cumulative Allowed
2 States 6
3 1:r1=0; 2:r2=0; 2:r3=0;
4 1:r1=0; 2:r2=0; 2:r3=1;
5 1:r1=1; 2:r2=0; 2:r3=0;
6 1:r1=1; 2:r2=0; 2:r3=1;
7 1:r1=1; 2:r2=1; 2:r3=0;
8 1:r1=1; 2:r2=1; 2:r3=1;
9 Ok
10 Witnesses
11 Positive: 1 Negative: 7
12 Condition exists (1:r1=1 /\ 2:r2=1 /\ 2:r3=0)
13 Observation C-wmb-is-B-cumulative Sometimes 1 7
14 Hash=50e5fc4aa803470487c5d3d26abf5b04
Similarly, the effect of the omission of B-cumulativity for release-acquire
chains is illustrated by this litmus test:
Weak Model Litmus Test #6
1 C C-release-acquire-is-B-cumulative.litmus
2
3 {
4 }
5
6 P0(int *x, int *y)
7 {
8 WRITE_ONCE(*x, 1);
9 smp_store_release(y, 1);
10 }
11
12 P1(int *y, int *z)
13 {
14 r1 = smp_load_acquire(y);
15 WRITE_ONCE(*z, 1);
16 }
17
18 P2(int *x, int *z)
19 {
20 r2 = READ_ONCE(*z);
21 smp_rmb();
22 r3 = READ_ONCE(*x);
23 }
24
25 exists (1:r1=1 /\ 2:r2=1 /\ 2:r3=0)
The strong model forbids this outcome:
Outcome for Weak Model Litmus Test #6 (strong model)
1 Test C-release-acquire-is-B-cumulative Allowed
2 States 7
3 1:r1=0; 2:r2=0; 2:r3=0;
4 1:r1=0; 2:r2=0; 2:r3=1;
5 1:r1=0; 2:r2=1; 2:r3=0;
6 1:r1=0; 2:r2=1; 2:r3=1;
7 1:r1=1; 2:r2=0; 2:r3=0;
8 1:r1=1; 2:r2=0; 2:r3=1;
9 1:r1=1; 2:r2=1; 2:r3=1;
10 No
11 Witnesses
12 Positive: 0 Negative: 7
13 Condition exists (1:r1=1 /\ 2:r2=1 /\ 2:r3=0)
14 Observation C-release-acquire-is-B-cumulative Never 0 7
15 Hash=05d2a37a17c72e47142a9dee610d1ba3
But the weak model allows it, as required:
Outcome for Weak Model Litmus Test #6
1 Test C-release-acquire-is-B-cumulative Allowed
2 States 8
3 1:r1=0; 2:r2=0; 2:r3=0;
4 1:r1=0; 2:r2=0; 2:r3=1;
5 1:r1=0; 2:r2=1; 2:r3=0;
6 1:r1=0; 2:r2=1; 2:r3=1;
7 1:r1=1; 2:r2=0; 2:r3=0;
8 1:r1=1; 2:r2=0; 2:r3=1;
9 1:r1=1; 2:r2=1; 2:r3=0;
10 1:r1=1; 2:r2=1; 2:r3=1;
11 Ok
12 Witnesses
13 Positive: 1 Negative: 7
14 Condition exists (1:r1=1 /\ 2:r2=1 /\ 2:r3=0)
15 Observation C-release-acquire-is-B-cumulative Sometimes 1 7
16 Hash=05d2a37a17c72e47142a9dee610d1ba3
Quick Quiz 1:
Given the great simplification arising from weakening cumulativity,
why not also weaken it for the strong model?
Answer
The changes to the coherence-point and RCU portions of the weak memory
model are primarily side effects of earlier changes:
1 -let strong-prop = fre? ; propbase* ; rfe? ; strong-fence ; hb* ; obs?
2 -let prop = (propbase & (W*W)) | strong-prop
3 -let cpord = nco | prop
4 +let strong-prop = fre? ; propbase* ; rfe? ; strong-fence ; hb* ; short-obs?
5 +let cpord = nco | strong-prop
6
7 acyclic cpord as propagation
8
9
10 (* Propagation between strong fences *)
11 -let rcu-order = hb* ; obs? ; cpord* ; fre? ; propbase* ; rfe?
12 +let rcu-order = hb* ; short-obs? ; cpord* ; fre? ; propbase* ; rfe?
13
14 (* Chains that can prevent the RCU grace-period guarantee *)
15 let gp-link = sync ; rcu-order
However, one important difference is illustrated by the following
litmus test:
Weak Model Litmus Test #7
1 C C-2+2W+o-wmb-o+o-wmb-o.litmus
2
3 {
4 }
5
6 P0(int *a, int *b)
7 {
8 WRITE_ONCE(*a, 2);
9 smp_wmb();
10 WRITE_ONCE(*b, 1);
11 }
12
13 P1(int *a, int *b)
14 {
15 WRITE_ONCE(*b, 2);
16 smp_wmb();
17 WRITE_ONCE(*a, 1);
18 }
19
20 exists
21 (b=2 /\ a=2)
The strong model forbids this outcome:
Outcome for Weak Model Litmus Test #7 (strong model)
1 Test C-2+2W+o-wmb-o+o-wmb-o Allowed
2 States 3
3 a=1; b=1;
4 a=1; b=2;
5 a=2; b=1;
6 No
7 Witnesses
8 Positive: 0 Negative: 3
9 Condition exists (b=2 /\ a=2)
10 Observation C-2+2W+o-wmb-o+o-wmb-o Never 0 3
11 Hash=8264db947f1b73b8be16f98dd6bf1634
But the weak model allows it, as required:
Outcome for Weak Model Litmus Test #7
1 Test C-2+2W+o-wmb-o+o-wmb-o Allowed
2 States 4
3 a=1; b=1;
4 a=1; b=2;
5 a=2; b=1;
6 a=2; b=2;
7 Ok
8 Witnesses
9 Positive: 1 Negative: 3
10 Condition exists (b=2 /\ a=2)
11 Observation C-2+2W+o-wmb-o+o-wmb-o Sometimes 1 3
12 Hash=8264db947f1b73b8be16f98dd6bf1634
The weak model does not require hardware support for this
“2+2W” litmus test because we never have found a use case
that isn't better served by some other pattern.
Acknowledgments
We owe thanks to H. Peter Anvin, Will Deacon, Andy Glew,
Derek Williams, Leonid Yegoshin, and Peter Zijlstra for their
patient explanations of their respective systems' memory models.
We are indebted to Peter Sewell, Susmit Sarkar, and their groups
for their seminal work formalizing many of these same memory models.
We all owe thanks to @@@
for their help making this human-readable.
We are also grateful to Jim Wasko for their support of this effort.
This work represents the views of the authors and does not necessarily
represent the views of University College London, INRIA Paris,
Scuola Superiore Sant'Anna, Harvard University, or IBM Corporation.
Linux is a registered trademark of Linus Torvalds.
Other company, product, and service names may be trademarks or
service marks of others.
Quick Quiz 1:
Given the great simplification arising from weakening cumulativity,
why not also weaken it for the strong model?
Answer:
That might well be the eventual outcome, but a very large amount of
discussion, experimentation, and further modeling would need to be
completed before we could in good conscience weaken cumulativity in
the strong model, particularly for release-acquire chains.
Back to Quick Quiz 1.