In the write-up, we are comparing how Separation Logic (abbreviated as SL) and Dynamic Frames Theory (abbreviated as DFT) tackle the frame problem. This turned to be a non-trivial, but quite useful exercise, at least, for me.
One problem is that the DFT is not explicit about some of its foundations, so we need to recover details. Another problem is that terminology differs and variable, state, value and address refer to somewhat different notions. Third, underlying logics used to express framing specification are different too.
So, we first clarify the problem, unify terminology and then discuss differences and similarities in tackling the frame problem.
The approaches of DFT and SL to tackle the frame problem are quite similar: one adds necessary annotations (framing specification
s) and use them to prove absence of aliasing.
However, terminology and details differ significantly. In order to unify approaches, we have developed a simple model of how absence of aliasing can be proved. We will use the model (its terminology and proof principle) to compare the DFT and the SL.
The details are described in a separate document. But here is a rough idea of how this works:
effect
of a mutator
footprint
of a (pure) expression
effect
and the footprint
are disjoint
mutator
has no effect on the expression
expression
value can be re-used in the new memory stateThere is an inconsistency in how frame
and framing
is used in literature, which may confuse a reader. Basically, the idea is to determine a memory region, which can be accessed by a piece of computation (i.e. read, write, allocate of de-allocate). And then state that any access to the rest of (allocated) memory is independent of the computation. So, there are two complimentary regions and frame
(and framing
) can be used to refer to both.
That was one of the reason to introduce footprint
and effect
instead of frame
. However, framing specification
is not confusing, since if one defines a region, then it's complement is implicitly defined too.
The DFT paper seems to use frame
to refer to a region which is accessed by a piece of computation. For example,
The modification is satisfied by every computation that only touches region
f
or at most allocates new memory.
Here f
is a dynamic frame
. In the write-up parlance, frame
refers to effect
of a computation here.
Another example is "f
frames v
" condition:
In a state in which this condition is true, we say that
f
framesv
or thatf
is a frame forv
. When that happens,v
depends only on locations inf
, i.e. leaving those locations untouched preserves the value ofv
.
In the write-up parlance, this describes a footprint
of a variable (which is an expression in the DFT).
However, occasionally the DFT paper uses term frame
inconsistent with the rest of the paper, e.g.
When specifying a piece of computation, we should also specify its frame, i.e. the part of the state that it operates upon.
There is also inconsistency of frame
usage among other texts. For example, the frame problem wiki page uses frame
to refer to what is unchanged:
In the logical context, actions are typically specified by what they change, with the implicit assumption that everything else (the frame) remains unchanged.
Another example is a Separation Logic
article in Communications of the ACM, which also uses frame
to refer to the untouched memory, e.g. Figure 3.
Dafny reference manual uses framing expressions
:
Frame expressions are used to denote the set of memory locations that a Dafny program element may read or write.
However, as we noted above regarding frame specification
s, such use doesn't introduce confusion, since by defining a set, we implicitly define its complement.
A most prominent difference is that the DFT stems from Object-Oriented Refinement paradigm, while SL is a low-level imperative paradigm equipped with Hoare triples with assertions about heap.
Thus, it's difficult to compare two approaches directly. They are however complimentary in some sense and can be even combined (e.g. Implicit Dynamic Frames).
In the context of the frame problem, it directly impacts the form how framing conditions are specified. The DFT supports encapsulation and refinement, which means a specification and its refinements (implementations) are separate entities (called modules
in DFT). The DFT is more expressive in the sense than vanilla SL.
In the semantics of SL's operations, a computation is aborted, if it tries to access an unallocated address. A precondition can contain assertions about heap, which can certify that some locations are allocated. In the sense, SL's preconditions serve as permissions (or capabilities) to access heap locations.
As the assertions about locations are explicit (of the form ), one is able to prove that a code accesses only allocated locations.
We assume that a program is split in a set of code units. In the DFT that can be methods, functions or expressions, in the SL it's commands C
of Hoare-triples {P} C {Q}
.
In the DFT, there is a common heap memory for all code units. That means that generally a code unit can affect any other code unit - in the sense, the DFT implies "global" reasoning.
In the SL, a well-specified code (which doesn't lead to abort
state) should access only the locations of heap, which existence is explicitly stated in its precondition (of the form , i.e. there is a heap cell at address with content ). It thus has the only way to affect other code units: via its effective heap after execution, which is described in its post-condition. Similarly, dependencies (or footprint) of the code are described in its pre-condition. The reasoning is thus "local" as we can concentrate only on the footprint
and effect
.
However, such "local" reasoning can be emulated in the DFT too: one can specify for each code unit its footprint and its effect ("f
frames v
" and "modifies v
" constructs). At the same time, "global" reasoning is more flexible, e.g. one can re-use dynamic frames for several operations or construct a new one from other dynamic frames.
SL supports low-level features, like pointer arithmetics and memory de-allocation, which are absent in the DFT. Explicit heap permissions make it straightforward to prove that a piece of code is well-specified in respect to heap access (i.e. doesn't try to dereference a non-allocated location).
Due to "global" reasoning, it can be more difficult to add pointer arithmetics and de-allocation to the DFT. Basically, when one tries to de-reference an expression, one should prove that it's an allocated address, i.e. in the DFT's parlance. When the only way to obtain a location value is to allocate something, then the location value acts as a permission to access it.
It's not so, when one can construct location values using pointer arithmetics or de-allocation is possible. One obviously has to prove that a location points to an allocated address every time a location is accessed. It can be implemented using dynamic frames, but effect
specifications should be made more expressible, to specify that a code unit can shrink its footprint
.
Besides different paradigms, there are differences in type systems, memory models and underlying logics, which are used to express statements about computations and prove them. Some differences are minor (and perhaps introduced to simplify the narrative), while others are more significant.
Memory model differ rather significantly among the DFT and SL. However, most of the differences stem from the paradigmatic differences and their intended usages: it looks like the SL is simplified to make it easier to reason about its properties.
A more practical version of SL will likely make its type system more expressive (which is also discussed in the SL paper).
As discussed out, it's perhaps difficult to introduce de-allocation in the DFT. However, as it stems from Object-Oriented paradigm, which typically assumes garbage collection, it doesn't seem to be a severe restriction.
Both DFT and SL assume an infinite set of memory locations (SL uses address
where DFT uses location
), however, sets of used or allocated locations are finite. Actually, an address
in (a flavor of) SL is an infinite integer, which allows using pointer arithmetics in SL, while locations
are unordered in DFT.
Locations are mapped to value
s in both cases. However, value
s in SL are very simple compared to value
s in DFT, i.e. they are just infinite integers. Whereas in DFT, value
s include at least integers, locations and sets.
The difference is not significant, as there can be (and are) flavors of SL with richer type systems (it's discussed in the SL paper too). It's likely that the type system in the SL paper is simplified to make it easier to reasoning about SL properties.
Memory model is more uniform in DFT: a state
is a finite mapping from location
s into value
s. Whereas is SL, state consists of store
and heap
. The latter is a finite mapping from address
es to value
s, i.e. the same concept as the state
in DFT. The former is a finite mapping from variable
s to value
s.
De-allocation of heap locations is possible in SL, while it's absent in DFT.
Variables in SL are quite distinct from variables in DFT. Actually, DFT uses specification variable
which is an expression, depending on the state
(corresponds to a pure function with state
as a parameter).
DFT also defines a program variable
, which is a special case of specification variable
, the values of the program variable
being the content of the state
at the constant address of the variable.
A variable
in SL corresponds to a program variable
in DFT, however, it's kept in a store
and is not subject to aliasing, as they are not addressable. SL uses variables from its predicate calculus as a rough analogue of DFT's specification variable
s.
Expressions in SL don't depend on heap
, only on store
. However, as mentioned before, in SL there are explicit assertions about heap
of form . And if one wants to safely read a location, it's existence should be stated in a pre-condition. Thus, possibility to access heap
in expressions is not really required, at least in case of pre-conditions.
In other cases, one can add a read operation, e.g.
Both DFT and SL allows expressing framing specification
s, however, their underlying logics are quite different.
The logic in DFT is sets-based. A dynamic frame
in DFT is a kind of specification variable
, which value is a set of allocated locations. A dynamic frame
can be constructed using set comprehensions and set operations. There seems to be two main framing specification
s in DFT:
f
- a computation preserves allocated locations other than f
(effect
)f
frames v - variable v
is framed by f
, in the sense that preserving f
preserves the value of v
(footprint
)SL employs "inductive definition of predicates on abstract data structures", i.e. a form of inductive types (though there are intuitionistic and classic SL flavors) together with separating conjunction
, which are used to specify pre- and post-conditions for a computation. Such pre- and post-conditions explicitly split the entire heap
in disjoint rejoins down to singleton (cell) and empty heaps.
DFT uses explicit disjointness
predicate, which can be assumed, asserted and/or proved. In SL, heap assertions are constructed in "disjoint-less" manner. Of course, there still arise proof conditions, i.e. if one states , heap fragment disjointness implies , and are addresses of heap cells.
Here we illustrate how DFT and SL approach the frame problem. The key problem is to be able to prove that an update of a location preserves content of another syntactically different location, e.g. in the SL case. Then, if there are several such facts involved in consequent reasoning, one need to construct such proofs for all of them. See A model to prove absence of aliasing for details.
Let's assume there is a spec variable a
and we want to prove that a modification of a program variable b
doesn't affect a
and we can reuse its value in the new state after update.
One can specify a dynamic frame
f
for a
: "f
frames a
". One also specifies that the effect of the update to b
: " b = x modifies g". If there is an evidence that "disjoint[f;g]", one can concude that a
and b
are independent, i.e.
.
In the simple case, when a
or b
are program variables, corresponding dynamic frames comprise addresses of them, i.e. and . In the case of a complex type, its dynamic frame can be constructed from dynamic frames of components, since a dynamic frame is a particular case of a specification variable.
Let's assume, there is a Hoare-tuple {P} C {Q} and we want to append a write: { b -> _ } [b] = x { b -> x}
. Q
may contain facts about heap, which can be invalidated by such write.
Actually, in SL we do not necessary to prove absence of aliasing explicitly, one just needs to construct a new post-condition for the combined program. This includes both aliasing and non-aliasing cases. In the latter we want to prove we can simply include Q
in the new post-condition, while in the former, we want an updated version of it.
let's assume that a predicate allocated(b, Q)
means that assertion Q
contains a singleton assertion . And !allocated(b, Q)
means there is no such singleton.
If there is aliasing that means alloc(b, Q)
, so there is for some and . We can thus construct new Q'
by substituting with .
That means !alloc(b, Q)
. We want to apply the SL's frame rule. Let's check whether b
was allocated in P
.
In that case C
deallocates the location b
, which means C; [b] = x
is not well-specified (i.e. will abort).
We now want to apply frame rule. But we need check that the C
doesn't modifies b
. If it does, there is obviously a conflict in how two pieces treat b
and we need to resolve it with appropriate renaming.
When resolved, . Thus, we can apply the frame rule to both pieces: { P * b -> _ } C { Q * b -> _ }
and { Q * b -> _ } [b] = x { Q * b -> x }
. We can construct a Hoare-triple for our resulting piece of code: { P * b -> - } C; [b] = x { Q * b -> x }