-
Notifications
You must be signed in to change notification settings - Fork 0
/
CJupiter.tla
77 lines (67 loc) · 2.51 KB
/
CJupiter.tla
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
------------------------------ MODULE CJupiter ------------------------------
(*
Specification of CJupiter; see Wei@OPODIS'2018.
*)
EXTENDS JupiterSerial, GraphStateSpace
-----------------------------------------------------------------------------
VARIABLES
css \* css[r]: the n-ary ordered state space at replica r \in Replica
vars == <<intVars, ctxVars, serialVars, css>>
-----------------------------------------------------------------------------
TypeOK ==
/\ TypeOKInt
/\ TypeOKCtx
/\ TypeOKSerial
/\ \A r \in Replica: IsSS(css[r])
-----------------------------------------------------------------------------
Init ==
/\ InitInt
/\ InitCtx
/\ InitSerial
/\ css = [r \in Replica |-> EmptySS]
-----------------------------------------------------------------------------
NextEdge(r, u, ss) == \* Return the first outgoing edge from u in ss at replica r
CHOOSE e \in ss.edge:
/\e.from = u
/\\A ue \in ss.edge \ {e}:
(ue.from = u) => tb(e.cop.oid, ue.cop.oid, serial[r])
Perform(r, cop) ==
LET xform == xForm(NextEdge, r, cop, css[r]) \* xform: [xcop, xss, lss]
IN /\ css' = [css EXCEPT ![r] = @ (+) xform.xss]
/\ SetNewAop(r, xform.xcop.op)
ClientPerform(c, cop) == Perform(c, cop)
ServerPerform(cop) ==
/\ Perform(Server, cop)
/\ Comm!SSendSame(ClientOf(cop), cop) \* broadcast the original cop
-----------------------------------------------------------------------------
DoOp(c, op) ==
LET cop == [op |-> op, oid |-> [c |-> c, seq |-> cseq[c]], ctx |-> ds[c]]
IN /\ ClientPerform(c, cop)
/\ Comm!CSend(cop)
Do(c) ==
/\ DoInt(DoOp, c)
/\ DoCtx(c)
/\ DoSerial(c)
Rev(c) ==
/\ RevInt(ClientPerform, c)
/\ RevCtx(c)
/\ RevSerial(c)
SRev ==
/\ SRevInt(ServerPerform)
/\ SRevCtx
/\ SRevSerial
-----------------------------------------------------------------------------
Next ==
\/ \E c \in Client: Do(c) \/ Rev(c)
\/ SRev
Fairness ==
WF_vars(SRev \/ \E c \in Client: Rev(c))
Spec == Init /\ [][Next]_vars \* /\ Fairness
-----------------------------------------------------------------------------
Compactness == \* Compactness of CJupiter: the CSSes at all replicas are the same.
Comm!EmptyChannel => Cardinality(Range(css)) = 1
THEOREM Spec => []Compactness
=============================================================================
\* Modification History
\* Last modified Tue Feb 05 11:07:47 CST 2019 by hengxin
\* Created Sat Sep 01 11:08:00 CST 2018 by hengxin