In consume, heap chunk removal is defined in such a way where ordering matters for performance of run-time checks (this is likely not just inherent to the specific heap removal functions, but also the structure of consume itself). For example, consider the symbolic states and specifications to be consumed:
First, acc(y.f) is looked up in the state. Since, it does not exist in the state ? provides acc(y.f) and then all possibly overlapping permissions are removed from the state, e.g. acc(x.f) and p(y). Even though the consume tells us that acc(x.f) is separated from acc(y.f), the verifier does recognize this information, and so the resulting state is ? and a run-time check for acc(y.f) is produced. Then, acc(x.f) is asserted and consumed in the ? state, so a run-time check is produced for acc(x.f) and ? is the resulting state after the consume. To summarize, this consume produces two run-time checks: acc(y.f) and acc(x.f) and results in the ? state after consumption. If the order of acc(y.f) and acc(x.f) is flipped, then only the run-time check for acc(y.f) is created and ? is the resulting state.
Of course, this issue is worse if the run-time check that could be statically discharged with one ordering is a predicate rather than an accessibility predicate. Recursive predicates can be expensive to check at run time, so choosing the wrong ordering of permissions in the spec to be consumed can be costly.
It is possible this can be fixed by leveraging information across the specification to be consumed. This next example can also benefit from such a solution:
state: ? && acc(x.f)
consume: acc(y.f) && x == y
Here, currently, the verifier will produce run-time checks for acc(y.f) and x == y and result in the ? state. Even if the order is changed to x == y && acc(y.f), the result will be the same. This is because information across a consume is asserted individually.
In consume, heap chunk removal is defined in such a way where ordering matters for performance of run-time checks (this is likely not just inherent to the specific heap removal functions, but also the structure of consume itself). For example, consider the symbolic states and specifications to be consumed:
First,
acc(y.f)is looked up in the state. Since, it does not exist in the state?providesacc(y.f)and then all possibly overlapping permissions are removed from the state, e.g.acc(x.f)andp(y). Even though the consume tells us thatacc(x.f)is separated fromacc(y.f), the verifier does recognize this information, and so the resulting state is?and a run-time check foracc(y.f)is produced. Then,acc(x.f)is asserted and consumed in the?state, so a run-time check is produced foracc(x.f)and?is the resulting state after the consume. To summarize, this consume produces two run-time checks:acc(y.f)andacc(x.f)and results in the?state after consumption. If the order ofacc(y.f)andacc(x.f)is flipped, then only the run-time check foracc(y.f)is created and?is the resulting state.Of course, this issue is worse if the run-time check that could be statically discharged with one ordering is a predicate rather than an accessibility predicate. Recursive predicates can be expensive to check at run time, so choosing the wrong ordering of permissions in the spec to be consumed can be costly.
It is possible this can be fixed by leveraging information across the specification to be consumed. This next example can also benefit from such a solution:
Here, currently, the verifier will produce run-time checks for
acc(y.f)andx == yand result in the?state. Even if the order is changed tox == y && acc(y.f), the result will be the same. This is because information across a consume is asserted individually.