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