[PPL-devel] Octagon Closure on Half Matrix Form

[Enea Zaffanella]

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 at cs.unipr.it
> http://www.cs.unipr.it/mailman/listinfo/ppl-devel
>