llvm dev - Jun 2014 - [LLVMdev] The implementation algorithm behind LLVM's RegionInfo class

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>

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

The draft is pretty clearly written (with some typos that correct
themselves).

I was just thinking if the implementation is only based on empirical
studies of example CFGs, then under what condition it fails. My OpenCL
barrier work right now is mainly using DT and PDT trees (instead of
dominance frontier). But the algorithm looks similar to what was
implemented in regioninfo's findRegionsWithEntry function. I am trying to
understand the connection between the two a bit better so that I can
maximize the re-use of what is already existing in the LLVM. I will keep
you updated with the progress. Thanks.

Best,
Paul


On Fri, Jun 27, 2014 at 3:55 PM, Tobias Grosser <tobias at grosser.es>
wrote:
> 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
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://lists.llvm.org/pipermail/llvm-dev/attachments/20140627/fc7e5146/attachment.html>

On Jun 27, 2014, at 1:55 PM, Tobias Grosser <tobias at grosser.es> wrote:
> 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.
I was looking at this recently since I want to create a MachineRegionPass, which
doesn’t currently exist. Can the existing RegionInfo be refactored to support
MachineBasicBlocks? I went to try doing it it, but then the DominanceFrontier it
depends on has a warning that it’s deprecated. Should I be looking somewhere
else or do I need to create something new (which I really don’t want to do)?

-Matt