Multi-phase exhaling of permissions

[viper-admin]

Created by @mschwerhoff on 2013-05-25 12:20
Last updated on 2016-04-15 11:59

The multi-phase exhaling as described in the permission paper by Heule, Summers et al. is not yet implemented in Silicon. This results, for example, in the unsoundness exhibited by the unexpectedly sucessful test case t2b in Sil:all/basic/fresh.sil.

[viper-admin]

@mschwerhoff on 2014-02-13 07:28:

• changed component from (none) to Permissions

[viper-admin]

@mueller55 on 2014-10-13 15:20:

• changed the assignee from @mschwerhoff to (none)

[viper-admin]

@alexanderjsummers commented on 2015-03-16 16:39

See issues/silicon/0030.sil

[viper-admin]

@mschwerhoff commented on 2016-02-25 11:21

See also #35

[viper-admin]

@mschwerhoff commented on 2016-02-25 11:23

Here is a short example illustrating an incompleteness and an unsoundness resulting from not supporting constraining blocks properly:

#!text

field map: Int

method test1(state: Ref)
  requires acc(state.map)
{
	var q: Perm
  inhale none < q

  constraining(q) {
    exhale acc(state.map, q) && acc(state.map, 1/2) // Fails, but should not
  }
}

method test2(state: Ref)
  requires acc(state.map)
{
	var q: Perm
  inhale none < q && q < write

  constraining(q) {
    exhale acc(state.map, write-q) && acc(state.map, q) // Unsoundly handled
  }
  
  assert false // Holds, but should not
}

[viper-admin]

Bitbucket user fhahn commented on 2016-04-15 11:59

I've found another example that may show a related problem. When using constraining, calling test3 fails, because there are insufficient permission to access P(r). Without constraining, Silicon manages to verify the example.

#!scala

predicate P(self: Ref) { true }

method test1(a: Ref, p: Perm) returns (res: Ref)
    requires p > none && p < write
    requires acc(P(a), p)
    ensures acc(P(res), p)
{
    assume false
}

method test3(r: Ref)
    requires acc(P(r))
{}

method test2()
{
    var r: Ref
    var p: Perm
    fresh p

    inhale acc(P(r), 1/2)

    constraining (p) { r := test1(r, p) }
    //r := test1(r, 1/2)

    inhale acc(P(r), write-perm(P(r)))

    assert perm(P(r)) == write
    test3(r)
}

[gauravpartha]

In a recent Viper meeting, we decided to stop the multi-phase exhale for Carbon. From now on Viper backends should always execute exhales from left to right. Carbon has been updated correspondingly (viperproject/carbon#411) and the Silver test suite as well (viperproject/silver#573)

@mschwerhoff: So, I guess we can close this issue?

[mschwerhoff]

@gauravpartha I'm happily closing this issue :-)