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

[Sameer Sahasrabuddhe via llvm-commits]

================
@@ -6767,117 +6789,155 @@ 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 represents barrier
+  *objects* that share resources in a way that prevents a thread from using 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 *init*
+
+    * 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 *join*.
-  * Barrier *leave*.
+  * Barrier *drop*.
 
     * Decrements *expected count* of the barrier *object* by one.
 
-  * Barrier *signal*.
+  * Barrier *arrive*.
 
-    * Increments *signal count* of the barrier *object* by one.
+    * Increments the *arrive count* of the barrier *object* by one.
+    * Depending on the implementation, *arrive* can also update the *expected count* of the
+      barrier *object* before the *arrive count* is incremented;
+      the new *expected count* can never be less than or equal to the *arrive count*,
+      otherwise the behavior is undefined.
 
   * Barrier *wait*.
 
 * Barrier modification operations are barrier operations that modify the barrier *object* state:
 
   * Barrier *init*.
-  * Barrier *leave*.
-  * Barrier *signal*.
+  * Barrier *drop*.
+  * Barrier *arrive*.
 
-* For a given barrier *object* ``BO``:
+* For a given barrier *object* ``BO``, the following relations exist in any
+  valid program execution:
 
-  * 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.
+  * All barrier modification operations on ``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:
 
-    * *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-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:
+      *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.
 
-    * ``J -> X`` in *thread-barrier-order<BO>*.
-    * There is no barrier *leave* ``L`` where ``J -> L -> X`` in *thread-barrier-order<BO>*.
-
-  * *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:
+  * *Barrier-participates-in<BO>* relates barrier operations to the barrier *waits* that depend on them
+    to complete. A barrier operation ``X`` may *barrier-participates-in<BO>* a barrier *wait* ``W``
+    if and only if all of the following is true:
----------------
ssahasra wrote:

"wait" operation has not been defined yet. Its definition needs to spell out how it "depends" on other operations, to "complete".

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