Skip to content

Instantly share code, notes, and snippets.

@parlarjb

parlarjb/deployment

Created June 1, 2017 20:47
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save parlarjb/f5c504b03b52cd5f99afa650574dc4b3 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save parlarjb/f5c504b03b52cd5f99afa650574dc4b3 to your computer and use it in GitHub Desktop.
Download ZIP

Revisions

  1. parlarjb created this gist Jun 1, 2017.
    72 changes: 72 additions & 0 deletions deployment
    View file
    Original file line number Diff line number Diff line change
    @@ -0,0 +1,72 @@
    ---------------------------- 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; *)