From 52af4dfd68b087552496d8118e6dc0698ae0a80c Mon Sep 17 00:00:00 2001 From: Nicholas Kariniemi Date: Wed, 26 Aug 2015 21:35:22 +0300 Subject: [PATCH] Buffers - wip --- csp/sync.csp | 83 ++++++++++++++++++++++++++++++++++++++++++++-------- 1 file changed, 71 insertions(+), 12 deletions(-) diff --git a/csp/sync.csp b/csp/sync.csp index c1852c5..3303e16 100644 --- a/csp/sync.csp +++ b/csp/sync.csp @@ -5,23 +5,23 @@ STATES = {0..S-1} channel input, render, up, down, save, saved, bufsave, bufsaved:CLIENTS.STATES apply(state, patch) = (state + patch) % S -diff(state1, state2) = (state2 - state1) % S +diffS(state1, state2) = (state2 - state1) % S empty(patch) = patch == 0 CLIENT(i, state, shadow) = - input!i?new_state - -> up!i!diff(shadow, new_state) - -> CLIENT'(i, state, shadow) + input!i?new_state:diff(STATES,{state}) + -> up!i!diffS(shadow, new_state) + -> CLIENT'(i, new_state, shadow) [] CLIENT'(i, state, shadow) CLIENT'(i, state, shadow) = down!i?patch -> if empty(patch) then CLIENT(i, state, state) else - if diff(apply(shadow, patch), apply(state, patch)) != 0 + if diffS(apply(shadow, patch), apply(state, patch)) != 0 then render!i!apply(state, patch) - -> up!i!diff(apply(shadow, patch), apply(state, patch)) + -> up!i!diffS(apply(shadow, patch), apply(state, patch)) -> CLIENT(i, apply(state, patch), apply(shadow, patch)) else render!i!apply(state, patch) @@ -30,13 +30,13 @@ CLIENT'(i, state, shadow) = down!i?patch SERVER(i, shadow) = up!i?patch -> save!i!patch - -> bufsaved!i?new_state - -> down!i!diff(apply(shadow, patch), new_state) + -> saved!i?new_state + -> down!i!diffS(apply(shadow, patch), new_state) -> SERVER(i, apply(shadow, patch)) [] bufsaved?j?new_state -> if (new_state == shadow) then SERVER(i, shadow) - else down!i!diff(shadow, new_state) -> SERVER(i, new_state) + else down!i!diffS(shadow, new_state) -> SERVER(i, new_state) BUF(i) = saved?j?new_state -> BUF'(i, j, new_state) BUF'(i, j, new_state) = saved?j'?new_state' -> BUF'(i, j', new_state') @@ -46,10 +46,69 @@ DB(state) = save?i?patch -> saved!i!apply(state, patch) -> DB(apply(state, patch)) -DBB = DB(0) - CONN(i, init) = (CLIENT(i, init, init) [|{| up.i, down.i |}|] SERVER(i, init)) [|{| bufsaved |}|] BUF(i) SYSTEM = (CONN(0,0) [|{| save.0, saved |}|] DB(0)) [|{| save.1, saved |}|] CONN(1,0) -assert SYSTEM :[deadlock free [F]] \ No newline at end of file +assert SYSTEM :[deadlock free [F]] +assert SYSTEM :[divergence-free] + +-- Suppose that there are a finite number n of inputs. +-- I.e. users click around and then, at some point, after +-- n actions. +LimitedInputs(0) = STOP +LimitedInputs(n) = input?i?state -> LimitedInputs(n-1) + +-- For instance, maybe only 3 actions occur. +LimitedSystem = LimitedInputs(3) [|{| input |}|] SYSTEM + +-- If we look only at render events on each side +channel rend:STATES +Rends = render?i?state -> rend!state -> Rends +RendersLeft = (LimitedSystem [|{| render |}|] Rends) \diff(Events, productions(rend)) +RendersRight = LimitedSystem \diff(Events, productions(render.1)) [|{| render |}|] Rends + +-- Then (for any chosen n) the final event on both side +-- should be a render of the same final state s +-- i.e. the final events are render.0.s and render.1.s +-- for some s. + +-- Can we specify this as a trace refinement? + +-- The trace of the renders of each side should look like this: +-- T^ +-- S^ + +-- What does it mean to say A [T= B? B trace-refines A i.e. traces(B) subset traces(A) +-- i.e. all possible traces of B occur within A + +-- What if we force each side to coordinate with a process that, when done, emits a certain render event and then stops. Like renderLeft, renderRight? +-- We could force it to behave in such a way that it can only stop if both render the same event at the same time. +-- And then assert that it stops and does not diverge? + +-- What does diverging mean again? + +-- assert SYSTEM [T= InputsLeftS +-- assert RendersLeft [T= RendersRight +-- assert RendersRight [T= RendersLeft + + +-- Suppose an event occurs every time the system is in sync. +-- Or, more simplified, every time the two clients are in sync (excluding the database). +channel sync +SYNC(state) = sync -> SYNC'(state, state) +SYNC'(state0, state1) = + render!0?state -> (if state == state1 then sync -> SYNC'(state, state) else SYNC'(state, state1)) +[] render!1?state -> (if state == state0 then sync -> SYNC'(state, state) else SYNC'(state0, state)) +[] input?a?b -> SYNC'(state0, state1) +[] up?a?b -> SYNC'(state0, state1) +[] down?a?b -> SYNC'(state0, state1) +[] save?a?b -> SYNC'(state0, state1) +[] saved?a?b -> SYNC'(state0, state1) +[] bufsave?a?b -> SYNC'(state0, state1) +[] bufsaved?a?b -> SYNC'(state0, state1) + +--[] e:diff(Events, {sync}) @ e -> SYNC'(state0, state1) +--DoNothingOnNonSyncEvents = [] e:diff(Events, {sync}) @ e -> DoNothingOnNonSyncEvents + +SyncSystem = SYSTEM [| diff(Events, {sync}) |] SYNC(0) \ No newline at end of file