News for hackers. Stuff that matters.
Re:QWaitCondition: Solving the Unavoidable Race (2014) by Bjartr on Wednesday February 17, 2021 @06:45PM (#26173474)
It'd be cool to see this, and the fix, modeled in TLA+
Re:QWaitCondition: Solving the Unavoidable Race (2014) by hwayne on Wednesday February 17, 2021 @08:49PM (#26174477)
plz stop nerdsniping me

More seriously, I'd love to see this modeled in Promela/Spin. There was a go bug a while back where I reproduced it in TLA+ and someone else reproduced it in Spin, and I personally liked the Spin solution a lot more. It seems well-suited for these kinds of problems!

Re:QWaitCondition: Solving the Unavoidable Race (2014) by nsm on Wednesday February 17, 2021 @09:54PM (#26174916)
Haha! My very first thought on reading the parent comment was "Hillel Wayne would be all over this!"
Re:QWaitCondition: Solving the Unavoidable Race (2014) by Bjartr on Thursday February 18, 2021 @09:28AM (#26180123)
Haha, sorry. Although I will say your blog is precisely where my interest in TLA+ originated from.