Octagon Closure on Half Matrix Form
Hello,
After reading a few of the papers on the PPL improvments to the Octagon domain, I have a question on reasoning about the equivalence between the half-matrix and full-matrix strong closure algorithms.
Looking at the function `strong_closure_assign()` in `Octagonal_Shape_templates.hh` my understanding is that it computes the strong closure on the triangular (half) matrix twice. So, for each of the k = 0..n steps it visits each cell in the half-matrix twice which is the same as, in the full matrix, visiting each cell and its coherent-cell.
Is my understanding correct? I am trying to reason about parallelizing some of the Octagon algorithms.
Thanks a bunch, Markus
Hello Markus.
I am not sure I would have described the algorithm exactly the way you did, but anyway I think that your understanding is basically correct.
The algorithm starts by computing shortest-path closure; strong closure is achieved at the end, by a step of strong coherence.
In order to compute shortest-path closure it performs the 3 nested loops twice, as you noticed, because in each row of the triangular matrix we have j <= i, as said in this comment:
// Since the index `j' of the inner loop will go from 0 up to `i', // the three nested loops have to be executed twice.
Hence, doing things twice is meant to be equivalent to considering (by coherence) also i < j <= 2n in a usual (square) matrix.
Hope my "rephrasing" is helpful.
Regards, Enea.
On 01/23/2016 01:12 AM, Markus Kusano wrote:
Hello,
After reading a few of the papers on the PPL improvments to the Octagon domain, I have a question on reasoning about the equivalence between the half-matrix and full-matrix strong closure algorithms.
Looking at the function `strong_closure_assign()` in `Octagonal_Shape_templates.hh` my understanding is that it computes the strong closure on the triangular (half) matrix twice. So, for each of the k = 0..n steps it visits each cell in the half-matrix twice which is the same as, in the full matrix, visiting each cell and its coherent-cell.
Is my understanding correct? I am trying to reason about parallelizing some of the Octagon algorithms.
Thanks a bunch, Markus _______________________________________________ PPL-devel mailing list PPL-devel@cs.unipr.it http://www.cs.unipr.it/mailman/listinfo/ppl-devel
Hi Enea,
Thanks for taking the time to go over that: I understand now.
Have a nice day, Markus
On Mon, Jan 25, 2016 at 7:03 PM, Enea Zaffanella zaffanella@cs.unipr.it wrote:
Hello Markus.
I am not sure I would have described the algorithm exactly the way you did, but anyway I think that your understanding is basically correct.
The algorithm starts by computing shortest-path closure; strong closure is achieved at the end, by a step of strong coherence.
In order to compute shortest-path closure it performs the 3 nested loops twice, as you noticed, because in each row of the triangular matrix we have j <= i, as said in this comment:
// Since the index `j' of the inner loop will go from 0 up to `i', // the three nested loops have to be executed twice.
Hence, doing things twice is meant to be equivalent to considering (by coherence) also i < j <= 2n in a usual (square) matrix.
Hope my "rephrasing" is helpful.
Regards, Enea.
On 01/23/2016 01:12 AM, Markus Kusano wrote:
Hello,
After reading a few of the papers on the PPL improvments to the Octagon domain, I have a question on reasoning about the equivalence between the half-matrix and full-matrix strong closure algorithms.
Looking at the function `strong_closure_assign()` in `Octagonal_Shape_templates.hh` my understanding is that it computes the strong closure on the triangular (half) matrix twice. So, for each of the k = 0..n steps it visits each cell in the half-matrix twice which is the same as, in the full matrix, visiting each cell and its coherent-cell.
Is my understanding correct? I am trying to reason about parallelizing some of the Octagon algorithms.
Thanks a bunch, Markus _______________________________________________ PPL-devel mailing list PPL-devel@cs.unipr.it http://www.cs.unipr.it/mailman/listinfo/ppl-devel
PPL-devel mailing list PPL-devel@cs.unipr.it http://www.cs.unipr.it/mailman/listinfo/ppl-devel
participants (2)
-
Enea Zaffanella -
Markus Kusano