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

[Fabian Ritter via llvm-commits]

================
@@ -6950,121 +6975,233 @@ Informally, we can deduce from the above formal model that execution barriers be
 * *Barrier-executes-before* relates the dynamic instances of operations from different threads together.
   For example, if ``A -> B`` in *barrier-executes-before*, then the execution of ``A`` must complete
   before the execution of ``B`` can complete.
-* When a barrier *signal* or *leave* causes the *signal count* of a barrier *object* to be identical to the
-  *expected count*, the *signal count* is reset to zero, and threads that have *joined* the barrier *object*
-  will:
 
-  * Wake-up if they were sleeping because of a barrier *wait*, **or**
-  * Skip the next barrier *wait* operation if they have not previously *waited*.
+  * This property can also be combined with *program-order*. For example, let two (non-barrier) operations
+    ``X`` and ``Y`` where ``X -> A`` and ``B -> Y`` in *program-order*, then we know that the execution
+    of ``X`` completes before the execution of ``Y`` does.
 
 * Barriers do not complete "out-of-thin-air"; a barrier *wait* ``W`` cannot depend on a barrier operation
   ``X`` to complete if ``W -> X`` in *barrier-executes-before*.
-* It is undefined behavior to operate on an uninitialized barrier.
+* It is undefined behavior to operate on an uninitialized barrier object.
 * It is undefined behavior for a barrier *wait* to never complete.
+* It is not mandatory to *drop* a barrier after *joining* it. The operations are not opposites; *drop*
+  affects future barrier operations by decrementing the *expected count* of the barrier *object*, which
+  can only be undone by re-*initializing* the barrier.
----------------
ritter-x2a wrote:

Or by an `arrive`? Or does that count as re-initializing?

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