10000 Fuerte simplify by graetzer · Pull Request #12270 · arangodb/arangodb · GitHub
[go: up one dir, main page]
Skip to content

Fuerte simplify #12270

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 31 commits into from
Aug 24, 2020
Merged

Fuerte simplify #12270

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
31 commits
Select commit Hold shift + click to select a range
2c04571
Simplify fuerte code
graetzer Jun 26, 2020
24c1529
fix #warning
graetzer Jun 26, 2020
3412930
Merge branch 'devel' of github.com:arangodb/arangodb into feature/fue…
graetzer Jun 29, 2020
002412b
change defaults
graetzer Jun 29, 2020
0a9ac62
slight fixes
graetzer Jun 30, 2020
95e2e4b
slight adjustments
graetzer Jul 1, 2020
9aa85fa
Starting HTTP/2 with Prior Knowledge
graetzer Jul 3, 2020
efa00a3
make consistent
graetzer Jul 3, 2020
46cb4a8
Merge branch 'feature/http2-prior-knowledge' into feature/fuerte-simp…
graetzer Jul 3, 2020
528a0f6
fix some requests
graetzer Jul 8, 2020
3fa1586
fix architectire
graetzer Jul 13, 2020
da6c3e4
Merge branch 'devel' of github.com:arangodb/arangodb into feature/fue…
graetzer Jul 13, 2020
a5e1da2
fix stuff
graetzer Jul 13, 2020
1426f9b
Properly cancel broken connections
graetzer Jul 14, 2020
e070136
remove extra log statements
graetzer Jul 14, 2020
05c578a
Merge branch 'devel' of github.com:arangodb/arangodb into feature/fue…
graetzer Jul 21, 2020
931c22e
remove unused code
graetzer Jul 21, 2020
a7bd312
some changes to vst
graetzer Jul 21, 2020
56e3a53
adjust TLA+ pluscal models
graetzer Jul 22, 2020
50da56c
Merge branch 'devel' of github.com:arangodb/arangodb into feature/fue…
graetzer Jul 22, 2020
b9208ea
fix some stuff
graetzer Jul 22, 2020
088a759
fix mistake
graetzer Jul 22, 2020
92a050f
fixing VST connection
graetzer Jul 23, 2020
67faddb
Merge remote-tracking branch 'origin/devel' into feature/fuerte-simplify
neunhoef Aug 20, 2020
b25c331
Correct mode: we call shutdownConnection when it is time.
neunhoef Aug 21, 2020
439abaa
File no longer necessary.
neunhoef Aug 21, 2020
17df268
Comment fixes.
neunhoef Aug 21, 2020
e4e9d4d
Add a forgotten alarm cancellation to model.
neunhoef Aug 21, 2020
092e27c
Fix cancellation in model.
neunhoef Aug 21, 2020
57e1777
Take latest transaction.
neunhoef Aug 21, 2020
d09a0a8
This is a sub-PR to suggest some changes. (#12495)
neunhoef Aug 24, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
adjust TLA+ pluscal models
  • Loading branch information
@graetzer
graetzer committed Jul 22, 2020
commit 56e3a53546b12b2161bbc6b4d350661f1ab6d0ca
115 changes: 47 additions & 68 deletions 3rdParty/fuerte/FuerteH1TCP.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ EXTENDS Integers, TLC, Sequences
--algorithm H1Connection {

variables \* VERIFIED
state = "Disconnected", \* this is a member variable in the program
state = "Created", \* this is a member variable in the program
active = FALSE, \* this is a member variable in the program
queueSize = 0, \* this is the length of the input queue
alarm = "off", \* this encodes, if an alarm is set
Expand All @@ -21,11 +21,11 @@ variables \* VERIFIED
\* finished

procedure startConnection() { \* VERIFIED
(* This is called whenever the connection broke and we want to immediately
reconnect. Therefore we know that the state is "Disconnected" and we
(* This is called whenever the connection was created and the first request is queued.
Therefore we know that the state is "Created" and we
are active and no alarm is set. *)
startConnectionBegin:
assert /\ state = "Disconnected"
assert /\ state = "Created"
/\ active
/\ asyncRunning = "none"
/\ alarm = "off";
Expand All @@ -37,11 +37,11 @@ procedure startConnection() { \* VERIFIED

procedure asyncWriteNextRequest() { \* VERIFIED
(* This is called whenever we are active and potentially want to continue
writing. It can also be called if we are in the "Failed" state. In this
writing. It can also be called if we are in the "Closed" state. In this
case the purpose is to reset the `active` flag, which is exclusively
done in this procedure. *)
asyncWriteNextRequestBegin:
assert /\ state \in {"Connected", "Failed"}
assert /\ state \in {"Connected", "Closed"}
/\ active
/\ asyncRunning = "none";
(* We use the check-set-check pattern to make sure we are not going to
Expand Down Expand Up @@ -87,11 +87,11 @@ process(fuerte = "fuertethread") {
if (Len(iocontext) >= 1 /\ Head(iocontext) = "activate") {
assert active /\ state /= "Connecting";
iocontext := Tail(iocontext);
if (state = "Disconnected") {
if (state = "Created") {
call startConnection();
} else if (state = "Connected") {
call asyncWriteNextRequest();
} else if (state = "Failed") {
} else if (state = "Closed") {
active := FALSE;
queueSize := 0;
};
Expand All @@ -100,16 +100,16 @@ process(fuerte = "fuertethread") {
or connectDone: \* VERIFIED
if (/\ Len(iocontext) >= 1
/\ Head(iocontext) \in {"connect", "connectBAD"}) {
assert active /\ state \in {"Connecting", "Disconnected", "Failed"};
assert active /\ state \in {"Connecting", "Created", "Closed"};
alarm := "off";
if (Head(iocontext) = "connect" /\ state = "Connecting") {
iocontext := Tail(iocontext);
state := "Connected";
} else {
(* for the sake of simplicity we ignore the retries here and
directly go to the Failed state *)
directly go to the Closed state *)
iocontext := Tail(iocontext);
state := "Failed";
state := "Closed";
queueSize := 0;
};
call asyncWriteNextRequest();
Expand All @@ -119,7 +119,7 @@ process(fuerte = "fuertethread") {
if (/\ Len(iocontext) >= 1
/\ Head(iocontext) \in {"write", "writeBAD"}) {
assert /\ active
/\ state \in {"Connected", "Disconnected", "Failed"}
/\ state \in {"Connected", "Closed"}
/\ writing;
writing := FALSE;
if (Head(iocontext) = "write" /\ state = "Connected") {
Expand All @@ -130,36 +130,26 @@ process(fuerte = "fuertethread") {
} else {
iocontext := Tail(iocontext);
alarm := "off";
if (state /= "Failed") {
state := "Disconnected";
call startConnection();
\* this for now ignores the retry if nothing was written yet,
\* this models that an error is returned to the client and we
\* try to reconnect and execute the next request
} else {
\* this is only to reset the `active` flag
call asyncWriteNextRequest();
}
state := "Closed";
\* this is only to reset the `active` flag
call asyncWriteNextRequest();
};
};

or readDone: \* VERIFIED
if (/\ Len(iocontext) >= 1
/\ Head(iocontext) \in {"read", "readBAD"}) {
assert active /\ state \in {"Connected", "Disconnected", "Failed"};
assert active /\ state \in {"Connected", "Closed"};
alarm := "off";
reading := FALSE;
if (Head(iocontext) = "read" /\ state = "Connected") {
iocontext := Tail(iocontext);
call asyncWriteNextRequest();
} else {
iocontext := Tail(iocontext);
if (state /= "Failed") {
state := "Disconnected";
call startConnection();
} else {
call asyncWriteNextRequest();
};
state := "Closed";
\* this is only to reset the `active` flag
call asyncWriteNextRequest();
};
};

Expand All @@ -168,7 +158,7 @@ process(fuerte = "fuertethread") {
iocontext := Tail(iocontext);
\* Note that we *do not* set active to FALSE here, since we want
\* to interfere as little as possible with the active business.
state := "Failed";
state := "Closed";
queueSize := 0;
alarm := "off";
if (asyncRunning = "connect") {
Expand Down Expand Up @@ -228,7 +218,7 @@ process(fuerte = "fuertethread") {
if (Len(iocontext) >= 1 /\ Head(iocontext) = "idleAlarm") {
iocontext := Tail(iocontext);
if (state = "Connected") {
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Let's add the condition ~ active here, as it is in the code. This does not pose problems in the model, I checked.

state := "Disconnected";
state := "Closed";
alarm := "off";
\* it is possible that the idle alarm was still set, since we have
\* gone to sleep and we have been posted on the iocontext beforehand
Expand Down Expand Up @@ -260,7 +250,7 @@ process(cancel = "cancelthread") {

}
*)
\* BEGIN TRANSLATION
\* BEGIN TRANSLATION - the hash of the PCal code: PCal-925ea62a5ed7f2fd7841f2836c7d799c
VARIABLES state, active, queueSize, alarm, asyncRunning, iocontext, reading,
writing, pc, stack

Expand All @@ -270,7 +260,7 @@ vars == << state, active, queueSize, alarm, asyncRunning, iocontext, reading,
ProcSet == {"fuertethread"} \cup {"clientthread"} \cup {"cancelthread"}

Init == (* Global variables *)
/\ state = "Disconnected"
/\ state = "Created"
/\ active = FALSE
/\ queueSize = 0
/\ alarm = "off"
Expand All @@ -284,7 +274,7 @@ Init == (* Global variables *)
[] self = "cancelthread" -> "cancelBegin"]

startConnectionBegin(self) == /\ pc[self] = "startConnectionBegin"
/\ Assert(/\ state = "Disconnected"
/\ Assert(/\ state = "Created"
/\ active
/\ asyncRunning = "none"
/\ alarm = "off",
Expand All @@ -300,7 +290,7 @@ startConnectionBegin(self) == /\ pc[self] = "startConnectionBegin"
startConnection(self) == startConnectionBegin(self)

asyncWriteNextRequestBegin(self) == /\ pc[self] = "asyncWriteNextRequestBegin"
/\ Assert(/\ state \in {"Connected", "Failed"}
/\ Assert(/\ state \in {"Connected", "Closed"}
/\ active
/\ asyncRunning = "none",
"Failure of assertion at line 44, column 3.")
Expand Down Expand Up @@ -383,7 +373,7 @@ activate == /\ pc["fuertethread"] = "activate"
THEN /\ Assert(active /\ state /= "Connecting",
"Failure of assertion at line 88, column 11.")
/\ iocontext' = Tail(iocontext)
/\ IF state = "Disconnected"
/\ IF state = "Created"
THEN /\ stack' = [stack EXCEPT !["fuertethread"] = << [ procedure |-> "startConnection",
pc |-> "loop" ] >>
\o stack["fuertethread"]]
Expand All @@ -395,7 +385,7 @@ activate == /\ pc["fuertethread"] = "activate"
\o stack["fuertethread"]]
/\ pc' = [pc EXCEPT !["fuertethread"] = "asyncWriteNextRequestBegin"]
/\ UNCHANGED << active, queueSize >>
ELSE /\ IF state = "Failed"
ELSE /\ IF state = "Closed"
THEN /\ active' = FALSE
/\ queueSize' = 0
ELSE /\ TRUE
Expand All @@ -410,15 +400,15 @@ activate == /\ pc["fuertethread"] = "activate"
connectDone == /\ pc["fuertethread"] = "connectDone"
/\ IF /\ Len(iocontext) >= 1
/\ Head(iocontext) \in {"connect", "connectBAD"}
THEN /\ Assert(active /\ state \in {"Connecting", "Disconnected", "Failed"},
THEN /\ Assert(active /\ state \in {"Connecting", "Created", "Closed"},
"Failure of assertion at line 103, column 11.")
/\ alarm' = "off"
/\ IF Head(iocontext) = "connect" /\ state = "Connecting"
THEN /\ iocontext' = Tail(iocontext)
/\ state' = "Connected"
/\ UNCHANGED queueSize
ELSE /\ iocontext' = Tail(iocontext)
/\ state' = "Failed"
/\ state' = "Closed"
/\ queueSize' = 0
/\ stack' = [stack EXCEPT !["fuertethread"] = << [ procedure |-> "asyncWriteNextRequest",
pc |-> "loop" ] >>
Expand All @@ -433,7 +423,7 @@ writeDone == /\ pc["fuertethread"] = "writeDone"
/\ IF /\ Len(iocontext) >= 1
/\ Head(iocontext) \in {"write", "writeBAD"}
THEN /\ Assert(/\ active
/\ state \in {"Connected", "Disconnected", "Failed"}
/\ state \in {"Connected", "Closed"}
/\ writing,
"Failure of assertion at line 121, column 11.")
/\ writing' = FALSE
Expand All @@ -446,17 +436,11 @@ writeDone == /\ pc["fuertethread"] = "writeDone"
/\ UNCHANGED << state, stack >>
ELSE /\ iocontext' = Tail(iocontext)
/\ alarm' = "off"
/\ IF state /= "Failed"
THEN /\ state' = "Disconnected"
/\ stack' = [stack EXCEPT !["fuertethread"] = << [ procedure |-> "startConnection",
pc |-> "loop" ] >>
\o stack["fuertethread"]]
/\ pc' = [pc EXCEPT !["fuertethread"] = "startConnectionBegin"]
ELSE /\ stack' = [stack EXCEPT !["fuertethread"] = << [ procedure |-> "asyncWriteNextRequest",
pc |-> "loop" ] >>
\o stack["fuertethread"]]
/\ pc' = [pc EXCEPT !["fuertethread"] = "asyncWriteNextRequestBegin"]
/\ state' = state
/\ state' = "Closed"
/\ stack' = [stack EXCEPT !["fuertethread"] = << [ procedure |-> "asyncWriteNextRequest",
pc |-> "loop" ] >>
\o stack["fuertethread"]]
/\ pc' = [pc EXCEPT !["fuertethread"] = "asyncWriteNextRequestBegin"]
/\ UNCHANGED << asyncRunning, reading >>
ELSE /\ pc' = [pc EXCEPT !["fuertethread"] = "loop"]
/\ UNCHANGED << state, alarm, asyncRunning, iocontext,
Expand All @@ -466,8 +450,8 @@ writeDone == /\ pc["fuertethread"] = "writeDone"
readDone == /\ pc["fuertethread"] = "readDone"
/\ IF /\ Len(iocontext) >= 1
/\ Head(iocontext) \in {"read", "readBAD"}
THEN /\ Assert(active /\ state \in {"Connected", "Disconnected", "Failed"},
"Failure of assertion at line 149, column 11.")
THEN /\ Assert(active /\ state \in {"Connected", "Closed"},
"Failure of assertion at line 142, column 11.")
/\ alarm' = "off"
/\ reading' = FALSE
/\ IF Head(iocontext) = "read" /\ state = "Connected"
Expand All @@ -478,25 +462,19 @@ readDone == /\ pc["fuertethread"] = "readDone"
/\ pc' = [pc EXCEPT !["fuertethread"] = "asyncWriteNextRequestBegin"]
/\ state' = state
ELSE /\ iocontext' = Tail(iocontext)
/\ IF state /= "Failed"
THEN /\ state' = "Disconnected"
/\ stack' = [stack EXCEPT !["fuertethread"] = << [ procedure |-> "startConnection",
pc |-> "loop" ] >>
\o stack["fuertethread"]]
/\ pc' = [pc EXCEPT !["fuertethread"] = "startConnectionBegin"]
ELSE /\ stack' = [stack EXCEPT !["fuertethread"] = << [ procedure |-> "asyncWriteNextRequest",
pc |-> "loop" ] >>
\o stack["fuertethread"]]
/\ pc' = [pc EXCEPT !["fuertethread"] = "asyncWriteNextRequestBegin"]
/\ state' = state
/\ state' = "Closed"
/\ stack' = [stack EXCEPT !["fuertethread"] = << [ procedure |-> "asyncWriteNextRequest",
pc |-> "loop" ] >>
\o stack["fuertethread"]]
/\ pc' = [pc EXCEPT !["fuertethread"] = "asyncWriteNextRequestBegin"]
ELSE /\ pc' = [pc EXCEPT !["fuertethread"] = "loop"]
/\ UNCHANGED << state, alarm, iocontext, reading, stack >>
/\ UNCHANGED << active, queueSize, asyncRunning, writing >>

cancellation == /\ pc["fuertethread"] = "cancellation"
/\ IF /\ Len(iocontext) >= 1 /\ Head(iocontext) = "cancel"
THEN /\ iocontext' = Tail(iocontext)
/\ state' = "Failed"
/\ state' = "Closed"
/\ queueSize' = 0
/\ alarm' = "off"
/\ IF asyncRunning = "connect"
Expand Down Expand Up @@ -576,7 +554,7 @@ handleIdleAlarm == /\ pc["fuertethread"] = "handleIdleAlarm"
/\ IF Len(iocontext) >= 1 /\ Head(iocontext) = "idleAlarm"
THEN /\ iocontext' = Tail(iocontext)
/\ IF state = "Connected"
THEN /\ state' = "Disconnected"
THEN /\ state' = "Closed"
/\ alarm' = "off"
ELSE /\ TRUE
/\ UNCHANGED << state, alarm >>
Expand Down Expand Up @@ -629,11 +607,11 @@ Next == fuerte \/ client \/ cancel

Spec == Init /\ [][Next]_vars

\* END TRANSLATION
\* END TRANSLATION - the hash of the generated TLA code (remove to silence divergence warnings): TLA-b4f0892f475b000215f25d9b188fcb51

\* Invariants to prove:

TypeOK == /\ state \in {"Disconnected", "Connecting", "Connected", "Failed"}
TypeOK == /\ state \in {"Created", "Connecting", "Connected", "Closed"}
/\ active \in {FALSE, TRUE}
/\ queueSize \in 0..2
/\ alarm \in {"off", "connectAlarm", "writeAlarm", "readAlarm",
Expand Down Expand Up @@ -672,5 +650,6 @@ NoSleepingBarber == /\ NothingForgottenOnQueue

=============================================================================
\* Modification History
\* Last modified Wed Jul 22 12:06:32 CEST 2020 by simon
\* Last modified Mon May 04 22:05:04 CEST 2020 by neunhoef
\* Created Mi 22. Apr 22:46:19 CEST 2020 by neunhoef
Loading
0