Polish and extend tutorial

[lemmy]

Polish

• Starvation -> NoStarvation, StarvationFree, or StarvationFreedom
• 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
• https://stackoverflow.com/questions/17063426/how-to-solve-starvation-with-notify-and-notifyall

[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]

This has been integrated into the tutorial with f3075bf and b0bbddc.

Fairness constraint with which NoStarvation holds for FairSpec of (deadlock-free) BlockingQueue, i.e. THEOREM FairSpec => Starvation.

diff --git a/BlockingQueue.tla b/BlockingQueue.tla
index 619f88e..e80ce57 100644
--- a/BlockingQueue.tla
+++ b/BlockingQueue.tla
@@ -116,12 +116,20 @@ MCIInv == TypeInv!1 /\ IInv
 
 PutEnabled == \A p \in Producers : ENABLED Put(p, p)
 
-FairSpec == Spec /\ WF_vars(Next) 
-                 /\ \A p \in Producers : WF_vars(Put(p, p)) 
+FairSpec == 
+    /\ Spec 
+    /\ \A t \in Producers: WF_vars(Put(t,t)) 
+    /\ \A t \in Consumers: WF_vars(Get(t)) 
+    /\ \A t \in Producers:
+        SF_vars(\E self \in Consumers: Get(self) /\ t \notin waitSet')
+    /\ \A t \in Consumers:
+        SF_vars(\E self \in Producers: Put(self, self) /\ t \notin waitSet')
 
 (* All producers will continuously be serviced. For this to be violated,    *)
 (* ASSUME Cardinality(Producers) > 1 has to hold (a single producer cannot  *)
 (* starve itself).                                                          *)
-Starvation == \A p \in Producers: []<>(<<Put(p, p)>>_vars)
+Starvation == 
+    /\ \A p \in Producers: []<>(<<Put(p, p)>>_vars)
+    /\ \A c \in Consumers: []<>(<<Get(c)>>_vars)
 
 =============================================================================

FairSpec == 
    /\ Spec 
    /\ \A t \in Producers: WF_vars(Put(t,t)) 
    /\ \A t \in Consumers: WF_vars(Get(t)) 
    /\ \A t \in Producers:
        SF_vars(\E self \in Consumers: Get(self) /\ t \notin waitSet')
    /\ \A t \in Consumers:
        SF_vars(\E self \in Producers: Put(self, self) /\ t \notin waitSet')

(* All producers will continuously be serviced. For this to be violated,    *)
(* ASSUME Cardinality(Producers) > 1 has to hold (a single producer cannot  *)
(* starve itself).                                                          *)
Starvation == 
    /\ \A p \in Producers: []<>(<<Put(p, p)>>_vars)
    /\ \A c \in Consumers: []<>(<<Get(c)>>_vars)

To check multiple configurations while verifying liveness properties:

1. Create a template/prototype config:

SPECIFICATION FairSpec
PROPERTY NoStarvation

CONSTANTS
  p1 = p1
  p2 = p2
  p3 = p3
  p4 = p4
  c1 = c1
  c2 = c2
  c3 = c3
  c4 = c4
CONSTANTS
  BufCapacity = BUF_
  Producers = PROD_
  Consumers = CONS_

2. Generate configs from template:

...
for i in 1 2 3; do sed -e "s/BUF_/$i/g" -e 's/PROD_/{p1,p2}/g' -e 's/CONS_/{c1,c2}/g' template.cfg > config$(date +%s).cfg && sleep 1; done
for i in 1 2 3; do sed -e "s/BUF_/$i/g" -e 's/PROD_/{p1,p2,p3}/g' -e 's/CONS_/{c1,c2}/g' template.cfg > config$(date +%s).cfg && sleep 1; done

3. Have TLC check each config:

for f in config*.cfg; do tlc -config $f ../BlockingQueue.tla ; done

Especially step 2. turned out to be error-prone. In comparison, Apalache's ConstInit feature is dead simple, foolproof, and takes a fraction of the time to set up.

---

Note that with the following variant of a fairness constraint (\in instead of \notin), the property NoStarvation no longer holds iff Cardinality(Producer \cup Consumers) >= bufCapacity /\ Cardinality(Producer) >= Cardinality(Consumer):

FairSpec2 == /\ Spec 
            /\ \A t \in Producers: 
                  SF_vars((\E self \in Consumers : c(self)) /\ t \in waitSet')

TLC2 Version 2.16 of Day Month 20?? (rev: 6932e19)
Running breadth-first search Model-Checking with fp 89 and seed 1334139005151507061 with 1 worker on 4 cores with 5952MB heap and 64MB offheap memory [pid: 179850] (Linux 5.4.0-72-generic amd64, Ubuntu 11.0.11 x86_64, MSBDiskFPSet, DiskStateQueue).
Parsing file /home/markus/src/TLA/_specs/models/tutorials/BlockingQueueTLA/Lamport/NonBlockingQueue.tla (file:/home/markus/src/TLA/_specs/models/tutorials/BlockingQueueTLA/Lamport/configs/../NonBlockingQueue.tla)
Parsing file /tmp/Naturals.tla (jar:file:/opt/toolbox/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /tmp/Sequences.tla (jar:file:/opt/toolbox/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Parsing file /tmp/FiniteSets.tla (jar:file:/opt/toolbox/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Semantic processing of module Naturals
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module NonBlockingQueue
Starting... (2021-05-04 14:24:43)
Implied-temporal checking--satisfiability problem has 1 branches.
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2021-05-04 14:24:43.
Progress(8) at 2021-05-04 14:24:43: 353 states generated, 100 distinct states found, 0 states left on queue.
Checking temporal properties for the complete state space with 100 total distinct states at (2021-05-04 14:24:43)
Error: Temporal properties were violated.

Error: The following behavior constitutes a counter-example:

State 1: <Initial predicate>
/\ buffer = <<>>
/\ waitSet = {}

State 2: <p line 66, col 12 to line 76, col 41 of module NonBlockingQueue>
/\ buffer = <<p3>>
/\ waitSet = {}

State 3: <p line 66, col 12 to line 76, col 41 of module NonBlockingQueue>
/\ buffer = <<p3>>
/\ waitSet = {p1}

State 4: <p line 66, col 12 to line 76, col 41 of module NonBlockingQueue>
/\ buffer = <<p3>>
/\ waitSet = {p1, p2}

State 5: <p line 66, col 12 to line 76, col 41 of module NonBlockingQueue>
/\ buffer = <<p3>>
/\ waitSet = {p1, p2, p3}

State 6: <c line 78, col 12 to line 88, col 41 of module NonBlockingQueue>
/\ buffer = <<>>
/\ waitSet = {p1, p3}

State 7: <p line 66, col 12 to line 76, col 41 of module NonBlockingQueue>
/\ buffer = <<p2>>
/\ waitSet = {p1, p3}

State 8: <p line 66, col 12 to line 76, col 41 of module NonBlockingQueue>
/\ buffer = <<p2>>
/\ waitSet = {p1, p2, p3}

State 9: <c line 78, col 12 to line 88, col 41 of module NonBlockingQueue>
/\ buffer = <<>>
/\ waitSet = {p1, p2}

State 10: <p line 66, col 12 to line 76, col 41 of module NonBlockingQueue>
/\ buffer = <<p3>>
/\ waitSet = {p1, p2}

State 11: <c line 78, col 12 to line 88, col 41 of module NonBlockingQueue>
/\ buffer = <<>>
/\ waitSet = {p1}

Back to state 3: <p line 66, col 12 to line 76, col 41 of module NonBlockingQueue>

Finished checking temporal properties in 00s at 2021-05-04 14:24:44
353 states generated, 100 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 8.
Finished in 01s at (2021-05-04 14:24:44)

[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

[lemmy]

Theorems have been moved and renamed, breaking BQF proof.

diff --git a/BlockingQueueFair.tla b/BlockingQueueFair.tla
index 4c6fc6e..c6a088b 100644
--- a/BlockingQueueFair.tla
+++ b/BlockingQueueFair.tla
@@ -1,5 +1,5 @@
 ------------------------- MODULE BlockingQueueFair -------------------------
-EXTENDS Naturals, Sequences, FiniteSets, Functions, SequencesExt, SequencesExtTheorems
+EXTENDS Naturals, Sequences, FiniteSets, Functions, SequencesExt, SequenceTheorems
 
 CONSTANTS Producers,   (* the (nonempty) set of producers                       *)
           Consumers,   (* the (nonempty) set of consumers                       *)
@@ -112,13 +112,13 @@ THEOREM ITypeInv == Spec => []TypeInv
                /\ buffer' = Append(buffer, p)
                /\ NotifyOther(waitSeqC)
                /\ UNCHANGED waitSeqP
-      BY <3>1, <2>1, TailTransitivityIsInjective
+      BY <3>1, <2>1, TailInjectiveSeq
       DEF NotifyOther, IsInjective
     <3>2. CASE /\ Len(buffer) = BufCapacity
                /\ Wait(waitSeqP, p)
                /\ UNCHANGED waitSeqC
       \* Put below so TLAPS knows about t \notin Range(waitSeqP)
-      BY <3>2, <2>1, AppendTransitivityIsInjective
+      BY <3>2, <2>1, AppendInjectiveSeq
       DEF Wait, IsInjective, Put
     <3>3. QED
       BY <2>1, <3>1, <3>2 DEF Put
@@ -129,13 +129,13 @@ THEOREM ITypeInv == Spec => []TypeInv
                /\ buffer' = Tail(buffer)
                /\ NotifyOther(waitSeqP)
                /\ UNCHANGED waitSeqC
-      BY <3>1, <2>2, TailTransitivityIsInjective
+      BY <3>1, <2>2, TailInjectiveSeq
       DEF NotifyOther, IsInjective
     <3>2. CASE /\ buffer = <<>>
                /\ Wait(waitSeqC, c)
                /\ UNCHANGED waitSeqP
       \* Get below so TLAPS knows about t \notin Range(waitSeqC)
-      BY <3>2, <2>2, AppendTransitivityIsInjective
+      BY <3>2, <2>2, AppendInjectiveSeq
       DEF Wait, IsInjective, Get
     <3>3. QED
       BY <2>2, <3>1, <3>2 DEF Get