deployment

---------------------------- MODULE Deployments ----------------------------
EXTENDS TLC, Integers

CONSTANT UPDATING, CORRUPT, ABORTED
CONSTANT SKIP_UPDATE

(* --algorithm deploy

variables servers = {"s1", "s2", "s3"},
          load_balancer = servers,
          update_flag = [s \in servers |-> FALSE],
            updated = [s \in servers |-> FALSE],
            hero \in servers;

define
  ZeroDowntime ==
    \E server \in load_balancer:
      updated[server] \notin {UPDATING, CORRUPT}
      
  SameVersion ==
    \A x,y \in load_balancer:
      updated[x] = updated[y]
      
  DeployComplete == (\A p \in DOMAIN pc: pc[p] = "Done") => \/ load_balancer = servers
                                                            \/ \A s \in servers \ load_balancer: updated[s] = CORRUPT
end define;

fair process update_server \in servers
begin 
 Update:
  await ((update_flag[self]=TRUE) \/ (update_flag[self] = SKIP_UPDATE));
  updated[self] := IF update_flag[self]=TRUE THEN UPDATING
  ELSE ABORTED;
  
 FinishUpdate:
   either await updated[self] = UPDATING; 
    Assign:
     with state \in {CORRUPT, TRUE} do
       updated[self] := state;
     end with;
   or await updated[self] = ABORTED; skip
   end either;
end process;

fair process start_update = "start_update"
  variable candidate_lb
  begin 
   StartUpdate:
     load_balancer := {hero};
     update_flag := [s \in servers |-> 
      IF s = hero THEN FALSE ELSE TRUE];

   Transition:
     await \A s \in (servers \ load_balancer): 
       updated[s] \in {TRUE, CORRUPT};
     candidate_lb := {x \in (servers \ load_balancer) : updated[x] = TRUE};
     
     load_balancer := IF candidate_lb /= {} THEN candidate_lb 
                  ELSE load_balancer;
     
     update_flag[hero] := IF load_balancer /= {hero} THEN TRUE 
                            ELSE SKIP_UPDATE;
   Finish:
     await updated[hero] \in {TRUE, CORRUPT, ABORTED};
     load_balancer := load_balancer \union IF updated[hero] \in {TRUE, ABORTED} THEN {hero} ELSE {};


end process;



end algorithm; *)

BAM https://docs.google.com/document/d/1SrA0aE9qZ3KpDiY4Q6EQzkSbY7qNmmqcQHYaP9Cgyok/

Comments in gdoc comments. Let me know if you can't see them.

@hwayne he's a coworker of mine, he was just leaving a note for future reference :)

I'm not able to see any Google Docs comment, I might need edit permissions