pull/378/head
SabrinaJewson 10 months ago
parent ff32f70202
commit af524a598c
No known key found for this signature in database
GPG Key ID: 3D5438FFA5F05564

@ -26,7 +26,7 @@ impl<T> Mutex<T> {
``` ```
Now for the lock function. We need to use an RMW here, since we need to both Now for the lock function. We need to use an RMW here, since we need to both
check whether it is locked and lock it if is not in a single atomic step; this check whether it is locked and lock it if it isnt in a single atomic step; this
can be most simply done with a `compare_exchange` (unlike before, it doesnt can be most simply done with a `compare_exchange` (unlike before, it doesnt
need to be in a loop this time). For the ordering, well just use `Relaxed` need to be in a loop this time). For the ordering, well just use `Relaxed`
since we dont know of any others yet. since we dont know of any others yet.
@ -158,7 +158,7 @@ case that doesnt seem to be enough, since even if atomics were used it still
would have the _option_ of reading `0` instead of `1`, and really if we want our would have the _option_ of reading `0` instead of `1`, and really if we want our
mutex to be sane, it should only be able to read `1`. mutex to be sane, it should only be able to read `1`.
So it seems that want we _want_ is to be able to apply the coherence rules from So it seems that what we _want_ is to be able to apply the coherence rules from
before to completely rule out zero from the set of the possible values — if we before to completely rule out zero from the set of the possible values — if we
were able to draw a large arrow from the Thread 1s `+= 1;` to Thread 2s were able to draw a large arrow from the Thread 1s `+= 1;` to Thread 2s
`guard`, then we could trivially then use the rule to rule out `0` as a value `guard`, then we could trivially then use the rule to rule out `0` as a value
@ -256,7 +256,7 @@ We now can trace back along the reverse direction of arrows from the `guard`
bubble to the `+= 1` bubble; we have established that Thread 2s load bubble to the `+= 1` bubble; we have established that Thread 2s load
happens-after the `+= 1` side effect, because Thread 2s CAS synchronizes-with happens-after the `+= 1` side effect, because Thread 2s CAS synchronizes-with
Thread 1s store. This both avoids the data race and gives the guarantee that Thread 1s store. This both avoids the data race and gives the guarantee that
`1` will be always read by Thread 2 (as long as locks after Thread 1, of `1` will be always read by Thread 2 (as long as it locks after Thread 1, of
course). course).
However, that is not the only execution of the program possible. Even with this However, that is not the only execution of the program possible. Even with this

@ -87,7 +87,7 @@ For instance, say we convince the compiler to emit this logic:
```text ```text
initial state: x = 0, y = 1 initial state: x = 0, y = 1
THREAD 1 THREAD2 THREAD 1 THREAD 2
y = 3; if x == 1 { y = 3; if x == 1 {
x = 1; y *= 2; x = 1; y *= 2;
} }

@ -24,7 +24,7 @@ The Abstract Machine has a few properties that are essential to understand:
that intentionally produce these executions like [Loom] and [Miri]. that intentionally produce these executions like [Loom] and [Miri].
1. Its model is highly formalized and not representative of what goes on 1. Its model is highly formalized and not representative of what goes on
underneath. Because C++ needs to be defined by a formal specification and underneath. Because C++ needs to be defined by a formal specification and
not just hand-wavy rules about “this is what allowed and this is what not just hand-wavy rules about “this is what is allowed and this is what
isnt”, the Abstract Machine defines things in a very mathematical and, isnt”, the Abstract Machine defines things in a very mathematical and,
well, _abstract_, way; instead of saying things like “the compiler is well, _abstract_, way; instead of saying things like “the compiler is
allowed to do X” it will find a way to define the system such that the allowed to do X” it will find a way to define the system such that the
@ -247,7 +247,7 @@ above the `2`:
Now to sort out the read operation in the middle. We can use the same rule as Now to sort out the read operation in the middle. We can use the same rule as
before to trace up to the first write and rule out us reading either the `0` before to trace up to the first write and rule out us reading either the `0`
value or the garbage that exists between it and `1`, but how to we choose value or the garbage that exists between it and `1`, but how do we choose
between the `1` and the `2`? Well, as it turns out there is a complement to the between the `1` and the `2`? Well, as it turns out there is a complement to the
rule we already defined which gives us the exact answer we need: rule we already defined which gives us the exact answer we need:

@ -279,7 +279,7 @@ two situations:
1. The `SeqCst` operation A synchronizes-with an `Acquire` or `AcqRel` operation 1. The `SeqCst` operation A synchronizes-with an `Acquire` or `AcqRel` operation
B which is sequenced-before another `SeqCst` operation C. Here, despite the B which is sequenced-before another `SeqCst` operation C. Here, despite the
fact that A happens-before C, A does not _strongly_ happen-before C and so is fact that A happens-before C, A does not _strongly_ happen-before C and so is
there not guaranteed to precede C in _S_. not guaranteed to precede C in _S_.
2. The `SeqCst` operation A is sequenced-before the `Release` or `AcqRel` 2. The `SeqCst` operation A is sequenced-before the `Release` or `AcqRel`
operation B, which synchronizes-with another `SeqCst` operation C. Similarly, operation B, which synchronizes-with another `SeqCst` operation C. Similarly,
despite the fact that A happens-before C, A might not precede C in _S_. despite the fact that A happens-before C, A might not precede C in _S_.

Loading…
Cancel
Save