grogers0

FiniteSeq(S) == UNION {[1..n -> S] : n \in 1..Cardinality(S)}
SeqAsSet(S) == {S[i] : i \in DOMAIN S}

HistoryIsLinearizable == \E order \in {<<>>} \union FiniteSeq(Timestamps) :
    /\ \A H \in SeqAsSet(history) : H.type = "response" => H.ts \in SeqAsSet(order)
    /\ \A H1_i, H2_i \in DOMAIN history :
        (history[H1_i].type = "response" /\ history[H2_i].type = "invoke" /\ H1_i < H2_i) =>
            (
                history[H2_i].ts \in SeqAsSet(order) =>
                    \E i1, i2 \in DOMAIN order :

grogers0

Accepted(ts) == /\ {m.acceptor : m \in SelectMessages("accepted", ts)} \in Quorums
                /\ {hpos \in DOMAIN history : history[hpos] = [type |-> "response", ts |-> ts]} = {}
                /\ history' = Append(history, [type |-> "response", ts |-> ts])
                /\ UNCHANGED <<msgs, ops, acceptorTS, acceptorValTS, acceptorValue>>

grogers0

RecvAccept(a, ts, v) == /\ acceptorTS[a] = ts
                        /\ acceptorValTS' = [acceptorValTS EXCEPT ![a] = ts]
                        /\ acceptorValue' = [acceptorValue EXCEPT ![a] = v]
                        /\ msgs' = msgs \union [type: {"accepted"}, acceptor: {a}, ts: {ts}, val: {v}]
                        /\ UNCHANGED <<ops, acceptorTS, history>>

grogers0

PromisedValue(ts) == LET promiseMsgs == SelectMessages("promise", ts)
                     IN (CHOOSE m \in promiseMsgs : \A m2 \in promiseMsgs : m.prevTS >= m2.prevTS).prevVal

Accept(ts) == /\ {m.acceptor : m \in SelectMessages("promise", ts)} \in Quorums
              /\ ops[ts].oldVal = PromisedValue(ts)
              /\ msgs' = msgs \union [type: {"accept"}, acceptor: Acceptors, ts: {ts}, val: {ops[ts].newVal}]
              /\ UNCHANGED <<ops, acceptorTS, acceptorValTS, acceptorValue, history>>

grogers0

RecvPrepare(a, ts) == /\ acceptorTS[a] = NoTS \/ acceptorTS[a] < ts
                      /\ acceptorTS' = [acceptorTS EXCEPT ![a] = ts]
                      /\ msgs' = msgs \union {[type |-> "promise", acceptor |-> a, ts |-> ts,
                                               prevTS |-> acceptorValTS[a], prevVal |-> acceptorValue[a]]}
                      /\ UNCHANGED <<ops, acceptorValTS, acceptorValue, history>>

grogers0

SelectMessages(type, ts) == {m \in msgs : m.type = type /\ m.ts = ts}

Prepare(ts) == /\ SelectMessages("prepare", ts) = {} \* Each timestamp must be unique
               /\ msgs' = msgs \union [type: {"prepare"}, acceptor: Acceptors, ts: {ts}]
               /\ history' = Append(history, [type |-> "invoke", ts |-> ts])
               /\ UNCHANGED <<ops, acceptorTS, acceptorValTS, acceptorValue>>

grogers0

Next == \/ \E ts \in Timestamps : \/ Prepare(ts)
                                  \/ Accept(ts)
                                  \/ Accepted(ts)
        \/ \E m \in msgs : \/ m.type = "prepare" /\ RecvPrepare(m.acceptor, m.ts)
                           \/ m.type = "accept" /\ RecvAccept(m.acceptor, m.ts, m.val)

grogers0

Messages == [type: {"prepare"}, acceptor: Acceptors, ts: Timestamps]
     \union [type: {"promise"}, acceptor: Acceptors, ts: Timestamps,
             prevTS: Timestamps \union {NoTS}, prevVal: Values]
     \union [type: {"accept"}, acceptor: Acceptors, ts: Timestamps, val: Values]
     \union [type: {"accepted"}, acceptor: Acceptors, ts: Timestamps, val: Values]
\* Each operation represents a CAS from an oldVal to a newVal. In Gryadka,
\*     reads are treated the same as CAS(val, val)
Operations == [oldVal: Values, newVal: Values]
Events == [type: {"invoke", "response"}, ts: Timestamps]

grogers0

\* msgs is the buffer of all messages. Messages can be delivered out of order or duplicated.
\* ops is the mapping from timestamp to CAS(old, new) for operations being proposed.
\* acceptorTS is the timestamp each acceptor is prepared for, only operations which match this value are accepted.
\* acceptorValTS is the timestamp of the last accepted value for each acceptor, or NoTS is none has been accepted yet.
\* acceptorValue is the last accepted value for each acceptor, or InitVal if none has been accepted yet.
\* history is the actual order of invoke/response actions for the operations identified by the timestamp.
VARIABLES msgs, ops, acceptorTS, acceptorValTS, acceptorValue, history

grogers0

\* Timestamps is the set of possible timestamps for operations to choose from.
\*     Each operation uses a unique timestamp.
\* Values is the set of possible values to set the register to.
\* Acceptors is the set of nodes which act as acceptors in the paxos sense.
\* Quorums is the set of all possible quorums, typically simple majorities.
CONSTANTS Timestamps, Values, Acceptors, Quorums

ASSUME Timestamps \subseteq Nat
ASSUME IsFiniteSet(Timestamps)
NoTS == -1