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

Force processes to synchronize on communication

Browse source 
Use parallel operation || instead of the (unsynchronized) interleave
	operation |||.
This commit is contained in:
Nicholas Kariniemi 2015-08-15 18:18:04 +03:00
parent 1b99e49563
commit 9f32a03d04
1 changed files with 7 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
csp/sync.csp
View file

@ -9,10 +9,10 @@ diff(state1, state2) = (state2 - state1) % S
empty(patch) = patch == 0 empty(patch) = patch == 0
CLIENT(i, state, shadow) = CLIENT(i, state, shadow) =
input.i?new_state input!i?new_state
-> up!i!diff(shadow, new_state) -> up!i!diff(shadow, new_state)
-> CLIENT(i, new_state, shadow) -> CLIENT(i, new_state, shadow)
[] down.i?patch [] down!i?patch
-> if empty(patch) -> if empty(patch)
then CLIENT(i, state, state) then CLIENT(i, state, state)
else else
@ -26,9 +26,9 @@ CLIENT(i, state, shadow) =
-> CLIENT(i, apply(state, patch), apply(shadow, patch)) -> CLIENT(i, apply(state, patch), apply(shadow, patch))
SERVER(i, shadow) = SERVER(i, shadow) =
up.i?patch up!i?patch
-> save!i!patch -> save!i!patch
-> saved.i?new_state -> saved!i?new_state
-> down!i!diff(apply(shadow, patch), new_state) -> down!i!diff(apply(shadow, patch), new_state)
-> SERVER(i, apply(shadow, patch)) -> SERVER(i, apply(shadow, patch))
[] saved?j?new_state [] saved?j?new_state
@ -38,11 +38,8 @@ SERVER(i, shadow) =
DB(state) = save?i?patch -> saved!i!apply(state, patch) -> DB(apply(state, patch)) DB(state) = save?i?patch -> saved!i!apply(state, patch) -> DB(apply(state, patch))
state = 0 CONN(i, init) = (CLIENT(i, init, init) [|{| up.i, down.i |}|] SERVER(i, init)) [|{| save, saved |}|] DB(init)
SYSTEM = CLIENT(0, state, state)
||| CLIENT(1, state, state) SYSTEM = CONN(0,0) ||| CONN(1,0)
||| SERVER(0, state)
||| SERVER(1, state)
||| DB(state)
assert SYSTEM :[deadlock free [F]] assert SYSTEM :[deadlock free [F]]