My favorites | Sign in
Project Home Wiki Issues Source
READ-ONLY: This project has been archived. For more information see this post.
Search
for
  Advanced search   Search tips   Subscriptions
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
 
Project Member Reported by nels.bec...@gmail.com, Jul 22, 2009
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
(No comment was entered for this change.)
Labels: -Priority-Medium Priority-High
Jul 26, 2009
Project Member #2 kevin.bi...@gmail.com
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
Project Member #3 nels.bec...@gmail.com
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. :-(

Powered by Google Project Hosting