[llvm] [AMDGPU][Doc] GFX12.5 Barrier Execution Model (PR #185632)

[Fabian Ritter via llvm-commits]

================
@@ -6769,117 +6791,147 @@ Execution Barriers
 
 .. note::
 
-  This specification is a work-in-progress (see lines annotated with :sup:`WIP`), and is not complete for GFX12.5.
+  The barrier execution model is experimental and subject to change.
 
 Threads can synchronize execution by performing barrier operations on barrier *objects* as described below:
 
 * Each barrier *object* has the following state:
 
-  * An unsigned positive integer *expected count*: counts the number of *signal* operations
+  * An unsigned positive integer *expected count*: counts the number of *arrive* operations
     expected for this barrier *object*.
-  * An unsigned non-negative integer *signal count*: counts the number of *signal* operations
+  * An unsigned non-negative integer *arrive count*: counts the number of *arrive* operations
     already performed on this barrier *object*.
 
-      * The initial value of *signal count* is zero.
-      * When an operation causes *signal count* to be equal to *expected count*, the barrier is completed,
-        and the *signal count* is reset to zero.
+      * The initial value of *arrive count* is zero.
+      * When an operation causes *arrive count* to be equal to *expected count*, the barrier is completed,
+        and the *arrive count* is reset to zero.
 
+* *Barrier-mutually-exclusive* is a symmetric relation between barrier *objects* that share resources
+  in a way that restricts how a thread can use them at the same time.
 * Barrier operations are performed on barrier *objects*. A barrier operation is a dynamic instance
   of one of the following:
 
-  * Barrier *init*.
-  * Barrier *join*.
-  * Barrier *leave*.
-
-    * Decrements *expected count* of the barrier *object* by one.
-
-  * Barrier *signal*.
-
-    * Increments *signal count* of the barrier *object* by one.
-
-  * Barrier *wait*.
-
-* Barrier modification operations are barrier operations that modify the barrier *object* state:
-
-  * Barrier *init*.
-  * Barrier *leave*.
-  * Barrier *signal*.
-
-* For a given barrier *object* ``BO``:
+  * Barrier *init*
 
-  * There is exactly one barrier *init* for ``BO``. :sup:`WIP`
-  * *Thread-barrier-order<BO>* is the subset of *program-order* that only
-    relates barrier operations performed on ``BO``.
-  * Let ``S`` be the set of barrier modification operations on ``BO``, then
-    *barrier-modification-order<BO>* is a strict total order over ``S``. It is the order
-    in which ``BO`` observes barrier operations that change its state.
+    * Barrier *init* takes an additional unsigned positive integer argument *k*.
+    * Sets the *expected count* of the *barrier object* to *k*.
+    * Resets the *arrive count* of the *barrier object* to zero.
 
-    * *Barrier-modification-order<BO>* is consistent with *happens-before*.
-    * Let ``A`` and ``B`` be two barrier modification operations where ``A -> B`` in
-      *thread-barrier-order<BO>*, then ``A -> B`` in *barrier-modification-order<BO>*.
-    * The first element in *barrier-modification-order<BO>* is a barrier *init*.
-      There is only one barrier *init* in *barrier-modification-order<BO>*.
+  * Barrier *join*.
 
-  * *Barrier-joined-before<BO>* is a strict partial order over barrier operations on ``BO``.
-    A barrier *join* ``J`` is *barrier-joined-before<BO>* a barrier operation ``X`` if and only if all
-    of the following is true:
+    * Allow the thread that executes the operation to *wait* on a barrier *object*.
 
-    * ``J -> X`` in *thread-barrier-order<BO>*.
-    * There is no barrier *leave* ``L`` where ``J -> L -> X`` in *thread-barrier-order<BO>*.
+  * Barrier *drop*.
 
-  * *Barrier-participates-in<BO>* is a partial order that relates barrier operations to barrier *waits*.
-    A barrier operation ``X`` may *barrier-participates-in<BO>* a barrier *wait* ``W`` if all of the following
-    is true:
+    * Decrements *expected count* of the barrier *object* by one.
 
-    * ``X`` and ``W`` are both performed on ``BO``.
-    * ``X`` is a barrier *signal* or *leave* operation.
-    * ``X`` does not *barrier-participates-in<BO>* another barrier *wait* ``W'`` in the same thread as ``W``.
-    * ``W -> X`` **not** in *thread-barrier-order<BO>*.
+  * Barrier *arrive*.
 
-  * *Barrier-participates-in<BO>* is consistent with *happens-before*.
+    * Increments the *arrive count* of the barrier *object* by one.
+    * If supported, an additional argument to  *arrive* can also update the *expected count* of the
+      barrier *object* before the *arrive count* is incremented;
+      the new *expected count* cannot be less than or equal to the *arrive count*,
+      otherwise the behavior is undefined.
 
-* Let ``S`` be the set of barrier operations that *barrier-participate-in<BO>* a barrier *wait* ``W`` for some
-  barrier *object* ``BO``, then all of the following is true:
+  * Barrier *wait*.
 
-  * ``S`` cannot be empty.
-  * The elements of ``S`` all exist in a continuous interval of *barrier-modification-order<BO>*.
-  * Let ``A`` be the first operation of ``S`` in *barrier-modification-order<BO>*, then the *signal count* of ``BO``
-    is zero before ``A`` is performed.
-  * Let ``B`` be the last operation of ``S`` in *barrier-modification-order<BO>*, then the *signal count* and
-    *expected count* of ``BO`` are equal after ``B`` is performed. ``B`` is the only barrier operation in ``S``
-    that causes the *signal count* and *expected count* of ``BO`` to be equal.
+    * Introduces execution dependencies between threads; this operation depends on
+      other barrier operations to complete.
 
-* For every barrier *signal* ``S`` performed on a barrier *object* ``BO``:
+* Barrier modification operations are barrier operations that modify the barrier *object* state:
 
-  * The immediate successor of ``S`` in *thread-barrier-order<BO>* is a barrier *wait*. :sup:`WIP`
+  * Barrier *init*.
+  * Barrier *drop*.
+  * Barrier *arrive*.
+
+* *Thread-barrier-order<BO>* is the subset of *program-order* that only
+  relates barrier operations performed on a barrier *object* ``BO``.
+* All barrier modification operations on a barrier *object* ``BO`` occur in a strict total order called
+  *barrier-modification-order<BO>*; It is the order in which ``BO`` observes barrier
+  operations that change its state. For any valid *barrier-modification-order<BO>*, the
+  following must be true:
+
+  * Let ``A`` and ``B`` be two barrier modification operations where ``A -> B`` in
+    *thread-barrier-order<BO>*, then ``A -> B`` is also in *barrier-modification-order<BO>*.
+  * The first element in *barrier-modification-order<BO>* is always a barrier *init*, otherwise
+    the behavior is undefined.
+
+* *barrier-participates-in* relates barrier operations to the barrier *waits* that depend on them
+  to complete. A barrier operation ``X`` *barrier-participates-in* a barrier *wait* ``W``
+  if and only if all of the following is true:
+
+  * ``X`` and ``W`` are both performed on the same barrier *object* ``BO``.
+  * ``X`` is a barrier *arrive* or *drop* operation.
+  * ``X`` does not *barrier-participate-in* another distinct barrier *wait* ``W'`` in the same thread as ``W``.
+  * ``W -> X`` not in *thread-barrier-order<BO>*.
+  * All dependent constraint and relations are satisfied as well. [0]_
+
+* For the set ``S`` consisting of all barrier operations that *barrier-participate-in* a barrier *wait* ``W`` for some
+  barrier *object* ``BO``:
+
+  * The elements of ``S`` all exist in a continuous, uninterrupted interval of *barrier-modification-order<BO>*.
+  * The *arrive count* of ``BO`` is zero before the first operation of ``S`` in *barrier-modification-order<BO>*.
+  * The *arrive count* and *expected count* of ``BO`` are equal after the last operation of ``S`` in
+    *barrier-modification-order<BO>*. The *arrive count* and *expected count* of ``BO`` cannot
+    equal at any other point in ``S``.
+
+* A barrier *join* ``J`` is *barrier-joined-before* a barrier operation ``X`` if and only if all
+  of the following is true:
+
+  * ``J -> X`` in *thread-barrier-order<BO>*.
+  * ``X`` is not a barrier *join*.
+  * There is no barrier *join* or *drop* ``JD`` where ``J -> JD -> X`` in *thread-barrier-order<BO>*.
+  * There is no barrier *join* ``J'`` on a distinct barrier *object* ``BO'`` such that ``J -> J' -> X`` in
+    *program-order*, and ``BO`` *barrier-mutually-exclusive* ``BO'``.
+
+* A barrier operation ``A`` *barrier-executes-before* another barrier operation ``B`` if any of the
+  following is true:
+
+  * ``A -> B`` in *program-order*.
+  * ``A -> B`` in *barrier-participates-in*.
+  * ``A`` *barrier-executes-before* some barrier operation ``X``, and ``X``
+    *barrier-executes-before* ``B``.
+
+* *Barrier-executes-before* is consistent with *barrier-modification-order<BO>*
+  for every barrier object ``BO``.
+* For every barrier *drop* ``D`` performed on a barrier *object* ``BO``:
+
+  * There is a barrier *join* ``J`` such that ``J -> D`` in *barrier-joined-before*;
+    otherwise, the behavior is undefined.
+  * ``D`` cannot cause the *expected count* of ``BO`` to become negative; otherwise, the behavior is undefined.
+
+* For every pair of barrier *arrive* ``A`` and barrier *drop* ``D`` performed on a barrier *object*
+  ``BO``, such that ``A -> D`` in *thread-barrier-order<BO>*, one of the following must be true:
+
+  * ``A`` does not *barrier-participates-in* any barrier *wait*.
+  * ``A`` *barrier-participates-in* at least one barrier *wait* ``W``
+    such that  ``W -> D`` in *barrier-executes-before*.
 
 * For every barrier *wait* ``W`` performed on a barrier *object* ``BO``:
 
-  * There is a barrier *join* ``J`` such that ``J -> W`` in *barrier-joined-before<BO>*. :sup:`WIP`
-
-* For every barrier *join* ``J`` performed on a barrier *object* ``BO``:
-
-  * ``J`` is not *barrier-joined-before<BO>* another barrier *join*.
-
-* *Barrier-executes-before* is a strict partial order defined over the union of all barrier operations
-  performed by all threads on all barriers. It is the transitive closure of all the following orders:
+  * There is a barrier *join* ``J`` such that ``J -> W`` in *barrier-joined-before*, and
+    ``J`` must *barrier-executes-before* at least one operation ``X`` that
+    *barrier-participates-in* ``W``; otherwise, the behavior is undefined.
 
-  * *Thread-barrier-order<BO>* for every barrier object ``BO``.
-  * *Barrier-participates-in<BO>* for every barrier object ``BO``.
+* *barrier-phase-with* is a symmetric relation over barrier operations defined as the
+  transitive closure of: *barrier-participates-in* and its inverse relation.
+* For every barrier operation ``A`` that *barrier-participates-in* a barrier *wait* ``W`` on a barrier *object* ``BO``:
 
-* *Barrier-executes-before* is consistent with *program-order*.
-* For every barrier *object* ``BO``:
+  * There is no barrier operation ``X`` on ``BO`` such that ``A -> X -> B`` in
----------------
ritter-x2a wrote:

What's `B`? Should that be `W`?

https://github.com/llvm/llvm-project/pull/185632