<div dir="ltr">The draft is pretty clearly written (with some typos that correct themselves). <div><br></div><div>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.<div>
<br></div><div>Best,</div><div>Paul</div></div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Fri, Jun 27, 2014 at 3:55 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:43, Paul Vario wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Thanks very much for the quick response. I have read the text many times,<br>
but it was not very clear to me why checking the two conditions involving<br>
dominance frontiers is equivalent to proving the pair {entry, exit} defines<br>
a refined region. I was asking for an mathematical proof really. It sounds<br>
to me like there should be a theorem or two in the graph theory endorsing<br>
it. Or do you mean, the implementation is solely based on empirical<br>
observation instead of theory. The reason I am interested in the<br>
formalization is that I find the current RegionInfo implementation very<br>
helpful in defining regions in between barriers in the OpenCL<br>
implementation on CPU. I haven't found a test case that breaks it. I got<br>
the right intuition, just could not figure out a way to formally prove it,<br>
neither did I find one in your regioninfo draft.<br>
</blockquote>
<br></div>
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?<br>

<br>
Also, please keep me updated with your OpenCL barrier work. This sounds very interesting.<br>
<br>
Cheers,<br>
Tobias<br>
<br>
</blockquote></div><br></div>