From 3c76e35449b9b6c765c4e08016a610c3bfa65781 Mon Sep 17 00:00:00 2001 From: SabrinaJewson Date: Sun, 28 Aug 2022 22:18:47 +0100 Subject: [PATCH] Add a more formal explanation of happens-before --- src/atomics/acquire-release.md | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/atomics/acquire-release.md b/src/atomics/acquire-release.md index 77c4ac7..ef630a3 100644 --- a/src/atomics/acquire-release.md +++ b/src/atomics/acquire-release.md @@ -210,6 +210,13 @@ possible execution, Thread 1’s `store` synchronizes-with Thread 2’s `load`, which causes that `store` and everything sequenced before it to happen-before the `load` and everything sequenced after it. +> More formally, we can say that A happens-before B if any of the following +> conditions are true: +> 1. A is sequenced-before B (i.e. A occurs before B on the same thread) +> 2. A synchronizes-with B (i.e. A is a `Release` operation and B is an +> `Acquire` operation that reads the value written by A) +> 3. A happens-before X, and X happens-before B (transitivity) + There is one more rule required for these to be useful, and that is _release sequences_: after a release store is performed on an atomic, happens-before arrows will connect together each subsequent value of the atomic as long as the