Polish and extend tutorial

[lemmy]

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 Polish and extend tutorial #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 Polish and extend tutorial #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

[lemmy]

Failed attempt to use Linchecker:

package org.kuppe;

import org.jetbrains.kotlinx.lincheck.LinChecker;
import org.jetbrains.kotlinx.lincheck.annotations.Operation;
import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.ModelCheckingCTest;
import org.jetbrains.kotlinx.lincheck.verifier.VerifierState;
import org.jetbrains.kotlinx.lincheck.verifier.linearizability.LinearizabilityVerifier;
import org.junit.Test;

@ModelCheckingCTest(requireStateEquivalenceImplCheck = false, threads = 2, verifier = LinearizabilityVerifier.class)
public class DeadlockChecker extends VerifierState {

	// BQ with capacity 1 deadlocks for more than 2 running threads RT s.t. RT ==
	// Producers \cup Consumers
	private final BlockingQueue<Integer> bq = new BlockingQueue<>(1);

	@Operation(blocking = true, causesBlocking = true)
	public void put() throws InterruptedException {
		bq.put(42); // Value is known to be irrelevant.
	}

	@Operation(blocking = true, causesBlocking = true)
	public Integer take() throws InterruptedException {
		return bq.take();
	}

	@Test
	public void test() {
		LinChecker.check(DeadlockChecker.class);
	}

	@Override
	protected Object extractState() {
		return bq;
	}
}

<?xml version="1.0" encoding="UTF-8"?>

<project xmlns="http://maven.apache.org/POM/4.0.0"
	xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
	xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
	<modelVersion>4.0.0</modelVersion>

	<groupId>org.kuppe.app</groupId>
	<artifactId>blockingqueue</artifactId>
	<version>1.0-SNAPSHOT</version>

	<name>BlockingQueue</name>
	<url>http://github.com/lemmy/BlockingQueue</url>

	<properties>
		<project.build.sourceEncoding>UTF-8</project.build.sourceEncoding>
		<maven.compiler.source>1.8</maven.compiler.source>
		<maven.compiler.target>1.8</maven.compiler.target>
	</properties>

	<dependencies>
		<dependency>
			<groupId>junit</groupId>
			<artifactId>junit</artifactId>
			<version>4.13.2</version>
			<scope>test</scope>
		</dependency>
		<dependency>
			<groupId>org.jetbrains.kotlinx</groupId>
			<artifactId>lincheck-jvm</artifactId>
			<version>2.12</version>
			<type>jar</type>
		</dependency>
	</dependencies>
	<repositories>
		<repository>
			<id>kotlin-bintray</id>
			<name>Kotlin Bintray</name>
			<url>https://kotlin.bintray.com/kotlinx/</url>
			<releases>
				<enabled>true</enabled>
			</releases>
			<snapshots>
				<enabled>false</enabled>
			</snapshots>
		</repository>
	</repositories>
	<build>
		<sourceDirectory>src</sourceDirectory>
		<testSourceDirectory>test</testSourceDirectory>
		<plugins>
			<plugin>
				<groupId>org.apache.maven.plugins</groupId>
				<artifactId>maven-compiler-plugin</artifactId>
				<configuration>
					<compilerArgument>-parameters</compilerArgument>
				</configuration>
			</plugin>
		</plugins>
	</build>
</project>

[lemmy]

@johnyf Do you think that starvation freedom (Starvation) for FairSpec can be proved with the new tlapm?

[lemmy]

The refinement BlockingQueue <- BlockingQueuePoisonApple below fails to check because BQ allows only Producer elements to be in buffer. Thus, append the Poison element to buffer in BQPA!Terminate violates the the refinement. The BQ spec should be more liberal s.t it does not assert anything about the elements in buffer. Alternatively, we could show refinement of BQPA with ProducerConsumer.tla (if it ever gets added to the repo).

A == INSTANCE BlockingQueue
                \* Replace Poison with some Producer. The high-level
                \* BlockingQueue spec is a peculiar about the elements
                \* in its buffer.  If this wouldn't be a tutorial but
                \* a real-world spec, the high-level spec would be
                \* corrected to be oblivious to the elements in buffer.
                WITH buffer <-
                    [ i \in DOMAIN buffer |-> IF buffer[i] = Poison
                                              THEN CHOOSE p \in (Producers \ waitSet): TRUE
                                              ELSE buffer[i] ]

(* The bang in 'A!Spec' makes 'A!Spec' an invalid token in the config BlockingQueueSplit.cfg.   *)
ASpec == A!Spec