Authors
David Costanzo
Zhong Shao
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