search

lemmy / BlockingQueue

Tutorial "Weeks of debugging can save you hours of TLA+". Each git commit introduces a new concept => check the git history!
https://youtu.be/wjsI0lTSjIo
MIT License
485 stars 21 forks source link

why bounded queues don't play well #13

Open stuarthalloway opened 6 months ago

stuarthalloway commented 6 months ago

https://github.com/lemmy/BlockingQueue/blob/a064863fd482e2cb15389db48d1a7297a6c30851/BlockingQueuePoisonApple.tla#L103

I think that this is because of an (unstated?) presumption that producers are unwilling to block forever, so with a bounded queue you would need a PutFail action that loses a poison pill.

Thanks for this tutorial, it has been great fun to work through!

lemmy commented 6 months ago

@stuarthalloway Thanks for the feedback.

Can you please explain your reasoning around a PutFail action? BQPA satisfies the stated liveness constraints. In other words, no producer has to block forever.