8000 Fix wrong assertion in fuerte (#14660) · arangodb/arangodb@414dae6 · GitHub
[go: up one dir, main page]

Skip to content

Commit 414dae6

Browse files
authored
Fix wrong assertion in fuerte (#14660)
* Move assertion to the right place where the model has it. * CHANGELOG. * Adjust model and code one more time.
1 parent a34b0c9 commit 414dae6

File tree

3 files changed

+17
-11
lines changed

3 files changed

+17
-11
lines changed

3rdParty/fuerte/FuerteH1TCP.tla

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -124,7 +124,7 @@ process(fuerte = "fuertethread") {
124124
or connectDone: \* VERIFIED
125125
if (/\ Len(iocontext) >= 1
126126
/\ Head(iocontext) \in {"connect", "connectBAD"}) {
127-
assert state \in {"Connecting", "Created", "Closed"};
127+
assert state \in {"Connecting", "Closed"};
128128
alarm := "off";
129129
if (Head(iocontext) = "connect" /\ state = "Connecting") {
130130
assert active;
@@ -259,7 +259,7 @@ process(cancel = "cancelthread") {
259259
260260
}
261261
*)
262-
\* BEGIN TRANSLATION - the hash of the PCal code: PCal-925ea62a5ed7f2fd7841f2836c7d799c
262+
\* BEGIN TRANSLATION - the hash of the PCal code: PCal-925ea62a5ed7f2fd7841f2836c7d799c (chksum(pcal) = "c5aa3da3" /\ chksum(tla) = "af7613cb")
263263
VARIABLES state, active, queueSize, alarm, asyncRunning, iocontext, reading,
264264
writing, pc, stack
265265

@@ -464,12 +464,12 @@ activate == /\ pc["fuertethread"] = "activate"
464464
connectDone == /\ pc["fuertethread"] = "connectDone"
465465
/\ IF /\ Len(iocontext) >= 1
466466
/\ Head(iocontext) \in {"connect", "connectBAD"}
467-
THEN /\ Assert(state \in {"Connecting", "Created", "Closed"},
468-
"Failure of assertion at line 127, column 11.")
467+
THEN /\ Assert(state \in {"Connecting", "Closed"},
468+
"Failure of assertion at line 128, column 11.")
469469
/\ alarm' = "off"
470470
/\ IF Head(iocontext) = "connect" /\ state = "Connecting"
471471
THEN /\ Assert(active,
472-
"Failure of assertion at line 130, column 13.")
472+
"Failure of assertion at line 131, column 13.")
473473
/\ iocontext' = Tail(iocontext)
474474
/\ state' = "Connected"
475475
/\ stack' = [stack EXCEPT !["fuertethread"] = << [ procedure |-> "asyncWriteNextRequest",
@@ -492,7 +492,7 @@ writeDone == /\ pc["fuertethread"] = "writeDone"
492492
/\ Head(iocontext) \in {"write", "writeBAD"}
493493
THEN /\ Assert(/\ state \in {"Connected", "Closed"}
494494
/\ writing,
495-
"Failure of assertion at line 145, column 11.")
495+
"Failure of assertion at line 146, column 11.")
496496
/\ writing' = FALSE
497497
/\ IF Head(iocontext) = "write" /\ state = "Connected"
498498
THEN /\ iocontext' = Tail(iocontext)
@@ -517,7 +517,7 @@ readDone == /\ pc["fuertethread"] = "readDone"
517517
/\ IF /\ Len(iocontext) >= 1
518518
/\ Head(iocontext) \in {"read", "readBAD"}
519519
THEN /\ Assert(state \in {"Connected", "Closed"},
520-
"Failure of assertion at line 163, column 11.")
520+
"Failure of assertion at line 164, column 11.")
521521
/\ alarm' = "off"
522522
/\ reading' = FALSE
523523
/\ IF Head(iocontext) = "read" /\ state = "Connected"
@@ -714,6 +714,6 @@ NoSleepingBarber == /\ NothingForgottenOnQueue
714714

715715
=============================================================================
716716
\* Modification History
717-
\* Last modified Fri Aug 21 16:03:16 CEST 2020 by neunhoef
717+
\* Last modified Thu Aug 19 14:45:44 CEST 2021 by neunhoef
718718
\* Last modified Wed Jul 22 12:06:32 CEST 2020 by simon
719719
\* Created Mi 22. Apr 22:46:19 CEST 2020 by neunhoef

3rdParty/fuerte/src/H1Connection.cpp

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -194,15 +194,17 @@ void H1Connection<ST>::finishConnect() {
194194
// If it has already gone off, we might have a completion handler
195195
// already posted on the iocontext. However, this will not touch anything
196196
// if we have first set the state to `Connected`.
197-
FUERTE_ASSERT(this->_active.load());
198197
auto exp = Connection::State::Connecting;
199198
if (this->_state.compare_exchange_strong(exp, Connection::State::Connected)) {
199+
FUERTE_ASSERT(this->_active.load());
200200
this->asyncWriteNextRequest(); // starts writing if queue non-empty
201201
} else {
202202
FUERTE_LOG_ERROR << "finishConnect: found state other than 'Connecting': "
203203
<< static_cast<int>(exp);
204-
FUERTE_ASSERT(false);
205-
// If this happens, we probably have a sleeping barber
204+
FUERTE_ASSERT(exp == Connection::State::Closed);
205+
// If this happens, then the connection has been shut down before
206+
// it could be fully connected, but the completion handler of the
207+
// connect call was still scheduled. No more work to do.
206208
}
207209
}
208210

CHANGELOG

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,10 @@
11
devel
22
-----
33

4+
* Fix wrong assertion in fuerte and move it to where the TLA+ model says
5+
it should be. This fixes a unit test failure occurring on newer Macs
6+
with a certain clang version.
7+
48
* Remove old fixPrototypeChain agency migration, which was introduced in 3.2
59
and is no longer necessary. This will make it impossible to upgrade
610
directly from a version < 3.2 to a version >= 3.9, provided one has

0 commit comments

Comments
 (0)
0