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

[Paul Vario]

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.

Thanks,
Paul


On Fri, Jun 27, 2014 at 3:25 PM, Tobias Grosser <tobias at grosser.es> wrote:

> On 27/06/2014 22:04, Paul Vario wrote:
>
>> Hi Tobi,
>>
>>         I have one additional question about the RegionInfo::isRegion
>> function. In the second case (i.e. Entry dominates Exit),  why is checking
>> the following two conditions are equivalent to checking it's a refined
>> region:
>>
>> For any BB in DF(exit), 1)  BB should be in DF(entry)
>>                                     2)  BB reachable only from entry
>> through
>> a path passing exit.
>>
>>         I.e., why is checking these two conditions is equivalent to ensure
>> single-entry, single-exit in the sense of Refined Region.
>>
>
> I tried to formalize this in section 3.1 of the paper I sent you (but
> did not look into this since almost four years), (no bug reports yet,
> despite regular use at least in Polly).
>
> Here the old text:
>
> If Entry dominates Exit, than Exit is not element of
> the dominance frontier of Entry. Every BB ∈ DF ( Exit ) will be element
> of the domi- nance frontier of Entry. So there are two conditions to
> check. First only basic blocks that are part of the dominance frontier
> of Exit are allowed to be element of the dominance frontier of Entry.
> And furthermore it has to be shown that these basic blocks can only be
> reached from Entry through a path passing Exit. To show this the
> derivedDomFrontier() function is used.  derivedDomFrontier ( BB, Entry,
> Exit ) checks if there exists a path from Entry to BB that does not pass
> Exit. This is done by checkng for every predecessor of BB, that if it
> is dominated by Entry it is also dominated by Exit.  It has still to be
> shown that there are no edges entering the region.  As all basic blocks
> are dominated by Entry the only case where edges enter the region is if
> Exit is dominated by Entry and has back edges pointing into the region.
> These back edges will point to basic blocks dominated by Entry but not
> by Exit. So the dominance frontier of Exit is not allowed to contain any
> basic blocks that are dominated by Entry.
>
> The code in lib/Analysis/RegionInfo.cpp matches this description almost
> one-to-one with the only change that derivedDomFrontier was renamed to
> isCommonDomFrontier().
>
> Did you read this text? Does it make sense to you? It is not a nicely
> written mathematical proof but may give an intuition.
>
> Out of interest, why are you interested in the formalization of the
> RegionInfo pass? Do you happen to have a test case where it is
> incorrect?
>
> Thanks,
> Tobias
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/llvm-dev/attachments/20140627/f64befe8/attachment.html>