| Issue 70: | Field permission is lost when method argument contains method call | |
| 2 people starred this issue and may be notified of changes. | Back to list |
This issue was originally reported by Daniel. When a method body under
analysis contains a method call on a field, arguments to that method call
that contain methods calls themselves can cause Plural to discard
permission to the field even when not necessary. Take for example the
following code:
@Share(use=Use.FIELDS, guarantee="Initialized")
public void sendRemove(...) {
//...
TwineAdvertisement lastAd = adManager.getAdByNameRec(nr.getID());
//...
}
where the class whose method contains this code has the following
invariant:
@State(name="Initialized", inv="share(adManager)")
Plural fails with a an error:
[SyncOrSwim]: argument this must be in state [alive] but is in [] and
argument this must have permissions [SHARE in [alive]] but it has NOTHING
What we have discovered is that when the method call (the argument) forces
a pack of the receiver, the permission to all fields is removed, which is
correct. The share permission should stay with the TEMP variable that was
the target of the load. Instead, the alias analysis says that the field and
the TEMP are the same, and removes any permission associated with it.
Jul 23, 2009
Project Member
#1
nels.bec...@gmail.com
Labels:
-Priority-Medium Priority-High
Jul 26, 2009
The issue only comes up because the receiver permission is a share, right? That's why Plural blows away the
field permissions, to simulate the possibility that the field value may have changed as a result of the method
call.
Interestingly, the problem here comes from Plural's insistence on following the execution order:
1. The outer field dereference is evaluated (with an unpack) ("adManager")
2. The argument (which forces a pack) ("nr.getId")
2. The outer method call ("getAdByNameRec")
Which is a bit counter-intuitive, but unfortunately correct: The "adManager" field value found *before* the
inner method call will be used for making the outer call.
*Solution A*
One solution we discussed was to combine Plural and the alias analysis into one analysis (right now Plural
runs the alias analysis separately). That way, the temp and the field could be correctly disentangled (meaning
set to point to different locations) before blowing away the field permissions. The temp should then still have
permissions, which can be used to satisfy the pre-condition of the subsequent method call.
Unfortunately, this solution promises to be quite a bit of work. In addition, it's somewhat risky, as it may be
tricky to get the aliasing analysis exactly right inside Plural. On the other hand, I think it's possible that all
that needs to be done is inlining the (usually one-liner) aliasing transfer function code into the respective
Plural transfer function methods at the right point. That would have the additional advantage that we may not
have to worry about using the "before" or "after" aliasing results any more, like we currently have to.
*Solution B*
Another possibility may be to somehow tell the alias analysis where it needs to decouple fields and temps. In
the simple case that is easy: every method call decouples, and the alias analysis can find these places by
itself. But in the current Plural implementation, we only decouple when share or pure permissions for the
receiver are available. Unfortunately, this optimization is vital in many cases. It's not clear how to feed this
information to the alias analysis, since Plural is the very analysis that determines what permissions are
available where, so there seems to be a circular dependency here. That's why we're back to solution A,
integrating the two into one.
Jul 27, 2009
Re: the evaluation order, yes it's true that this is how it's evaluated. I checked out the spec just to be sure! It seems like integrating the two is one way to accomplish this correctly, and really it might not be that much work, although it would make our already-complicated transfers functions even more so. However, it seems like from a conceptual standpoint that the opposite of Solution B might actually be the correct one. A standard, sound alias analysis must always assume that temps & fields have been separated after a method call. If we did that, then PLURAL could have a wrapper around it that would then (somehow...) reestablish the link between temps & fields when appropriate. Frankly this issue is really annoying but there is a workaround that is simple enough that I have a feeling this will not get fixed any time soon. :-( |