Rely-Guarantee Reasoning in Whiley

[DavePearce]

This relates to RFC#0008 "Static Variables" and should become an RFC which extends it

Rely-Guarantee reasoning is an important paradigm for reasoning about concurrent computation (see history). An interesting question is how it could be implemented in Whiley. For the purposes of this discussion, we'll assume that Whiley has static variables which support a volatile (or similar) modifier.

A typical verification task might look like this:

type nat is (int x) where x >= 0

volatile nat counter = 0

method broken(nat amount)
modifies counter:
    // (1)
    counter = counter + amount
    // (2)
    counter = counter - amount

In order to verify this program, we can only assume that the invariant holds any time the shared global variable is accessed. Thus, the above program is broken. This is because, at the second statement, we can only assume that counter >= 0 and not that counter >= amount.

In order to implement the above, we need the verification condition generation to version volatile variables differently from regular global variables.

[DavePearce]

(see also #45 and #31)

[DavePearce]

See also this paper:

• Owicki-Gried for Reasoning for C11 RAR