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

[Pierre van Houtryve 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
----------------
Pierre-vh wrote:

Done

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