## 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:

- 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.
- 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.
- 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.
- 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

- 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. - Hongseok Yang and Peter W. O'Hearn. A Semantic Basis for Local Reasoning.
*Proc. of FOSSACS'02*. Lecture Notes in Computer Science, Springer, 2002. - 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 - Local Reasoning and Separation Logic.