[LLVMdev] The implementation algorithm behind LLVM's RegionInfo class

[Tobias Grosser]

On 27/06/2014 22:43, Paul Vario wrote:
> Thanks very much for the quick response. I have read the text many times,
> but it was not very clear to me why checking the two conditions involving
> dominance frontiers is equivalent to proving the pair {entry, exit} defines
> a refined region. I was asking for an mathematical proof really. It sounds
> to me like there should be a theorem or two in the graph theory endorsing
> it. Or do you mean, the implementation is solely based on empirical
> observation instead of theory. The reason I am interested in the
> formalization is that I find the current RegionInfo implementation very
> helpful in defining regions in between barriers in the OpenCL
> implementation on CPU. I haven't found a test case that breaks it. I got
> the right intuition, just could not figure out a way to formally prove it,
> neither did I find one in your regioninfo draft.

The code was written as a student project during my masters and I never 
got around to write a paper or a formal mathematical proof. I believe 
the description should give an intuition for the prove, but I am 
currently a little too loaded to do it myself. Obviously, I would be 
interested in any kind of further formalisation. Is there a specific 
part of the description that is unclear to you and that would allow you 
to possibly develop a proof?

Also, please keep me updated with your OpenCL barrier work. This sounds 
very interesting.

Cheers,
Tobias