Download Deliverable 5.2 - Evaluation of Core Framework

HATS Deliverable D5.2
Evaluation of Core Framework
We also model the dependency between run() method of SyncServerAcceptorThread and the instantiation
of ConnectionThread as a partial interleaving of AcceptorThreadRun and ThreadPools synchronising the
events createConnectionThread .t for all threads t. The set {|c|} denotes the set of possible events associated
with c. In the case of {|createConnectionThread |}, it is equivalent to the following set.
{t : Thread • createConnectionThread .t}
The behavioural aspect of the synchronisation server is hence given by the following parallel combination of
processes.
process Behaviours = SyncServerMain |[ acceptorThread ]| ThreadAcceptor
We now consider the resource model of the synchronisation server. A synchronisation server has the replication snapshot, the boolean field acceptingConnections and the set field connectionsReplication as
shared resources, we therefore model these resources as the following interleaving.
process Resources = AcceptConnectionCondition 9 Connections 9 ReplicationSnapshot
The synchronisation server is then modelled by the following process SyncServer , defined as a parallel
combination of its behaviours and resources, synchronising on all possible events of the resource processes.
process SyncServer = Behaviours |[ ResourcesEvents ]| Resources
The set of events ResourcesEvents is defined as follows.
set
ResourcesEvents =
{|isAcceptingConnection, setAcceptingConnection, refreshSnapshot, clearSnapshot, getItems,
numberOfClientThread , containsThread , addClientThread , removeThread |}
O.6
Synchronisation Client
We now consider the process for modelling the sychronisation client. We define the process ClientDB as the
client file store, so that our model can relate different replication sessions.
channel replaceItem, appendItem : File
function
update(c, cps) = if c ∈ ran cps then cps else cps a hci
notWithId (q) = λ f • fst(f ) 6= fst(q)
size(i , fs) = let item = hs : fs | fst(s) = i i within (if item = hi then 0 else snd (head item))
updateItems(f , ps) = hs : ps | fst(s) 6= fst(f )i a h(a, b) : hs : ps | fst(s) = fst(f )i • (a, (b + snd (f )))i
process
ClientDB (cps, fs) =
cmd .i .CheckPointId ?c : CheckPoint!(c ∈
/ ran cps) → ClientDB (update(c, cps), fs)
2 cmd .i .FileCmd ?fid : FileId !size(fid , fs) → ClientDB (cps, fs)
2 replaceItem?f : File → ClientDB (cps, filterSeq(notWithId (f ))(fs) a hf i)
2 appendItem?f : File → ClientDB (cps, updateItems(f , fs))
193