8000 Fix wrong assertion in fuerte by neunhoef · Pull Request #14660 · arangodb/arangodb · GitHub
[go: up one dir, main page]
Skip to content

Fix wrong assertion in fuerte #14660

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 4 commits into from
Aug 19, 2021
Merged

Fix wrong assertion in fuerte #14660

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
e0f0efb
Move assertion to the right place where the model has it.
neunhoef Aug 18, 2021
e501135
CHANGELOG.
neunhoef Aug 18, 2021
c4cac92
Adjust model and code one more time.
neunhoef Aug 19, 2021
b77b72e
Merge branch 'devel' into bug-fix/fuerte-wrong-assertion
neunhoef Aug 19, 2021
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
16 changes: 8 additions & 8 deletions 3rdParty/fuerte/FuerteH1TCP.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -124,7 +124,7 @@ process(fuerte = "fuertethread") {
or connectDone: \* VERIFIED
if (/\ Len(iocontext) >= 1
/\ Head(iocontext) \in {"connect", "connectBAD"}) {
assert state \in {"Connecting", "Created", "Closed"};
assert state \in {"Connecting", "Closed"};
alarm := "off";
if (Head(iocontext) = "connect" /\ state = "Connecting") {
assert active;
Expand Down Expand Up @@ -259,7 +259,7 @@ process(cancel = "cancelthread") {

}
*)
\* BEGIN TRANSLATION - the hash of the PCal code: PCal-925ea62a5ed7f2fd7841f2836c7d799c
\* BEGIN TRANSLATION - the hash of the PCal code: PCal-925ea62a5ed7f2fd7841f2836c7d799c (chksum(pcal) = "c5aa3da3" /\ chksum(tla) = "af7613cb")
VARIABLES state, active, queueSize, alarm, asyncRunning, iocontext, reading,
writing, pc, stack

Expand Down Expand Up @@ -464,12 +464,12 @@ activate == /\ pc["fuertethread"] = "activate"
connectDone == /\ pc["fuertethread"] = "connectDone"
/\ IF /\ Len(iocontext) >= 1
/\ Head(iocontext) \in {"connect", "connectBAD"}
THEN /\ Assert(state \in {"Connecting", "Created", "Closed"},
"Failure of assertion at line 127, column 11.")
THEN /\ Assert(state \in {"Connecting", "Closed"},
"Failure of assertion at line 128, column 11.")
/\ alarm' = "off"
/\ IF Head(iocontext) = "connect" /\ state = "Connecting"
THEN /\ Assert(active,
"Failure of assertion at line 130, column 13.")
"Failure of assertion at line 131, column 13.")
/\ iocontext' = Tail(iocontext)
/\ state' = "Connected"
/\ stack' = [stack EXCEPT !["fuertethread"] = << [ procedure |-> "asyncWriteNextRequest",
Expand All @@ -492,7 +492,7 @@ writeDone == /\ pc["fuertethread"] = "writeDone"
/\ Head(iocontext) \in {"write", "writeBAD"}
THEN /\ Assert(/\ state \in {"Connected", "Closed"}
/\ writing,
"Failure of assertion at line 145, column 11.")
"Failure of assertion at line 146, column 11.")
/\ writing' = FALSE
/\ IF Head(iocontext) = "write" /\ state = "Connected"
THEN /\ iocontext' = Tail(iocontext)
Expand All @@ -517,7 +517,7 @@ readDone == /\ pc["fuertethread"] = "readDone"
/\ IF /\ Len(iocontext) >= 1
/\ Head(iocontext) \in {"read", "readBAD"}
THEN /\ Assert(state \in {"Connected", "Closed"},
"Failure of assertion at line 163, column 11.")
"Failure of assertion at line 164, column 11.")
/\ alarm' = "off"
/\ reading' = FALSE
/\ IF Head(iocontext) = "read" /\ state = "Connected"
Expand Down Expand Up @@ -714,6 +714,6 @@ NoSleepingBarber == /\ NothingForgottenOnQueue

=============================================================================
\* Modification History
\* Last modified Fri Aug 21 16:03:16 CEST 2020 by neunhoef
\* Last modified Thu Aug 19 14:45:44 CEST 2021 by neunhoef
\* Last modified Wed Jul 22 12:06:32 CEST 2020 by simon
\* Created Mi 22. Apr 22:46:19 CEST 2020 by neunhoef
8 changes: 5 additions & 3 deletions 3rdParty/fuerte/src/H1Connection.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -194,15 +194,17 @@ void H1Connection<ST>::finishConnect() {
// If it has already gone off, we might have a completion handler
// already posted on the iocontext. However, this will not touch anything
// if we have first set the state to `Connected`.
FUERTE_ASSERT(this->_active.load());
auto exp = Connection::State::Connecting;
if (this->_state.compare_exchange_strong(exp, Connection::State::Connected)) {
FUERTE_ASSERT(this->_active.load());
this->asyncWriteNextRequest(); // starts writing if queue non-empty
} else {
FUERTE_LOG_ERROR << "finishConnect: found state other than 'Connecting': "
<< static_cast<int>(exp);
FUERTE_ASSERT(false);
// If this happens, we probably have a sleeping barber
FUERTE_ASSERT(exp == Connection::State::Closed);
// If this happens, then the connection has been shut down before
// it could be fully connected, but the completion handler of the
// connect call was still scheduled. No more work to do.
}
}

Expand Down
4 changes: 4 additions & 0 deletions CHANGELOG
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,10 @@
devel
-----

* Fix wrong assertion in fuerte and move it to where the TLA+ model says
it should be. This fixes a unit test failure occurring on newer Macs
with a certain clang version.

* Remove old fixPrototypeChain agency migration, which was introduced in 3.2
and is no longer necessary. This will make it impossible to upgrade
directly from a version < 3.2 to a version >= 3.9, provided one has
Expand Down
0