162 lines
No EOL
6.3 KiB
Text
162 lines
No EOL
6.3 KiB
Text
NUM_CLIENTS = 4
|
|
NUM_DB_STATES = 10
|
|
CLIENTS = {0..NUM_CLIENTS-1}
|
|
TIMES = {0..NUM_DB_STATES-1}
|
|
|
|
channel save:CLIENTS
|
|
channel render:CLIENTS.TIMES
|
|
channel up:CLIENTS.TIMES
|
|
channel down:CLIENTS.TIMES
|
|
channel saved:CLIENTS.TIMES
|
|
channel report_queue:CLIENTS.TIMES
|
|
|
|
next_t(t) = (t + 1) % NUM_DB_STATES
|
|
|
|
CLIENT(i, t) =
|
|
up!i!t -> CLIENT'(i, t)
|
|
[] CLIENT'(i, t)
|
|
|
|
CLIENT'(i, t) =
|
|
down!i?server_t
|
|
-> render!i!server_t
|
|
-> CLIENT(i, server_t)
|
|
|
|
SERVER(i, client_t) =
|
|
up!i?server_t
|
|
-> save!i
|
|
-> saved!i?new_server_t
|
|
-> down!i!new_server_t
|
|
-> SERVER(i, new_server_t)
|
|
[] report_queue?j:diff(CLIENTS,{i})?new_server_t
|
|
-> if new_server_t == client_t
|
|
then SERVER(i, client_t)
|
|
else down!i!new_server_t
|
|
-> SERVER(i, new_server_t)
|
|
|
|
DB(t) =
|
|
save?i
|
|
-> saved!i!next_t(t)
|
|
-> DB(next_t(t))
|
|
|
|
REPORTQUEUE(i) =
|
|
saved?j:diff(CLIENTS,{i})?t
|
|
-> REPORTQUEUE'(i, j, t)
|
|
REPORTQUEUE'(i, j, t) =
|
|
saved?j':diff(CLIENTS,{i})?new_t
|
|
-> REPORTQUEUE'(i, j', new_t)
|
|
[] report_queue!j!t -> REPORTQUEUE(i)
|
|
|
|
SERVER_WITH_REPORTS(i, t0) = (SERVER(i, t0) [|{| report_queue |}|] REPORTQUEUE(i))
|
|
CONN(i, t0) = CLIENT(i, t0) [|{| up.i, down.i |}|] SERVER_WITH_REPORTS(i, t0)
|
|
CONNS(t0) = [| productions(saved) |] i:CLIENTS @ CONN(i, t0)
|
|
SYSTEM = DB(0) [|{| save, saved |}|] CONNS(0)
|
|
|
|
-----------------------------------------
|
|
-- Assertions
|
|
-----------------------------------------
|
|
|
|
assert SYSTEM :[deadlock free [F]]
|
|
assert SYSTEM :[divergence-free]
|
|
|
|
-----------------------------------------
|
|
-- One way sync: changes on one client will sync to other client
|
|
-----------------------------------------
|
|
|
|
-- Suppose we limit our implementation to say that each
|
|
-- user makes a finite number of changes n.
|
|
MaxInputs(0) = SKIP
|
|
MaxInputs(n) = up?i?t -> MaxInputs(n-1)
|
|
|
|
-- Suppose we limit inputs to client 0.
|
|
|
|
OnlyClient(i) = up!i?t -> OnlyClient(i)
|
|
ClientZeroInput = OnlyClient(0) [|{| up |}|] SYSTEM
|
|
|
|
OneInputFromClientZero = (OnlyClient(0) [|{| up |}|] MaxInputs(1)) [|{| up |}|] SYSTEM
|
|
|
|
-- Now we show that a change on client 0 will make it to client 1.
|
|
|
|
SyncOneInput = up.0.0 -> render.1.1 -> STOP
|
|
assert SyncOneInput [FD= OneInputFromClientZero \diff(Events, union(productions(up.0), {render.1.1}))
|
|
|
|
-- Expanding on this: what if we have two changes? We just care that, eventually, both of them get synced.
|
|
SyncTwoInputs = up.0.0 -> up.0.1 -> render.1.2 -> STOP
|
|
|
|
assert SyncTwoInputs [FD= (ClientZeroInput [|{| up |}|] MaxInputs(2)) \diff(Events, union(productions(up.0), {render.1.2}))
|
|
|
|
-- Can we do this for an arbitrary n changes?
|
|
OneWaySync(n) = up.0.0 -> OneWaySync'(n, n-1)
|
|
OneWaySync'(n, 0) = render.1.n -> STOP
|
|
OneWaySync'(n, i) = up.0.n-i -> OneWaySync'(n, i-1)
|
|
|
|
OneSideInputs(n) = (ClientZeroInput [|{| up |}|] MaxInputs(n)) \diff(Events, union(productions(up.0), {render.1.n}))
|
|
|
|
assert OneWaySync(1) [FD= OneSideInputs(1)
|
|
assert OneWaySync(9) [FD= OneSideInputs(9)
|
|
|
|
-----------------------------------------
|
|
-- Two way sync: changes on both clients will sync to both
|
|
-----------------------------------------
|
|
|
|
-- Start simple.
|
|
-- Let's just constrain our system to say, first client 0 does a change then client 1 does a change.
|
|
|
|
AlternateInputs = up.0.0 -> up.1?t -> STOP
|
|
|
|
-- Then our specification becomes simple. If client 0 inputs something then client one inputs something, at some point both should call render with the state after both changes hit the database (t=2).
|
|
TwoWaySync = up.0.0 -> ((up.1.0 -> TwoWaySyncRender) |~|
|
|
(up.1.1 -> TwoWaySyncRender))
|
|
TwoWaySyncRender = ((render.0.2 -> render.1.2 -> STOP) |~|
|
|
(render.1.2 -> render.0.2 -> STOP))
|
|
|
|
assert TwoWaySync [FD= (SYSTEM [|{| up |}|] AlternateInputs) \diff(Events, union(union(productions(up.0), productions(up.1)), {render.0.2, render.1.2}))
|
|
|
|
-- Let's extend this to an arbitrary number of inputs from either client (we don't care which). In the end we expect both to render the same DB state.
|
|
-- This is basically the general specification for eventual consistency. We are saying that supposing n finite inputs
|
|
-- from either client, eventually both of the clients get in sync and then stop.
|
|
|
|
Sync(n) = (up.0.0 -> Sync'(n, n-1)) |~| (up.1.0 -> Sync'(n, n-1))
|
|
Sync'(n, 0) = (render.0.n -> render.1.n -> STOP) |~| (render.1.n -> render.0.n -> STOP)
|
|
Sync'(n, m) = |~| i:CLIENTS, t:TIMES @ up!i!t -> Sync'(n, m-1)
|
|
|
|
assert Sync(5) [FD= (SYSTEM [|{| up |}|] MaxInputs(5)) \diff(Events, union(productions(up), {render.0.5, render.1.5}))
|
|
|
|
-----------------------------------------
|
|
-- 3 way sync: changes on 3 clients will sync to all
|
|
-----------------------------------------
|
|
|
|
-- Can we extend our previous result to 3 clients?
|
|
|
|
SyncThree(n) = |~| i:CLIENTS @ up!i!0 -> SyncThree'(n, n-1)
|
|
SyncThree'(n, 0) =
|
|
(render.0.n -> render.1.n -> render.2.n -> STOP) |~|
|
|
(render.0.n -> render.2.n -> render.1.n -> STOP) |~|
|
|
(render.1.n -> render.0.n -> render.2.n -> STOP) |~|
|
|
(render.1.n -> render.2.n -> render.0.n -> STOP) |~|
|
|
(render.2.n -> render.0.n -> render.1.n -> STOP) |~|
|
|
(render.2.n -> render.1.n -> render.0.n -> STOP)
|
|
SyncThree'(n, m) = |~| i:CLIENTS, t:TIMES @ up!i!t -> SyncThree'(n, m-1)
|
|
|
|
MaxInputSystem(n) = SYSTEM [|{| up |}|] MaxInputs(n)
|
|
assert SyncThree(5) [FD= MaxInputSystem(5) \diff(Events, union(productions(up), {render.i.5 | i <- CLIENTS}))
|
|
|
|
-----------------------------------------
|
|
-- N way sync: changes on n clients will sync to all
|
|
-----------------------------------------
|
|
|
|
sequences({}) = {<>}
|
|
sequences(a) = {<z>^z' | z <- a, z' <- sequences(diff(a, {z}))}
|
|
|
|
renderAll(sequence, t) = ; i:sequence @ render!i.t -> SKIP
|
|
|
|
SyncAll(n) = |~| i:CLIENTS @ up!i!0 -> SyncAll'(n, n-1)
|
|
SyncAll'(n, 0) = |~| renderSeq:sequences(CLIENTS) @ renderAll(renderSeq, n); STOP
|
|
SyncAll'(n, m) = |~| i:CLIENTS, t:TIMES @ up!i!t -> SyncAll'(n, m-1)
|
|
|
|
-- Number of changes allowed: 1, 5, 9
|
|
assert SyncAll(1) [FD= MaxInputSystem(1) \diff(Events, union(productions(up), {render.i.1 | i <- CLIENTS}))
|
|
assert SyncAll(5) [FD= MaxInputSystem(5) \diff(Events, union(productions(up), {render.i.5 | i <- CLIENTS}))
|
|
assert SyncAll(9) [FD= MaxInputSystem(9) \diff(Events, union(productions(up), {render.i.9 | i <- CLIENTS}))
|
|
|
|
-- This proves that given n clients, if we restrict them to x inputs total from any client in any order, eventually all n clients will render the same state i.e. they will be in sync.
|
|
-- Note that this doesn't say anything about timing other except that eventually it will happen. |