From 86991daa56e83c4d69ad977639644a94c44ddec3 Mon Sep 17 00:00:00 2001 From: Ben Manes Date: Sun, 12 Sep 2021 20:46:23 -0700 Subject: [PATCH] Add linearizability tests --- .github/workflows/analysis.yml | 2 - .github/workflows/lincheck.yml | 31 ++++ caffeine/build.gradle | 1 + .../caffeine/cache/BoundedLincheckTest.java | 42 +++++ .../MpscGrowableArrayQueueLincheckTest.java | 96 +++++++++++ .../caffeine/cache/UnboundedLincheckTest.java | 39 +++++ .../testing/AbstractLincheckMapTest.java | 158 ++++++++++++++++++ caffeine/testing.gradle | 17 +- checksum.xml | 1 + gradle/dependencies.gradle | 2 + 10 files changed, 386 insertions(+), 3 deletions(-) create mode 100644 .github/workflows/lincheck.yml create mode 100644 caffeine/src/test/java/com/github/benmanes/caffeine/cache/BoundedLincheckTest.java create mode 100644 caffeine/src/test/java/com/github/benmanes/caffeine/cache/MpscGrowableArrayQueueLincheckTest.java create mode 100644 caffeine/src/test/java/com/github/benmanes/caffeine/cache/UnboundedLincheckTest.java create mode 100644 caffeine/src/test/java/com/github/benmanes/caffeine/cache/testing/AbstractLincheckMapTest.java diff --git a/.github/workflows/analysis.yml b/.github/workflows/analysis.yml index 4675be16a8..2b2f81a75f 100644 --- a/.github/workflows/analysis.yml +++ b/.github/workflows/analysis.yml @@ -27,8 +27,6 @@ jobs: path: | ~/.gradle/wrapper ~/.gradle/caches - ~/.sonar/cache - ~/.m2 key: ${{ runner.os }}-${{ github.job }}-${{ matrix.java }}-${{ hashFiles('**/*.gradle') }} restore-keys: ${{ runner.os }}-gradle - name: Run analyzers diff --git a/.github/workflows/lincheck.yml b/.github/workflows/lincheck.yml new file mode 100644 index 0000000000..f6dbc8fb7a --- /dev/null +++ b/.github/workflows/lincheck.yml @@ -0,0 +1,31 @@ +name: lincheck +on: [ push, pull_request ] + +env: + ORG_GRADLE_PROJECT_checksumFailOn: build_finish + ORG_GRADLE_PROJECT_checksumIgnore: false + ORG_GRADLE_PROJECT_checksumPrint: true + JAVA_VERSION: 16 + +jobs: + lincheck: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v2.3.4 + - name: Set up JDK ${{ env.JAVA_VERSION }} + uses: actions/setup-java@v2 + with: + distribution: 'zulu' + java-version: ${{ env.JAVA_VERSION }} + - name: Cache Gradle packages + uses: actions/cache@v2.1.6 + with: + path: | + ~/.gradle/wrapper + ~/.gradle/caches + key: ${{ runner.os }}-${{ github.job }}-${{ matrix.java }}-${{ hashFiles('**/*.gradle') }} + restore-keys: ${{ runner.os }}-gradle + - name: Run lincheck + run: | + set -eux + ./gradlew lincheckTests diff --git a/caffeine/build.gradle b/caffeine/build.gradle index 231a444fd2..0b2103c86b 100644 --- a/caffeine/build.gradle +++ b/caffeine/build.gradle @@ -42,6 +42,7 @@ dependencies { testImplementation testLibraries.junit testImplementation testLibraries.testng testImplementation testLibraries.jctools + testImplementation testLibraries.lincheck testImplementation libraries.commonsLang3 testImplementation testLibraries.guavaTestLib diff --git a/caffeine/src/test/java/com/github/benmanes/caffeine/cache/BoundedLincheckTest.java b/caffeine/src/test/java/com/github/benmanes/caffeine/cache/BoundedLincheckTest.java new file mode 100644 index 0000000000..358e64123e --- /dev/null +++ b/caffeine/src/test/java/com/github/benmanes/caffeine/cache/BoundedLincheckTest.java @@ -0,0 +1,42 @@ +/* + * Copyright 2021 Ben Manes. All Rights Reserved. + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package com.github.benmanes.caffeine.cache; + +import java.time.Duration; +import java.util.concurrent.ConcurrentMap; + +import org.testng.annotations.Test; + +import com.github.benmanes.caffeine.cache.testing.AbstractLincheckMapTest; + +/** + * Linearization test cases for {@link BoundedLocalCache}. + * + * @author ben.manes@gmail.com (Ben Manes) + */ +@Test(groups = "lincheck") +public final class BoundedLincheckTest extends AbstractLincheckMapTest { + + @Override + protected ConcurrentMap create() { + Cache cache = Caffeine.newBuilder() + .expireAfterWrite(Duration.ofDays(1)) + .maximumSize(Long.MAX_VALUE) + .executor(Runnable::run) + .build(); + return cache.asMap(); + } +} diff --git a/caffeine/src/test/java/com/github/benmanes/caffeine/cache/MpscGrowableArrayQueueLincheckTest.java b/caffeine/src/test/java/com/github/benmanes/caffeine/cache/MpscGrowableArrayQueueLincheckTest.java new file mode 100644 index 0000000000..f153be8a42 --- /dev/null +++ b/caffeine/src/test/java/com/github/benmanes/caffeine/cache/MpscGrowableArrayQueueLincheckTest.java @@ -0,0 +1,96 @@ +/* + * Copyright 2021 Ben Manes. All Rights Reserved. + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package com.github.benmanes.caffeine.cache; + +import java.util.ArrayList; +import java.util.Map; +import java.util.Queue; + +import org.jetbrains.kotlinx.lincheck.LinChecker; +import org.jetbrains.kotlinx.lincheck.annotations.Operation; +import org.jetbrains.kotlinx.lincheck.annotations.Param; +import org.jetbrains.kotlinx.lincheck.paramgen.IntGen; +import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.ModelCheckingOptions; +import org.jetbrains.kotlinx.lincheck.strategy.stress.StressOptions; +import org.jetbrains.kotlinx.lincheck.verifier.VerifierState; +import org.testng.annotations.Test; + +/** + * Linearizability checks for {@link MpscGrowableArrayQueue}. This tests the JCTools' version until + * our copy is resync'd due to requiring an iterator for reporting the state. + * + * @author ben.manes@gmail.com (Ben Manes) + */ +@Param(name = "element", gen = IntGen.class, conf = "1:5") +public final class MpscGrowableArrayQueueLincheckTest extends VerifierState { + private final Queue queue; + + public MpscGrowableArrayQueueLincheckTest() { + queue = new org.jctools.queues.MpscGrowableArrayQueue<>(4, 65_536); + } + + @Operation + public boolean offer(@Param(name = "element") int e) { + return queue.offer(e); + } + + @Operation + public synchronized Integer poll() { + return queue.poll(); + } + + /** + * This test checks that the concurrent map is linearizable with bounded model checking. Unlike + * stress testing, this approach can also provide a trace of an incorrect execution. However, it + * uses sequential consistency model, so it can not find any low-level bugs (e.g., missing + * 'volatile'), and thus, it it recommended to have both test modes. + *

+ * This test requires the following JVM arguments, + *

    + *
  • --add-opens java.base/jdk.internal.misc=ALL-UNNAMED + *
  • --add-exports java.base/jdk.internal.util=ALL-UNNAMED + *
+ */ + @Test(groups = "lincheck") + public void modelCheckingTest() { + var options = new ModelCheckingOptions() + .iterations(100) // the number of different scenarios + .invocationsPerIteration(10_000); // how deeply each scenario is tested + new LinChecker(getClass(), options).check(); + } + + /** This test checks that the concurrent map is linearizable with stress testing. */ + @Test(groups = "lincheck") + public void stressTest() { + var options = new StressOptions() + .iterations(100) // the number of different scenarios + .invocationsPerIteration(10_000); // how deeply each scenario is tested + new LinChecker(getClass(), options).check(); + } + + /** + * Provides something with correct equals and hashCode methods that can be + * interpreted as an internal data structure state for faster verification. The only limitation is + * that it should be different for different data structure states. For {@link Map} it itself is + * used. + * + * @return object representing internal state + */ + @Override + protected Object extractState() { + return new ArrayList(queue); + } +} diff --git a/caffeine/src/test/java/com/github/benmanes/caffeine/cache/UnboundedLincheckTest.java b/caffeine/src/test/java/com/github/benmanes/caffeine/cache/UnboundedLincheckTest.java new file mode 100644 index 0000000000..24e74e4ed5 --- /dev/null +++ b/caffeine/src/test/java/com/github/benmanes/caffeine/cache/UnboundedLincheckTest.java @@ -0,0 +1,39 @@ +/* + * Copyright 2021 Ben Manes. All Rights Reserved. + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package com.github.benmanes.caffeine.cache; + +import java.util.concurrent.ConcurrentMap; + +import org.testng.annotations.Test; + +import com.github.benmanes.caffeine.cache.testing.AbstractLincheckMapTest; + +/** + * Linearization test cases for {@link UnboundedLocalCache}. + * + * @author ben.manes@gmail.com (Ben Manes) + */ +@Test(groups = "lincheck") +public final class UnboundedLincheckTest extends AbstractLincheckMapTest { + + @Override + protected ConcurrentMap create() { + Cache cache = Caffeine.newBuilder() + .executor(Runnable::run) + .build(); + return cache.asMap(); + } +} diff --git a/caffeine/src/test/java/com/github/benmanes/caffeine/cache/testing/AbstractLincheckMapTest.java b/caffeine/src/test/java/com/github/benmanes/caffeine/cache/testing/AbstractLincheckMapTest.java new file mode 100644 index 0000000000..d9b344e0f2 --- /dev/null +++ b/caffeine/src/test/java/com/github/benmanes/caffeine/cache/testing/AbstractLincheckMapTest.java @@ -0,0 +1,158 @@ +/* + * Copyright 2021 Ben Manes. All Rights Reserved. + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package com.github.benmanes.caffeine.cache.testing; + +import java.util.Map; +import java.util.concurrent.ConcurrentMap; + +import org.jetbrains.kotlinx.lincheck.LinChecker; +import org.jetbrains.kotlinx.lincheck.annotations.Operation; +import org.jetbrains.kotlinx.lincheck.annotations.Param; +import org.jetbrains.kotlinx.lincheck.paramgen.IntGen; +import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.ModelCheckingOptions; +import org.jetbrains.kotlinx.lincheck.strategy.stress.StressOptions; +import org.jetbrains.kotlinx.lincheck.verifier.VerifierState; +import org.testng.annotations.Test; + +/** + * Linearizability checks for a concurrent map. + * + * @author afedorov2602@gmail.com (Alexander Fedorov) + * @author ben.manes@gmail.com (Ben Manes) + */ +@Param(name = "key", gen = IntGen.class, conf = "1:5") +@Param(name = "value", gen = IntGen.class, conf = "1:10") +public abstract class AbstractLincheckMapTest extends VerifierState { + private final ConcurrentMap map; + + public AbstractLincheckMapTest() { + map = create(); + } + + /** Returns the map instance to test against. */ + protected abstract ConcurrentMap create(); + + @Operation + public boolean containsKey(@Param(name = "key") int key) { + return map.containsKey(key); + } + + @Operation + public boolean containsValue(@Param(name = "value") int value) { + return map.containsValue(value); + } + + @Operation + public Integer get(@Param(name = "key") int key) { + return map.get(key); + } + + @Operation + public Integer put(@Param(name = "key") int key, @Param(name = "value") int value) { + return map.put(key, value); + } + + @Operation + public Integer putIfAbsent(@Param(name = "key") int key, @Param(name = "value") int value) { + return map.putIfAbsent(key, value); + } + + @Operation + public Integer replace(@Param(name = "key") int key, @Param(name = "value") int nextValue) { + return map.replace(key, nextValue); + } + + @Operation + public boolean replaceConditionally(@Param(name = "key") int key, + @Param(name = "value") int previousValue, @Param(name = "value") int nextValue) { + return map.replace(key, previousValue, nextValue); + } + + @Operation + public Integer remove(@Param(name = "key") int key) { + return map.remove(key); + } + + @Operation + public boolean removeConditionally(@Param(name = "key") int key, + @Param(name = "value") int previousValue) { + return map.remove(key, previousValue); + } + + @Operation + public Integer computeIfAbsent(@Param(name = "key") int key, + @Param(name = "value") int nextValue) { + return map.computeIfAbsent(key, k -> nextValue); + } + + @Operation + public Integer computeIfPresent(@Param(name = "key") int key, + @Param(name = "value") int nextValue) { + return map.computeIfPresent(key, (k, v) -> nextValue); + } + + @Operation + public Integer compute(@Param(name = "key") int key, @Param(name = "value") int nextValue) { + return map.compute(key, (k, v) -> nextValue); + } + + @Operation + public Integer merge(@Param(name = "key") int key, @Param(name = "value") int nextValue) { + return map.merge(key, nextValue, (k, v) -> v + nextValue); + } + + /** + * This test checks that the concurrent map is linearizable with bounded model checking. Unlike + * stress testing, this approach can also provide a trace of an incorrect execution. However, it + * uses sequential consistency model, so it can not find any low-level bugs (e.g., missing + * 'volatile'), and thus, it it recommended to have both test modes. + *

+ * This test requires the following JVM arguments, + *

    + *
  • --add-opens java.base/jdk.internal.misc=ALL-UNNAMED + *
  • --add-exports java.base/jdk.internal.util=ALL-UNNAMED + *
+ */ + @Test(groups = "lincheck") + public void modelCheckingTest() { + var options = new ModelCheckingOptions() + .iterations(100) // the number of different scenarios + .invocationsPerIteration(1_000); // how deeply each scenario is tested + new LinChecker(getClass(), options).check(); + } + + /** This test checks that the concurrent map is linearizable with stress testing. */ + @Test(groups = "lincheck") + public void stressTest() { + var options = new StressOptions() + .iterations(100) // the number of different scenarios + .invocationsPerIteration(10_000); // how deeply each scenario is tested + new LinChecker(getClass(), options).check(); + } + + /** + * Provides something with correct equals and hashCode methods that can be + * interpreted as an internal data structure state for faster verification. The only limitation is + * that it should be different for different data structure states. For {@link Map} it itself is + * used. + * + * @return object representing internal state + */ + @Override + protected Object extractState() { + return map; + } +} diff --git a/caffeine/testing.gradle b/caffeine/testing.gradle index 7e5169ffc9..3741c0428f 100644 --- a/caffeine/testing.gradle +++ b/caffeine/testing.gradle @@ -57,6 +57,11 @@ task isolatedTests(type: Test, group: 'Cache tests') { useTestNG() } +task lincheckTests(type: Test, group: 'Cache tests') { + description = 'Tests that assert linearizability' + useTestNG() +} + task junitTests(type: Test, group: 'Cache tests', description: 'JUnit tests', dependsOn: jar) { useJUnit() tasks.test.dependsOn(it) @@ -71,10 +76,20 @@ tasks.withType(Test) { options.includeGroups = ['slow'] } else if (name.startsWith('isolated')) { options.includeGroups = ['isolated'] + testLogging.events 'started' + } else if (name.startsWith('lincheck')) { + options.includeGroups = ['lincheck'] + jvmArgs += [ + '--add-opens', 'java.base/jdk.internal.misc=ALL-UNNAMED', + '--add-exports', 'java.base/jdk.internal.util=ALL-UNNAMED', + ] + testLogging.events 'started' + maxHeapSize = '2g' + failFast = true } else { options { threadCount = Math.max(6, Runtime.getRuntime().availableProcessors() - 1) - excludeGroups = ['slow', 'isolated'] + excludeGroups = ['slow', 'isolated', 'lincheck'] jvmArgs '-XX:+UseG1GC', '-XX:+ParallelRefProcEnabled' parallel = 'methods' } diff --git a/checksum.xml b/checksum.xml index 5492c95835..3b0c6d5c5b 100644 --- a/checksum.xml +++ b/checksum.xml @@ -202,6 +202,7 @@ + diff --git a/gradle/dependencies.gradle b/gradle/dependencies.gradle index 31e7acaf04..21fd6396f4 100644 --- a/gradle/dependencies.gradle +++ b/gradle/dependencies.gradle @@ -72,6 +72,7 @@ ext { jcacheTck: '1.1.1', jctools: '3.3.0', junit: '4.13.2', + lincheck: '2.14.1', mockito: '3.12.4', paxExam: '4.13.4', testng: '7.4.0', @@ -162,6 +163,7 @@ ext { jcacheTckTests: "javax.cache:cache-tests:${testVersions.jcacheTck}:tests", jctools: "org.jctools:jctools-core:${testVersions.jctools}", junit: "junit:junit:${testVersions.junit}", + lincheck: "org.jetbrains.kotlinx:lincheck-jvm:${testVersions.lincheck}", mockito: "org.mockito:mockito-core:${testVersions.mockito}", osgiCompile: "org.ops4j.pax.exam:pax-exam-junit4:${testVersions.paxExam}", osgiRuntime: [