[llvm] [RFC][Uniformity] add proof section uniformity is safe to use across transforms (PR #170628)

[Nicolai Hähnle via llvm-commits]

================
@@ -713,3 +713,310 @@ relation over dynamic instances and a :ref:`controlled m-converged
 <controlled_m_converged>` property of static instances. The :ref:`uniformity
 analysis <uniformity-analysis>` implemented in LLVM includes this for targets
 that support convergence control tokens.
+
+Preservation of Uniformity at Use
+=================================
+
+Introduction
+------------
+
+In execution of a program, the outputs produced by two converged dynamic
+instances of a static instance are *uniform* if they compare equal; 
+otherwise, *divergent*. In any given program, uniformity is determined 
+through static analysis, which depends on the current state of the program’s 
+control flow. During execution, a transformation may alter the original 
+structure of the program, potentially leading to a change in control flow.
+
+When a group of threads executes the same program in parallel, the program's 
+control flow determines which subset of threads will execute any given static 
+instance. With the change in control flow, it is possible that the new set of 
+threads reaching a static instance includes some threads that did not previously 
+execute it.
+
+Although the original set of threads continues to execute the same static 
+instance, the inclusion of these additional threads may change the 
+classification. This means that during execution, a static instance marked 
+as *uniform* by the analysis may be marked as *divergent* after a transformation
+that changes the control flow of the original program.
+
+However, our proof in this document demonstrates that this conservative 
+classification does not impact the uniformity of "the original subset of threads"
+that executed the static instance in the original program.
+
+In this document, we have defined a set of observable :ref:`fundamental properties<convergence-valid-transform>`
+in any program that are essential for a transformation to be considered valid. 
+Building on these properties, our proof demonstrates that any valid 
+transformation preserves "the uniformity of each value at its use". That is, for 
+a given program *P* and a valid transformation *R* resulting in a transformed 
+program *P'*, any assumptions about uniformity built into *P'* are preserved in
+*P''*.
+
+Concepts
+--------
+
+**Static instance**
+
+Each occurrence of an instruction or a constant literal in the program source 
+is called a *static instance*.
+
+**Dynamic instance**
+
+When a thread executes a program, each execution of a static instance produces 
+a distinct *dynamic instance* of that instruction. The dynamic instance of
+a constant literal is simply its value.
+
+Both terms, *static instance* and *dynamic instance*, match the definitions 
+used in the LLVM specification of  :ref:`convergence and uniformity<convergence-dynamic-instances>`.
----------------
nhaehnle wrote:

This is redundant. Make sure your text actually integrates with the rest of the document that you're editing. Just link to the "Threads and Dynamic Instances" section if you need to.

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