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

there is a machine m 3 , with a tombstone for u that dominates the resource r 1 ;
or with notation, if (7), then previously

∃ m 3 ,rs 3 . ( ,rs 3 , )= nw [ m 3 ] ∧¬ rs 3 [ u ] .live ∧ rs 3 [ u ] ≥ r 1 (8)

Conversely, if (7) is false, then for [ u r 1 ]either m 2 does not know about r 1 ,or

m 2 has a resource that m 1 does not know about. Regular synchronization takes
care of reconciling the state in these cases.
This property suggests a secondary protocol for asynchronous garbage col-
lection: periodically retrieve the version vector and all records from a partner
machine, then garbage collect live records whenever condition (7) holds. DFS-R
implements such a secondary protocol, but we observed that condition (7) in the
presence of non-atomic joins is no longer necessary and sucient for detecting
missed tombstones. In general, condition (7) is only sucient for detecting when
the standard join does not ensure convergence.

→

8 Implementation Checking

A common theme in the previous sections has been that we could take advantage
of somewhat subtle properties of a simple transition system to achieve goals,
such as garbage collection, conflict resolution, and reconciling concurrent rename
conflicts; but small modifications could break everything, and innocent looking
solutions could be broken in complicated ways.
In view of the complexity of the problem and the encouraging results with the
OCaml prototype we therefore decided to simulate the production version of the
synchronization core of DFS-R using model-checking techniques. This Section
describes the components that comprise the simulator. In summary, the simula-
tor works by exercising different combinations of file system operations followed
by synchronization steps in alternation, then it backtracks to visit different com-
binations. Some traces get pruned by partial order reduction techniques. This
drastically reduces redundancies in the search tree. Backtracking search requires
replacing the memory layer such that old state can easily be retrieved. To relieve
the simulator from suspending threads at arbitrary points we ensure that the
core makes use of suitable thread abstraction allowing it to single step through
large non-blocking atomic units. Finally, certain components are abstracted to
gain speed and control.
Thus, the main ingredients in our software model-checking experiment were:

1. Identifying a suitable vocabulary of actions to exercise.
2. Providing a memory layer that supports ecient backtracking.
3. Providing a threading layer that supports context switching and control of
which threads run.
4. Virtualize components that change device state.
5. Prune search using partial order reduction techniques.

Ideally, one would like a general framework to be able to handle simulating
systems, such as DFS-R. At the time we developed the framework, nothing