runs a recovery procedure (such as fsck) before resuming
normal operation. Hoare logic does not provide a notion
that at any point during procedure’s execution, a recovery
procedure may run. The rest of this section describes how
CHL extends Hoare logic to handle crashes.
Traditional Hoare logic distinguishes between partial
correctness, where we prove that terminating programs
give correct answers, and total correctness, where we also
prove termination. We use Coq’s built-in termination
checker to guarantee that our system calls always finish,
when no crashes occur. However, we model cases where a
program still runs forever, because it keeps crashing and
then crashing again during recovery, ad infinitum. For that
reason, our specifications can be interpreted as total correctness for crash-free executions and partial correctness
for crashing executions, which makes sense, since the
underlying hardware platform refuses to give the programmer a way to guarantee normal termination in the presence
of crashes.
3. 1. Example
Many file-system operations must update two or more disk
blocks atomically. For example, when creating a file, the
file system must both mark an inode as allocated as well as
update the directory in which the file is created (to record
the file name with the allocated inode number). To ensure
correct behavior under crashes, a common approach is
to use a write-ahead log. Logging guarantees that, if a file-system operation crashed while applying its changes to the
disk, then after a crash, a recovery procedure can finish the
job by applying the log contents. Write-ahead logging makes
it possible to avoid the undesirable intermediate state where
the inode is allocated but not recorded in the directory,
effectively losing an inode. Many file systems, including
widely used ones like Linux’s ext4,
34 employ logging exactly
for this reason.
The simple procedure shown in Figure 2 captures the
essence of file-system calls that must update two or more
blocks. The procedure performs two disk writes using a
write-ahead log, which supplies the log_begin, log_commit,
and log_write APIs. The procedure log_write appends
a block’s content to an in-memory log, instead of updating
the disk block in place. The procedure log_commit writes
the log to disk, writes a commit record, and then copies the
block contents from the log to the blocks’ locations on disk.
If this procedure crashes and the system reboots, the recovery procedure runs. The recovery procedure looks for the
commit record. If there is a commit record, it completes the
operation by copying the block contents from the log into
the proper locations and then cleans the log.
If there is no commit record, then the recovery procedure just cleans the log. If there is a crash during recovery,
then after reboot the recovery procedure runs again. In principle, this may happen several times. If the recovery finishes,
however, then either both blocks have been updated or neither has. Thus, in the atomic_two_write procedure from
Figure 2, the write-ahead log guarantees that either both
writes happen or neither does, no matter when and how
many crashes happen.
CHL makes it possible to write specifications for procedures such as atomic_two_write and the write-ahead
logging system, as we will explain in the rest of the section.
3. 2. Crash conditions
CHL needs a way for developers to write down predicates
about disk states, such as a description of the possible intermediate states where a crash could occur. To do this, CHL
extends Hoare logic with crash conditions, similar in spirit
to prior work on fail-stop processors33, Section
3 and fault conditions from concurrent work,
28 but formalized precisely
to allow for executable implementations and machine-checked proofs.
For modularity, CHL should allow reasoning about just
one part of the disk, rather than having to specify the contents of the entire disk at all times. For example, we want
to specify what happens with the two blocks that atomic_
two_write updates and not have to say anything about the
rest of the disk. To do this, CHL employs separation logic,
30
which is a way of combining predicates on disjoint parts of
a store (in our case, the disk). The basic predicate in separation logic is a points-to relation, written as a v, which
means that address a has value v. Given two predicates x and
y, separation logic allows CHL to produce a combined predicate x y. The operator means that the disk can be split
into two disjoint parts, where one satisfies the x predicate,
and the other satisfies y.
To reason about the behavior of a procedure in the presence of crashes, CHL allows a developer to capture both
the state at the end of the procedure’s crash-free execution
and the intermediate states during the procedure’s execution in which a crash could occur. For example, Figure 3
shows the CHL specification for FSCQ’s disk_write. (In
our implementation of CHL, these specifications are written in Coq code; we show here an easier-to-read version.)
We will describe the precise notation shortly, but for now,
note that the specification has four parts: the procedure
about which we are reasoning, disk_write(a, v); the
precondition, disk: a 〈v0, vs〉 other_blocks; the postcondition if there are no crashes, disk: a 〈v, [v0]⊕vs〉
other_blocks; and the crash condition, disk: a 〈v0, vs〉
def atomic_two_write(a1, v1, a2, v2):
log_begin()
log_write(a1, v1)
log_write(a2, v2)
log_commit()
Figure 2. Pseudocode of atomic_two_write.
SPEC disk_write(a, v)
PRE disk: a ; 〈v0, vs〉 ; other_blocks
POST disk: a ; 〈v, [v0]⊕ vs〉 ; other_blocks
CRASH disk: a ; 〈v0, vs〉 ; other_blocks ∨
a ; 〈v, [v0]⊕ vs〉) ; other_blocks
Figure 3. Specification for disk_write.