Notices by Wolf480pl (wolf480pl@mstdn.io), page 7

@ayo (inb4 it's toast)

@mwk I imagine it as a combine harvester chasing bitstream formats.

(I'd add some captions on the picture below but it's kinda late)

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.

meetup idea:

setting up distcc on everyone's computer to see how fast we can compile LLVM together

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.

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

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

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?

well ok it helps if you make it use the nonces in order (with wraparound) instead of picking any unused nonce every time it sends 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.

If I post a tech rant / a description of a problem I have, and you don't understand it, feel free to ask questions.

Like, I'd prefer if people were like "you used the word $W which i don't know, what does that even mean" instead of being like "I don't know what he's talking about so I'll stay silent"

@mikoto does Pokemon count?

@lcamtuf you sure you're into soldering and not into blacksmithing?

I just read through https://learntla.com (all of Core and some of the Topics) in two days and...

It was quite enjoyable.

It's been a long time since I've read a tutorial or a manual start-to-finish and I forgot how much nicer it is, compared to learning only the pieces you immediately need, and never knowing what else is possible.

You should try that too.

I think the desire to get immediate answers to your current problem, as opposed to developing a broader understanding of the tools you're working with, is part of what led to the LLM chatbot brainrot we're seeing these days.

And I think practicing the skill of actually reading the manual start-to-finish removes some of that temptation, makes you less prone to being misled by some LLM, and is a tiny step towards making those AI companies have less power over people.

@cnlohr stop evolving Wi-Fi

wireless networks were never supposed to be that fast

wanted to send files with speeds over 1Gbit/s? We had a tool for that, it's called SFP+

@foone

@kspalaiologos and so far I encountered three cathegories of code that turned out completely inscrutable to me:

Scala, React, and whatever Pipewire is written in (not sure if it's just GObject, or a special evolution of GObject found in gstreamer, or some different beast).