Skip to content
Permalink
master
Switch branches/tags

Name already in use

A tag already exists with the provided branch name. Many Git commands accept both tag and branch names, so creating this branch may cause unexpected behavior. Are you sure you want to create this branch?
Go to file
 
 
Cannot retrieve contributors at this time
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.