Encoding of spatial conjunction in Boogie

Mar 25, 2012 at 2:00 PM
Edited Mar 25, 2012 at 2:00 PM

How is the concept of the spatial conjunction (also known as the "star operator") from separation logic encoded in Boogie?

For example, suppose I have the following assertion in a language like Chalice:

assert c1.x == 1 && c2.x == 2

where c1,c2 are instances of some class, x is an attribute of that class, and the star operator is written as &&.

When this is translated to Boogie, how does Boogie specify that c1.x == 1 and c2.x == 2 must hold in two separate heaps (or two separate parts of a larger heap)?

Apr 5, 2012 at 3:19 AM

Chalice makes use of access predicates to achieve what separation logic uses separating conjunction as.  The condition you wrote above says nothing about whether or not c1 and c2 are equal (well, actually it does, since you equated the two respective x fields with 1 and 2; this implies that c1 and c2 are different).

If you want to say that c1.x and c2.x live in separate heaps, you would write:  acc(c1.x) && acc(c2.x).  Roughly speaking, you can think of && in Chalice as separating conjunction and think of the separation-logic "points to" relation

    c.x |-> _

as acc(c.x).

Chalice "evaluates" (that is, interprets) expressions use the two semantic transformations "inhale" and "exhale".  I refer you to the paper:  "A basis for verifying multi-threaded programs" by Leino and Müller, ESOP 2009.  For more of a comparison between Chalice and separation logic, I refer you to "Relationship between Separation Logic and Implicit Dynamic Frames" by Parkinson and Summers, ESOP 2011.

Apr 5, 2012 at 11:51 AM

Thanks Rustan. Based on what you have said, I have written the following assertion in Chalice:

assert acc(c1.x) && acc(c2.x) && c1.x == 3 && c2.x == 5;

Now, the acc's should say that c1.x and c2.x hold in separate heaps. But when I look at the auto-generated Boogie output file, I get the following code snippet for the above assertion:

// assert
  Heap#_42 := Heap;
  Mask#_43 := Mask;
  Credits#_44 := Credits;

  // begin exhale (assert)
  exhaleMask#_45 := Mask#_43;

  //checking whether c1.x == 3 holds...

  assert {:msg "  21.44: Receiver might be null."} true ==> (c1#2 != null);
  assert {:msg "  21.44: Location might not be readable."} true ==> CanRead(Mask#_43, c1#2, C.x);
  assert {:msg "  21.5: Assertion might not hold. The expression at 21.44 might not evaluate to true."} Heap#_42[c1#2, C.x] == 3;

  //checking whether c1.x == 3 holds...

  assert {:msg "  21.60: Receiver might be null."} true ==> (c2#4 != null);
  assert {:msg "  21.60: Location might not be readable."} true ==> CanRead(Mask#_43, c2#4, C.x);
  assert {:msg "  21.5: Assertion might not hold. The expression at 21.60 might not evaluate to true."} Heap#_42[c2#4, C.x] == 5;

  then there is some more code checking whether acc(c1.x) and acc(c2.x) holds...
  // end exhale

From this it would appear that Boogie performs look-ups on the same heap variable (in this case, Heap#_42).

So how exactly does Boogie represent heap separation, in the translation from Chalice to Boogie? Is the separation implicit in the heap look-up?

Apr 5, 2012 at 8:31 PM

There is only one heap, just like there's just one heap when the program executes.  But an activation record (like a method) only has access to certain parts of the heap.  Access to the heap is tracked by the Mask (which I think Peter and I wrote as a caligraphic P in our paper).

What does "holding in separate heaps" really mean?  It means that you could partition the memory in such a way that the two memory locations (in your example, c1.x and c2.x) are placed in different partitions.  The inhale and exhale operations, which operate on the Mask, make sure of that.  But the values stored in the various memory locations are all modeled in the Boogie variable called Heap.

Again, Peter's and my ESOP 2009 paper attempts to describes these things.  In Chalice, you don't really think of things as being "separate heaps", even though you can take that viewpoint as well.  To get the usual Chalice mindset, I recommend the Chalice tutorial:  "Verification of concurrent programs in Chalice", by Leino, Müller, and Smans (lecture notes from FOSAD 2009).  You can find it from the Chalice page, http://research.microsoft.com/en-us/projects/chalice/.