Wolf480plDec 20, 2024

So yesterday TLA+ made me realize that the property of my protocol that I'm trying to verify makes no sense (the incorrect behaviour is indistinguishable from a client's PoV from a correct behaviour).

So I was thinking how I could make it distinguishable in a way that will work not only in TLA+ but also in real life, and it turns out I could really use pings in the protocol.

Then I looked into my WIP testsuite for this protocol from 2 years ago, and guess what I found?

Show threadWolf480plDec 20, 2024

def assertNoMoreMessages(self):
[...]
self.send(b"ping %s" % nonce) #FIXME: this is non-standard
self.assertRecv(b"pong %s" % nonce)

yup turns out back then I also figured out some things can't be tested without a ping

Show threadWolf480plDec 20, 2024

Of course the problem with pings with nonces in TLA+ is that the set of possible nonces must be larger than the worst-case-scenario number of in-flight pings.

So if you simulate a TCP connection with 2 queues, one in each direction, up to 5 messages in each

then you need 11 different nonces (ok maybe 10 would suffice), which means you get extra 11!-ish states from all the ways your queues can be stuffed with various pings and pongs...

Show threadIgnas KielaDec 20, 2024
@wolf480pl why though? wouldn't TCP guarantees of in-order delivery essentially drop all of the states?
Show threadWolf480plDec 20, 2024
@ignaloidas because I was letting the client send the pings in an arbitrary order 😅
Show threadIgnas KielaDec 20, 2024
@wolf480pl right, but what I'm saying is that noonce isn't really something that you even need at all in TLA+, the model would be equisatisfiable if you just sent pings without a noonce and sent pongs to a specific ping message (by say, numbering messages in general). It's state that you don't generally need.

I've been doing a bunch of stuff with SAT and SMT solvers on the side and eliminating unnecessary state has provided me with way faster solutions most of the time (there's a balance to be had between size of state and complexity of the problem, but most problems aren't that hard).
Show threadWolf480pl
@ignaloidas if I drop the nonce, then how can I verify that the server does indeed respond to every ping, as opposed to ignoring them sometimes?
Dec 20, 2024 at 10:05pmWeb
Show threadIgnas KielaDec 20, 2024
@wolf480pl hmm, that is indeed harder without noonces

Though, I will note that with sequential ones, store a state with latest recieved pong, and if new pong comes larger than one over the last one, that's invalid. Comparing all-to-all is way much more complex than one extra state variable
Show threadWolf480plDec 20, 2024

@ignaloidas oh, this isn't state in the process.

I'm not storing a list of all oustanding pings in the process.

It exists in the messages sitting in the queues.

Show threadWolf480plDec 20, 2024
@ignaloidas (the queues are my model of a TCP connection)
Show threadIgnas KielaDec 20, 2024
@wolf480pl I mean it's still state space that TLA steps through.

Though also, checking if some pings are ignored in the queue seems a tad weird.
Show threadWolf480plDec 20, 2024

@ignaloidas yeah but like

if the pings in the queue don't have numbers in them

then the client cannot check if the received pong is more than last+1

Show threadIgnas KielaDec 20, 2024
@wolf480pl with the standard TCP assumptions this seems correct:

One side counts how many pings it has recieved, sends pongs with noonce of that+1
Other side stores the last pong it recived, if new one is that+1 then accept and store, else invalid
Show threadWolf480plDec 20, 2024

@ignaloidas so you have nonces in pongs, but not in pings, and relying on part of the specification of the server process to verify that the server process is correct... meh...

I could have the client count how many pings are outstanding, but the problem with that is I'd have to then say "eventually, the number of oustanding pings equals zero" which won't be true because the client can always fill the queue with pings and keep adding more as soon as it receives a pong

Show threadIgnas KielaDec 20, 2024
@wolf480pl FWIW the "eventually, the number of oustanding pings equals zero" also wouldn't work if/when you start treating TCP as an unreliable channel (can cut off at any arbitrary point)

Also, wouldn't the server want to know in some way which messages have been definitely received anyways, for which you'd want to know what pongs have been returned?