lemmy/blockingqueue

Tutorial "Weeks of debugging can save you hours of TLA+". Each git commit introduces a new concept => check the git history!

💻 Working as a Software Engineer at Microsoft on TLA+.

blockingqueue's Issues

Polish and extend tutorial

Polish

• Starvation -> NoStarvation
• Invariant -> NoDeadlock or DeadlockFree (proof has theorem DeadlockFreedom)
• Java take vs. TLA get action names
• Align bound variable x in \E x \in waitSet... in Notify with Wait and Next, i.e. t
• Inconsistent terminology around processes and threads
• Comment and spec contradictory (conjunct even seems superfluous):

  BlockingQueue/BlockingQueuePoisonPill.tla

  Lines 95 to 97 in a064863

  	\* ...there a fewer Poison messages in the buffer than (non-terminated)
  	\* Consumers.
  	\/ Cardinality(cons) < Cardinality({i \in DOMAIN buffer: buffer[i]=Poison})

Extend

• Mention spurious wakeups of POSIX and the Windows API that are modeled in v11
• Incorporate advanced liveness that makes BlockingQueue.tla even without waitSeqC ... starvation free. See @xxyzzn PlusCal variant below: b0bbddc #5 (comment)
• Prove liveness with TLAPS 1.5
• Integrate high-level ProducerConsumer spec into the tutorial
  • 977dc67
  • Highest level: counter, Higher level: set
  • Does this change anything WRT Apalache's bottleneck when it comes to longer traces?
  • For a ProducerConsumer.tla it should be straightforward to check refinement of BlockingQueuePoisonApple (see #5 (comment))
  • With buffer a sequence, the View = <<Len(buffer), waitSet>> achieves a state-space reduction identical to modeling buffer as a counter.
• Explore variants of spec where the number of producers and consumers changes dynamically (service scales up/down)
• Contrast with https://github.com/microsoft/coyote/tree/main/Samples/BoundedBuffer example (created after I asked a project member to contribute a solution to https://github.com/lemmy/lets-prove-blocking-queue)
  • https://cloudblogs.microsoft.com/opensource/2020/07/14/extreme-programming-meets-systematic-testing-using-coyote/
  • https://microsoft.github.io/coyote/#samples/tasks/bounded-buffer/
  • Does not do notifyOther but only notifyAll (PulseAll)
  • "The bug in the above implementation was not obvious. In fact, the authors had to spend some time poring over Coyote’s reproducible trace before finally grokking the bug. This speaks to the effectiveness of tools like Coyote and the inability of humans to always foresee subtle race conditions like the above. While the BoundedBuffer implementation may seem academic, it’s important to generalize the lessons from this exercise and see how they can apply to your production services." https://cloudblogs.microsoft.com/opensource/2020/07/14/extreme-programming-meets-systematic-testing-using-coyote/
• See if Kotlin's Linchecker finds the deadlock
  ** No support for wait/notify/notifyAll yet (https://twitter.com/nkoval_/status/1365050321077157892)

Code pointers

• https://opensource.apple.com/source/libpthread/libpthread-218.1.3/src/pthread_cond.c
• https://code.woboq.org/userspace/glibc/nptl/pthread_cond_wait.c.html
• https://probablydance.com/2020/10/31/using-tla-in-the-real-world-to-understand-a-glibc-bug/
• https://docs.microsoft.com/en-us/dotnet/api/system.threading.monitor.pulse?view=net-6.0

Activate "Automatic Module Parsing" for VSCode Codespace

https://github.com/alygin/vscode-tlaplus/wiki/Automatic-Module-Parsing

BlockingQueue/.devcontainer/devcontainer.json

Lines 10 to 13 in 0761ecf

	"settings": {
	"tlaplus.tlc.modelChecker.options": "-deadlock -dump dot BlockingQueue.dot",
	"tlaplus.java.options": "-XX:+UseParallelGC -cp CommunityModules.jar"
	},

https://github.com/tlaplus/Examples/blob/f49468c12a3236ff1b39447f531378b85889e38e/.devcontainer/devcontainer.json#L14-L16

TLAPS.tla outdated

tlaplus/tlapm#15 makes it necessary to update TLAPS.tla in this repository to the newest version in TLAPM.

No deadlock on macOS with POSIX threads

TLDR: On macOS, don't lock a mutex that has not been initialized, don't wait on a condition that has not been initialized.

Everything that is written below is super interesting and plausible. However, it is all wrong! Spurious wakeups are a red herring, and the real problem is the way more mundane/trivial coding bug below that only manifests on macOS.
The missing initialization would have been detectable on macOS with a test that asserts the consistency of the elements that are enqueued and dequeued. It is also obvious, that trace validation would have spotted the bug immediately.

diff --git a/impl/producer_consumer.c b/impl/producer_consumer.c
index bf7efda..46cfdfe 100644
--- a/impl/producer_consumer.c
+++ b/impl/producer_consumer.c
@@ -73,6 +73,9 @@ int main(int argc, char * argv[]) {
 
        printf("Buffer size = %d, # Producers = %d, # Consumers = %d\n", buff_size, numProducers, numConsumers);
 
+       pthread_mutex_init(&mutex, NULL);
+       pthread_cond_init(&modify, NULL);
+
        /* Allocate space for the buffer */
        buffer = malloc(sizeof(int) * buff_size);
        pthread_t prods[numProducers], cons[numConsumers];

Works with:

markus@avocado:~$ gcc --version
gcc (Ubuntu 9.3.0-17ubuntu1~20.04) 9.3.0

Fails with:

markus@armbook ~ % gcc --version
Configured with: --prefix=/Applications/Xcode.app/Contents/Developer/usr --with-gxx-include-dir=/Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX.sdk/usr/include/c++/4.2.1
Apple clang version 12.0.0 (clang-1200.0.32.27)
Target: arm64-apple-darwin20.1.0
Thread model: posix
InstalledDir: /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin

---

Red herring: spurious wake-ups

The C code (POSIX) deadlocks on Windows and Linux but doesn't deadlocked on Intel (MacBook Pro Retina Early 2015) or Apple Silicon M1 mac. However, the Cocoa variant below deadlocks as expected. This seemingly has to do with the likelihood of pthread_cond.c causing spurious wake-ups (signal is effectively broadcast?) on macOS, which POSIX generally allows for performance reasons. Also see a related SO discussion.

---

• 10.7.0 (Lion): http://www.opensource.apple.com/source/Libc/Libc-763.11/pthreads/pthread_cond.c
• 10.8.0 (Mountain Lion): http://www.opensource.apple.com/source/Libc/Libc-825.24/pthreads/pthread_cond.c
• 10.10.0 (Yosemite): http://www.opensource.apple.com/source/libpthread/libpthread-105.1.4/src/pthread_cond.c
• 10.11.0 (El Capitan): http://www.opensource.apple.com/source/libpthread/libpthread-137.1.1/src/pthread_cond.c
• 10.12.0 (Sierra): http://www.opensource.apple.com/source/libpthread/libpthread-218.1.3/src/pthread_cond.c
• 10.13.0 (High Sierra): http://www.opensource.apple.com/source/libpthread/libpthread-301.1.6/src/pthread_cond.c
• 10.14.0 (Mojave): http://www.opensource.apple.com/source/libpthread/libpthread-330.201.1/src/pthread_cond.c
• 10.14.1 (Mojave/latest): http://www.opensource.apple.com/source/libpthread/libpthread-330.220.2/src/pthread_cond.c

(list copied from a Rust issue at rust-lang/rust#62291)

why bounded queues don't play well

BlockingQueue/BlockingQueuePoisonApple.tla

Line 103 in a064863

\* on the same page that "Poison pills work reliably only with unbounded queues."

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!

Questions about "Weeks of Debugging Can Save You Hours of TLA+"

Hi, Kuppe:
I have read your great talk presentation from here：
https://bitbucket.org/lemmster/blockingqueue

But I have a little confused about the state graph in “BlockingQueue in PlusCal” section，as attached.

Highlighted in red box.
If the "p1" is already in the waitset, the 'put' action should not occur because we have only one producer and it is blocked now.
PS: the state graph in this git project has no such action.

I’m not sure if my understanding is correct or if that PDF is out of date.
Please help. Thanks