<div dir="ltr">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. <div>
<br></div><div>Thanks,</div><div>Paul</div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Fri, Jun 27, 2014 at 3:25 PM, Tobias Grosser <span dir="ltr"><<a href="mailto:tobias@grosser.es" target="_blank">tobias@grosser.es</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="">On 27/06/2014 22:04, Paul Vario wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Hi Tobi,<br>
<br>
        I have one additional question about the RegionInfo::isRegion<br>
function. In the second case (i.e. Entry dominates Exit),  why is checking<br>
the following two conditions are equivalent to checking it's a refined<br>
region:<br>
<br>
For any BB in DF(exit), 1)  BB should be in DF(entry)<br>
                                    2)  BB reachable only from entry through<br>
a path passing exit.<br>
<br>
        I.e., why is checking these two conditions is equivalent to ensure<br>
single-entry, single-exit in the sense of Refined Region.<br>
</blockquote>
<br></div>
I tried to formalize this in section 3.1 of the paper I sent you (but<br>
did not look into this since almost four years), (no bug reports yet,<br>
despite regular use at least in Polly).<br>
<br>
Here the old text:<br>
<br>
If Entry dominates Exit, than Exit is not element of<br>
the dominance frontier of Entry. Every BB ∈ DF ( Exit ) will be element<br>
of the domi- nance frontier of Entry. So there are two conditions to<br>
check. First only basic blocks that are part of the dominance frontier<br>
of Exit are allowed to be element of the dominance frontier of Entry.<br>
And furthermore it has to be shown that these basic blocks can only be<br>
reached from Entry through a path passing Exit. To show this the<br>
derivedDomFrontier() function is used.  derivedDomFrontier ( BB, Entry,<br>
Exit ) checks if there exists a path from Entry to BB that does not pass<br>
Exit. This is done by checkng for every predecessor of BB, that if it<br>
is dominated by Entry it is also dominated by Exit.  It has still to be<br>
shown that there are no edges entering the region.  As all basic blocks<br>
are dominated by Entry the only case where edges enter the region is if<br>
Exit is dominated by Entry and has back edges pointing into the region.<br>
These back edges will point to basic blocks dominated by Entry but not<br>
by Exit. So the dominance frontier of Exit is not allowed to contain any<br>
basic blocks that are dominated by Entry.<br>
<br>
The code in lib/Analysis/RegionInfo.cpp matches this description almost<br>
one-to-one with the only change that derivedDomFrontier was renamed to<br>
isCommonDomFrontier().<br>
<br>
Did you read this text? Does it make sense to you? It is not a nicely<br>
written mathematical proof but may give an intuition.<br>
<br>
Out of interest, why are you interested in the formalization of the<br>
RegionInfo pass? Do you happen to have a test case where it is<br>
incorrect?<br>
<br>
Thanks,<br>
Tobias<br>
</blockquote></div><br></div>