Models and Software Model Checking of a Distributed File Replication System - Formal Methods and Hybrid Real-Time Systems - page 17

experimenting with design ideas on protocol substrates. Our take-away was to
remain using priority inversion as the conflict resolution mechanism in DFS-R.
To avoid divergence we imposed stronger restrictions on the order of processing
updates.

7 Distributed Garbage Collection

Our presentation of DFS-R has so far no mechanism to garbage collect data-
base records for deleted files. We need the database records so that file deletion
can be replicated in a timely manner, but when all replicating machines agree
that a file has been deleted, it should in principle be possible to remove the
tombstone. Prior solutions to detecting when to delete dead resources involve
two way commit protocols [12,13,14] to either agree on the when to add ma-
chines to a network, or when to safely collect resources marked for deletion.
Solutions in replication systems, such as, Clearinghouse [15], NTFRS and other
replications systems use a timeout based collection of tombstones: If a record
has been marked as tombstone for 30 or 60 days, simply delete it from the data-
base. Fig. 10 contains the corresponding transition that performs the garbage
collection non-deterministically.

GarbageCollect ( nw,m,u ):
let ( vv, rs, in )= nw [ m ] ,r = rs [ u ]
assume ¬r.live
rs := rs \ [ u → r ]

Fig. 10. Tombstone garbage collection

This solution does not address deleting content on machines that have been
disconnected beyond the timeout value of the tombstones. While this situation
reflects lack of consensus it also widens the likelihood that this content may
reappear in other machines if the oine machine later makes changes to this
content or if the machine has to recover from database loss.
It turns out that with synchronous joins we have a necessary and sucient
basis for detecting tombstones. The key is, as in (2), that version vectors maintain
a trace of previously observed changes.
Let m 1 ,m 2 be machines, such that ( vv 1 ,rs 1 , )= nw [ m 1 ], ( vv 2 ,rs 2 , )=
nw [ m 2 ]and[ u → r 1 ] ∈ rs 1 . The resource r 1 is subsumed by a tombstone if

we have:

u

∧ rs 2 [ u ] .gvsn ∈ vv 1

r 1 .gvsn ∈ vv 2 ∧ ∈ rs 2 ∨ (7)

rs 2 [ u ] .gvsn = r 1 .gvsn

The system with SyncJoin , GarbageCollect and the file system operations sat-
isfies the following invariant: Whenever (7) holds, then some time in the past,