Table of Contents

MODEL, SPECIFICATION, AND VERIFICATION OF MUSIC

open util/ordering [Time] as trace
open util/integer

...

open util/ordering [Time] as trace
open util/integer
open util/ordering [LockRef] as queue
/* ========================================================================
TEMPORAL STRUCTURE
Note that if time has a scope of x, there will be exactly x times and
x-1 real events.
======================================================================== */

sig Time { }

abstract sig Event { pre: Time, post: Time }
sig Null extends Event { } -- null events can only be at beginning of trace
fact NullEvent { all e: Null | no s: SystemState | e.pre = s.time }

fact TemporalStructure {
all t: Time - trace/last | one e: Event | e.pre = t
all t: trace/last | no e: Event | e.pre = t
all e: Event | e.post = (e.pre).next }

/* ========================================================================
ABOUT LOCKREFS AND TIMESTAMPS
======================================================================== */

sig LockRef { }

pred PastQueue [g: set LockRef, f: lone LockRef, -- (g, f) is older
q: set LockRef, p: lone LockRef] { -- than (q, p)
(g = q)
=> (f != p && ( (some f && some p && queue/lt [f, p])
|| (some f && no p) ) )
else ( (g in q)
&& ( (some f && some p && queue/lte [f, p])
|| (some f && no p)
|| (no f && some p && p in (q - g))
|| (no f && no p) ) ) }

pred PastPtr [f: LockRef, s: SystemState] {
f in s.trueQset && (no s.trueQptr || queue/gt [s.trueQptr, f]) }

pred CurrentOrPastPtr [f: LockRef, s: SystemState] {
f in s.trueQset && (no s.trueQptr || queue/gte [s.trueQptr, f]) }

sig Timestamp {ref: LockRef, tme: Time}

fact TimestampsAreRecords { all p0, p1: Timestamp |
(p0.ref = p1.ref && p0.tme = p1.tme) => p0 = p1 }

pred EarlierTimestamp [t0, t1: Timestamp] {-- true if t0 is earlier than t1
queue/lt [t0.ref, t1.ref] || (t0.ref = t1.ref && lt [t0.tme, t1.tme]) }

pred EarlierOrEqualTimestamp [t0, t1: Timestamp] {
queue/lt [t0.ref, t1.ref] || (t0.ref = t1.ref && lte [t0.tme, t1.tme]) }

pred PastTimestamp [t: Timestamp, s: SystemState ] {
PastPtr [t.ref, s] || (t.ref = s.trueQptr && lt [t.tme, s.time]) }

pred CurrentOrPastTimestamp [t: Timestamp, s: SystemState ] {
PastPtr [t.ref, s] || (t.ref = s.trueQptr && lte [t.tme, s.time]) }

/* ========================================================================
ABOUT MESSAGES
======================================================================== */

abstract sig Message { stamp: Timestamp, val: Value }

abstract sig RepMsg extends Message { cli: Client }
sig RepPutMsg, RepGetMsg extends RepMsg { }

fact RepMsgsAreRecords { all m0, m1: RepMsg |
(m0.cli = m1.cli && m0.stamp = m1.stamp && m0.val = m1.val) => m0 = m1 }

abstract sig ClientMsg extends Message { rep: Replica }
abstract sig ClientPutMsg, ClientGetMsg extends ClientMsg { }
sig ClientPutAck, ClientPutNack, ClientPutNohold extends ClientPutMsg {}
sig ClientGetAck, ClientGetNack, ClientGetNohold extends ClientGetMsg {}

fact ClientMsgsAreRecords { all m0, m1: ClientMsg |
(m0.rep = m1.rep && m0.stamp = m1.stamp && m0.val = m1.val) => m0 = m1 }

/* ========================================================================
SYSTEM STATE AND TRACES
There is only one key, which is not explicit.
Replicas of the lock store may not be the same as MUSIC replicas, but
there is a one-to-one correspondence between replicas of the two types.
Also, operations on the lock store are atomic, reliable, and sequential.
If a lock store replica is dead, it is modeled as a replica whose value is
very out-of-date, as only a quorum of replicas need have the true value.
======================================================================== */

sig Client { }

sig Value { } one sig True, False extends Value { }

sig Replica { } fact { # Replica = 5 }

abstract sig ClientState { }
one sig Dead, Live, Enqueued, Critical, MustGet, MustPut, MustPut4Synch,
SynchGetting, SynchPutting, Getting, Putting extends ClientState { }

abstract sig ReplicaState { }
one sig Failed, Started extends ReplicaState { }

sig SystemState {
time: Time,
-- lock store
-- real state
Qset: Replica -> LockRef,
Qptr: Replica -> lone LockRef,
trueDataSynchFlag: True + False, -- true value in eventu.consis. data
-- history variables
trueQset: set LockRef,
trueQptr: lone LockRef,
synchFlag: True + False,
-- client state
-- real state
clientRef: Client -> lone LockRef,
clientState: Client -> one ClientState,
clientTask: Client -> lone (ClientPutAck + ClientGetAck),
-- what client is waiting for
clientInputs: Client -> ClientMsg,
-- history variables
trueTimestamp: Timestamp,
trueValue: Value,
-- music state
repState: Replica -> one ReplicaState,
repInputs: Replica -> RepMsg,
repTask: Replica -> lone RepMsg, -- what replica is working on
-- music's view of data store
-- real state
writePending: Timestamp -> lone Value,
writeSucceeded: Timestamp -> lone Value,
defined: set Time,
-- derived variables
trueDataTimestamp: Timestamp,
trueDataValue: Value,
} {
some (writePending + writeSucceeded)

-- the true data tuple is the written tuple with the highest timestamp
all t: Timestamp, v: Value |
( (t -> v) in (writePending + writeSucceeded)
&& (no t': Timestamp, v': Value |
(t' -> v') in (writePending + writeSucceeded)
&& EarlierTimestamp [t, t'] )
) => (t = trueDataTimestamp && v = trueDataValue)
}

pred DataStoreDefined [s: SystemState] {
-- the datastore is well-defined when it has a true tuple in writeSucceeded
some s.trueDataTimestamp
&& (s.trueDataTimestamp -> s.trueDataValue) in s.writeSucceeded }

fact UpdateOfDefinedSet {
all e: TraceEvent, s: e.prest, s': e.postst |
DataStoreDefined [s] => s'.defined = s.defined + s.time
else s'.defined = s.defined }

pred InitialState [s: SystemState] {
s.trueQset = queue/first && no s.trueQptr
s.Qset = (Replica -> queue/first) && no s.Qptr
Client.(s.clientState) in Dead && some s.trueValue
some s.trueTimestamp
(s.trueTimestamp).ref = queue/first && lt [(s.trueTimestamp).tme,s.time]
s.synchFlag = False && s.trueDataSynchFlag = False
no s.clientRef && no s.clientTask && no s.clientInputs
Replica.(s.repState) in Failed && no s.repInputs && no s.repTask
no s.writePending && no s.defined
s.writeSucceeded = (s.trueTimestamp -> s.trueValue) }

pred LockStoreInvariant [s: SystemState] {
-- LockRefs are ordered. A queue is represented by a set of lockRefs and
-- an optional pointer. The set contains all the lockRefs that have ever
-- been enqueued (ordered implicitly by the order on lockRefs, which is
-- also the order of use). If there is a pointer, it points to the current
-- lockHolder. If there is no pointer, all lockRefs in the set have been
-- used and released.
-- Unused lockRefs are always larger than queued ones.
all f0: s.trueQset, f1: LockRef - s.trueQset | queue/lt [f0, f1]
-- The trueQptr is in the trueQset.
s.trueQptr in s.trueQset
-- A replica's Qset must be the trueQset or a subset of it that is a
-- "prefix" of it, in the sense of the ordering on lockRefs.
all r: Replica |
( r.(s.Qset) in s.trueQset
&& all f0: r.(s.Qset), f1: s.trueQset - r.(s.Qset) | queue/lt [f0, f1] )
-- A replica's Qptr is in the replica's Qset.
all r: Replica | r.(s.Qptr) in r.(s.Qset)
-- A replica's queue must be a current or past truth.
all r: Replica |
( (r.(s.Qset) = s.trueQset && r.(s.Qptr) = s.trueQptr)
|| PastQueue [r.(s.Qset), r.(s.Qptr), s.trueQset, s.trueQptr] )
-- At least a quorum of replicas have the true queue.
let correctQueues =
{ r: Replica | r.(s.Qset) = s.trueQset && r.(s.Qptr) = s.trueQptr } |
gte [ # correctQueues, 3]
-- this is a basic safety property for the implementation of the synch flag
s.trueDataSynchFlag = False => s.synchFlag = False
}

pred ClientStateInvariant [s: SystemState] {
-- includes client's relation to music
-- A client's lockRef is found in the trueQset.
all c: Client | c.(s.clientRef) in s.trueQset
-- A client's lockRef is unique among clients, and is always in the
-- trueQset.
let repMsgRef = { c: Client, f: LockRef |
some m: Replica.(s.repInputs + s.repTask) |
(c = m.cli && f = m.stamp.ref) } |
let clientMsgRef = { c: Client, f: LockRef |
some m: c.(s.clientInputs + s.clientTask) |
f = m.stamp.ref && f = c.(s.clientRef) } |
( (all f: LockRef | lone (s.clientRef + repMsgRef + clientMsgRef).f)
&& (all f: Client.(s.clientRef + repMsgRef + clientMsgRef) |
f in s.trueQset )
)
-- properties of client states
all c: Client | c.(s.clientState) in (Dead + Live)
=> ( no c.(s.clientRef)
&& no c.(s.clientTask) )
all c: Client | c.(s.clientState) in Enqueued
=> ( some c.(s.clientRef)
&& ! PastPtr [c.(s.clientRef), s]
&& no c.(s.clientTask) )
all c: Client | c.(s.clientState) in Critical + MustGet
=> ( some c.(s.clientRef)
&& CurrentOrPastPtr [c.(s.clientRef), s]
&& no c.(s.clientTask) )
all c: Client | c.(s.clientState) in MustPut + MustPut4Synch
=> ( some c.(s.clientRef)
&& CurrentOrPastPtr [c.(s.clientRef),s]
&& some c.(s.clientTask) -- only the task value is significant
&& c.(s.clientTask) in ClientPutAck )
all c: Client | c.(s.clientState) in SynchGetting + Getting
=> ( some c.(s.clientRef)
&& CurrentOrPastPtr [c.(s.clientRef), s]
&& some c.(s.clientTask) -- only replica and stamp are significant
&& c.(s.clientTask) in ClientGetAck )
all c: Client | c.(s.clientState) in SynchPutting + Putting
=> ( some c.(s.clientRef)
&& CurrentOrPastPtr [c.(s.clientRef), s]
&& some c.(s.clientTask) && c.(s.clientTask) in ClientPutAck )
-- the client task must be in the client's current epoch
all c: Client, m: ClientMsg |
m in c.(s.clientTask) => m.stamp.ref = c.(s.clientRef)
}

pred MusicStateInvariant [s: SystemState] {
-- includes Music's relation to datastore
-- If a replica has a task, it is started.
all r: Replica | some r.(s.repTask) => r.(s.repState) = Started
-- writes being waited for are writes pending or succeeded
all r: Replica, m: RepPutMsg |
(r -> m) in s.repTask
=> (m.stamp -> m.val) in s.writePending + s.writeSucceeded
}

pred DataStoreInvariant [s: SystemState] {
-- datastore writes are in the past
all t: (s.writeSucceeded).Value | PastTimestamp [t, s]
-- writes pending are in the past or present
all t: (s.writePending).Value | CurrentOrPastTimestamp [t, s]
-- if the "write sets" have a timestamp overlap, then the values are
-- consistent
all t: Timestamp, v, v': Value |
( (t -> v) in s.writePending && (t -> v') in s.writeSucceeded )
=> v = v'
-- all times in the defined set are in the past
all t: s.defined | lt [t, s.time]
}

pred GlobalConsistencyInvariant [s: SystemState] {
-- in general, these constraints cover all clients and all lockRefs, not
-- just the lockholding client and trueQptr
-- no current or future true timestamps
PastTimestamp [s.trueTimestamp, s]
-- no future messages or tasks
all m:
Client.(s.clientTask+s.clientInputs) + Replica.(s.repInputs+s.repTask) |
CurrentOrPastTimestamp [m.stamp, s]
-- no current or future data store writes
all t: (s.writePending + s.writeSucceeded).Value |
CurrentOrPastTimestamp [t, s]
-- if a client has a lockRef, and the true timestamp is in the same epoch,
-- then the true timestamp is in the past with respect to this epoch;
-- NOTE this is a subtle constraint, implying that whatever local clock is
-- being used, it can distinguish well enough between sequential actions
-- of the same client
all c: Client |
( some c.(s.clientRef) && s.trueTimestamp.ref = c.(s.clientRef) )
=> lt [s.trueTimestamp.tme, s.time]
-- same as above for datastore writes
all c: Client, t: (s.writePending + s.writeSucceeded).Value |
( some c.(s.clientRef) && t.ref = c.(s.clientRef) )
=> lt [t.tme, s.time]
-- if a client has a task, it is in the present or past with respect to
-- the client's epoch
all c: Client, m: c.(s.clientTask) | lte [m.stamp.tme, s.time]
-- if a client has a task, then all repInputs and repTasks with the same
-- lockRef have the same time or an earlier one
all c: Client, m: c.(s.clientTask),
m': Replica.(s.repInputs + s.repTask) |
m'.stamp.ref = m.stamp.ref => trace/lte [m'.stamp.tme, m.stamp.tme]
-- same as above for datastore writes
all c: Client, m: c.(s.clientTask), t: Timestamp |
( t in (s.writePending + s.writeSucceeded).Value
&& t.ref = m.stamp.ref )
=> lte [t.tme, m.stamp.tme]
-- if a client has a lockRef but no task, then all repInputs and repTasks
-- with the same lockRef are in the present or past
all c: Client, m: Replica.(s.repInputs + s.repTask) |
( some c.(s.clientRef) && no c.(s.clientTask)
&& m.stamp.ref = c.(s.clientRef) )
=> trace/lte [m.stamp.tme, s.time]
-- same as above for datastore writes
all c: Client, t: (s.writePending + s.writeSucceeded).Value |
( some c.(s.clientRef) && no c.(s.clientTask)
&& t.ref = c.(s.clientRef) )
=> trace/lte [t.tme, s.time]
-- across the global state, consistent pairings of timestamps and values
let msgPairings = { t: Timestamp, v: Value |
some m: ClientPutMsg + RepPutMsg |
( m in Client.(s.clientTaskopen util/ordering [LockRef] as queue

TEMPORAL STRUCTURE

Note that if time has a scope of x, there will be exactly x times and
x-1 real events.