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

Create ( nw,m,uid,parent,name ):
let ( vv, rs, in )= nw [ m ], v =1+max( vv [ m ])
assume ∀ [ → ( ,rs , )] ∈ nw . uid ∈ rs ( uid is fresh in nw )
rs [ parent ] .live ∧ name is fresh under parent
vv [ m ]:= vv [ m ] ∪{v}
rs [ uid ]:= {gvsn =( m, v ) , parent,name,clock = v, live = true }

Update ( nw,m,uid ):
let ( vv, rs, in )= nw [ m ], v =1+max( vv [ m ]), clock =max( v, rs [ uid ] .clock +1)
assume rs [ uid ] .live
vv [ m ]:= vv [ m ] ∪{v}
rs [ uid ]:= rs [ uid ] with {clock, gvsn =( m, v ) }

Rename ( nw, m, uid, parent ,name ):
let ( vv, rs, in )= nw [ m ], v =1+max( vv [ m ]), clock =max( v, rs [ uid ] .clock +1)
assume rs [ uid ] .live ∧ rs [ parent ] .live ∧ name is fresh under parent
Rename maintains tree-shape of directory hierarchy
vv [ m ]:= vv [ m ] }

rs [ uid ]:= rs [ uid ] with {gvsn =( m, v ) , parent = parent ,clock,name = name }

∪{ v

Delete ( nw,m,uid ):
let ( vv, rs, in )= nw [ m ], v =1+max( vv [ m ]), clock =max( v, rs [ uid ] .clock +1)
assume rs [ uid ] .live

( ∀uid ∈ rs . rs [ uid ] .parent = uid ∨¬rs [ uid ] .live )

∧

vv [ m ]:= vv [ m ] ∪{v}
rs [ uid ]:= rs [ uid ] with {gvsn =( m, v ) ,clock,live = false }

Fig. 2. Basic file system operations

to c , b to a ,then c to b . The names of the two files are swapped, but each record
is name conflicting with the configuration on m 1 .Sowhen m 1 synchronizes with
m 2 , it will be resolving two name conflicts instead of performing the swap.
Our first observation is that the resulting system maintains a basic invariant:
the versions of all records are tracked in the version vectors.

∀ [ → ( vv, rs, )] ∈ nw, [ →{ gvsn =( m, v ) } ] ∈ rs . v ∈ vv [ m ] (2)

Thus, a more network ecient version of BasicSyncJoin proceeds by
1. The receiving machine m 1 gets version vector vv 2 from the sender m 2 .
2. It then subtracts vv 1 from vv 2 ,forming vv Δ := vv 2 \ vv 1 .
3. The sending machine is asked for records whose versions are in vv Δ .
4. The database of m 1 is updated as in BasicSyncJoin .
The more refined version of global consistency we seek can also be formulated in
terms of version vectors, namely, that databases coincide on all shared versions:

r 1 .gvsn ∈ vv 2 ∨ rs 2 [ u ]= r 1 ∨ rs 2 [ u ] .gvsn ∈ vv 1 ,

(3)

for every m 1 ,m 2 , such that ( vv 1 ,rs 1 , )= nw [ m 1 ], ( vv 2 ,rs 2 , )= nw [ m 2 ]and
[ u → r 1 ] ∈ rs 1 .