123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121 |
- .EQ
- delim $#
- .EN
- .NH 3
- Invariants
- .LP
- Reclamation is tricky enough to warrant explicit statement
- of the invariants that are needed and the reasons they are true.
- This section will use the notation
- $b.e#
- and
- $b.e sub 1#
- to denote the allocation and
- closing epochs of block
- $b#.
- The invariants are:
- .IP (i)
- If $b# points at $bb#, then $bb.e <= b.e < bb.e sub 1#.
- .IP (ii)
- If $b# points at $bb#, then no other block $b'# with $b'.e = b.e# points at $bb#.
- .IP (iii)
- If $b# is not marked
- .CW BsCopied
- and points at $bb# such that $b.e = bb.e#, then no other block $b'# points at $bb#.
- .IP (iv)
- If $b# is in the active file system and points at $bb# then no other block $b'# in the
- active file system points at $bb#.
- .IP (v)
- If $b'# is a (possibly indirect) copy of $b#, then only one of $b# and $b'# is in the active file system.
- .LP
- Invariant (i) lets us reclaim blocks using the file system low epoch.
- Invariant (iii) lets us reclaim some blocks immediately once they are unlinked.
- Invariants (ii), (iv), and (v) are helpful in proving (i) and (iii); collectively they
- say that taking snapshots doesn't break the active file system.
- .PP
- Freshly allocated blocks start filled with nil pointers,
- and thus satisfy all the invariants. We need to check that
- copying a block, zeroing a pointer, and setting a pointer
- preserve the invariants.
- .LP
- $"BlockCopy" (b)#
- allocates a new block
- $b'# and copies the active and open block $b# into $b'#.
- .IP (i)
- Since $b# is open, all the blocks $bb# it points to are also
- active, and thus they have $bb.e sub 1# set to positive infinity
- (well,
- .CW ~0 ).
- Thus (i) is satisfied.
- .IP (ii)
- Since $b'.e# will be set to the current epoch, and $b.e# is less
- than the current epoch (it's copy-on-write), $b.e < b'.e# so (ii)
- is vacuously satisfied.
- .IP (iii)
- Since $b.e < b'.e#, all the pointers in $b# are to blocks with epochs less than $b'.e#.
- Thus (iii) is vacuously satisfied for both $b'#.
- Since $"blockCopy"# sets the
- .CW BsCopied
- flag, (iii) is vacuously satisfied for $b#.
- .IP (iv),(v)
- Since no pointers to $b# or $b'# were modified,
- (iv) and (v) are unchanged.
- .LP
- $"BlockRemoveLink" (b -> bb)# removes from block $b# the pointer to $bb#
- .IP
- Zeroing a pointer only restricts the preconditions on the
- invariants, so it's always okay.
- By (iii), if $b# is not
- .CW BsCopied
- and $b.e = bb.e#, then no other $b'# anywhere
- points at $bb#, so $bb# can be freed.
- .LP
- $"BlockSetLink" (b->bb sub 0 , bb sub 1)# changes the pointer in block $b# from $bb sub 0# to $bb sub 1#.
- We derive sufficient conditions on $bb sub 1#, and then
- examine the possible values of $bb sub 0# and $bb sub 1#.
- .IP (i)
- Since we're changing $b#, $b.e# is the current epoch.
- If $bb sub 1# is open, then (i) is satisfied.
- .IP (ii)
- If either $b.e != bb sub 1 .e# or $bb sub 1# is an orphan, then (ii) is satisfied.
- .IP (iii)
- If either $b.e != bb sub 1 .e# or $b# is marked
- .CW BsCopied
- or $bb sub 1# is an orphan, then (iii) is satisfied.
- .IP (iv)
- If $bb sub 1# is not currently active or $bb sub 1# is an orphan, then (iv) is satisfied.
- .IP (v)
- If $bb sub 1# is a copy of $bb sub 0# or $bb sub 1# is empty, then (v) is satisfied.
- .LP
- $"BlockSetLink" (b -> bb sub 0 , "blockAlloc" ())# allocates a new block and points $b# at it.
- .IP
- Since $bb sub 1# in this case is newly allocated, it is open, an orphan, and empty, and thus
- the invariants are satisfied.
- .LP
- $"BlockSetLink" (b -> bb sub 0 , "blockCopy" (bb sub 0 ))# copies $bb sub 0# and points
- $b# at the copy.
- .IP
- Since $bb sub 1# is newly allocated, it is open and an orphan. Thus (i)-(iv) are satisfied.
- Since $bb sub 1# is a copy of $bb sub 0#, (v) is satisfied.
- .LP
- $"BlockSetLink" (b -> "nil" , "oldRoot" )# changes a nil pointer to point
- at a snapshot root.
- .IP (i)
- Invariant (i) is broken, but the
- .CW snap
- field in the entry will be used to make sure
- we don't access the snapshot after it has been reclaimed.
- .IP (ii)
- Since the epoch of $"oldRoot"# is less than the current epoch but $b.e# is equal
- to the current epoch, (ii) is vacuously true.
- .IP (iii)
- XXX
- .IP (iv)
- XXX
- .IP (v)
- XXX
- .PP
- Ta da!
- xxx
- yyyy
- zzz
|