Skip to content

Instantly share code, notes, and snippets.

@seansu4you87

seansu4you87/VitessDeadMasterRecovery2.tla

Created December 7, 2020 21:11
Show Gist options
  • Save seansu4you87/f2f84d239cba2f4eab947a178f1dbb96 to your computer and use it in GitHub Desktop.
Save seansu4you87/f2f84d239cba2f4eab947a178f1dbb96 to your computer and use it in GitHub Desktop.
Download ZIP
Vitess Dead Master Recovery
Raw
VitessDeadMasterRecovery2.tla
--------------------- MODULE VitessDeadMasterRecovery2 ---------------------
EXTENDS Integers, TLC, FiniteSets, Sequences
CONSTANTS NULL
\* Orc state machine
CONSTANTS ORC_RECV,
\* Send <disconnect_ssr, replica: 1> messages to replicas
\* - Replica should change ssr_master to NULL
\* - process_write_storage_request needs to response a NULL value in ssr_master
\* Wait for acks
ORC_DISCONNECT_REPLICA, ORC_WAIT_DISCONNECT_REPLICA,
ORC_READ_REPLICA, ORC_WAIT_READ_REPLICA,
ORC_BROADCAST, ORC_WAIT_BROADCAST,
ORC_WRITE_TOPO, ORC_WAIT_WRITE_TOPO,
ORC_FINISH
\* Topo state machine
CONSTANTS TOPO_RECV,
TOPO_NOTIFY
MasterIdx == 1
Replicas == 1..5
Vtgates == 51..52
Topo == 98
Orc == 99
Client == 100
DataValues == 0..5
IdSpace == 1..200
Messages ==
\* Vtgate messages
[rid: IdSpace, type: {"write_query_request"}, vtgate: Vtgates, value: DataValues]
\union [rid: IdSpace, type: {"write_query_response"}, value: DataValues, err: { TRUE, FALSE }]
\union [rid: IdSpace, type: {"read_query_request"}, vtgate: Vtgates]
\union [rid: IdSpace, type: {"read_query_response"}, value: DataValues]
\union [ type: {"topo_change"}, new_master: Replicas, listener: Vtgates]
\* Replica messages
\union [rid: IdSpace, type: {"write_storage_request"}, from: Vtgates, value: DataValues, replica: Replicas]
\union [rid: IdSpace, type: {"write_storage_response"}, caller: Vtgates, value: DataValues, err: { TRUE, FALSE }]
\union [rid: IdSpace, type: {"read_storage_request"}, from: Vtgates \union { Orc }, replica: Replicas]
\union [rid: IdSpace, type: {"read_storage_response"}, caller: Vtgates \union { Orc }, value: DataValues]
\union [rid: IdSpace, type: {"promote"}, new_master: Replicas, destination: Replicas]
\union [rid: IdSpace, type: {"disconnect_request"}, replica: Replicas]
\union [rid: IdSpace, type: {"disconnect_response"}, replica: Replicas, value: DataValues]
\* Orc messages
\union [ type: {"dmr"}]
\union [rid: IdSpace, type: {"promote_ack"}, new_master: Replicas]
\union [rid: IdSpace, type: {"write_topo_ack"}, new_master: Replicas]
\* Topo messages
\union [rid: IdSpace, type: {"write_topo"}, new_master: Replicas]
CreateReplica(i) == [
value |-> 0,
is_master |-> IF i = MasterIdx THEN TRUE ELSE FALSE,
current_master |-> MasterIdx
]
(**************************** pluscal dmr ********************************
--algorithm dmr {
variables \* Most recently send messages
AA_send_log = {},
\* Most recently received message
AA_recv_log = NULL,
\* All messages sent to the network
network = {
[type |-> "dmr"]
},
\* Processed messages
processed = {},
\* Values stored in Replicas
storage_value = [rid \in Replicas |-> 0],
\* Who each replica believes is the master right now
ssr_master = [rid \in Replicas |-> MasterIdx],
\* Who each vtgate believes is the master right now
vtgate_master = [vtgid \in Vtgates |-> MasterIdx]
define {
\* Need 2 or 3 of the replicas to agree on the master for an SSR write to take place
CanWrite(replica) == Cardinality({ rid \in Replicas : ssr_master[rid] = replica }) > 1
}
macro Send(m) {
AA_send_log := { m };
network := network \union AA_send_log;
}
macro BatchSend(ms) {
AA_send_log := ms;
network := network \union AA_send_log;
}
macro Process(m) {
AA_recv_log := m;
processed := processed \union { m };
}
macro Retry(m) {
Send(m);
}
\***************************************************************************
\* Client Macros
\***************************************************************************
macro step_through_test() {
when wait_rid = -1;
when step <= Len(test);
wait_rid := test[step].message.rid;
\* print <<"Sending ", test[step].message>>;
Send(test[step].message);
}
macro process_vtgate_read_response() {
with (m \in network) {
when m.type = "read_query_response";
when m \notin processed;
Process(m);
\* print <<"Received ", m>>;
\* NOTE(yu): assert that client and server are in agreement
assert m.value = test[step].expected;
wait_rid := -1;
step := step + 1;
}
}
macro process_vtgate_write_response_ok() {
with (m \in network) {
when m.type = "write_query_response" /\ ~m.err;
when m \notin processed;
Process(m);
\* print <<"Received ", m>>;
\* NOTE(yu): assert that client and server are in agreement
assert m.value = test[step].expected;
wait_rid := -1;
step := step + 1;
}
}
macro process_vtgate_write_response_err() {
with (m \in network) {
when m.type = "write_query_response" /\ m.err;
when m \notin processed;
\* TODO(yu): this is cheating a bit, but due to TLC's checking algorithm, need to
\* shortcircuit. TLC will discover the infinite loop first, before the
\* other kinds of errors.
\*
\* Also hard coded the vtgate lol, it is 52, because w1 is hardcoded to
\* always send to 52
when CanWrite(vtgate_master[52]);
Process(m);
\* Cheat by just adding 100 to the rid
wait_rid := test[step].message.rid + 100;
test[step].message.rid := wait_rid;
Retry(test[step].message);
}
}
macro finish_test() {
when step > Len(test);
\* print <<"TEST PASSED!">>;
\* NOTE(yu): This should eventually happen!
}
\***************************************************************************
\* Vtgate Macros
\***************************************************************************
macro process_read_query_request() {
with (m \in network) {
when m.type = "read_query_request" /\ m.vtgate = self;
when m \notin processed;
Process(m);
Send([
rid |-> m.rid,
type |-> "read_storage_request",
replica |-> vtgate_master[self],
from |-> self
]);
}
}
macro process_write_query_request() {
with (m \in network) {
when m.type = "write_query_request" /\ m.vtgate = self;
when m \notin processed;
Process(m);
Send([
rid |-> m.rid,
type |-> "write_storage_request",
value |-> m.value,
replica |-> vtgate_master[self],
from |-> self
]);
}
}
macro process_read_storage_response() {
with (m \in network) {
when m.type = "read_storage_response" /\ m.caller = self;
when m \notin processed;
Process(m);
Send([
rid |-> m.rid,
type |-> "read_query_response",
value |-> m.value
]);
}
}
macro process_write_storage_response() {
with (m \in network) {
when m.type = "write_storage_response" /\ m.caller = self;
when m \notin processed;
Process(m);
Send([
rid |-> m.rid,
type |-> "write_query_response",
value |-> m.value,
err |-> m.err
]);
}
}
macro process_topo_change() {
with (m \in network) {
when m.type = "topo_change" /\ m.listener = self;
when m \notin processed;
Process(m);
vtgate_master[self] := m.new_master;
}
}
\***************************************************************************
\* Replica Macros
\***************************************************************************
macro process_read_storage_request() {
with (m \in network) {
when m.type = "read_storage_request" /\ m.replica = self;
when m \notin processed;
Process(m);
\* NOTE(yu): Only read/write if you think you are the master!
\* Letting replicas who don't believe they're master to respond for now
\* - This allows to catch more interesting edge cases
\* - Instead of failing fast, we relax the reqs such that the client
\* just needs to have a consistent view
\*
\* Also I allow the the read request to be used to simulate a read_gtid response
\* out of laziness right now
\* assert ssr_master = self;
Send([
rid |-> m.rid,
type |-> "read_storage_response",
value |-> storage_value[self],
caller |-> m.from
]);
}
}
macro process_write_storage_request() {
with (m \in network) {
when m.type = "write_storage_request" /\ m.replica = self;
when m \notin processed;
Process(m);
\* storage_value[self] := m.value;
\* NOTE(yu): Simulate SSR by making everything synchronous
\* The replica receiving the write request will always change the value.
\* If ssr_master for other replicas point to self, then also change the value.
storage_value := IF CanWrite(self)
THEN
[rid \in Replicas |->
IF \/ rid = self
\/ ssr_master[rid] = self
THEN m.value
ELSE storage_value[rid]
]
ELSE
storage_value;
\* NOTE(yu): Only read/write if you think you are the master!
\* Letting replicas who don't believe they're master to respond for now
\* - This allows to catch more interesting edge cases
\* - Instead of failing fast, we relax the reqs such that the client
\* just needs to have a consistent view
\* assert ssr_master = self;
Send([
rid |-> m.rid,
type |-> "write_storage_response",
value |-> storage_value[self],
caller |-> m.from,
err |-> IF CanWrite(self) THEN FALSE ELSE TRUE
]);
}
}
macro process_promote() {
with (m \in network) {
when m.type = "promote" /\ m.destination = self;
when m \notin processed;
Process(m);
ssr_master[self] := m.new_master;
Send([
rid |-> m.rid,
type |-> "promote_ack",
new_master |-> ssr_master[self]
])
}
}
macro process_disconnect_request() {
with (m \in network) {
when m.type = "disconnect_request" /\ m.replica = self;
when m \notin processed;
Process(m);
ssr_master[self] := NULL;
Send([
rid |-> m.rid,
type |-> "disconnect_response",
replica |-> m.replica,
value |-> storage_value[self]
]);
}
}
\***************************************************************************
\* Orc Macros
\***************************************************************************
macro recv_dmr() {
when orc_state = ORC_RECV;
with (m \in network) {
when m.type = "dmr";
when m \notin processed;
Process(m);
orc_state := ORC_DISCONNECT_REPLICA;
orc_request := m;
}
}
macro disconnect_replicas() {
when orc_state = ORC_DISCONNECT_REPLICA;
disconnect_replicas_waitlist := { pid \in Replicas : pid # orc_master };
BatchSend({ [
rid |-> pid,
type |-> "disconnect_request",
replica |-> pid
] : pid \in disconnect_replicas_waitlist });
orc_state := ORC_WAIT_DISCONNECT_REPLICA;
}
macro wait_disconnect_replicas_ack() {
when orc_state = ORC_WAIT_DISCONNECT_REPLICA;
with (m \in network) {
when m.type = "disconnect_response";
when m \notin processed;
Process(m);
disconnect_replicas_waitlist := disconnect_replicas_waitlist \ { m.replica };
orc_state := IF Cardinality(disconnect_replicas_waitlist) > 0
THEN ORC_WAIT_DISCONNECT_REPLICA
ELSE ORC_READ_REPLICA;
}
}
macro read_replica_gtid() {
when orc_state = ORC_READ_REPLICA;
replica_gtid_ack_waitlist := { pid \in Replicas : pid # orc_master };
BatchSend({ [
rid |-> pid,
type |-> "read_storage_request",
from |-> self,
replica |-> pid
] : pid \in replica_gtid_ack_waitlist });
orc_state := ORC_WAIT_READ_REPLICA;
}
macro wait_replica_gtid_ack() {
when orc_state = ORC_WAIT_READ_REPLICA;
with (m \in network) {
when m.type = "read_storage_response" /\ m.caller = self;
when m \notin processed;
Process(m);
replica_gtid_ack_waitlist := replica_gtid_ack_waitlist \ { m.rid };
new_master_candidate_gtid := IF new_master_candidate_gtid = NULL \/ new_master_candidate_gtid < m.value
THEN m.value
ELSE new_master_candidate_gtid;
new_master_candidate := IF new_master_candidate_gtid = m.value
THEN m.rid
ELSE new_master_candidate;
orc_state := IF Cardinality(replica_gtid_ack_waitlist) > 0
THEN ORC_WAIT_READ_REPLICA
ELSE ORC_BROADCAST;
}
}
macro broadcast_promotion() {
when orc_state = ORC_BROADCAST;
promote_ack_waitlist := { pid \in Replicas : pid # orc_master };
BatchSend({ [
rid |-> pid,
type |-> "promote",
new_master |-> new_master_candidate,
destination |-> pid
] : pid \in promote_ack_waitlist });
orc_state := ORC_WAIT_BROADCAST;
}
macro wait_promotions_ack() {
when orc_state = ORC_WAIT_BROADCAST;
with (m \in network) {
when m.type = "promote_ack";
when m \notin processed;
Process(m);
promote_ack_waitlist := promote_ack_waitlist \ { m.rid };
orc_state := IF Cardinality(promote_ack_waitlist) > 0
THEN ORC_WAIT_BROADCAST
ELSE ORC_WRITE_TOPO;
}
}
macro write_topo() {
when orc_state = ORC_WRITE_TOPO;
Send([
rid |-> new_master_candidate,
type |-> "write_topo",
new_master |-> new_master_candidate
]);
orc_state := ORC_WAIT_WRITE_TOPO;
}
macro wait_write_topo_ack() {
when orc_state = ORC_WAIT_WRITE_TOPO;
with (m \in network) {
when m.type = "write_topo_ack";
when m \notin processed;
Process(m);
orc_master := new_master_candidate;
orc_state := ORC_FINISH;
}
}
macro finish_dmr() {
when orc_state = ORC_FINISH;
orc_request := NULL;
orc_state := ORC_RECV;
disconnect_replicas_waitlist := {};
replica_gtid_ack_waitlist := {};
new_master_candidate := NULL;
new_master_candidate_gtid := NULL;
promote_ack_waitlist := {};
\* TODO(yu): any other cleanup?
}
\***************************************************************************
\* Topo Macros
\***************************************************************************
macro recv_write_topo() {
when topo_state = TOPO_RECV;
with (m \in network) {
when m.type = "write_topo";
when m \notin processed;
Process(m);
topo_request := m;
topo_master := topo_request.new_master;
topo_state := TOPO_NOTIFY;
Send([
rid |-> topo_request.rid,
type |-> "write_topo_ack",
new_master |-> topo_master
]);
}
}
macro notify_topo_listeners() {
when topo_state = TOPO_NOTIFY;
BatchSend({ [
type |-> "topo_change",
new_master |-> topo_request.new_master,
listener |-> pid
] : pid \in Vtgates });
topo_request := NULL;
topo_state := TOPO_RECV;
}
\***************************************************************************
\* Processes
\***************************************************************************
process (client \in { Client })
variables step = 1,
wait_rid = -1,
r0 = [rid |-> 1, type |-> "read_query_request", vtgate |-> 51],
w1 = [rid |-> 2, type |-> "write_query_request", vtgate |-> 52, value |-> 1],
r1 = [rid |-> 3, type |-> "read_query_request", vtgate |-> 51],
test = <<
[message |-> r0, expected |-> 0],
[message |-> w1, expected |-> 1],
[message |-> r1, expected |-> 1]
>>;
{
client_start: while(TRUE) {
either step_through_test();
or process_vtgate_read_response();
or process_vtgate_write_response_ok();
or process_vtgate_write_response_err();
or finish_test();
}
}
process (vtgate \in Vtgates)
{
vtgate_start: while(TRUE) {
either process_read_query_request();
or process_write_query_request();
or process_read_storage_response();
or process_write_storage_response();
or process_topo_change();
}
}
process (replica \in Replicas)
variables \* storage_value = 0,
\* ssr_master = MasterIdx;
\* replica_state = REPLICA_WRITE_RECV,
\* replica_write_request = NULL;
{
replica_start: while(TRUE) {
either process_read_storage_request();
or process_write_storage_request();
\* or recv_write_storage_request();
\* or wait_ssr_ack();
\* or ack_write_storage_request();
or process_promote();
or process_disconnect_request();
}
}
process (orc \in { Orc })
variables orc_request = NULL,
orc_state = ORC_RECV;
orc_master = MasterIdx;
disconnect_replicas_waitlist = {};
replica_gtid_ack_waitlist = {};
new_master_candidate = NULL,
new_master_candidate_gtid = NULL,
promote_ack_waitlist = {};
{
orc_start: while(TRUE) {
\* 1. Process dmr message
\* 2. Disconnect all replicas (no master) from master
\* 3. Broadcast a promote message to all replicas (no master)
\* 4. Wait for acks from replicas
\* 5. Send write_topo message with new master value
\* 6. Wait for ack from topo
\* 7. Done
either recv_dmr()
or disconnect_replicas();
or wait_disconnect_replicas_ack();
or read_replica_gtid();
or wait_replica_gtid_ack();
or broadcast_promotion()
or wait_promotions_ack()
or write_topo()
or wait_write_topo_ack()
or finish_dmr()
}
}
process (topo \in { Topo })
variables topo_request = NULL,
topo_state = TOPO_RECV,
topo_master = MasterIdx;
{
topo_start: while(TRUE) {
either recv_write_topo();
or notify_topo_listeners();
}
}
}
***************************************************************************)
\* BEGIN TRANSLATION (chksum(pcal) = "9ef5895" /\ chksum(tla) = "d87e4ef9")
VARIABLES AA_send_log, AA_recv_log, network, processed, storage_value,
ssr_master, vtgate_master
(* define statement *)
CanWrite(replica) == Cardinality({ rid \in Replicas : ssr_master[rid] = replica }) > 1
VARIABLES step, wait_rid, r0, w1, r1, test, orc_request, orc_state,
orc_master, disconnect_replicas_waitlist, replica_gtid_ack_waitlist,
new_master_candidate, new_master_candidate_gtid,
promote_ack_waitlist, topo_request, topo_state, topo_master
vars == << AA_send_log, AA_recv_log, network, processed, storage_value,
ssr_master, vtgate_master, step, wait_rid, r0, w1, r1, test,
orc_request, orc_state, orc_master, disconnect_replicas_waitlist,
replica_gtid_ack_waitlist, new_master_candidate,
new_master_candidate_gtid, promote_ack_waitlist, topo_request,
topo_state, topo_master >>
ProcSet == ({ Client }) \cup (Vtgates) \cup (Replicas) \cup ({ Orc }) \cup ({ Topo })
Init == (* Global variables *)
/\ AA_send_log = {}
/\ AA_recv_log = NULL
/\ network = {
[type |-> "dmr"]
}
/\ processed = {}
/\ storage_value = [rid \in Replicas |-> 0]
/\ ssr_master = [rid \in Replicas |-> MasterIdx]
/\ vtgate_master = [vtgid \in Vtgates |-> MasterIdx]
(* Process client *)
/\ step = [self \in { Client } |-> 1]
/\ wait_rid = [self \in { Client } |-> -1]
/\ r0 = [self \in { Client } |-> [rid |-> 1, type |-> "read_query_request", vtgate |-> 51]]
/\ w1 = [self \in { Client } |-> [rid |-> 2, type |-> "write_query_request", vtgate |-> 52, value |-> 1]]
/\ r1 = [self \in { Client } |-> [rid |-> 3, type |-> "read_query_request", vtgate |-> 51]]
/\ test = [self \in { Client } |-> <<
[message |-> r0[self], expected |-> 0],
[message |-> w1[self], expected |-> 1],
[message |-> r1[self], expected |-> 1]
>>]
(* Process orc *)
/\ orc_request = [self \in { Orc } |-> NULL]
/\ orc_state = [self \in { Orc } |-> ORC_RECV]
/\ orc_master = [self \in { Orc } |-> MasterIdx]
/\ disconnect_replicas_waitlist = [self \in { Orc } |-> {}]
/\ replica_gtid_ack_waitlist = [self \in { Orc } |-> {}]
/\ new_master_candidate = [self \in { Orc } |-> NULL]
/\ new_master_candidate_gtid = [self \in { Orc } |-> NULL]
/\ promote_ack_waitlist = [self \in { Orc } |-> {}]
(* Process topo *)
/\ topo_request = [self \in { Topo } |-> NULL]
/\ topo_state = [self \in { Topo } |-> TOPO_RECV]
/\ topo_master = [self \in { Topo } |-> MasterIdx]
client(self) == /\ \/ /\ wait_rid[self] = -1
/\ step[self] <= Len(test[self])
/\ wait_rid' = [wait_rid EXCEPT ![self] = test[self][step[self]].message.rid]
/\ AA_send_log' = { (test[self][step[self]].message) }
/\ network' = (network \union AA_send_log')
/\ UNCHANGED <<AA_recv_log, processed, step, test>>
\/ /\ \E m \in network:
/\ m.type = "read_query_response"
/\ m \notin processed
/\ AA_recv_log' = m
/\ processed' = (processed \union { m })
/\ Assert(m.value = test[self][step[self]].expected,
"Failure of assertion at line 132, column 13 of macro called at line 520, column 21.")
/\ wait_rid' = [wait_rid EXCEPT ![self] = -1]
/\ step' = [step EXCEPT ![self] = step[self] + 1]
/\ UNCHANGED <<AA_send_log, network, test>>
\/ /\ \E m \in network:
/\ m.type = "write_query_response" /\ ~m.err
/\ m \notin processed
/\ AA_recv_log' = m
/\ processed' = (processed \union { m })
/\ Assert(m.value = test[self][step[self]].expected,
"Failure of assertion at line 145, column 13 of macro called at line 521, column 21.")
/\ wait_rid' = [wait_rid EXCEPT ![self] = -1]
/\ step' = [step EXCEPT ![self] = step[self] + 1]
/\ UNCHANGED <<AA_send_log, network, test>>
\/ /\ \E m \in network:
/\ m.type = "write_query_response" /\ m.err
/\ m \notin processed
/\ CanWrite(vtgate_master[52])
/\ AA_recv_log' = m
/\ processed' = (processed \union { m })
/\ wait_rid' = [wait_rid EXCEPT ![self] = test[self][step[self]].message.rid + 100]
/\ test' = [test EXCEPT ![self][step[self]].message.rid = wait_rid'[self]]
/\ AA_send_log' = { (test'[self][step[self]].message) }
/\ network' = (network \union AA_send_log')
/\ step' = step
\/ /\ step[self] > Len(test[self])
/\ UNCHANGED <<AA_send_log, AA_recv_log, network, processed, step, wait_rid, test>>
/\ UNCHANGED << storage_value, ssr_master, vtgate_master, r0,
w1, r1, orc_request, orc_state, orc_master,
disconnect_replicas_waitlist,
replica_gtid_ack_waitlist,
new_master_candidate,
new_master_candidate_gtid,
promote_ack_waitlist, topo_request, topo_state,
topo_master >>
vtgate(self) == /\ \/ /\ \E m \in network:
/\ m.type = "read_query_request" /\ m.vtgate = self
/\ m \notin processed
/\ AA_recv_log' = m
/\ processed' = (processed \union { m })
/\ AA_send_log' = { ( [
rid |-> m.rid,
type |-> "read_storage_request",
replica |-> vtgate_master[self],
from |-> self
]) }
/\ network' = (network \union AA_send_log')
/\ UNCHANGED vtgate_master
\/ /\ \E m \in network:
/\ m.type = "write_query_request" /\ m.vtgate = self
/\ m \notin processed
/\ AA_recv_log' = m
/\ processed' = (processed \union { m })
/\ AA_send_log' = { ( [
rid |-> m.rid,
type |-> "write_storage_request",
value |-> m.value,
replica |-> vtgate_master[self],
from |-> self
]) }
/\ network' = (network \union AA_send_log')
/\ UNCHANGED vtgate_master
\/ /\ \E m \in network:
/\ m.type = "read_storage_response" /\ m.caller = self
/\ m \notin processed
/\ AA_recv_log' = m
/\ processed' = (processed \union { m })
/\ AA_send_log' = { ( [
rid |-> m.rid,
type |-> "read_query_response",
value |-> m.value
]) }
/\ network' = (network \union AA_send_log')
/\ UNCHANGED vtgate_master
\/ /\ \E m \in network:
/\ m.type = "write_storage_response" /\ m.caller = self
/\ m \notin processed
/\ AA_recv_log' = m
/\ processed' = (processed \union { m })
/\ AA_send_log' = { ( [
rid |-> m.rid,
type |-> "write_query_response",
value |-> m.value,
err |-> m.err
]) }
/\ network' = (network \union AA_send_log')
/\ UNCHANGED vtgate_master
\/ /\ \E m \in network:
/\ m.type = "topo_change" /\ m.listener = self
/\ m \notin processed
/\ AA_recv_log' = m
/\ processed' = (processed \union { m })
/\ vtgate_master' = [vtgate_master EXCEPT ![self] = m.new_master]
/\ UNCHANGED <<AA_send_log, network>>
/\ UNCHANGED << storage_value, ssr_master, step, wait_rid, r0,
w1, r1, test, orc_request, orc_state,
orc_master, disconnect_replicas_waitlist,
replica_gtid_ack_waitlist,
new_master_candidate,
new_master_candidate_gtid,
promote_ack_waitlist, topo_request, topo_state,
topo_master >>
replica(self) == /\ \/ /\ \E m \in network:
/\ m.type = "read_storage_request" /\ m.replica = self
/\ m \notin processed
/\ AA_recv_log' = m
/\ processed' = (processed \union { m })
/\ AA_send_log' = { ( [
rid |-> m.rid,
type |-> "read_storage_response",
value |-> storage_value[self],
caller |-> m.from
]) }
/\ network' = (network \union AA_send_log')
/\ UNCHANGED <<storage_value, ssr_master>>
\/ /\ \E m \in network:
/\ m.type = "write_storage_request" /\ m.replica = self
/\ m \notin processed
/\ AA_recv_log' = m
/\ processed' = (processed \union { m })
/\ storage_value' = IF CanWrite(self)
THEN
[rid \in Replicas |->
IF \/ rid = self
\/ ssr_master[rid] = self
THEN m.value
ELSE storage_value[rid]
]
ELSE
storage_value
/\ AA_send_log' = { ( [
rid |-> m.rid,
type |-> "write_storage_response",
value |-> storage_value'[self],
caller |-> m.from,
err |-> IF CanWrite(self) THEN FALSE ELSE TRUE
]) }
/\ network' = (network \union AA_send_log')
/\ UNCHANGED ssr_master
\/ /\ \E m \in network:
/\ m.type = "promote" /\ m.destination = self
/\ m \notin processed
/\ AA_recv_log' = m
/\ processed' = (processed \union { m })
/\ ssr_master' = [ssr_master EXCEPT ![self] = m.new_master]
/\ AA_send_log' = { ( [
rid |-> m.rid,
type |-> "promote_ack",
new_master |-> ssr_master'[self]
]) }
/\ network' = (network \union AA_send_log')
/\ UNCHANGED storage_value
\/ /\ \E m \in network:
/\ m.type = "disconnect_request" /\ m.replica = self
/\ m \notin processed
/\ AA_recv_log' = m
/\ processed' = (processed \union { m })
/\ ssr_master' = [ssr_master EXCEPT ![self] = NULL]
/\ AA_send_log' = { ( [
rid |-> m.rid,
type |-> "disconnect_response",
replica |-> m.replica,
value |-> storage_value[self]
]) }
/\ network' = (network \union AA_send_log')
/\ UNCHANGED storage_value
/\ UNCHANGED << vtgate_master, step, wait_rid, r0, w1, r1,
test, orc_request, orc_state, orc_master,
disconnect_replicas_waitlist,
replica_gtid_ack_waitlist,
new_master_candidate,
new_master_candidate_gtid,
promote_ack_waitlist, topo_request,
topo_state, topo_master >>
orc(self) == /\ \/ /\ orc_state[self] = ORC_RECV
/\ \E m \in network:
/\ m.type = "dmr"
/\ m \notin processed
/\ AA_recv_log' = m
/\ processed' = (processed \union { m })
/\ orc_state' = [orc_state EXCEPT ![self] = ORC_DISCONNECT_REPLICA]
/\ orc_request' = [orc_request EXCEPT ![self] = m]
/\ UNCHANGED <<AA_send_log, network, orc_master, disconnect_replicas_waitlist, replica_gtid_ack_waitlist, new_master_candidate, new_master_candidate_gtid, promote_ack_waitlist>>
\/ /\ orc_state[self] = ORC_DISCONNECT_REPLICA
/\ disconnect_replicas_waitlist' = [disconnect_replicas_waitlist EXCEPT ![self] = { pid \in Replicas : pid # orc_master[self] }]
/\ AA_send_log' = { [
rid |-> pid,
type |-> "disconnect_request",
replica |-> pid
] : pid \in disconnect_replicas_waitlist'[self] }
/\ network' = (network \union AA_send_log')
/\ orc_state' = [orc_state EXCEPT ![self] = ORC_WAIT_DISCONNECT_REPLICA]
/\ UNCHANGED <<AA_recv_log, processed, orc_request, orc_master, replica_gtid_ack_waitlist, new_master_candidate, new_master_candidate_gtid, promote_ack_waitlist>>
\/ /\ orc_state[self] = ORC_WAIT_DISCONNECT_REPLICA
/\ \E m \in network:
/\ m.type = "disconnect_response"
/\ m \notin processed
/\ AA_recv_log' = m
/\ processed' = (processed \union { m })
/\ disconnect_replicas_waitlist' = [disconnect_replicas_waitlist EXCEPT ![self] = disconnect_replicas_waitlist[self] \ { m.replica }]
/\ orc_state' = [orc_state EXCEPT ![self] = IF Cardinality(disconnect_replicas_waitlist'[self]) > 0
THEN ORC_WAIT_DISCONNECT_REPLICA
ELSE ORC_READ_REPLICA]
/\ UNCHANGED <<AA_send_log, network, orc_request, orc_master, replica_gtid_ack_waitlist, new_master_candidate, new_master_candidate_gtid, promote_ack_waitlist>>
\/ /\ orc_state[self] = ORC_READ_REPLICA
/\ replica_gtid_ack_waitlist' = [replica_gtid_ack_waitlist EXCEPT ![self] = { pid \in Replicas : pid # orc_master[self] }]
/\ AA_send_log' = { [
rid |-> pid,
type |-> "read_storage_request",
from |-> self,
replica |-> pid
] : pid \in replica_gtid_ack_waitlist'[self] }
/\ network' = (network \union AA_send_log')
/\ orc_state' = [orc_state EXCEPT ![self] = ORC_WAIT_READ_REPLICA]
/\ UNCHANGED <<AA_recv_log, processed, orc_request, orc_master, disconnect_replicas_waitlist, new_master_candidate, new_master_candidate_gtid, promote_ack_waitlist>>
\/ /\ orc_state[self] = ORC_WAIT_READ_REPLICA
/\ \E m \in network:
/\ m.type = "read_storage_response" /\ m.caller = self
/\ m \notin processed
/\ AA_recv_log' = m
/\ processed' = (processed \union { m })
/\ replica_gtid_ack_waitlist' = [replica_gtid_ack_waitlist EXCEPT ![self] = replica_gtid_ack_waitlist[self] \ { m.rid }]
/\ new_master_candidate_gtid' = [new_master_candidate_gtid EXCEPT ![self] = IF new_master_candidate_gtid[self] = NULL \/ new_master_candidate_gtid[self] < m.value
THEN m.value
ELSE new_master_candidate_gtid[self]]
/\ new_master_candidate' = [new_master_candidate EXCEPT ![self] = IF new_master_candidate_gtid'[self] = m.value
THEN m.rid
ELSE new_master_candidate[self]]
/\ orc_state' = [orc_state EXCEPT ![self] = IF Cardinality(replica_gtid_ack_waitlist'[self]) > 0
THEN ORC_WAIT_READ_REPLICA
ELSE ORC_BROADCAST]
/\ UNCHANGED <<AA_send_log, network, orc_request, orc_master, disconnect_replicas_waitlist, promote_ack_waitlist>>
\/ /\ orc_state[self] = ORC_BROADCAST
/\ promote_ack_waitlist' = [promote_ack_waitlist EXCEPT ![self] = { pid \in Replicas : pid # orc_master[self] }]
/\ AA_send_log' = { [
rid |-> pid,
type |-> "promote",
new_master |-> new_master_candidate[self],
destination |-> pid
] : pid \in promote_ack_waitlist'[self] }
/\ network' = (network \union AA_send_log')
/\ orc_state' = [orc_state EXCEPT ![self] = ORC_WAIT_BROADCAST]
/\ UNCHANGED <<AA_recv_log, processed, orc_request, orc_master, disconnect_replicas_waitlist, replica_gtid_ack_waitlist, new_master_candidate, new_master_candidate_gtid>>
\/ /\ orc_state[self] = ORC_WAIT_BROADCAST
/\ \E m \in network:
/\ m.type = "promote_ack"
/\ m \notin processed
/\ AA_recv_log' = m
/\ processed' = (processed \union { m })
/\ promote_ack_waitlist' = [promote_ack_waitlist EXCEPT ![self] = promote_ack_waitlist[self] \ { m.rid }]
/\ orc_state' = [orc_state EXCEPT ![self] = IF Cardinality(promote_ack_waitlist'[self]) > 0
THEN ORC_WAIT_BROADCAST
ELSE ORC_WRITE_TOPO]
/\ UNCHANGED <<AA_send_log, network, orc_request, orc_master, disconnect_replicas_waitlist, replica_gtid_ack_waitlist, new_master_candidate, new_master_candidate_gtid>>
\/ /\ orc_state[self] = ORC_WRITE_TOPO
/\ AA_send_log' = { ( [
rid |-> new_master_candidate[self],
type |-> "write_topo",
new_master |-> new_master_candidate[self]
]) }
/\ network' = (network \union AA_send_log')
/\ orc_state' = [orc_state EXCEPT ![self] = ORC_WAIT_WRITE_TOPO]
/\ UNCHANGED <<AA_recv_log, processed, orc_request, orc_master, disconnect_replicas_waitlist, replica_gtid_ack_waitlist, new_master_candidate, new_master_candidate_gtid, promote_ack_waitlist>>
\/ /\ orc_state[self] = ORC_WAIT_WRITE_TOPO
/\ \E m \in network:
/\ m.type = "write_topo_ack"
/\ m \notin processed
/\ AA_recv_log' = m
/\ processed' = (processed \union { m })
/\ orc_master' = [orc_master EXCEPT ![self] = new_master_candidate[self]]
/\ orc_state' = [orc_state EXCEPT ![self] = ORC_FINISH]
/\ UNCHANGED <<AA_send_log, network, orc_request, disconnect_replicas_waitlist, replica_gtid_ack_waitlist, new_master_candidate, new_master_candidate_gtid, promote_ack_waitlist>>
\/ /\ orc_state[self] = ORC_FINISH
/\ orc_request' = [orc_request EXCEPT ![self] = NULL]
/\ orc_state' = [orc_state EXCEPT ![self] = ORC_RECV]
/\ disconnect_replicas_waitlist' = [disconnect_replicas_waitlist EXCEPT ![self] = {}]
/\ replica_gtid_ack_waitlist' = [replica_gtid_ack_waitlist EXCEPT ![self] = {}]
/\ new_master_candidate' = [new_master_candidate EXCEPT ![self] = NULL]
/\ new_master_candidate_gtid' = [new_master_candidate_gtid EXCEPT ![self] = NULL]
/\ promote_ack_waitlist' = [promote_ack_waitlist EXCEPT ![self] = {}]
/\ UNCHANGED <<AA_send_log, AA_recv_log, network, processed, orc_master>>
/\ UNCHANGED << storage_value, ssr_master, vtgate_master, step,
wait_rid, r0, w1, r1, test, topo_request,
topo_state, topo_master >>
topo(self) == /\ \/ /\ topo_state[self] = TOPO_RECV
/\ \E m \in network:
/\ m.type = "write_topo"
/\ m \notin processed
/\ AA_recv_log' = m
/\ processed' = (processed \union { m })
/\ topo_request' = [topo_request EXCEPT ![self] = m]
/\ topo_master' = [topo_master EXCEPT ![self] = topo_request'[self].new_master]
/\ topo_state' = [topo_state EXCEPT ![self] = TOPO_NOTIFY]
/\ AA_send_log' = { ( [
rid |-> topo_request'[self].rid,
type |-> "write_topo_ack",
new_master |-> topo_master'[self]
]) }
/\ network' = (network \union AA_send_log')
\/ /\ topo_state[self] = TOPO_NOTIFY
/\ AA_send_log' = { [
type |-> "topo_change",
new_master |-> topo_request[self].new_master,
listener |-> pid
] : pid \in Vtgates }
/\ network' = (network \union AA_send_log')
/\ topo_request' = [topo_request EXCEPT ![self] = NULL]
/\ topo_state' = [topo_state EXCEPT ![self] = TOPO_RECV]
/\ UNCHANGED <<AA_recv_log, processed, topo_master>>
/\ UNCHANGED << storage_value, ssr_master, vtgate_master, step,
wait_rid, r0, w1, r1, test, orc_request,
orc_state, orc_master,
disconnect_replicas_waitlist,
replica_gtid_ack_waitlist, new_master_candidate,
new_master_candidate_gtid, promote_ack_waitlist >>
Next == (\E self \in { Client }: client(self))
\/ (\E self \in Vtgates: vtgate(self))
\/ (\E self \in Replicas: replica(self))
\/ (\E self \in { Orc }: orc(self))
\/ (\E self \in { Topo }: topo(self))
Spec == Init /\ [][Next]_vars
\* END TRANSLATION
\* Verifying that all messages fit the schema
TypeOk ==
/\ network \subseteq Messages
/\ processed \subseteq Messages
\* Storage end state, NOTE(yu): not used for now since this current definition isn't deterministic
StorageEndState == <>[](storage_value = <<1, 1, 1>>)
\* Vtgates' POV of topology, NOTE(yu): not used since this def isn't correct
VtgateTopoEndState == <>[](vtgate_master[1] # 1 /\ vtgate_master[2] # 1 /\ vtgate_master[3] # 1)
\* We eventually process all messages
Live == <>[](network \ processed = {})
\* Client's test script of r0, w1, r1 is completed
TestCompleted == <>[](step[100] = 3)
=============================================================================
\* Modification History
\* Last modified Sun Dec 06 18:12:47 PST 2020 by sean_yu
\* Created Fri Nov 20 23:19:29 PST 2020 by sean_yu
Raw
wtf.txt
STATE
vtgate_master = <1, 2>
ssr_master = <1, 2, 2>
storage_value = <0, 1, 1>
orc
master = 2
candidate = 2
topo
master = 2
SCRIPT
r0 = read_query_request(@vt51)
w1 = write_query_request(@vt52, 1)
r1 = read_query_request(@vt51)
BEGIN
--r0
...
--read_query_response 0
--w1
--dmr
--disc(@r2)
--disc(@r3)
recv disc(@r2) ->
-- disc_ack(@r2)
recv disc(@r3) ->
-- disc_ack(@r3)
recv disc_ack(@r2)
recv disc_ack(@r3)
--read_storage_request(@r2)
--read_storage_request(@r3)
recv read_storage_request(@r2) ->
--read_storage_response(@r2, 0)
recv read_storage_request(@r3) ->
--read_storage_response(@r3, 0)
recv read_storage_response(@r2, 0)
recv read_storage_response(@r3, 0)
--promote(@r2, 2)
--promote(@r3, 2)
recv promote(@r2, 2) ->
--promote_ack(@r2)
recv promote(@r3, 2) ->
--promote_ack(@r3)
recv promote_ack(@r2)
recv promote_ack(@r3)
--write_topo(2)
recv write_topo(2) ->
--write_topo_ack
topo_change(@vt51, 2)
--topo_change(@vt52, 2)
recv write_topo_ack
recv topo_change(@vt52, 2)
recv w1 ->
--write_storage_request(@r2, 1)
recv write_storage_request(@r2, 1) ->
--write_storage_response(@vt52)
recv write_storage_response(@vt52) ->
--write_query_response
recv write_query_response
--r1
recv r1 ->
--read_storage_request(@r1)
recv read_storage_request(@r1) ->
--read_storage_response(0)
recv read_storage_response(0) ->
--read_query_response(0)
recv read_query_response(0)
BIG FAT ERROR YES IT IS WORKING 0 \= 1
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment