Created by @mschwerhoff on 2015-12-28 20:12
Last updated on 2016-01-06 17:22
Regular Permissions
Consider the following functions:
#!text
function fun01(x: Ref, y: Ref, b: Bool): Int
requires b ? acc(x.f) : acc(y.f)
function fun02(x: Ref, y: Ref, b: Bool): Int
requires acc(x.f, b ? write : none)
requires acc(y.f, !b ? write : none)
The footprint/frame/snapshot of fun01 is tight, i.e. it only consists of x.f or y.f, depending on b. Hence, assigning to, e.g. y.f does not interfere with fun01(x, y, true) == old(fun01(x, y, true)).
In contrast, the footprint/frame/snapshot of fun02 is not tight, i.e. it consists of x.f and y.f. Hence, assigning to, e.g. y.f does prevent fun02(x, y, true) == old(fun02(x, y, true)) from verifying.
Quantified Permissions
A similar situation arises with quantified permissions:
#!text
function fun01(xs: Seq[Ref], i: Int): Int
requires 0 <= i && i < |xs|
requires forall j: Int :: 0 <= j && j < |xs| && j == i ==> acc(xs[j].f, write)
function fun02(xs: Seq[Ref], i: Int): Int
requires 0 <= i && i < |xs|
requires forall j: Int :: 0 <= j && j < |xs| ==> acc(xs[j].f, j == i ? write : none)
Analogous to the situation above, assigning to xs[1].f does not interfere with framing fun01(xs, 0), but it does interfere with fun02(xs, 0).
Comments
- Carbon exhibits the same issue (for regular permissions)
- For QPs, it should be possible to overcome the issue by narrowing down the domain definition from the condition c(x) to the conditionalised permission expression c(x) ? p(x) : none
Attachments:
Regular Permissions
Consider the following functions:
The footprint/frame/snapshot of
fun01is tight, i.e. it only consists ofx.fory.f, depending onb. Hence, assigning to, e.g.y.fdoes not interfere withfun01(x, y, true) == old(fun01(x, y, true)).In contrast, the footprint/frame/snapshot of
fun02is not tight, i.e. it consists ofx.fandy.f. Hence, assigning to, e.g.y.fdoes preventfun02(x, y, true) == old(fun02(x, y, true))from verifying.Quantified Permissions
A similar situation arises with quantified permissions:
Analogous to the situation above, assigning to
xs[1].fdoes not interfere with framingfun01(xs, 0), but it does interfere withfun02(xs, 0).Comments
Attachments:
tighter_fvf_domains.diff