[PATCH] D26348: Allow convergent attribute for function arguments

[Nicolai Hähnle via Phabricator via llvm-commits]

nhaehnle added inline comments.


================
Comment at: docs/LangRef.rst:1147
+    In some parallel execution models, there exist operations with one or more
+    arguments that must be uniform across threads. Such arguments are called
+    ``convergent``.
----------------
hfinkel wrote:
> nhaehnle wrote:
> > mehdi_amini wrote:
> > > `uniform` isn't defined in the LangRef.
> > Right, this is also used in the paragraph below. This whole paragraph isn't intended to be normative, but to provide context that allows one to understand the actual condition. Perhaps this could be phrased better. What about:
> > 
> > "In some parallel execution models, there exist operations that are executed simultaneously for multiple threads, and one or more arguments of the operation must have the same value across all simultaneously executing threads."
> I think that would be better. I still find the current text in this paragraph and the next confusing because understanding them hinges on understanding the term `uniform` which we never define.
Okay, that's what the current version says.


================
Comment at: docs/LangRef.rst:1164
+    Two executions e1 and e2 of a function are compatible (with respect to
+    convergent function arguments) if for every call site CS to a function with
+    a convergent argument, the sequences e1(CS) and e2(CS) of values supplied
----------------
hfinkel wrote:
> So, the clarify, we need to ensure compatibility between all call sites with a convergent argument, or all call sites with a convergent argument to the same function, or all call sites with a convergent argument subject to some other condition?
I hope we're not talking past each other, but for the definition of compatibility, each call site is considered separately.

Compatibility is a property of a pair of executions; it is satisfied if a certain property is satisfied at each call site to a function with convergent arguments.

When one proves that a transformation preserves compatibility, one would look at each call-site in the transformed code, and prove the property based on the fact that it was satisfied at some call-site in the original code, but the definition of compatibility itself is never concerned with the interaction or relationship of multiple call sites to each other.


https://reviews.llvm.org/D26348