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?
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
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...
So, last time I figured out I need pings in my protocol to check that a certain other message isn't still sitting in a queue / as a kind of synchronization fence.
So I added pings to the model, and now I'm making the client send a ping immediately after that other message, and...
ofc it doesn't compile because sending 2 messages means modifying the queue twice, which, in Pluscal, can't be done in a single label.
Well ok, let's add a label inbetween the messages then.
But a label is a place where the process is allowed to get preempted.
And yeah sending 2 messages isn't atomic IRL so it makes sense to have a label between them.
So what's the first thing TLC does when I do that?
It fills up the recv queue so that the server is blocked
then it fills up the send queue except for one free spot
then it sends the message that requires a ping after it
then the client is stuck at the new label, unable to send bc sendq is full, unable to recv because wrong label
And like, yes I can make only allow it to send that first message if there are 2 free slots in the send queue.
But how does that generalize to multiple clients?
IRL each would have a separate TCP connection to the server, but currently I model them all as a single pair of queues, one from clients to server, one from server to clients.
So if one client checks that there are 2 slots in a queue, sends first msg, then another client sends a different one, I'm still stuck.
I guess I'll have to have a separate pair of queues for each client, and have the server non-deterministically choose which one it receives from. That's closer to reality, too.
The nice thing about that is that each queue has its own bound, so checking for 2 empty slots makes sense.
The problem with that is that each queue has its own bound, so state space goes to the mooooon!
Alternatively, I could allow atomically sending 2 messages together.
That's not something I can/want to do in reality, so doing that in the model could potentially hide some bugs.
Oh, also, I tried just disabling deadlock checking, but I have my own liveness properties which also fail when the client gets stuck :/
I guess per-client queues it is... I haven't started testing with multiple clients anyway, so the state space is a Future Wolf problem.
Or... I could allow the model to temporarily exceed the queue bound when sending the follow-up ping...
That'd be smart, it'd be max 1 over queue bound per process, and like
2 * MaxQueue + nClients
is less than
2 * MaxQueue * nClients
when nClients >= 2.
I might do that later when I start running the model with multiple clients, if it turns out that the state space grows too big...
okay, this works
27 412 states, 12 257 unique
just to model a single client subscribing and unsubscribing to a single channel, to which it's always allowed to subscribe, and assuming the server knows that on its own without asking any upstream
well ok I could go down to
686 states, 372 unique
by limiting message queues to 2 instead of 5
but where is the fun in that?
Ok, so you know what's the drawback of having a separate queue from each client, and the server non-deterministically choosing which to receive from?
There's nothing forcing the server to be fair.
It could just always receive from the first client and ignore the second.
Fortunately in TLA+ you can specify custom fairness properties as part of the spec. And I already had to specify one when I let the server do things other than receiving.
I had sth like (with pseudocode for actual queue states):
[]<>(\E c \in Clients : queue[c] is nonempty} => []<>(\E c \in Clients : queue[c] is nonempty and queue[c]' = tail(queue[c])
looks like to make this fair between clients, it should be:
\A c \in Clients : []<>(queue[c] is nonempty) => []<>(queue[c] is nonempty and queue[c]' = tail(queue[c]))
@ignaloidas although now that I read your post again, I'm not sure that's what you meant...
Are you saying there shouldn't be separate states for "1 ping in queue", "2 pings in queue", "3 pings in queue", "2 pings in outboind queue and 1 pong in inbound queue", etc?
@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.
@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
@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
Wolf480pl
Ignas Kiela