Technical reports

A separation logic framework for HOL

Thomas Tuerk

June 2011, 271 pages

This technical report is based on a dissertation submitted December 2010 by the author for the degree of Doctor of Philosophy to the University of Cambridge, Downing College.

DOI: 10.48456/tr-799

Abstract

Separation logic is an extension of Hoare logic due to O’Hearn and Reynolds. It was designed for reasoning about mutable data structures. Because separation logic supports local reasoning, it scales better than classical Hoare logic and can easily be used to reason about concurrency. There are automated separation logic tools as well as several formalisations in interactive theorem provers. Typically, the automated separation logic tools are able to reason about shallow properties of large programs. They usually consider just the shape of data structures, not their data-content. The formalisations inside theorem provers can be used to prove interesting, deep properties. However, they typically lack automation. Another shortcoming is that there are a lot of slightly different separation logics. For each programming language and each interesting property a new kind of separation logic seems to be invented.

In this thesis, a general framework for separation logic is developed inside the HOL4 theorem prover. This framework is based on Abstract Separation Logic, an abstract, high level variant of separation logic. Abstract Separation Logic is a general separation logic such that many other separation logics can be based on it. This framework is instantiatiated in a first step to support a stack with read and write permissions following ideas of Parkinson, Bornat and Calcagno. Finally, the framework is further instantiated to build a separation logic tool called Holfoot. It is similar to the tool Smallfoot, but extends it from reasoning about shape properties to fully functional specifications.

To my knowledge this work presents the first formalisation of Abstract Separation Logic inside a theorem prover. By building Holfoot on top of this formalisation, I could demonstrate that Abstract Separation Logic can be used as a basis for realistic separation logic tools. Moreover, this work demonstrates that it is feasable to implement such separation logic tools inside a theorem prover. Holfoot is highly automated. It can verify Smallfoot examples automatically inside HOL4. Moreover, Holfoot can use the full power of HOL4. This allows Holfoot to verify fully functional specifications. Simple fully functional specifications can be handled automatically using HOL4’s tools and libraries or external SMT solvers. More complicated ones can be handled using interactive proofs inside HOL4. In contrast, most other separation logic tools can reason just about the shape of data structures. Others reason only about data properties that can be solved using SMT solvers.

Full text

PDF (2.4 MB)

BibTeX record

@TechReport{UCAM-CL-TR-799,
  author =	 {Tuerk, Thomas},
  title = 	 {{A separation logic framework for HOL}},
  year = 	 2011,
  month = 	 jun,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-799.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-799},
  number = 	 {UCAM-CL-TR-799}
}