michael/grub-fork
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

Buffers - Add a client-side download buffer as well

Browse source 
--> No deadlock but state explosion. Not sure if syncing still works.
This commit is contained in:
Nicholas Kariniemi 2015-08-26 22:21:40 +03:00
parent e47f79ac7b
commit 432ee48162
1 changed files with 12 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
csp/sync.csp
View file

@ -2,7 +2,9 @@ N = 2
S = 3 S = 3
CLIENTS = {0..N-1} CLIENTS = {0..N-1}
STATES = {0..S-1} STATES = {0..S-1}
channel input, render, up, down, save, saved, bufsave, bufsaved:CLIENTS.STATES PATCHES = {0..S-1}
channel input, render, saved, bufsaved:CLIENTS.STATES
channel up, down, save, bufdown:CLIENTS.PATCHES
apply(state, patch) = (state + patch) % S apply(state, patch) = (state + patch) % S
diffS(state1, state2) = (state2 - state1) % S diffS(state1, state2) = (state2 - state1) % S
@ -14,7 +16,7 @@ CLIENT(i, state, shadow) =
-> CLIENT'(i, new_state, shadow) -> CLIENT'(i, new_state, shadow)
[] CLIENT'(i, state, shadow) [] CLIENT'(i, state, shadow)
CLIENT'(i, state, shadow) = down!i?patch CLIENT'(i, state, shadow) = bufdown!i?patch
-> if empty(patch) -> if empty(patch)
then CLIENT(i, state, state) then CLIENT(i, state, state)
else else
@ -25,6 +27,10 @@ CLIENT'(i, state, shadow) = down!i?patch
-> CLIENT(i, apply(state, patch), apply(shadow, patch)) -> CLIENT(i, apply(state, patch), apply(shadow, patch))
else CLIENT(i, apply(state, patch), apply(shadow, patch)) else CLIENT(i, apply(state, patch), apply(shadow, patch))
DOWNBUF(i) = down!i?patch -> DOWNBUF'(i, patch)
DOWNBUF'(i, patch) = down!i?patch' -> DOWNBUF'(i, patch')
[] bufdown!i!patch -> DOWNBUF(i)
SERVER(i, shadow) = SERVER(i, shadow) =
up!i?patch up!i?patch
-> save!i!patch -> save!i!patch
@ -36,16 +42,15 @@ SERVER(i, shadow) =
then SERVER(i, shadow) then SERVER(i, shadow)
else down!i!diffS(shadow, new_state) -> SERVER(i, new_state) else down!i!diffS(shadow, new_state) -> SERVER(i, new_state)
BUF(i) = saved?j:diff(CLIENTS,{i})?new_state -> BUF'(i, j, new_state) SAVEDBUF(i) = saved?j:diff(CLIENTS,{i})?new_state -> SAVEDBUF'(i, j, new_state)
BUF'(i, j, new_state) = saved?j':diff(CLIENTS,{i})?new_state' -> BUF'(i, j', new_state') SAVEDBUF'(i, j, new_state) = saved?j':diff(CLIENTS,{i})?new_state' -> SAVEDBUF'(i, j', new_state')
[] bufsaved!j!new_state -> BUF(i) [] bufsaved!j!new_state -> SAVEDBUF(i)
DB(state) = save?i?patch DB(state) = save?i?patch
-> saved!i!apply(state, patch) -> saved!i!apply(state, patch)
-> DB(apply(state, patch)) -> DB(apply(state, patch))
CONN(i, init) = (CLIENT(i, init, init) [|{| up.i, down.i |}|] SERVER(i, init)) [|{| bufsaved |}|] BUF(i) CONN(i, init) = (CLIENT(i, init, init) [|{| bufdown.i |}|] DOWNBUF(i)) [|{| up.i, down.i |}|] (SERVER(i, init) [|{| bufsaved |}|] SAVEDBUF(i))
SYSTEM = (CONN(0,0) [|{| save.0, saved |}|] DB(0)) [|{| save.1, saved |}|] CONN(1,0) SYSTEM = (CONN(0,0) [|{| save.0, saved |}|] DB(0)) [|{| save.1, saved |}|] CONN(1,0)
assert SYSTEM :[deadlock free [F]] assert SYSTEM :[deadlock free [F]]
@ -103,7 +108,6 @@ SYNC'(state0, state1) =
[] down?a?b -> SYNC'(state0, state1) [] down?a?b -> SYNC'(state0, state1)
[] save?a?b -> SYNC'(state0, state1) [] save?a?b -> SYNC'(state0, state1)
[] saved?a?b -> SYNC'(state0, state1) [] saved?a?b -> SYNC'(state0, state1)
[] bufsave?a?b -> SYNC'(state0, state1)
[] bufsaved?a?b -> SYNC'(state0, state1) [] bufsaved?a?b -> SYNC'(state0, state1)
--[] e:diff(Events, {sync}) @ e -> SYNC'(state0, state1) --[] e:diff(Events, {sync}) @ e -> SYNC'(state0, state1)