[PPL-devel] join-like operation

[Enea Zaffanella]

Hello Piotr.

I am not sure I have fully understood your requirements.
For instance, I am not sure what you mean by "constraints over unshared 
dimensions":
to my eyes, constraint y <= z is binding both shared and unshared 
dimensions.
Please, take all of the following with a grain of salt, as I will write 
as I think, without proper testing of my ideas.

As far as I can tell, your join-like operator is not going to be well 
defined ...

Consider two polyhedra A and B, each one having a single, unshared 
dimension (i.e., no shared dimensions at all).
A is defined by constraint a <= 1, B is defined by constraint b >= 0.
Let's try and define your join-like polyhedron (on dimensions a and b).

One such polyhedron is C_0 defined by { a <= 1, b >= 0 }.
However, for each integer k >= 1, we could take polyhedron C_k defined 
by { a <= 1, b >= 0, a <= b - k + 1}.
Now (modulo silly mistakes on my side) for each C_k we have

   proj_{a}(C_k) = A
   proj_{b}(C_k) = B

i.e., all of the C_k are good candidates as results for your join-like 
operation.
When you have more than one candidate, the smaller the better, right?
So, since C_k is a strict subset of C_{k-1}, C_k is better than C_{k-1}.
The limit of this descending chain of polyhedra is C defined by { a <= 
0, b >= 0 }.
However, this polyhedron does not satisfy the required properties 
(namely, pi_{a}(C) is not a superset of A).

Can you confirm that here above I have not made silly mistakes?

Note: one may say that in the example above C_0 is going to be a better 
candidate since it is not "guessing" new constraints (namely, all its 
constraints occur in the arguments). However, I doubt such a "syntactic" 
way of reasoning would lead to a well defined operator either.

Are there other (implicit?) conditions that would make this operator 
well defined?

Enea.


On 04/25/2017 09:30 AM, Piotr Mardziel wrote:
> Hello PPL developers;
>
> I'm finding myself in need of a particular join-like operation but I'm
> having trouble finding the necessary operations in PPL to make it
> work. I figure that the need for this operation would be common
> especially when implementing inter-procedural program analyses so I'm
> suspicious that I'm just missing the right terminology for it. Let me
> explain this operation:
>
> The setup has two polyhedra that model two sets of program variables
> with some variables shared but some variables not shared. For example:
>
> polyhedron A has the constraint x ≤ y, w = 1
> polyhedron B has the constraint y ≤ z, w = 2
>
> Note that each of those two only has 3 space dimensions but the are
> not intended to represent the same 3 variables, hence I gave them
> names to distinguish them. Thus we see that y and w is shared between
> the two polyhedra, whereas x or z are only represented in A or B
> respectively.
>
> Want I need is to join these two (thus requiring to first expand their
> dimensions to include all 4 dimensions) such that the result is a
> polyhedron C that "effectively" joins shared dimensions but preserves
> constraints over unshared dimensions, in this case I would like
> outcome C to have constraints x ≤ y ≤ z, 1 ≤ w ≤ 2 .
>
> The problem is that to expand each input polyhedron to 4 dimensions,
> one either has to embed or project and then follow it up with either
> join or meet. The join doesn't handle the x,y,z portion of this
> problem correctly whereas meet doesn't handle the w portion correctly.
>
> More technical, I need an operation over A, B to return a C with
>
>          γ(A) ⊆ { π_{x,y,w} (e) | e ∈ γ(C) }
>          γ(B) ⊆ { π_{y,z,w} (e) | e ∈ γ(C) }
>
> Where γ is concretization, and π_{...}(e) is a projection of a tuple e
> to a subset of its dimensions. Top trivially satisfies this
> requirement but the polyhedron {x ≤ y ≤ z, 1 ≤ w ≤ 2} also satisfies
> it and does so much more precisely (is minimal in terms of a
> concretized subset relation).
>
> Am I missing something obvious here? Any help would be greatly appreciated.
>
> Best,
> Piotr (Peter) Mardziel
> _______________________________________________
> PPL-devel mailing list
> PPL-devel at cs.unipr.it
> http://www.cs.unipr.it/mailman/listinfo/ppl-devel