often knows the return address that
must be used.
Local reasoning and separation logic. Modular reasoning is the key technique for making program verification
scale. Development of a certified software system would benefit from a top-down approach where programmers
first work out the high-level design and
specification, then decompose the entire system into smaller modules, refine high-level specifications into actual implementation, and finally certify
each component and link everything
together into a complete system.
However, there is yet another critical dimension to making program
verification modular. Traditional
Hoare logics often use program specifications with arbitrarily large “
footprints.” Separation logic17, 27 advocates
“local reasoning” using small-footprint specifications; that is, the specification of each module (or procedure)
should refer only to data structures
actually touched by a module’s underlying code. By concisely specifying
the separation of heap and other resources, separation logic provides succinct yet powerful inference rules for
reasoning about shared mutable data
structures and pointer anti-aliasing.
Concurrent separation logic (CSL) 25
applies the same idea to reasoning
about shared-memory concurrent
programs, assuming the invariant
that there always exists a partition of
memory among different concurrent
entities and that each entity can access only its own part of memory. This
assumption might seem simple but is
surprisingly powerful. There are two
important points about the invariant:
First, the partition is logical; programmers do not need to change their model of the physical machine, which has
only one global shared data heap, and
the logical partition can be enforced
through separation logic primitives.
Second, the partition is not static and
can be adjusted dynamically during
program execution by transferring the
ownership of memory from one entity
to the other.
Under CSL, a shared-memory pro-
gram can be certified as if it were a
sequential program since it is always
manipulating its private heap; to ac-
cess shared memory, it must invoke
an atomic operation that transfers re-
sources between the shared heap and
the local heap. Several recent efforts
have extended CSL with rely-guarantee
reasoning, so even lock-free concur-
rent code can be certified using modu-
lar small-footprint specifications.
figure 2. using domain-specific logics to verify modules.
shao-fig2.pdf 1 10/8/10 4:45PM shao-fig2.pdf 1 10/8/10 4:45PM
(a) one-for-all Logic (a) The One-for-All Logic (a) Th One-for-All Logic
(b) Domain-Specific Logics (b) Domain-Specific Logics (b) Domain-Specific Logics
figure 3. an open framework for building certified software.
oCAP Inference rules
Formal machine model
dECEmBEr 2010 | vol. 53 | No. 12 | CommuniCaTionS of ThE aCm 63