A Case for Behavior-Preserving Actions in Separation Logic

Last modified: Thu Dec 13 02:51:08 2012 GMT.

Authors

Abstract

Separation Logic is a widely-used tool that allows for local reasoning about imperative programs with pointers. A straightforward definition of this "local reasoning" is that, whenever a program runs safely on some state, any additional state has no effect on the program's behavior. In the presence of nondeterminism, however, local reasoning must be defined as something more subtle; specifically, additional state is allowed to decrease the amount of nondeterminism of the program. This subtlety causes difficulty in proving various metatheoretical facts about Separation Logic and its variants. Four specific examples are: (1) specifying the behavior of a program on its minimal footprint does not provide a complete specification; (2) data refinement requires a rather unintuitive restriction that the memory used by an abstract module be a subset of the memory used by a concrete module refining the abstract one; (3) Relational Separation Logic requires quite a bit of additional work to prove the frame rule sound; and (4) it is quite tricky to define a model of Separation Logic in which the total domain of memory is finite. In this paper, we show how to cleanly resolve all of these issues by strengthening the definition of local reasoning to eliminate the subtlety. We contend that this solution will also similarly resolve future metatheoretical issues.

Published

Proc. 10th Asian Symposium on Programming Languages and Systems (APLAS'12), Kyoto, Japan, December 2012. Lecture Notes in Computer Science Vol. 7705, pages 332-349. [pdf]

Slides: [pptm]

Extended TR: [pdf]

Coq proofs for theorems of Section 3 ("Impact on a Concrete Separation Logic"): [Coq file] [pdf translation of Coq file] [pdf translation without proofs]

Coq proofs for theorems of Section 4 ("The Abstract Logic"): [Coq file] [translation] [translation without proofs]

colophon