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.