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+
[ Parent
| on HN ]
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!