Task Description for M.Sc. Thesis

Author. Murat Baktiev
Time frame. June 2006 - November 2006
Advisor. Jan Schwinghammer
Responsible professor. Gert Smolka

Permutation Semantics of Separation Logic

Context.

Separation Logic extends traditional Hoare Logic with assertions that describe the heap using the separation conjunction p∗q. This provides an elegant mechanism to formalise sharing properties in the heap. For instance, the assertion x→e∗x→e' is true for heaps that consist of two distinct cells, pointed to by x and y, respectively, and implies that the program variables x and y cannot be aliased. The separation conjunction opens the way to local reasoning about programs by means of a frame rule: for a proved program {p}c{q} it is possible to add invariants r for heap regions that are inaccessible for the program, to derive {p∗r}c{q∗r}.

Soundness of this reasoning principle relies on tracking computations on extended heaps (described by assertion p∗r) by those on the part described by p. Finding a corresponding computation sequence raises a subtle point in connection with dynamic memory allocation: The choice of a fresh location may well be different after extending a heap. This difficulty has traditionally been solved by modelling allocation by non-determinism.Here, we want to take a different approach and make explicit that computations in fact remain the same when extending the initial heap, up to the choice of fresh locations.

Task description.

The thesis shall develop the semantics of Separation Logic in the case where memory allocation follows a deterministic strategy, rather than abstracting this by (excessive) non-determinism. Beginning our investigation with a small While-language, the eventual goal is to extend the results to more expressive languages. Concretely, this work involves the following tasks:

  1. Formalising the operational semantics of a small While-language with dynamic allocation and deallocation of memory. A crucial aspect is to define the action of a permutation of location names on heaps and programs.
  2. We expect the semantics developed in part 1 to satisfy a permutation theorem: Running a consistently renamed program on a correspondingly renamed heap leads to the same result, up to a renaming of locations in the final heap. The formal statement and proof of this theorem will be a first central contribution of this thesis.
  3. The next task is to design a separation logic (Reynolds, 2002; Yang & O'Hearn 2002), and define the semantics of assertions. They will have to be invariant under location permutations, in a suitable sense. A proof of this property, in combination with the permutation theorem, will then be used to prove soundness of the logic: Provable Hoare triples are semantically valid.
  4. Depending on time, we want to evaluate the approach and investigate if it scales to more expressive languages. Candidates are extensions with procedures or shared-variable concurrency (e.g., O'Hearn 2004).

Some references

  1. John C. Reynolds. Separation Logic: A logic for shared mutable data structures. Pages 55-74. of Proc. 17th Symposium on Logic in Computer Science. IEEE Computer Society, 2002.
  2. Hongseok Yang and Peter W. O'Hearn. A Semantic Basis for Local Reasoning. Proc. of FOSSACS'02. Lecture Notes in Computer Science, Springer, 2002.
  3. Peter W. O'Hearn. Resources, Concurrency and Local Reasoning. Pages 4967 of Proc. CONCUR'04 vol. 3170 of Lecture Notes in Computer Science, Springer, 2004
  4. Local Reasoning and Separation Logic.