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

Thu Mar 12 02:20:33 PDT 2026

================
@@ -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:
 
     * ``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-participates-in<BO>* is consistent with *happens-before*.
+    * ``X`` is a barrier *arrive* or *drop* operation.
+    * ``X`` does not already *barrier-participate-in<BO>* a 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]_
 
 * 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 *object* ``BO``, then all of the following is true.
 
-  * ``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``
+  * Let ``A`` be the first operation of ``S`` in *barrier-modification-order<BO>*, then the *arrive 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
+  * Let ``B`` be the last operation of ``S`` in *barrier-modification-order<BO>*, then the *arrive 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.
+    that causes the *arrive count* and *expected count* of ``BO`` to be equal.
+
+* 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*.
+  * For some barrier *object* ``BO``, ``A-> B`` in *barrier-participates-in<BO>*.
+  * ``A`` *barrier-executes-before* some barrier operation ``X``, and ``X``
+    *barrier-executes-before* ``B``.
 
-* For every barrier *signal* ``S`` performed on a barrier *object* ``BO``:
+* *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``:
 
-  * The immediate successor of ``S`` in *thread-barrier-order<BO>* is a barrier *wait*. :sup:`WIP`
+  * 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-ordered<BO>*, one of the following must be true:
+
+  * If ``A`` does not *barrier-participates-in<BO>* any barrier *wait*.
+  * ``A`` *barrier-participates-in<BO>* 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`
+  * There is at least one barrier operation that *barrier-participates-in<BO>* ``W``.
+  * There is a barrier *join* ``J`` such that ``J -> W`` in *barrier-joined-before*.
+  * ``J`` must *barrier-executes-before<BO>* at least one operation ``X`` that
+    *barrier-participates-in<BO>* ``W``; otherwise, the behavior is undefined.
 
 * For every barrier *join* ``J`` performed on a barrier *object* ``BO``:
 
-  * ``J`` is not *barrier-joined-before<BO>* another barrier *join*.
+  * ``J`` is not *barrier-joined-before* another barrier *join*.
----------------
ssahasra wrote:

The definition of `barrier-joined-before` says that the right hand side is not a *join*. So this is trivially satisfied. Clearly not what the intention is.

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