Resource Reasoning and Labelled Separation Logic

This thesis develops resource reasoning with separation logic in the areas of modular program specification, program optimization, and concurrency verification for heap-manipulating programs.

In the first part, we investigate the resources that are required for modular and complete program specifications. Since the safety footprints of a program (the resources required for safe execution) do not always yield complete specifications, we first characterize the notion of the relevance footprint. We show that the relevance footprints are the only elements essential for a complete specification, and also identify the conditions for sufficiency. We then introduce a novel semantic model of heaps which establishes the correspondence between safety and relevance footprints, and we identify a general condition that guarantees this correspondence in arbitrary resource models.

In the second part, we present labelled separation logic for introducing optimizations such as automatic parallelization in heap manipulating programs. In order to detect dependences between distant statements in a program, we annotate spatial conjuncts in separation logic formulae with the labels of accessing commands, and propagate these labels through program proofs. We also identify the notion of ‘allocation dependences’ which, in addition to standard stack and heap dependences, are needed to ensure the safety of optimizations.

In the final part, we address the analysis of resource ownership transfers in concurrent programs, and present an algorithm for automating concurrent separation logic proofs. This is based on a form of labelled separation logic in which ownership constraints are tracked through a proof and ownership is inferred from heap accesses at arbitrary program points. Unlike previous methods, the algorithm presented here does not require user annotations about ownership distribution, and we demonstrate how it can verify programs that could not be handled by previous methods.