Algebraische Kalküle für Separationslogik

• Antragsteller: Professor Dr. Bernhard Möller
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2011 bis 2015
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 188417285

• Erstellungsjahr: 2017

Zusammenfassung der Projektergebnisse

Extending standard Hoare logic, Separation Logic (SL) introduces spatial assertions for reasoning about portions of computer memory and assertions about concurrent programs. The separating conjunction P ∗ Q holds in a given state if the memory there can be split into disjoint parts that satisfy the assertions P and Q, resp. A central tool is the frame rule {P } Q {R} ⇒ {P ∗S } Q { R∗S}. Once statement Q has been shown correct w.r.t. precondition P and postcondition R, the proof remains valid when a disjoint portion of memory satisfying S is added to P and R; a side condition is that the free variables of S must not be changed by Q. An analogous concurrency rule holds in the encompassing setting of concurrent SL. A main project result was an algebraic model of this in terms of semirings and Kleene algebras. Further abstraction from syntactic details allowed simplifications in the presentation and proofs of the original SL inference rules as well as of more general new ones. A big advantage of the abstraction is that the laws are generally applicable and do not depend on the particular storage model used; hence they can be instantiated for a variety of SL applications. Additional research yielded abstract and fully point-free axiomatisations of frequently used special assertion classes in SL that are characterised by simple (in-)equational laws. To validate the approach, the theory has been applied to quite non-trivial data structures with pointers, such as threaded trees or doubly-linked lists, and corresponding algorithms. A second main project theme concerned the extension of SL to concurrent settings, in particular to Concurrent Kleene Algebra (CKA). In the original CKA model the meaning of a program is the set of its possible traces, and every such trace is a graph with events as vertices and the (causal/spatial/temporal) dependences between them as edges. The basic operators are sequential and concurrent composition ; and | (in early papers also denoted ∗ for its similarity to separating conjunction) of event-disjoint components. They need to satisfy the fundamental exchange law (P | Q) ; (R | S) ≤ (P ; R) | (Q ; S), where ≤ roughly means that the left hand side is more sequential than the right hand side. In the project several further semantic models of CKA have been developed. Moreover, a theory of abstraction operators allows replacing program components by their interfaces while preserving the fundamental laws. This can be used to effect selective hiding of internal events. A connecting investigation concerned a simple relational semantics of sequential SL. Although this does not yield a CKA, since the exchange law fails, under certain restrictions it satisfies a dual, reverse exchange law with the converse order ≥ and still admits reasonable variants of the concurrency and frame rules. Moreover, contrary to the original CKA model, relations offer a non-trivial test algebra allowing a simple and intuitive model of assertions. Another structure with the reverse exchange law has been formed by an algebraic semantics for Petri nets. There separating conjunction reflects splitting and combining of markings. A variety of useful and frequently applied inference rules have been derived; their usability has been shown in a standard mutex example with algebraic proofs of safety and liveness.

Projektbezogene Publikationen (Auswahl)

• Concurrency and local reasoning under reverse exchange. Science of Computer Programming, 85:204-223, 2014
  H.-H. Dang and B. Möller
  
• Developments in Concurrent Kleene Algebra. In P. Hofner, P. Jipsen, W. Kahl and M. E. Müller (eds.): Relational and Algebraic Methods in Computer Science (RAMiCS 2014), LNCS 8428. Springer 2014, 1–18
  C.A.R. Hoare, S. van Staden, B. Möller, G. Struth, J. Villard, H. Zhu and P. O’Hearn
  
• Exploring Modal Worlds. J. Log. Algebr. Meth. Program. 83(2):135–153, 2014
  H.-H. Dang, R. Glück, B. Möller, P. Roocks, A. Zelend
  
• In P. Höfner, P. Jipsen, W. Kahl and M. E. Müller (eds.): Relational and Algebraic Methods in Computer Science (RAMiCS 2014), LNCS 8428. Springer 2014, 157–172
  Han-Hing Dang: Abstract Dynamic Frames
  
• Exploring an Interface Model for CKA. In R. Hinze, J. Voigtlander (eds.): Mathematics of Program Construction (MPC 2015). LNCS 2129. Springer 2015, 1–29
  B. Möller, C.A.R Hoare
  
• Extended transitive separation logic. J. Log. Algebr. Meth. Program. 84(3): 303–325 (2015)
  H.-H. Dang, Bernhard Möller
  
• Modal algebra and Petri nets. Acta Informatica 52(2-3):109-132 (2015)
  H.-H. Dang, B. Möller
  
• Developments in Concurrent Kleene Algebra. J. Log. Algebr. Meth. Program. 85(4): 617–636 (2016)
  C.A.R. Hoare, S. van Staden, B. Möller, G. Struth, H. Zhu
  
• A Discrete Geometric Model of Concurrent Program Execution. In J. Bowen, H. Zhu (eds.): Unifying Theories of Programming — 6th International Symposium, UTP, Reykjavik, Iceland, June 4–5, 2016, Revised Selected Papers. LNCS 10134. Springer 2017, 1–25
  B. Möller, C.A.R Hoare, M. Müller, G. Struth