Conversation
| ensures acc(parent.Mem(), definitions.ReadL20) | ||
| ensures acc(child.Mem(), definitions.ReadL20) | ||
|
|
||
| WithCancel(parent Context) (child Context, cancel CancelFunc) |
There was a problem hiding this comment.
the comment/question in the function WithValue about child and parent possibly being aliased also applies here. Here however, I would fix the spec but comment the function until we have a closure implementation, otherwise Gobra will complain about a missing definition for CancelFunc
There was a problem hiding this comment.
As stated, the function WithCancel, WithDeadline, and WithTimeout are currently commented out due to unsupported closures. But the conversation at #30 (comment) still applies to the Parent-Child context relationships.
| // --- | ||
|
|
||
| requires acc(parent.Mem(), definitions.ReadL20) | ||
|
|
||
| ensures acc(parent.Mem(), definitions.ReadL20) | ||
| ensures acc(child.Mem(), definitions.ReadL20) | ||
|
|
||
| WithDeadline(parent Context, d time.Time) (child Context, cancel CancelFunc) |
There was a problem hiding this comment.
same comments as for WithCancel and WithValue
| ensures acc(parent.Mem(), definitions.ReadL20) | ||
| ensures acc(child.Mem(), definitions.ReadL20) | ||
|
|
||
| WithTimeout(parent Context, timeout time.Duration) (child Context, cancel CancelFunc) |
There was a problem hiding this comment.
Same question as for WithValue and the other similar functions
|
|
||
| // --- | ||
|
|
||
| // XXX! used frequently but not in the router |
There was a problem hiding this comment.
Is it used in some dependency of the router?
…he postcondition for Err.
…l permission due to potential aliasing. Giving up child permissions should grant you parent permission again with a magic wand.
| preserves acc(Mem(), definitions.ReadL20) | ||
| requires acc(key.Mem(), _) | ||
| requires isComparable(key) | ||
| ensures acc(key.Mem(), _) |
There was a problem hiding this comment.
This is not necessary: the precondition requires acc(key.Mem(), _) causes a positive amount of permissions (less than the caller holds) to be transferred to the callee, which implies that the caller always retains acc(key.Mem(), _) - as such, no need to transfer them back
| requires acc(val.Mem(), _) | ||
| ensures child.Mem() | ||
| ensures child.Mem() --* parent.Mem() | ||
| ensures acc(val.Mem(), _) |
| or interface. | ||
| */ | ||
|
|
||
| preserves acc(parent.Mem(), definitions.ReadL20) |
There was a problem hiding this comment.
Hmm maybe we do not need to provide full permission to both parent and child - maybe, any positive permission amount p is good enough, as long as it is the same for parent and child and as long as the magic wand is changed to use that fraction on both side. Nonetheless, my intuition for requiring full permission is that you shouldn't access directly a Context that is an internal Context of another - you should only do this after knowing that the outermost Context is no longer used. I would keep it as it is and change in the future if we require a more expressive contract
| preserves acc(Mem(), definitions.ReadL20) | ||
| ensures isClosed ==> c.Closed() | ||
| ensures (!isClosed && c != nil) ==> | ||
| acc(c.RecvChannel(), definitions.ReadL20) |
There was a problem hiding this comment.
a very subtle point that I just noticed is that c.RecvChannel() is not duplicable. More than that, c1.RecvChannel() together with c2.RecvChannel() implies that c1 and c2 must be different
There was a problem hiding this comment.
Would simply using a wildcard permission satisfy this unsoundness on line 38?
Here is the initial outline of the specification of the context package. There are still things to be changed and some main questions lie in the following areas:
Should the
Donemethod be labeled aspure? The downside is we cannot introduce the ghost return value indicating whether or not the channel was previously closed. The specification for the returned channel also needs to be refined but I am ignoring that for now.The
Errmethod internally obtains and releases a mutex. A Context is safe to pass to multiple goroutines and from the view of the caller, could in theory only require read access to theMempredicate. The question here is if that is actually sound.The
Valuemethod (and consequentlyWithValuefunction) currently requires that thekeybe a primitive type. However, according to the Go docs using a primitive type should be avoided and in the Scion project, the keys are only used with a new type declaration similar to the below snippet. Thus, enforcing a primitive type will not work.WithDeadline,WithTimeout, andWithCancelall return a cancel function. We would need support for closures in order to specify this (I think). What I am most unsure about is, that calling this function should release all resources held by the context but this effect would also change the return values of the methods Err, and Done.