Skip to content

Instantly share code, notes, and snippets.

@aquarhead
Created June 1, 2021 14:53
Show Gist options
  • Save aquarhead/0460115d36b2e34604b8bfb904cf289e to your computer and use it in GitHub Desktop.
Save aquarhead/0460115d36b2e34604b8bfb904cf289e to your computer and use it in GitHub Desktop.
SPECIFICATION Spec
\* Add statements after this line.
CONSTANTS
OUTDATED = "outdated"
UPDATING = "updating"
UPDATED = "updated"
INVARIANTS
SameVersion
ZeroDowntime
AllUpdated
---- MODULE zerodt ----
EXTENDS TLC, Integers
CONSTANTS OUTDATED, UPDATING, UPDATED
(* --algorithm deploy
variables
servers = {"s1", "s2", "s3"},
load_balancer = servers,
can_update = [s \in servers |-> FALSE],
state = [s \in servers |-> OUTDATED];
define
SameVersion ==
\A x, y \in load_balancer:
state[x] = state[y]
ZeroDowntime ==
\E server \in load_balancer:
state[server] /= UPDATING
AllUpdated ==
(\A p \in DOMAIN pc: pc[p] = "Done") => load_balancer = servers
end define;
fair process update_server \in servers
begin
Update:
await can_update[self];
state[self] := UPDATING;
FinishUpdate:
state[self] := UPDATED;
end process;
fair process start_update = "start_update"
begin
StartUpdate:
load_balancer := {"s1"};
can_update := [s \in servers |->
IF s = "s1" THEN FALSE ELSE TRUE];
Transition:
await \A s \in (servers \ load_balancer):
state[s] = UPDATED;
load_balancer := servers \ load_balancer;
can_update["s1"] := TRUE;
Finish:
await state["s1"] = UPDATED;
load_balancer := load_balancer \union {"s1"};
end process;
end algorithm *)
====
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment