lemmy
commented
3 years ago 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>
Polish
Starvation->NoStarvationInvariant->NoDeadlockorDeadlockFree(proof has theoremDeadlockFreedom)takevs. TLAgetaction namesxin\E x \in waitSet...inNotifywithWaitandNext, i.e.tprocessesandthreadsExtend
BlockingQueue.tlaeven withoutwaitSeqC... starvation free. See @xxyzzn PlusCal variant below:~ https://github.com/lemmy/BlockingQueue/commit/b0bbddc1b28e9c8150fc2ccf7ce2f46da53d631d https://github.com/lemmy/BlockingQueue/issues/5#issuecomment-831626034buffera sequence, theView = <<Len(buffer), waitSet>>achieves a state-space reduction identical to modelingbufferas a counter.notifyOtherbut onlynotifyAll(PulseAll)wait/notify/notifyAllyet (https://twitter.com/nkoval_/status/1365050321077157892)Code pointers