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

machine maintains n (= 3) resources, each resource is identified by a number
0 ,...,n − 1, and a designated root folder is identified by the number − 1. A

resource has a parent , which is a number 1, and a clock used to

impose a total ordering on resources. Resources can be updated by changing the
parent and clock , but only if the update does not introduce a self-loop. Fig.7.
contains the minimal amount of Zing declarations to define two machines each
with three resources all residing under a common root.
A model checker is well suited at specifying a set of possible configurations
implicitly by using non-deterministic choices. Thus, we arrive at a non-flat con-
figuration by first moving files around randomly on each machine, with each
move incrementing globalClock and using its value as the clock on the moved
resources.

− 1 , 0 ,...,n −

class Node {
int parent;
int clock;

} ;
array Tree[3] Node;

class Machine {
Tree tree = new Tree {{ -1,0 } , { -1,0 } , { -1,0 }} ;

atomic bool cycle( int node, int parent) {
return (parent != -1) &&
(parent == node cycle(node, tree[parent].parent));

}

atomic void move( int node, int parent, int clock) {
assume (!cycle(node, parent));
tree[node].parent = parent;
tree[node].clock = clock;

}

} ;
array Machines[2] Machine;
static Machines machines;
static int globalClock = 0;

Fig. 7. Replicating machine in Zing

It remains to define synchronization in Zing. Our model for synchronization is
that machines send the state of a random node to a random machine. It requires
the recipient to determine the outcome based on the state of a single node. Thus,
traces can be identified as sequences of triples

node 1 , src 1 , dst 1 , node 2 , src 2 , dst 2 ,...,