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

network topologies. In other configurations there are reliable, but slow, wide-
area networks and there is a need for file locking. With state transfer only, it is
not possible to undo operations with arbitrary fine-grained control.

3 A State-Based File Replication System

In this Section we will outline the essence of a file replication system. While
highly simplified, it reflects some of the early protocol design maneuvers.

3.1 Components

Network. Abstractly, the problem at hand is to replicate files in a network of
connected machines. Each machine maintains a file system view and a database.
The network topology is indicated by a set of in-bound connections per machine.
We assume a well-formed network, comprising of a digraph without self-loops,
where each node is labeled by a unique machine identifier. A connected network
is furthermore desirable for convergence.

m
→ nw ∈ Network = MachineId Machine

mch ∈ Machine = FileSystem × DataBase × inbound

m ∈ MachineId = Globally unique identifier for a machine

in ∈ inbound = MachineId -set

File System. For our purposes, a file system is a collection of files each uniquely
identified by an identifier, which is unique per file system. In NTFS, such identi-
fiers are 64 bit numbers, called file reference numbers , on Unix-like file systems,
these are called inodes . Each file has a file name, a parent directory and file
data. One would typically expect a file system to be dictated as a tree-like struc-
ture comprising of files identified by file paths as strings, but this view turns
out to be unsuitable for several reasons. For example, such a view is open to
situations where files are moved around, such that the same path gets identified
with completely different files. Identifying a file with an identifier makes it eas-
ier to support ecient replication of renaming directories with a large number
of children, but makes it very hard to support merging contents from differ-
ent directories. A file system is well-formed when the ancestral relations form a
uniquely rooted connected tree (only the root has itself as a parent).

m
→ fs ∈ FileSystem = FileId FileRecord

file ∈ FileRecord = { name : Name , parent : FileId, data : Data }

fid ∈ FileId = Numeral

Database. The file system only maintains information that is local to the ma-
chine where the files reside. In order to realize a file replication system, one
needs to maintain information reflecting the shared state between machines. In
DFS-R, this state is a database consisting of version vector and a set of records,
one per replicated file.