Exhaling and Inhaling in Boogie

May 31, 2012 at 2:11 PM
Edited May 31, 2012 at 2:20 PM

From what I understand, during a method call, the callee inhales the pre-condition from the caller, and exhales the post-condition back to the caller after the method has executed. The exhale/inhale includes transfer of access permissions.

I have two implementation-related questions in this regard:

  1. What exactly is the role of the temporary variables exhale_mask and inhale_heap in the Boogie encoding?
  2. Consider the translation from a higher level language (call it HL) into Boogie. Then what constraints must HL satisfy in order for us to have a Boogie encoding that only needs to use a single (global) heap variable and a single (global) mask variable? In other words, how "simple" must HL be in order for us to get away with a global heap and mask, and hence not have to worry about temporary heap and mask variables during the exhale/inhale phases?

Please also point me to related resources that address these topics.

Thanks in advance for your advice!

Oct 17, 2012 at 12:35 AM

The exhale_mask and inhale_heap variables are used in the encoding of the Exhale and Inhale operations.  They temporarily store the value of the old or new mask or heap.  The general issue is this:  To exhale an "acc(y)", the encoding needs to do:

assert Mask[this, y] == 100;  // I'm writing "100" to denote full permission here
Mask[this, y] := 0;  // and I'm writing 0 to denote no permission

If a later conjunct mentions "y" and this reference were to be checked to have the appropriate permission (i.e., that the specification is well-formed), the encoding would do:

assert Mask[this, y] > 0;

but this check would fail if the Mask has been updated to 0.  So, instead, a temporary variable is used, so that both the original Mask and the updated Mask can be used.

What I described in the general idea, but it isn't actually how things are done.  The well-formedness check is done by a separate Inhale operation.  Moreover, there have been some recent changes that change the "havoc" operation to take place during Exhale rather than during Inhale (as in the first implementation of Chalice).  In any case, perhaps what I said give you a sense of why you might want to have temporary variables like exhale_mask and inhale_heap.

For other HLs and verifiers, there are many variations of the encodings that you can use.  I'm afraid I don't know how to answer your question any better than that.

To learn more about Inhale and Exhale, I suggest reading:

K. Rustan M. Leino and Peter Müller. A basis for verifying multi-threaded programs. In ESOP 2009, volume 5502 of LNCS, pages 378-393. Springer 2009. [PDF]

For some design improvements and some newer details, see:

Stefan Heule, K. Rustan M. Leino, Peter Müller, and Alexander J. Summers. Fractional permissions without the fractions.  It has just been accepted to VMCAI 2013.