---- MODULE simple_rpc_threads_flushing ---- EXTENDS TLC, Sequences, Integers \* Version that handles pending requests before closing the connection (* Connection is cut at arbitrary times: connection-breaker *) (* Checked properties: *) \* check_query_responses: Check responses ok or queries marked FAILED \* ghost_got_close_ack: if server closes first, and there's no connection cut, the \* remote end should get (close), and server should get (ack-close) (* TODO: check threads eventually always stopped. strange error while checking Termination *) (* TODO: Feature: Fail queries when connection is not cut, but remote end just doesn't reply *) (* TODO: Feature: Handle invalid messages. conn-in *) EMPTY_QUEUE == <<>> WAITING_RESPONSE == "WAITING_RESPONSE" FAILED == "FAILED" CLOSE == -1 CLOSE_CLEAN == -2 BrokenSocket(s) == s = <<"connection-cut">> CliResponses == [sq1 |-> "cr1", sq2 |-> "cr2", sq3 |-> "cr3", sq4 |-> "cr4"] SrvQueries == DOMAIN CliResponses SrvQueryResults == {CliResponses[q]: q \in SrvQueries} SrvResponses == [q1 |-> "r1", q2 |-> "r2", q3 |-> "r3", q4 |-> "r4"] CliQueries == DOMAIN SrvResponses CliQueryResults == {SrvResponses[q]: q \in CliQueries} WireMsgs == {"(close)", "(ack-close)"} \cup SrvQueries \cup SrvQueryResults \cup CliQueries \cup CliQueryResults QueryStates == [q: SrvQueries, res: SrvQueryResults \union {WAITING_RESPONSE, FAILED}] Min(a,b) == IF a < b THEN a ELSE b Prefixes(max, s) == {<<>>} \union {SubSeq(s, 1, l): l \in 1..Min(max, Len(s))} SeqOf(seq, set) == \A i \in DOMAIN seq: seq[i] \in set \/ Print(<<"SeqOf", i, seq[i], set >>, FALSE ) (* --algorithm simple_rpc_threads_flushing \* Variables variables WaitForServerQueriesBeforeClosing \in BOOLEAN, flag_serverTriesToClose \in BOOLEAN, flag_remote_waits_for_close \in BOOLEAN, IncomingQueries \in Prefixes(3, << "q1", "q2", "q3", "q4" >> ), OutgoingQueries \in Prefixes(3, << "sq1", "sq2", "sq3" >> ), sockIn = EMPTY_QUEUE, sockOut = EMPTY_QUEUE, mbQueryRes = EMPTY_QUEUE, mbQuery = EMPTY_QUEUE, mbQueryCopy = EMPTY_QUEUE, mbOut = EMPTY_QUEUE, mbRequests = EMPTY_QUEUE, queriesToSend = OutgoingQueries, sentQueries = <<>>, send_ack_close = FALSE, send_close = FALSE, ghost_droppedQueries = <<>>, (* Queries that don't get responses due to closed connection *) ghost_received_sockOut_msgs = <<>>, ghost_received_sockIn_msgs = <<>>, ghost_got_close_ack = FALSE, \* Definitions define QueryIds == DOMAIN sentQueries TypeInvariant == /\ SeqOf(sentQueries, QueryStates) /\ SeqOf(mbOut, SrvQueries \cup CliQueryResults \union {"(close)", "(ack-close)", "close", "flush-and-ack-close"}) /\ SeqOf(mbQuery, QueryIds \union {CLOSE, CLOSE_CLEAN}) /\ SeqOf(mbQueryCopy, QueryIds \union {CLOSE, CLOSE_CLEAN}) /\ SeqOf(mbQueryRes, SrvQueryResults \union {"close", "fail"}) /\ BrokenSocket(sockIn) \/ SeqOf(sockIn, WireMsgs) /\ BrokenSocket(sockOut) \/ SeqOf(sockOut, WireMsgs) QueueEmpty(q) == q = EMPTY_QUEUE QueuePeek(q) == Head(q) ConnThreads == {"conn-out", "conn-in", "query-joiner", "query-send"} ConnThreadsStopped == \A t \in ConnThreads: pc[t] = "Done" NoThreadsStopped == \A t \in ConnThreads: pc[t] /= "Done" ConnectionTermination == <>(ConnThreadsStopped) ghost_HavePendingRequests == \E i \in DOMAIN sentQueries: sentQueries[i].res = WAITING_RESPONSE Query(query, response) == [q |-> query, res |-> response] SeqMap(s, Op(_)) == [i \in DOMAIN s |-> Op(s[i])] WaitingQueries == SeqMap(SelectSeq(sentQueries, LAMBDA q: q.res = WAITING_RESPONSE), LAMBDA q: q.q) AllQueriesDone == Len(sentQueries) = Len(OutgoingQueries) /\ WaitingQueries = <<>> end define \* Macros macro QueuePop(q) begin q := Tail(q); end macro; macro QueuePush(q, v) begin q := Append(q, v); end macro; macro QueueReceive(q, v) begin await ~QueueEmpty(q); v := QueuePeek(q); q := Tail(q); end macro; macro SocketSend(s, v) begin if ~BrokenSocket(s) then QueuePush(s, v); end if; end macro; macro SocketReceive(s, v) begin await ~QueueEmpty(s); if BrokenSocket(s) then v := "connection-cut"; else v := QueuePeek(s); s := Tail(s); end if; end macro; macro MarkDroppedQueries() begin if ghost_droppedQueries = <<>> then ghost_droppedQueries := WaitingQueries \o queriesToSend; end if; end macro; macro error(msg) begin assert Print(msg, FALSE); end macro; \* API operations macro SendQuery(query) begin QueuePush(sentQueries, Query(query, WAITING_RESPONSE)); QueuePush(mbQuery, Len(sentQueries)); end macro; macro SetQueryResult(id, val) begin assert sentQueries[id].res = WAITING_RESPONSE; sentQueries := id :> [q |-> sentQueries[id].q, res |-> val] @@ [i \in DOMAIN sentQueries \ {id} |-> sentQueries[i]]; end macro; procedure CleanShutdown() (* remote-conn-close! *) (* Wait pending requests have received responses / failed *) (* Completely abort / ignore pending incoming requests *) begin CleanShutdown_entry: send_close := TRUE; QueuePush(mbQuery, CLOSE_CLEAN); shutdown_loop: await ConnThreadsStopped \/ ~QueueEmpty(mbRequests); if ~QueueEmpty(mbRequests) then mbRequests := EMPTY_QUEUE; goto shutdown_loop; else return; end if; end procedure; \* Processes process tOut="conn-out" variables tOut_msg = FALSE, tOut_flush = FALSE; begin (* IN: mbOut *) (* OUT: sockOut, mbQuery (close) *) conn_out: QueueReceive( mbOut, tOut_msg); if BrokenSocket(sockOut) then skip; elsif tOut_msg = "(close)" then SocketSend( sockOut, tOut_msg); (* Server requests close *) goto notify_sender; elsif tOut_msg = "flush-and-ack-close" then tOut_flush := TRUE; else SocketSend( sockOut, tOut_msg); goto conn_out; end if; flush_out_queue: if tOut_flush /\ ~( QueueEmpty(mbOut) /\ QueueEmpty(mbRequests)) then QueueReceive(mbOut, tOut_msg); if tOut_msg = "close" then skip; elsif tOut_msg = "(close)" then SocketSend(sockOut, tOut_msg); goto notify_sender; else SocketSend(sockOut, tOut_msg); end if; flush_out_queue_loop: goto flush_out_queue; end if; notify_sender: QueuePush( mbQuery, CLOSE ); end process; process tIn="conn-in" variables tIn_msg = FALSE; begin (* IN: sockIn *) (* OUT: mbQueryRes, mbRequests, (mbQuery on failure), mbOut (flush-and-ack-close) *) conn_in: SocketReceive(sockIn, tIn_msg); ghost_received_sockIn_msgs := Append(ghost_received_sockIn_msgs, tIn_msg); if tIn_msg = "(close)" then (* Start shutdown *) send_ack_close := TRUE; QueuePush(mbOut, "flush-and-ack-close"); QueuePush(mbQueryRes, "close"); elsif tIn_msg = "(ack-close)" then ghost_got_close_ack := TRUE; elsif tIn_msg \in CliQueries then (* Received a request *) QueuePush( mbRequests, tIn_msg); goto conn_in; elsif tIn_msg \in SrvQueryResults then QueuePush(mbQueryRes, tIn_msg); goto conn_in; elsif tIn_msg = "connection-cut" then (* Fail *) QueuePush(mbQueryRes, "fail"); QueuePush(mbQuery, CLOSE); else error("Invalid message"); end if; end process; process tJoin="query-joiner" variables tJoin_q = FALSE, tJoin_res = FALSE, tJoin_fail_remaining = FALSE; begin (* IN: mbQueryCopy, mbQueryRes, (mbQuery during fail_remaining) *) (* OUT: ( mbQuery <- CLOSE during fail_remaining) *) query_joiner: QueueReceive(mbQueryCopy, tJoin_q); if tJoin_q = CLOSE then tJoin_fail_remaining := TRUE; elsif tJoin_q = CLOSE_CLEAN then skip; else join_get_resp: (* Get response *) QueueReceive(mbQueryRes, tJoin_res); if tJoin_res \in {"close", "fail"} then SetQueryResult(tJoin_q, FAILED); tJoin_fail_remaining := TRUE; else set_query_result: SetQueryResult(tJoin_q, tJoin_res); goto query_joiner; end if; end if; fail_remaining: if tJoin_fail_remaining then fail_remaining_loop: if ~QueueEmpty(mbQueryCopy) then if QueuePeek(mbQueryCopy) \notin {CLOSE, CLOSE_CLEAN} then SetQueryResult(QueuePeek(mbQueryCopy), FAILED); end if; QueuePop(mbQueryCopy); goto fail_remaining_loop; elsif ~QueueEmpty(mbQuery) then (* peek&pop requires disable-interrupts, because mbQuery is read from multiple threads *) if QueuePeek(mbQuery) \notin {CLOSE, CLOSE_CLEAN} then SetQueryResult(QueuePeek(mbQuery), FAILED); QueuePop(mbQuery); goto fail_remaining_loop; else (* Stop *) QueuePop(mbQuery); replace_close: QueuePush(mbQuery, CLOSE); end if; end if; end if; end process; process tSend="query-send" variables tSend_q = FALSE; begin (* IN: mbQuery *) (* OUT: mbQueryCopy, mbOut *) query_send: QueueReceive( mbQuery, tSend_q ); QueuePush( mbQueryCopy, tSend_q ); if tSend_q = CLOSE then QueuePush( mbOut, "close" ); elsif tSend_q = CLOSE_CLEAN then QueuePush( mbOut, "(close)" ); else QueuePush( mbOut, sentQueries[tSend_q].q ); goto query_send; end if; end process; \* Connection breaker process tBreaker = "connection-breaker" begin maybe_break_connection: either sockIn := <<"connection-cut">>; sockOut := <<"connection-cut">>; MarkDroppedQueries(); or skip; end either; end process; \* The server \* Creates responses for the received queries. process tServer="server" variables tServer_req = FALSE, checkId = 0; begin server: await \/ ConnThreadsStopped \/ ~QueueEmpty(mbRequests) \/ ~QueueEmpty(queriesToSend) \/ flag_serverTriesToClose; if ConnThreadsStopped then skip; elsif QueueEmpty(queriesToSend) /\ flag_serverTriesToClose then call CleanShutdown(); else either (* Handle a request *) (* in maybe-do-request *) QueueReceive(mbRequests, tServer_req ); (* Send response *) QueuePush(mbOut, SrvResponses[tServer_req]); or (* Send a query *) await NoThreadsStopped /\ ~QueueEmpty(queriesToSend); SendQuery(QueuePeek(queriesToSend)); QueuePop(queriesToSend); end either; server_loopy: goto server; end if; send_ack_close: (* Order is important *) if send_close then assert ConnThreadsStopped; (* in create-remote-connection *) SocketSend(sockOut, "(close)"); elsif send_ack_close then assert ConnThreadsStopped; (* in create-remote-connection *) SocketSend(sockOut, "(ack-close)"); end if; check_query_responses: \* Check each query is either marked FAILED or has a correct reply \* This is NOT part of the implementation if checkId < Len(sentQueries) then checkId := checkId + 1; if LET query == sentQueries[checkId] IN query.res = CliResponses[query.q] then (* Ok response *) (* ghost_droppedQueries is just a heuristic, drop the entry if it was marked to be dropped *) if /\ ghost_droppedQueries /= <<>> /\ sentQueries[checkId].q = Head(ghost_droppedQueries) then ghost_droppedQueries := Tail(ghost_droppedQueries); end if; goto check_query_responses; elsif (* Remote end closed before queries were replied to *) /\ ghost_droppedQueries /= <<>> /\ sentQueries[checkId].q = Head(ghost_droppedQueries) then (* Queries must be marked failed *) assert sentQueries[checkId].res = FAILED; ghost_droppedQueries := Tail(ghost_droppedQueries); goto check_query_responses; else error( <<"Query result wrong", checkId, sentQueries[checkId] >> ); end if; end if; server_stop: if ~BrokenSocket(sockIn) then (* TODO: remove this hack *) assert ~WaitForServerQueriesBeforeClosing \/ queriesToSend = <<>>; end if; (* Should receive (ack-close) when "conditions" *) assert ( /\ flag_serverTriesToClose /\ WaitForServerQueriesBeforeClosing /\ flag_remote_waits_for_close /\ ~BrokenSocket(sockIn)) => ghost_got_close_ack; end process; \* \* Remote end \* process tRemote = "remote-end" variables remoteMsgs = IncomingQueries \o << "(close)" >> , rmsg = FALSE, expResps = EMPTY_QUEUE, tRemote_received = FALSE; begin other: either (* Send message *) await <<>> /= remoteMsgs; await \/ ~WaitForServerQueriesBeforeClosing \/ Head(remoteMsgs) /= "(close)" \/ AllQueriesDone; QueueReceive(remoteMsgs, rmsg); if rmsg = "(close)" then if flag_remote_waits_for_close /\ flag_serverTriesToClose then goto handle_query; else SocketSend(sockIn, rmsg); QueuePush(expResps, "(ack-close)"); MarkDroppedQueries(); goto other; end if; else (* Send query *) SocketSend(sockIn, rmsg); QueuePush(expResps, SrvResponses[rmsg]); goto other; end if; or (* Handle message from server *) await ~QueueEmpty(sockOut); handle_query: SocketReceive(sockOut, tRemote_received); ghost_received_sockOut_msgs := Append(ghost_received_sockOut_msgs, tRemote_received); if tRemote_received = "connection-cut" \/ BrokenSocket(sockIn) then goto other_stop; elsif tRemote_received \in SrvQueries then (* Respond to query from server *) SocketSend(sockIn, CliResponses[tRemote_received]); elsif tRemote_received = "(close)" then SocketSend(sockIn, "(ack-close)"); remoteMsgs := <<>>; goto other_stop; else (* Check result to our query was as expected *) assert tRemote_received = QueuePeek(expResps); QueuePop(expResps); if tRemote_received = "(ack-close)" then goto other_stop; end if; end if; other_loopy: goto other; or (* Nothing more to send *) (* TODO: never-triggers *) await QueueEmpty(remoteMsgs) /\ QueueEmpty(expResps) /\ ~flag_serverTriesToClose; end either; other_stop: skip; end process; end algorithm;*) \* BEGIN TRANSLATION \* Label send_ack_close of process tServer at line 350 col 1 changed to send_ack_close_ VARIABLES WaitForServerQueriesBeforeClosing, flag_serverTriesToClose, flag_remote_waits_for_close, IncomingQueries, OutgoingQueries, sockIn, sockOut, mbQueryRes, mbQuery, mbQueryCopy, mbOut, mbRequests, queriesToSend, sentQueries, send_ack_close, send_close, ghost_droppedQueries, ghost_received_sockOut_msgs, ghost_received_sockIn_msgs, ghost_got_close_ack, pc, stack (* define statement *) QueryIds == DOMAIN sentQueries TypeInvariant == /\ SeqOf(sentQueries, QueryStates) /\ SeqOf(mbOut, SrvQueries \cup CliQueryResults \union {"(close)", "(ack-close)", "close", "flush-and-ack-close"}) /\ SeqOf(mbQuery, QueryIds \union {CLOSE, CLOSE_CLEAN}) /\ SeqOf(mbQueryCopy, QueryIds \union {CLOSE, CLOSE_CLEAN}) /\ SeqOf(mbQueryRes, SrvQueryResults \union {"close", "fail"}) /\ BrokenSocket(sockIn) \/ SeqOf(sockIn, WireMsgs) /\ BrokenSocket(sockOut) \/ SeqOf(sockOut, WireMsgs) QueueEmpty(q) == q = EMPTY_QUEUE QueuePeek(q) == Head(q) ConnThreads == {"conn-out", "conn-in", "query-joiner", "query-send"} ConnThreadsStopped == \A t \in ConnThreads: pc[t] = "Done" NoThreadsStopped == \A t \in ConnThreads: pc[t] /= "Done" ConnectionTermination == <>(ConnThreadsStopped) ghost_HavePendingRequests == \E i \in DOMAIN sentQueries: sentQueries[i].res = WAITING_RESPONSE Query(query, response) == [q |-> query, res |-> response] SeqMap(s, Op(_)) == [i \in DOMAIN s |-> Op(s[i])] WaitingQueries == SeqMap(SelectSeq(sentQueries, LAMBDA q: q.res = WAITING_RESPONSE), LAMBDA q: q.q) AllQueriesDone == Len(sentQueries) = Len(OutgoingQueries) /\ WaitingQueries = <<>> VARIABLES tOut_msg, tOut_flush, tIn_msg, tJoin_q, tJoin_res, tJoin_fail_remaining, tSend_q, tServer_req, checkId, remoteMsgs, rmsg, expResps, tRemote_received vars == << WaitForServerQueriesBeforeClosing, flag_serverTriesToClose, flag_remote_waits_for_close, IncomingQueries, OutgoingQueries, sockIn, sockOut, mbQueryRes, mbQuery, mbQueryCopy, mbOut, mbRequests, queriesToSend, sentQueries, send_ack_close, send_close, ghost_droppedQueries, ghost_received_sockOut_msgs, ghost_received_sockIn_msgs, ghost_got_close_ack, pc, stack, tOut_msg, tOut_flush, tIn_msg, tJoin_q, tJoin_res, tJoin_fail_remaining, tSend_q, tServer_req, checkId, remoteMsgs, rmsg, expResps, tRemote_received >> ProcSet == {"conn-out"} \cup {"conn-in"} \cup {"query-joiner"} \cup {"query-send"} \cup {"connection-breaker"} \cup {"server"} \cup {"remote-end"} Init == (* Global variables *) /\ WaitForServerQueriesBeforeClosing \in BOOLEAN /\ flag_serverTriesToClose \in BOOLEAN /\ flag_remote_waits_for_close \in BOOLEAN /\ IncomingQueries \in Prefixes(3, << "q1", "q2", "q3", "q4" >> ) /\ OutgoingQueries \in Prefixes(3, << "sq1", "sq2", "sq3" >> ) /\ sockIn = EMPTY_QUEUE /\ sockOut = EMPTY_QUEUE /\ mbQueryRes = EMPTY_QUEUE /\ mbQuery = EMPTY_QUEUE /\ mbQueryCopy = EMPTY_QUEUE /\ mbOut = EMPTY_QUEUE /\ mbRequests = EMPTY_QUEUE /\ queriesToSend = OutgoingQueries /\ sentQueries = <<>> /\ send_ack_close = FALSE /\ send_close = FALSE /\ ghost_droppedQueries = <<>> /\ ghost_received_sockOut_msgs = <<>> /\ ghost_received_sockIn_msgs = <<>> /\ ghost_got_close_ack = FALSE (* Process tOut *) /\ tOut_msg = FALSE /\ tOut_flush = FALSE (* Process tIn *) /\ tIn_msg = FALSE (* Process tJoin *) /\ tJoin_q = FALSE /\ tJoin_res = FALSE /\ tJoin_fail_remaining = FALSE (* Process tSend *) /\ tSend_q = FALSE (* Process tServer *) /\ tServer_req = FALSE /\ checkId = 0 (* Process tRemote *) /\ remoteMsgs = IncomingQueries \o << "(close)" >> /\ rmsg = FALSE /\ expResps = EMPTY_QUEUE /\ tRemote_received = FALSE /\ stack = [self \in ProcSet |-> << >>] /\ pc = [self \in ProcSet |-> CASE self = "conn-out" -> "conn_out" [] self = "conn-in" -> "conn_in" [] self = "query-joiner" -> "query_joiner" [] self = "query-send" -> "query_send" [] self = "connection-breaker" -> "maybe_break_connection" [] self = "server" -> "server" [] self = "remote-end" -> "other"] CleanShutdown_entry(self) == /\ pc[self] = "CleanShutdown_entry" /\ send_close' = TRUE /\ mbQuery' = Append(mbQuery, CLOSE_CLEAN) /\ pc' = [pc EXCEPT ![self] = "shutdown_loop"] /\ UNCHANGED << WaitForServerQueriesBeforeClosing, flag_serverTriesToClose, flag_remote_waits_for_close, IncomingQueries, OutgoingQueries, sockIn, sockOut, mbQueryRes, mbQueryCopy, mbOut, mbRequests, queriesToSend, sentQueries, send_ack_close, ghost_droppedQueries, ghost_received_sockOut_msgs, ghost_received_sockIn_msgs, ghost_got_close_ack, stack, tOut_msg, tOut_flush, tIn_msg, tJoin_q, tJoin_res, tJoin_fail_remaining, tSend_q, tServer_req, checkId, remoteMsgs, rmsg, expResps, tRemote_received >> shutdown_loop(self) == /\ pc[self] = "shutdown_loop" /\ ConnThreadsStopped \/ ~QueueEmpty(mbRequests) /\ IF ~QueueEmpty(mbRequests) THEN /\ mbRequests' = EMPTY_QUEUE /\ pc' = [pc EXCEPT ![self] = "shutdown_loop"] /\ stack' = stack ELSE /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc] /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])] /\ UNCHANGED mbRequests /\ UNCHANGED << WaitForServerQueriesBeforeClosing, flag_serverTriesToClose, flag_remote_waits_for_close, IncomingQueries, OutgoingQueries, sockIn, sockOut, mbQueryRes, mbQuery, mbQueryCopy, mbOut, queriesToSend, sentQueries, send_ack_close, send_close, ghost_droppedQueries, ghost_received_sockOut_msgs, ghost_received_sockIn_msgs, ghost_got_close_ack, tOut_msg, tOut_flush, tIn_msg, tJoin_q, tJoin_res, tJoin_fail_remaining, tSend_q, tServer_req, checkId, remoteMsgs, rmsg, expResps, tRemote_received >> CleanShutdown(self) == CleanShutdown_entry(self) \/ shutdown_loop(self) conn_out == /\ pc["conn-out"] = "conn_out" /\ ~QueueEmpty(mbOut) /\ tOut_msg' = QueuePeek(mbOut) /\ mbOut' = Tail(mbOut) /\ IF BrokenSocket(sockOut) THEN /\ TRUE /\ pc' = [pc EXCEPT !["conn-out"] = "flush_out_queue"] /\ UNCHANGED << sockOut, tOut_flush >> ELSE /\ IF tOut_msg' = "(close)" THEN /\ IF ~BrokenSocket(sockOut) THEN /\ sockOut' = Append(sockOut, tOut_msg') ELSE /\ TRUE /\ UNCHANGED sockOut /\ pc' = [pc EXCEPT !["conn-out"] = "notify_sender"] /\ UNCHANGED tOut_flush ELSE /\ IF tOut_msg' = "flush-and-ack-close" THEN /\ tOut_flush' = TRUE /\ pc' = [pc EXCEPT !["conn-out"] = "flush_out_queue"] /\ UNCHANGED sockOut ELSE /\ IF ~BrokenSocket(sockOut) THEN /\ sockOut' = Append(sockOut, tOut_msg') ELSE /\ TRUE /\ UNCHANGED sockOut /\ pc' = [pc EXCEPT !["conn-out"] = "conn_out"] /\ UNCHANGED tOut_flush /\ UNCHANGED << WaitForServerQueriesBeforeClosing, flag_serverTriesToClose, flag_remote_waits_for_close, IncomingQueries, OutgoingQueries, sockIn, mbQueryRes, mbQuery, mbQueryCopy, mbRequests, queriesToSend, sentQueries, send_ack_close, send_close, ghost_droppedQueries, ghost_received_sockOut_msgs, ghost_received_sockIn_msgs, ghost_got_close_ack, stack, tIn_msg, tJoin_q, tJoin_res, tJoin_fail_remaining, tSend_q, tServer_req, checkId, remoteMsgs, rmsg, expResps, tRemote_received >> flush_out_queue == /\ pc["conn-out"] = "flush_out_queue" /\ IF tOut_flush /\ ~( QueueEmpty(mbOut) /\ QueueEmpty(mbRequests)) THEN /\ ~QueueEmpty(mbOut) /\ tOut_msg' = QueuePeek(mbOut) /\ mbOut' = Tail(mbOut) /\ IF tOut_msg' = "close" THEN /\ TRUE /\ pc' = [pc EXCEPT !["conn-out"] = "flush_out_queue_loop"] /\ UNCHANGED sockOut ELSE /\ IF tOut_msg' = "(close)" THEN /\ IF ~BrokenSocket(sockOut) THEN /\ sockOut' = Append(sockOut, tOut_msg') ELSE /\ TRUE /\ UNCHANGED sockOut /\ pc' = [pc EXCEPT !["conn-out"] = "notify_sender"] ELSE /\ IF ~BrokenSocket(sockOut) THEN /\ sockOut' = Append(sockOut, tOut_msg') ELSE /\ TRUE /\ UNCHANGED sockOut /\ pc' = [pc EXCEPT !["conn-out"] = "flush_out_queue_loop"] ELSE /\ pc' = [pc EXCEPT !["conn-out"] = "notify_sender"] /\ UNCHANGED << sockOut, mbOut, tOut_msg >> /\ UNCHANGED << WaitForServerQueriesBeforeClosing, flag_serverTriesToClose, flag_remote_waits_for_close, IncomingQueries, OutgoingQueries, sockIn, mbQueryRes, mbQuery, mbQueryCopy, mbRequests, queriesToSend, sentQueries, send_ack_close, send_close, ghost_droppedQueries, ghost_received_sockOut_msgs, ghost_received_sockIn_msgs, ghost_got_close_ack, stack, tOut_flush, tIn_msg, tJoin_q, tJoin_res, tJoin_fail_remaining, tSend_q, tServer_req, checkId, remoteMsgs, rmsg, expResps, tRemote_received >> flush_out_queue_loop == /\ pc["conn-out"] = "flush_out_queue_loop" /\ pc' = [pc EXCEPT !["conn-out"] = "flush_out_queue"] /\ UNCHANGED << WaitForServerQueriesBeforeClosing, flag_serverTriesToClose, flag_remote_waits_for_close, IncomingQueries, OutgoingQueries, sockIn, sockOut, mbQueryRes, mbQuery, mbQueryCopy, mbOut, mbRequests, queriesToSend, sentQueries, send_ack_close, send_close, ghost_droppedQueries, ghost_received_sockOut_msgs, ghost_received_sockIn_msgs, ghost_got_close_ack, stack, tOut_msg, tOut_flush, tIn_msg, tJoin_q, tJoin_res, tJoin_fail_remaining, tSend_q, tServer_req, checkId, remoteMsgs, rmsg, expResps, tRemote_received >> notify_sender == /\ pc["conn-out"] = "notify_sender" /\ mbQuery' = Append(mbQuery, CLOSE) /\ pc' = [pc EXCEPT !["conn-out"] = "Done"] /\ UNCHANGED << WaitForServerQueriesBeforeClosing, flag_serverTriesToClose, flag_remote_waits_for_close, IncomingQueries, OutgoingQueries, sockIn, sockOut, mbQueryRes, mbQueryCopy, mbOut, mbRequests, queriesToSend, sentQueries, send_ack_close, send_close, ghost_droppedQueries, ghost_received_sockOut_msgs, ghost_received_sockIn_msgs, ghost_got_close_ack, stack, tOut_msg, tOut_flush, tIn_msg, tJoin_q, tJoin_res, tJoin_fail_remaining, tSend_q, tServer_req, checkId, remoteMsgs, rmsg, expResps, tRemote_received >> tOut == conn_out \/ flush_out_queue \/ flush_out_queue_loop \/ notify_sender conn_in == /\ pc["conn-in"] = "conn_in" /\ ~QueueEmpty(sockIn) /\ IF BrokenSocket(sockIn) THEN /\ tIn_msg' = "connection-cut" /\ UNCHANGED sockIn ELSE /\ tIn_msg' = QueuePeek(sockIn) /\ sockIn' = Tail(sockIn) /\ ghost_received_sockIn_msgs' = Append(ghost_received_sockIn_msgs, tIn_msg') /\ IF tIn_msg' = "(close)" THEN /\ send_ack_close' = TRUE /\ mbOut' = Append(mbOut, "flush-and-ack-close") /\ mbQueryRes' = Append(mbQueryRes, "close") /\ pc' = [pc EXCEPT !["conn-in"] = "Done"] /\ UNCHANGED << mbQuery, mbRequests, ghost_got_close_ack >> ELSE /\ IF tIn_msg' = "(ack-close)" THEN /\ ghost_got_close_ack' = TRUE /\ pc' = [pc EXCEPT !["conn-in"] = "Done"] /\ UNCHANGED << mbQueryRes, mbQuery, mbRequests >> ELSE /\ IF tIn_msg' \in CliQueries THEN /\ mbRequests' = Append(mbRequests, tIn_msg') /\ pc' = [pc EXCEPT !["conn-in"] = "conn_in"] /\ UNCHANGED << mbQueryRes, mbQuery >> ELSE /\ IF tIn_msg' \in SrvQueryResults THEN /\ mbQueryRes' = Append(mbQueryRes, tIn_msg') /\ pc' = [pc EXCEPT !["conn-in"] = "conn_in"] /\ UNCHANGED mbQuery ELSE /\ IF tIn_msg' = "connection-cut" THEN /\ mbQueryRes' = Append(mbQueryRes, "fail") /\ mbQuery' = Append(mbQuery, CLOSE) ELSE /\ Assert(Print("Invalid message", FALSE), "Failure of assertion at line 139, column 3 of macro called at line 235, column 5.") /\ UNCHANGED << mbQueryRes, mbQuery >> /\ pc' = [pc EXCEPT !["conn-in"] = "Done"] /\ UNCHANGED mbRequests /\ UNCHANGED ghost_got_close_ack /\ UNCHANGED << mbOut, send_ack_close >> /\ UNCHANGED << WaitForServerQueriesBeforeClosing, flag_serverTriesToClose, flag_remote_waits_for_close, IncomingQueries, OutgoingQueries, sockOut, mbQueryCopy, queriesToSend, sentQueries, send_close, ghost_droppedQueries, ghost_received_sockOut_msgs, stack, tOut_msg, tOut_flush, tJoin_q, tJoin_res, tJoin_fail_remaining, tSend_q, tServer_req, checkId, remoteMsgs, rmsg, expResps, tRemote_received >> tIn == conn_in query_joiner == /\ pc["query-joiner"] = "query_joiner" /\ ~QueueEmpty(mbQueryCopy) /\ tJoin_q' = QueuePeek(mbQueryCopy) /\ mbQueryCopy' = Tail(mbQueryCopy) /\ IF tJoin_q' = CLOSE THEN /\ tJoin_fail_remaining' = TRUE /\ pc' = [pc EXCEPT !["query-joiner"] = "fail_remaining"] ELSE /\ IF tJoin_q' = CLOSE_CLEAN THEN /\ TRUE /\ pc' = [pc EXCEPT !["query-joiner"] = "fail_remaining"] ELSE /\ pc' = [pc EXCEPT !["query-joiner"] = "join_get_resp"] /\ UNCHANGED tJoin_fail_remaining /\ UNCHANGED << WaitForServerQueriesBeforeClosing, flag_serverTriesToClose, flag_remote_waits_for_close, IncomingQueries, OutgoingQueries, sockIn, sockOut, mbQueryRes, mbQuery, mbOut, mbRequests, queriesToSend, sentQueries, send_ack_close, send_close, ghost_droppedQueries, ghost_received_sockOut_msgs, ghost_received_sockIn_msgs, ghost_got_close_ack, stack, tOut_msg, tOut_flush, tIn_msg, tJoin_res, tSend_q, tServer_req, checkId, remoteMsgs, rmsg, expResps, tRemote_received >> join_get_resp == /\ pc["query-joiner"] = "join_get_resp" /\ ~QueueEmpty(mbQueryRes) /\ tJoin_res' = QueuePeek(mbQueryRes) /\ mbQueryRes' = Tail(mbQueryRes) /\ IF tJoin_res' \in {"close", "fail"} THEN /\ Assert(sentQueries[tJoin_q].res = WAITING_RESPONSE, "Failure of assertion at line 150, column 3 of macro called at line 254, column 7.") /\ sentQueries' = (tJoin_q :> [q |-> sentQueries[tJoin_q].q, res |-> FAILED] @@ [i \in DOMAIN sentQueries \ {tJoin_q} |-> sentQueries[i]]) /\ tJoin_fail_remaining' = TRUE /\ pc' = [pc EXCEPT !["query-joiner"] = "fail_remaining"] ELSE /\ pc' = [pc EXCEPT !["query-joiner"] = "set_query_result"] /\ UNCHANGED << sentQueries, tJoin_fail_remaining >> /\ UNCHANGED << WaitForServerQueriesBeforeClosing, flag_serverTriesToClose, flag_remote_waits_for_close, IncomingQueries, OutgoingQueries, sockIn, sockOut, mbQuery, mbQueryCopy, mbOut, mbRequests, queriesToSend, send_ack_close, send_close, ghost_droppedQueries, ghost_received_sockOut_msgs, ghost_received_sockIn_msgs, ghost_got_close_ack, stack, tOut_msg, tOut_flush, tIn_msg, tJoin_q, tSend_q, tServer_req, checkId, remoteMsgs, rmsg, expResps, tRemote_received >> set_query_result == /\ pc["query-joiner"] = "set_query_result" /\ Assert(sentQueries[tJoin_q].res = WAITING_RESPONSE, "Failure of assertion at line 150, column 3 of macro called at line 258, column 7.") /\ sentQueries' = (tJoin_q :> [q |-> sentQueries[tJoin_q].q, res |-> tJoin_res] @@ [i \in DOMAIN sentQueries \ {tJoin_q} |-> sentQueries[i]]) /\ pc' = [pc EXCEPT !["query-joiner"] = "query_joiner"] /\ UNCHANGED << WaitForServerQueriesBeforeClosing, flag_serverTriesToClose, flag_remote_waits_for_close, IncomingQueries, OutgoingQueries, sockIn, sockOut, mbQueryRes, mbQuery, mbQueryCopy, mbOut, mbRequests, queriesToSend, send_ack_close, send_close, ghost_droppedQueries, ghost_received_sockOut_msgs, ghost_received_sockIn_msgs, ghost_got_close_ack, stack, tOut_msg, tOut_flush, tIn_msg, tJoin_q, tJoin_res, tJoin_fail_remaining, tSend_q, tServer_req, checkId, remoteMsgs, rmsg, expResps, tRemote_received >> fail_remaining == /\ pc["query-joiner"] = "fail_remaining" /\ IF tJoin_fail_remaining THEN /\ pc' = [pc EXCEPT !["query-joiner"] = "fail_remaining_loop"] ELSE /\ pc' = [pc EXCEPT !["query-joiner"] = "Done"] /\ UNCHANGED << WaitForServerQueriesBeforeClosing, flag_serverTriesToClose, flag_remote_waits_for_close, IncomingQueries, OutgoingQueries, sockIn, sockOut, mbQueryRes, mbQuery, mbQueryCopy, mbOut, mbRequests, queriesToSend, sentQueries, send_ack_close, send_close, ghost_droppedQueries, ghost_received_sockOut_msgs, ghost_received_sockIn_msgs, ghost_got_close_ack, stack, tOut_msg, tOut_flush, tIn_msg, tJoin_q, tJoin_res, tJoin_fail_remaining, tSend_q, tServer_req, checkId, remoteMsgs, rmsg, expResps, tRemote_received >> fail_remaining_loop == /\ pc["query-joiner"] = "fail_remaining_loop" /\ IF ~QueueEmpty(mbQueryCopy) THEN /\ IF QueuePeek(mbQueryCopy) \notin {CLOSE, CLOSE_CLEAN} THEN /\ Assert(sentQueries[(QueuePeek(mbQueryCopy))].res = WAITING_RESPONSE, "Failure of assertion at line 150, column 3 of macro called at line 267, column 7.") /\ sentQueries' = ((QueuePeek(mbQueryCopy)) :> [q |-> sentQueries[(QueuePeek(mbQueryCopy))].q, res |-> FAILED] @@ [i \in DOMAIN sentQueries \ {(QueuePeek(mbQueryCopy))} |-> sentQueries[i]]) ELSE /\ TRUE /\ UNCHANGED sentQueries /\ mbQueryCopy' = Tail(mbQueryCopy) /\ pc' = [pc EXCEPT !["query-joiner"] = "fail_remaining_loop"] /\ UNCHANGED mbQuery ELSE /\ IF ~QueueEmpty(mbQuery) THEN /\ IF QueuePeek(mbQuery) \notin {CLOSE, CLOSE_CLEAN} THEN /\ Assert(sentQueries[(QueuePeek(mbQuery))].res = WAITING_RESPONSE, "Failure of assertion at line 150, column 3 of macro called at line 275, column 7.") /\ sentQueries' = ((QueuePeek(mbQuery)) :> [q |-> sentQueries[(QueuePeek(mbQuery))].q, res |-> FAILED] @@ [i \in DOMAIN sentQueries \ {(QueuePeek(mbQuery))} |-> sentQueries[i]]) /\ mbQuery' = Tail(mbQuery) /\ pc' = [pc EXCEPT !["query-joiner"] = "fail_remaining_loop"] ELSE /\ mbQuery' = Tail(mbQuery) /\ pc' = [pc EXCEPT !["query-joiner"] = "replace_close"] /\ UNCHANGED sentQueries ELSE /\ pc' = [pc EXCEPT !["query-joiner"] = "Done"] /\ UNCHANGED << mbQuery, sentQueries >> /\ UNCHANGED mbQueryCopy /\ UNCHANGED << WaitForServerQueriesBeforeClosing, flag_serverTriesToClose, flag_remote_waits_for_close, IncomingQueries, OutgoingQueries, sockIn, sockOut, mbQueryRes, mbOut, mbRequests, queriesToSend, send_ack_close, send_close, ghost_droppedQueries, ghost_received_sockOut_msgs, ghost_received_sockIn_msgs, ghost_got_close_ack, stack, tOut_msg, tOut_flush, tIn_msg, tJoin_q, tJoin_res, tJoin_fail_remaining, tSend_q, tServer_req, checkId, remoteMsgs, rmsg, expResps, tRemote_received >> replace_close == /\ pc["query-joiner"] = "replace_close" /\ mbQuery' = Append(mbQuery, CLOSE) /\ pc' = [pc EXCEPT !["query-joiner"] = "Done"] /\ UNCHANGED << WaitForServerQueriesBeforeClosing, flag_serverTriesToClose, flag_remote_waits_for_close, IncomingQueries, OutgoingQueries, sockIn, sockOut, mbQueryRes, mbQueryCopy, mbOut, mbRequests, queriesToSend, sentQueries, send_ack_close, send_close, ghost_droppedQueries, ghost_received_sockOut_msgs, ghost_received_sockIn_msgs, ghost_got_close_ack, stack, tOut_msg, tOut_flush, tIn_msg, tJoin_q, tJoin_res, tJoin_fail_remaining, tSend_q, tServer_req, checkId, remoteMsgs, rmsg, expResps, tRemote_received >> tJoin == query_joiner \/ join_get_resp \/ set_query_result \/ fail_remaining \/ fail_remaining_loop \/ replace_close query_send == /\ pc["query-send"] = "query_send" /\ ~QueueEmpty(mbQuery) /\ tSend_q' = QueuePeek(mbQuery) /\ mbQuery' = Tail(mbQuery) /\ mbQueryCopy' = Append(mbQueryCopy, tSend_q') /\ IF tSend_q' = CLOSE THEN /\ mbOut' = Append(mbOut, "close") /\ pc' = [pc EXCEPT !["query-send"] = "Done"] ELSE /\ IF tSend_q' = CLOSE_CLEAN THEN /\ mbOut' = Append(mbOut, "(close)") /\ pc' = [pc EXCEPT !["query-send"] = "Done"] ELSE /\ mbOut' = Append(mbOut, (sentQueries[tSend_q'].q)) /\ pc' = [pc EXCEPT !["query-send"] = "query_send"] /\ UNCHANGED << WaitForServerQueriesBeforeClosing, flag_serverTriesToClose, flag_remote_waits_for_close, IncomingQueries, OutgoingQueries, sockIn, sockOut, mbQueryRes, mbRequests, queriesToSend, sentQueries, send_ack_close, send_close, ghost_droppedQueries, ghost_received_sockOut_msgs, ghost_received_sockIn_msgs, ghost_got_close_ack, stack, tOut_msg, tOut_flush, tIn_msg, tJoin_q, tJoin_res, tJoin_fail_remaining, tServer_req, checkId, remoteMsgs, rmsg, expResps, tRemote_received >> tSend == query_send maybe_break_connection == /\ pc["connection-breaker"] = "maybe_break_connection" /\ \/ /\ sockIn' = <<"connection-cut">> /\ sockOut' = <<"connection-cut">> /\ IF ghost_droppedQueries = <<>> THEN /\ ghost_droppedQueries' = WaitingQueries \o queriesToSend ELSE /\ TRUE /\ UNCHANGED ghost_droppedQueries \/ /\ TRUE /\ UNCHANGED <> /\ pc' = [pc EXCEPT !["connection-breaker"] = "Done"] /\ UNCHANGED << WaitForServerQueriesBeforeClosing, flag_serverTriesToClose, flag_remote_waits_for_close, IncomingQueries, OutgoingQueries, mbQueryRes, mbQuery, mbQueryCopy, mbOut, mbRequests, queriesToSend, sentQueries, send_ack_close, send_close, ghost_received_sockOut_msgs, ghost_received_sockIn_msgs, ghost_got_close_ack, stack, tOut_msg, tOut_flush, tIn_msg, tJoin_q, tJoin_res, tJoin_fail_remaining, tSend_q, tServer_req, checkId, remoteMsgs, rmsg, expResps, tRemote_received >> tBreaker == maybe_break_connection server == /\ pc["server"] = "server" /\ \/ ConnThreadsStopped \/ ~QueueEmpty(mbRequests) \/ ~QueueEmpty(queriesToSend) \/ flag_serverTriesToClose /\ IF ConnThreadsStopped THEN /\ TRUE /\ pc' = [pc EXCEPT !["server"] = "send_ack_close_"] /\ UNCHANGED << mbQuery, mbOut, mbRequests, queriesToSend, sentQueries, stack, tServer_req >> ELSE /\ IF QueueEmpty(queriesToSend) /\ flag_serverTriesToClose THEN /\ stack' = [stack EXCEPT !["server"] = << [ procedure |-> "CleanShutdown", pc |-> "send_ack_close_" ] >> \o stack["server"]] /\ pc' = [pc EXCEPT !["server"] = "CleanShutdown_entry"] /\ UNCHANGED << mbQuery, mbOut, mbRequests, queriesToSend, sentQueries, tServer_req >> ELSE /\ \/ /\ ~QueueEmpty(mbRequests) /\ tServer_req' = QueuePeek(mbRequests) /\ mbRequests' = Tail(mbRequests) /\ mbOut' = Append(mbOut, (SrvResponses[tServer_req'])) /\ UNCHANGED <> \/ /\ NoThreadsStopped /\ ~QueueEmpty(queriesToSend) /\ sentQueries' = Append(sentQueries, (Query((QueuePeek(queriesToSend)), WAITING_RESPONSE))) /\ mbQuery' = Append(mbQuery, (Len(sentQueries'))) /\ queriesToSend' = Tail(queriesToSend) /\ UNCHANGED <> /\ pc' = [pc EXCEPT !["server"] = "server_loopy"] /\ stack' = stack /\ UNCHANGED << WaitForServerQueriesBeforeClosing, flag_serverTriesToClose, flag_remote_waits_for_close, IncomingQueries, OutgoingQueries, sockIn, sockOut, mbQueryRes, mbQueryCopy, send_ack_close, send_close, ghost_droppedQueries, ghost_received_sockOut_msgs, ghost_received_sockIn_msgs, ghost_got_close_ack, tOut_msg, tOut_flush, tIn_msg, tJoin_q, tJoin_res, tJoin_fail_remaining, tSend_q, checkId, remoteMsgs, rmsg, expResps, tRemote_received >> server_loopy == /\ pc["server"] = "server_loopy" /\ pc' = [pc EXCEPT !["server"] = "server"] /\ UNCHANGED << WaitForServerQueriesBeforeClosing, flag_serverTriesToClose, flag_remote_waits_for_close, IncomingQueries, OutgoingQueries, sockIn, sockOut, mbQueryRes, mbQuery, mbQueryCopy, mbOut, mbRequests, queriesToSend, sentQueries, send_ack_close, send_close, ghost_droppedQueries, ghost_received_sockOut_msgs, ghost_received_sockIn_msgs, ghost_got_close_ack, stack, tOut_msg, tOut_flush, tIn_msg, tJoin_q, tJoin_res, tJoin_fail_remaining, tSend_q, tServer_req, checkId, remoteMsgs, rmsg, expResps, tRemote_received >> send_ack_close_ == /\ pc["server"] = "send_ack_close_" /\ IF send_close THEN /\ Assert(ConnThreadsStopped, "Failure of assertion at line 351, column 3.") /\ IF ~BrokenSocket(sockOut) THEN /\ sockOut' = Append(sockOut, "(close)") ELSE /\ TRUE /\ UNCHANGED sockOut ELSE /\ IF send_ack_close THEN /\ Assert(ConnThreadsStopped, "Failure of assertion at line 355, column 3.") /\ IF ~BrokenSocket(sockOut) THEN /\ sockOut' = Append(sockOut, "(ack-close)") ELSE /\ TRUE /\ UNCHANGED sockOut ELSE /\ TRUE /\ UNCHANGED sockOut /\ pc' = [pc EXCEPT !["server"] = "check_query_responses"] /\ UNCHANGED << WaitForServerQueriesBeforeClosing, flag_serverTriesToClose, flag_remote_waits_for_close, IncomingQueries, OutgoingQueries, sockIn, mbQueryRes, mbQuery, mbQueryCopy, mbOut, mbRequests, queriesToSend, sentQueries, send_ack_close, send_close, ghost_droppedQueries, ghost_received_sockOut_msgs, ghost_received_sockIn_msgs, ghost_got_close_ack, stack, tOut_msg, tOut_flush, tIn_msg, tJoin_q, tJoin_res, tJoin_fail_remaining, tSend_q, tServer_req, checkId, remoteMsgs, rmsg, expResps, tRemote_received >> check_query_responses == /\ pc["server"] = "check_query_responses" /\ IF checkId < Len(sentQueries) THEN /\ checkId' = checkId + 1 /\ IF LET query == sentQueries[checkId'] IN query.res = CliResponses[query.q] THEN /\ IF /\ ghost_droppedQueries /= <<>> /\ sentQueries[checkId'].q = Head(ghost_droppedQueries) THEN /\ ghost_droppedQueries' = Tail(ghost_droppedQueries) ELSE /\ TRUE /\ UNCHANGED ghost_droppedQueries /\ pc' = [pc EXCEPT !["server"] = "check_query_responses"] ELSE /\ IF /\ ghost_droppedQueries /= <<>> /\ sentQueries[checkId'].q = Head(ghost_droppedQueries) THEN /\ Assert(sentQueries[checkId'].res = FAILED, "Failure of assertion at line 381, column 7.") /\ ghost_droppedQueries' = Tail(ghost_droppedQueries) /\ pc' = [pc EXCEPT !["server"] = "check_query_responses"] ELSE /\ Assert(Print((<<"Query result wrong", checkId', sentQueries[checkId'] >>), FALSE), "Failure of assertion at line 139, column 3 of macro called at line 386, column 7.") /\ pc' = [pc EXCEPT !["server"] = "server_stop"] /\ UNCHANGED ghost_droppedQueries ELSE /\ pc' = [pc EXCEPT !["server"] = "server_stop"] /\ UNCHANGED << ghost_droppedQueries, checkId >> /\ UNCHANGED << WaitForServerQueriesBeforeClosing, flag_serverTriesToClose, flag_remote_waits_for_close, IncomingQueries, OutgoingQueries, sockIn, sockOut, mbQueryRes, mbQuery, mbQueryCopy, mbOut, mbRequests, queriesToSend, sentQueries, send_ack_close, send_close, ghost_received_sockOut_msgs, ghost_received_sockIn_msgs, ghost_got_close_ack, stack, tOut_msg, tOut_flush, tIn_msg, tJoin_q, tJoin_res, tJoin_fail_remaining, tSend_q, tServer_req, remoteMsgs, rmsg, expResps, tRemote_received >> server_stop == /\ pc["server"] = "server_stop" /\ IF ~BrokenSocket(sockIn) THEN /\ Assert(~WaitForServerQueriesBeforeClosing \/ queriesToSend = <<>>, "Failure of assertion at line 391, column 3.") ELSE /\ TRUE /\ Assert(( /\ flag_serverTriesToClose /\ WaitForServerQueriesBeforeClosing /\ flag_remote_waits_for_close /\ ~BrokenSocket(sockIn)) => ghost_got_close_ack, "Failure of assertion at line 394, column 1.") /\ pc' = [pc EXCEPT !["server"] = "Done"] /\ UNCHANGED << WaitForServerQueriesBeforeClosing, flag_serverTriesToClose, flag_remote_waits_for_close, IncomingQueries, OutgoingQueries, sockIn, sockOut, mbQueryRes, mbQuery, mbQueryCopy, mbOut, mbRequests, queriesToSend, sentQueries, send_ack_close, send_close, ghost_droppedQueries, ghost_received_sockOut_msgs, ghost_received_sockIn_msgs, ghost_got_close_ack, stack, tOut_msg, tOut_flush, tIn_msg, tJoin_q, tJoin_res, tJoin_fail_remaining, tSend_q, tServer_req, checkId, remoteMsgs, rmsg, expResps, tRemote_received >> tServer == server \/ server_loopy \/ send_ack_close_ \/ check_query_responses \/ server_stop other == /\ pc["remote-end"] = "other" /\ \/ /\ <<>> /= remoteMsgs /\ \/ ~WaitForServerQueriesBeforeClosing \/ Head(remoteMsgs) /= "(close)" \/ AllQueriesDone /\ ~QueueEmpty(remoteMsgs) /\ rmsg' = QueuePeek(remoteMsgs) /\ remoteMsgs' = Tail(remoteMsgs) /\ IF rmsg' = "(close)" THEN /\ IF flag_remote_waits_for_close /\ flag_serverTriesToClose THEN /\ pc' = [pc EXCEPT !["remote-end"] = "handle_query"] /\ UNCHANGED << sockIn, ghost_droppedQueries, expResps >> ELSE /\ IF ~BrokenSocket(sockIn) THEN /\ sockIn' = Append(sockIn, rmsg') ELSE /\ TRUE /\ UNCHANGED sockIn /\ expResps' = Append(expResps, "(ack-close)") /\ IF ghost_droppedQueries = <<>> THEN /\ ghost_droppedQueries' = WaitingQueries \o queriesToSend ELSE /\ TRUE /\ UNCHANGED ghost_droppedQueries /\ pc' = [pc EXCEPT !["remote-end"] = "other"] ELSE /\ IF ~BrokenSocket(sockIn) THEN /\ sockIn' = Append(sockIn, rmsg') ELSE /\ TRUE /\ UNCHANGED sockIn /\ expResps' = Append(expResps, (SrvResponses[rmsg'])) /\ pc' = [pc EXCEPT !["remote-end"] = "other"] /\ UNCHANGED ghost_droppedQueries \/ /\ ~QueueEmpty(sockOut) /\ pc' = [pc EXCEPT !["remote-end"] = "handle_query"] /\ UNCHANGED <> \/ /\ QueueEmpty(remoteMsgs) /\ QueueEmpty(expResps) /\ ~flag_serverTriesToClose /\ pc' = [pc EXCEPT !["remote-end"] = "other_stop"] /\ UNCHANGED <> /\ UNCHANGED << WaitForServerQueriesBeforeClosing, flag_serverTriesToClose, flag_remote_waits_for_close, IncomingQueries, OutgoingQueries, sockOut, mbQueryRes, mbQuery, mbQueryCopy, mbOut, mbRequests, queriesToSend, sentQueries, send_ack_close, send_close, ghost_received_sockOut_msgs, ghost_received_sockIn_msgs, ghost_got_close_ack, stack, tOut_msg, tOut_flush, tIn_msg, tJoin_q, tJoin_res, tJoin_fail_remaining, tSend_q, tServer_req, checkId, tRemote_received >> handle_query == /\ pc["remote-end"] = "handle_query" /\ ~QueueEmpty(sockOut) /\ IF BrokenSocket(sockOut) THEN /\ tRemote_received' = "connection-cut" /\ UNCHANGED sockOut ELSE /\ tRemote_received' = QueuePeek(sockOut) /\ sockOut' = Tail(sockOut) /\ ghost_received_sockOut_msgs' = Append(ghost_received_sockOut_msgs, tRemote_received') /\ IF tRemote_received' = "connection-cut" \/ BrokenSocket(sockIn) THEN /\ pc' = [pc EXCEPT !["remote-end"] = "other_stop"] /\ UNCHANGED << sockIn, remoteMsgs, expResps >> ELSE /\ IF tRemote_received' \in SrvQueries THEN /\ IF ~BrokenSocket(sockIn) THEN /\ sockIn' = Append(sockIn, (CliResponses[tRemote_received'])) ELSE /\ TRUE /\ UNCHANGED sockIn /\ pc' = [pc EXCEPT !["remote-end"] = "other_loopy"] /\ UNCHANGED << remoteMsgs, expResps >> ELSE /\ IF tRemote_received' = "(close)" THEN /\ IF ~BrokenSocket(sockIn) THEN /\ sockIn' = Append(sockIn, "(ack-close)") ELSE /\ TRUE /\ UNCHANGED sockIn /\ remoteMsgs' = <<>> /\ pc' = [pc EXCEPT !["remote-end"] = "other_stop"] /\ UNCHANGED expResps ELSE /\ Assert(tRemote_received' = QueuePeek(expResps), "Failure of assertion at line 445, column 7.") /\ expResps' = Tail(expResps) /\ IF tRemote_received' = "(ack-close)" THEN /\ pc' = [pc EXCEPT !["remote-end"] = "other_stop"] ELSE /\ pc' = [pc EXCEPT !["remote-end"] = "other_loopy"] /\ UNCHANGED << sockIn, remoteMsgs >> /\ UNCHANGED << WaitForServerQueriesBeforeClosing, flag_serverTriesToClose, flag_remote_waits_for_close, IncomingQueries, OutgoingQueries, mbQueryRes, mbQuery, mbQueryCopy, mbOut, mbRequests, queriesToSend, sentQueries, send_ack_close, send_close, ghost_droppedQueries, ghost_received_sockIn_msgs, ghost_got_close_ack, stack, tOut_msg, tOut_flush, tIn_msg, tJoin_q, tJoin_res, tJoin_fail_remaining, tSend_q, tServer_req, checkId, rmsg >> other_loopy == /\ pc["remote-end"] = "other_loopy" /\ pc' = [pc EXCEPT !["remote-end"] = "other"] /\ UNCHANGED << WaitForServerQueriesBeforeClosing, flag_serverTriesToClose, flag_remote_waits_for_close, IncomingQueries, OutgoingQueries, sockIn, sockOut, mbQueryRes, mbQuery, mbQueryCopy, mbOut, mbRequests, queriesToSend, sentQueries, send_ack_close, send_close, ghost_droppedQueries, ghost_received_sockOut_msgs, ghost_received_sockIn_msgs, ghost_got_close_ack, stack, tOut_msg, tOut_flush, tIn_msg, tJoin_q, tJoin_res, tJoin_fail_remaining, tSend_q, tServer_req, checkId, remoteMsgs, rmsg, expResps, tRemote_received >> other_stop == /\ pc["remote-end"] = "other_stop" /\ TRUE /\ pc' = [pc EXCEPT !["remote-end"] = "Done"] /\ UNCHANGED << WaitForServerQueriesBeforeClosing, flag_serverTriesToClose, flag_remote_waits_for_close, IncomingQueries, OutgoingQueries, sockIn, sockOut, mbQueryRes, mbQuery, mbQueryCopy, mbOut, mbRequests, queriesToSend, sentQueries, send_ack_close, send_close, ghost_droppedQueries, ghost_received_sockOut_msgs, ghost_received_sockIn_msgs, ghost_got_close_ack, stack, tOut_msg, tOut_flush, tIn_msg, tJoin_q, tJoin_res, tJoin_fail_remaining, tSend_q, tServer_req, checkId, remoteMsgs, rmsg, expResps, tRemote_received >> tRemote == other \/ handle_query \/ other_loopy \/ other_stop Next == tOut \/ tIn \/ tJoin \/ tSend \/ tBreaker \/ tServer \/ tRemote \/ (\E self \in ProcSet: CleanShutdown(self)) \/ (* Disjunct to prevent deadlock on termination *) ((\A self \in ProcSet: pc[self] = "Done") /\ UNCHANGED vars) Spec == Init /\ [][Next]_vars Termination == <>(\A self \in ProcSet: pc[self] = "Done") \* END TRANSLATION ================================================================================