| 2 |
- |
1 |
.EQ
|
|
|
2 |
delim $#
|
|
|
3 |
.EN
|
|
|
4 |
.NH 3
|
|
|
5 |
Invariants
|
|
|
6 |
.LP
|
|
|
7 |
Reclamation is tricky enough to warrant explicit statement
|
|
|
8 |
of the invariants that are needed and the reasons they are true.
|
|
|
9 |
This section will use the notation
|
|
|
10 |
$b.e#
|
|
|
11 |
and
|
|
|
12 |
$b.e sub 1#
|
|
|
13 |
to denote the allocation and
|
|
|
14 |
closing epochs of block
|
|
|
15 |
$b#.
|
|
|
16 |
The invariants are:
|
|
|
17 |
.IP (i)
|
|
|
18 |
If $b# points at $bb#, then $bb.e <= b.e < bb.e sub 1#.
|
|
|
19 |
.IP (ii)
|
|
|
20 |
If $b# points at $bb#, then no other block $b'# with $b'.e = b.e# points at $bb#.
|
|
|
21 |
.IP (iii)
|
|
|
22 |
If $b# is not marked
|
|
|
23 |
.CW BsCopied
|
|
|
24 |
and points at $bb# such that $b.e = bb.e#, then no other block $b'# points at $bb#.
|
|
|
25 |
.IP (iv)
|
|
|
26 |
If $b# is in the active file system and points at $bb# then no other block $b'# in the
|
|
|
27 |
active file system points at $bb#.
|
|
|
28 |
.IP (v)
|
|
|
29 |
If $b'# is a (possibly indirect) copy of $b#, then only one of $b# and $b'# is in the active file system.
|
|
|
30 |
.LP
|
|
|
31 |
Invariant (i) lets us reclaim blocks using the file system low epoch.
|
|
|
32 |
Invariant (iii) lets us reclaim some blocks immediately once they are unlinked.
|
|
|
33 |
Invariants (ii), (iv), and (v) are helpful in proving (i) and (iii); collectively they
|
|
|
34 |
say that taking snapshots doesn't break the active file system.
|
|
|
35 |
.PP
|
|
|
36 |
Freshly allocated blocks start filled with nil pointers,
|
|
|
37 |
and thus satisfy all the invariants. We need to check that
|
|
|
38 |
copying a block, zeroing a pointer, and setting a pointer
|
|
|
39 |
preserve the invariants.
|
|
|
40 |
.LP
|
|
|
41 |
$"BlockCopy" (b)#
|
|
|
42 |
allocates a new block
|
|
|
43 |
$b'# and copies the active and open block $b# into $b'#.
|
|
|
44 |
.IP (i)
|
|
|
45 |
Since $b# is open, all the blocks $bb# it points to are also
|
|
|
46 |
active, and thus they have $bb.e sub 1# set to positive infinity
|
|
|
47 |
(well,
|
|
|
48 |
.CW ~0 ).
|
|
|
49 |
Thus (i) is satisfied.
|
|
|
50 |
.IP (ii)
|
|
|
51 |
Since $b'.e# will be set to the current epoch, and $b.e# is less
|
|
|
52 |
than the current epoch (it's copy-on-write), $b.e < b'.e# so (ii)
|
|
|
53 |
is vacuously satisfied.
|
|
|
54 |
.IP (iii)
|
|
|
55 |
Since $b.e < b'.e#, all the pointers in $b# are to blocks with epochs less than $b'.e#.
|
|
|
56 |
Thus (iii) is vacuously satisfied for both $b'#.
|
|
|
57 |
Since $"blockCopy"# sets the
|
|
|
58 |
.CW BsCopied
|
|
|
59 |
flag, (iii) is vacuously satisfied for $b#.
|
|
|
60 |
.IP (iv),(v)
|
|
|
61 |
Since no pointers to $b# or $b'# were modified,
|
|
|
62 |
(iv) and (v) are unchanged.
|
|
|
63 |
.LP
|
|
|
64 |
$"BlockRemoveLink" (b -> bb)# removes from block $b# the pointer to $bb#
|
|
|
65 |
.IP
|
|
|
66 |
Zeroing a pointer only restricts the preconditions on the
|
|
|
67 |
invariants, so it's always okay.
|
|
|
68 |
By (iii), if $b# is not
|
|
|
69 |
.CW BsCopied
|
|
|
70 |
and $b.e = bb.e#, then no other $b'# anywhere
|
|
|
71 |
points at $bb#, so $bb# can be freed.
|
|
|
72 |
.LP
|
|
|
73 |
$"BlockSetLink" (b->bb sub 0 , bb sub 1)# changes the pointer in block $b# from $bb sub 0# to $bb sub 1#.
|
|
|
74 |
We derive sufficient conditions on $bb sub 1#, and then
|
|
|
75 |
examine the possible values of $bb sub 0# and $bb sub 1#.
|
|
|
76 |
.IP (i)
|
|
|
77 |
Since we're changing $b#, $b.e# is the current epoch.
|
|
|
78 |
If $bb sub 1# is open, then (i) is satisfied.
|
|
|
79 |
.IP (ii)
|
|
|
80 |
If either $b.e != bb sub 1 .e# or $bb sub 1# is an orphan, then (ii) is satisfied.
|
|
|
81 |
.IP (iii)
|
|
|
82 |
If either $b.e != bb sub 1 .e# or $b# is marked
|
|
|
83 |
.CW BsCopied
|
|
|
84 |
or $bb sub 1# is an orphan, then (iii) is satisfied.
|
|
|
85 |
.IP (iv)
|
|
|
86 |
If $bb sub 1# is not currently active or $bb sub 1# is an orphan, then (iv) is satisfied.
|
|
|
87 |
.IP (v)
|
|
|
88 |
If $bb sub 1# is a copy of $bb sub 0# or $bb sub 1# is empty, then (v) is satisfied.
|
|
|
89 |
.LP
|
|
|
90 |
$"BlockSetLink" (b -> bb sub 0 , "blockAlloc" ())# allocates a new block and points $b# at it.
|
|
|
91 |
.IP
|
|
|
92 |
Since $bb sub 1# in this case is newly allocated, it is open, an orphan, and empty, and thus
|
|
|
93 |
the invariants are satisfied.
|
|
|
94 |
.LP
|
|
|
95 |
$"BlockSetLink" (b -> bb sub 0 , "blockCopy" (bb sub 0 ))# copies $bb sub 0# and points
|
|
|
96 |
$b# at the copy.
|
|
|
97 |
.IP
|
|
|
98 |
Since $bb sub 1# is newly allocated, it is open and an orphan. Thus (i)-(iv) are satisfied.
|
|
|
99 |
Since $bb sub 1# is a copy of $bb sub 0#, (v) is satisfied.
|
|
|
100 |
.LP
|
|
|
101 |
$"BlockSetLink" (b -> "nil" , "oldRoot" )# changes a nil pointer to point
|
|
|
102 |
at a snapshot root.
|
|
|
103 |
.IP (i)
|
|
|
104 |
Invariant (i) is broken, but the
|
|
|
105 |
.CW snap
|
|
|
106 |
field in the entry will be used to make sure
|
|
|
107 |
we don't access the snapshot after it has been reclaimed.
|
|
|
108 |
.IP (ii)
|
|
|
109 |
Since the epoch of $"oldRoot"# is less than the current epoch but $b.e# is equal
|
|
|
110 |
to the current epoch, (ii) is vacuously true.
|
|
|
111 |
.IP (iii)
|
|
|
112 |
XXX
|
|
|
113 |
.IP (iv)
|
|
|
114 |
XXX
|
|
|
115 |
.IP (v)
|
|
|
116 |
XXX
|
|
|
117 |
.PP
|
|
|
118 |
Ta da!
|
|
|
119 |
xxx
|
|
|
120 |
yyyy
|
|
|
121 |
zzz
|