diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/Lincheck.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/Lincheck.kt index 3200c0f23..108eb8d8b 100644 --- a/src/jvm/main/org/jetbrains/kotlinx/lincheck/Lincheck.kt +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/Lincheck.kt @@ -14,9 +14,11 @@ import org.jetbrains.kotlinx.lincheck.execution.ExecutionResult import org.jetbrains.kotlinx.lincheck.execution.ExecutionScenario import org.jetbrains.kotlinx.lincheck.execution.parallelResults import org.jetbrains.kotlinx.lincheck.strategy.LincheckFailure +import org.jetbrains.kotlinx.lincheck.strategy.managed.ManagedCTestConfiguration import org.jetbrains.kotlinx.lincheck.strategy.managed.forClasses import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.ModelCheckingOptions import org.jetbrains.kotlinx.lincheck.strategy.verify +import org.jetbrains.kotlinx.lincheck.transformation.LincheckJavaAgent.ensureObjectIsTransformed import org.jetbrains.kotlinx.lincheck.transformation.withLincheckJavaAgent import org.jetbrains.kotlinx.lincheck.verifier.Verifier import kotlin.reflect.jvm.javaMethod @@ -25,7 +27,7 @@ import kotlin.reflect.jvm.javaMethod object Lincheck { /** * This method will explore the interleavings of [block] body - * and track exceptions thrown from it. + * and track exceptions thrown from it (threads are created by the user in the [block]). * * @param invocations number of different interleavings of code in the [block] * that should be explored. @@ -33,7 +35,8 @@ object Lincheck { */ @JvmStatic fun verifyWithModelChecker( - invocations: Int = 1, + invocations: Int = ManagedCTestConfiguration.DEFAULT_INVOCATIONS, + verifierClass: Class? = null, block: () -> R ): LincheckFailure? { val scenario = scenario { @@ -48,11 +51,12 @@ object Lincheck { .addCustomScenario(scenario) .addGuarantee(forClasses(Lincheck::class).allMethods().ignore()) .addGuarantee(forClasses(Wrapper::class).allMethods().ignore()) - .verifier(ExecutionExceptionsVerifier::class.java) + .verifier(verifierClass ?: ExecutionExceptionsVerifier::class.java) val testCfg = options.createTestConfigurations(Wrapper::class.java) withLincheckJavaAgent(testCfg.instrumentationMode) { + ensureObjectIsTransformed(block) val strategy = testCfg.createStrategy(Wrapper::class.java, scenario, null, null) val verifier = testCfg.createVerifier() diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/ArrayReadWriteRunWithLambdaTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/ArrayReadWriteRunWithLambdaTest.kt new file mode 100644 index 000000000..a01010e4e --- /dev/null +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/ArrayReadWriteRunWithLambdaTest.kt @@ -0,0 +1,24 @@ +/* + * Lincheck + * + * Copyright (C) 2019 - 2024 JetBrains s.r.o. + * + * This Source Code Form is subject to the terms of the + * Mozilla Public License, v. 2.0. If a copy of the MPL was not distributed + * with this file, You can obtain one at http://mozilla.org/MPL/2.0/. + */ + +package org.jetbrains.kotlinx.lincheck_test.representation + +import kotlin.random.Random + +class ArrayReadWriteRunWithLambdaTest : BaseRunWithLambdaRepresentationTest("array_read_write_run_with_lambda.txt") { + private val array = IntArray(3) + + @Suppress("UNUSED_VARIABLE") + override fun operation() { + val index = Random.nextInt(array.size) + array[index]++ + val y = array[index] + } +} \ No newline at end of file diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/AtomicReferencesNamesRunWithLambdaTests.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/AtomicReferencesNamesRunWithLambdaTests.kt new file mode 100644 index 000000000..1ac4378b3 --- /dev/null +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/AtomicReferencesNamesRunWithLambdaTests.kt @@ -0,0 +1,104 @@ +/* + * Lincheck + * + * Copyright (C) 2019 - 2024 JetBrains s.r.o. + * + * This Source Code Form is subject to the terms of the + * Mozilla Public License, v. 2.0. If a copy of the MPL was not distributed + * with this file, You can obtain one at http://mozilla.org/MPL/2.0/. + */ + +package org.jetbrains.kotlinx.lincheck_test.representation + +import java.util.concurrent.atomic.* + +class AtomicReferencesNamesRunWithLambdaTests : BaseRunWithLambdaRepresentationTest("atomic_references_names_trace_run_with_lambda.txt") { + + private val atomicReference = AtomicReference(Node(1)) + private val atomicInteger = AtomicInteger(0) + private val atomicLong = AtomicLong(0L) + private val atomicBoolean = AtomicBoolean(true) + + private val atomicReferenceArray = AtomicReferenceArray(arrayOf(Node(1))) + private val atomicIntegerArray = AtomicIntegerArray(intArrayOf(0)) + private val atomicLongArray = AtomicLongArray(longArrayOf(0L)) + + private val wrapper = AtomicReferenceWrapper() + + override fun operation() { + atomicReference.compareAndSet(atomicReference.get(), Node(2)) + atomicReference.set(Node(3)) + + atomicInteger.compareAndSet(atomicInteger.get(), 2) + atomicInteger.set(3) + + atomicLong.compareAndSet(atomicLong.get(), 2) + atomicLong.set(3) + + atomicBoolean.compareAndSet(atomicBoolean.get(), true) + atomicBoolean.set(false) + + atomicReferenceArray.compareAndSet(0, atomicReferenceArray.get(0), Node(2)) + atomicReferenceArray.set(0, Node(3)) + + atomicIntegerArray.compareAndSet(0, atomicIntegerArray.get(0), 1) + atomicIntegerArray.set(0, 2) + + atomicLongArray.compareAndSet(0, atomicLongArray.get(0), 1) + atomicLongArray.set(0, 2) + + wrapper.reference.set(Node(5)) + wrapper.array.compareAndSet(0, 1 ,2) + + staticValue.compareAndSet(0, 2) + staticValue.set(0) + + AtomicReferenceWrapper.staticValue.compareAndSet(1, 2) + AtomicReferenceWrapper.staticValue.set(3) + + staticArray.compareAndSet(1, 0, 1) + AtomicReferenceWrapper.staticArray.compareAndSet(1, 0, 1) + } + + private data class Node(val name: Int) + + private class AtomicReferenceWrapper { + val reference = AtomicReference(Node(0)) + val array = AtomicIntegerArray(10) + + companion object { + @JvmStatic + val staticValue = AtomicInteger(1) + @JvmStatic + val staticArray = AtomicIntegerArray(3) + } + } + + companion object { + @JvmStatic + private val staticValue = AtomicInteger(0) + @JvmStatic + val staticArray = AtomicIntegerArray(3) + } +} + +class AtomicReferencesFromMultipleFieldsRunWithLambdaTest : BaseRunWithLambdaRepresentationTest("atomic_references_name_two_fields_trace_run_with_lambda.txt") { + + private var atomicReference1: AtomicReference + private var atomicReference2: AtomicReference + + init { + val ref = AtomicReference(Node(1)) + atomicReference1 = ref + atomicReference2 = ref + } + + override fun operation() { + atomicReference1.compareAndSet(atomicReference2.get(), Node(2)) + } + + private data class Node(val name: Int) + +} + + diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/BaseTraceRepresentationTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/BaseTraceRepresentationTest.kt index a54fbf9b3..0d7e6d1e2 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/BaseTraceRepresentationTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/BaseTraceRepresentationTest.kt @@ -10,6 +10,7 @@ package org.jetbrains.kotlinx.lincheck_test.representation +import org.jetbrains.kotlinx.lincheck.Lincheck import org.jetbrains.kotlinx.lincheck.annotations.Operation import org.jetbrains.kotlinx.lincheck.checkImpl import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.ModelCheckingOptions @@ -49,6 +50,24 @@ abstract class BaseTraceRepresentationTest(private val outputFileName: String) { } +abstract class BaseRunWithLambdaRepresentationTest(private val outputFileName: String) { + /** + * Implement me and place the logic to check its trace. + */ + @Operation + abstract fun operation() + + @Test + fun testRunWithModelChecker() { + val failure = Lincheck.verifyWithModelChecker( + verifierClass = FailingVerifier::class.java + ) { + operation() + } + failure.checkLincheckOutput(outputFileName) + } +} + class FailingVerifier(@Suppress("UNUSED_PARAMETER") sequentialSpecification: Class<*>) : Verifier { override fun verifyResults(scenario: ExecutionScenario?, results: ExecutionResult?) = false } diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/VariableReadWriteRunWithLambdaTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/VariableReadWriteRunWithLambdaTest.kt new file mode 100644 index 000000000..1887b973f --- /dev/null +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/VariableReadWriteRunWithLambdaTest.kt @@ -0,0 +1,21 @@ +/* + * Lincheck + * + * Copyright (C) 2019 - 2024 JetBrains s.r.o. + * + * This Source Code Form is subject to the terms of the + * Mozilla Public License, v. 2.0. If a copy of the MPL was not distributed + * with this file, You can obtain one at http://mozilla.org/MPL/2.0/. + */ + +package org.jetbrains.kotlinx.lincheck_test.representation + +class VariableReadWriteRunWithLambdaTest : BaseRunWithLambdaRepresentationTest("variable_read_write_run_with_lambda.txt") { + private var x = 0 + + @Suppress("UNUSED_VARIABLE") + override fun operation() { + x++ + val y = --x + } +} \ No newline at end of file diff --git a/src/jvm/test/resources/expected_logs/array_read_write_run_with_lambda.txt b/src/jvm/test/resources/expected_logs/array_read_write_run_with_lambda.txt new file mode 100644 index 000000000..460373c3f --- /dev/null +++ b/src/jvm/test/resources/expected_logs/array_read_write_run_with_lambda.txt @@ -0,0 +1,26 @@ += Invalid execution results = +| ----------------------------------- | +| Thread 1 | +| ----------------------------------- | +| run(() -> kotlin.Unit): kotlin.Unit | +| ----------------------------------- | + +The following interleaving leads to the error: +| ----------------------------------- | +| Thread 1 | +| ----------------------------------- | +| run(() -> kotlin.Unit): kotlin.Unit | +| ----------------------------------- | + +Detailed trace: +| -------------------------------------------------------------------------------------------------------------------------------------------------------------------- | +| Thread 1 | +| -------------------------------------------------------------------------------------------------------------------------------------------------------------------- | +| run(() -> kotlin.Unit): kotlin.Unit | +| failure$1.invoke() at BaseRunWithLambdaRepresentationTest$testRunWithModelChecker$failure$1.invoke(BaseTraceRepresentationTest.kt:62) | +| ArrayReadWriteRunWithLambdaTest#1.operation() at BaseRunWithLambdaRepresentationTest$testRunWithModelChecker$failure$1.invoke(BaseTraceRepresentationTest.kt:65) | +| IntArray#1[0].READ: 1 at ArrayReadWriteRunWithLambdaTest.operation(ArrayReadWriteRunWithLambdaTest.kt:21) | +| IntArray#1[0].WRITE(2) at ArrayReadWriteRunWithLambdaTest.operation(ArrayReadWriteRunWithLambdaTest.kt:21) | +| IntArray#1[0].READ: 2 at ArrayReadWriteRunWithLambdaTest.operation(ArrayReadWriteRunWithLambdaTest.kt:22) | +| result: kotlin.Unit | +| -------------------------------------------------------------------------------------------------------------------------------------------------------------------- | diff --git a/src/jvm/test/resources/expected_logs/atomic_references_name_two_fields_trace_run_with_lambda.txt b/src/jvm/test/resources/expected_logs/atomic_references_name_two_fields_trace_run_with_lambda.txt new file mode 100644 index 000000000..895091973 --- /dev/null +++ b/src/jvm/test/resources/expected_logs/atomic_references_name_two_fields_trace_run_with_lambda.txt @@ -0,0 +1,27 @@ += Invalid execution results = +| ----------------------------------- | +| Thread 1 | +| ----------------------------------- | +| run(() -> kotlin.Unit): kotlin.Unit | +| ----------------------------------- | + +The following interleaving leads to the error: +| ----------------------------------- | +| Thread 1 | +| ----------------------------------- | +| run(() -> kotlin.Unit): kotlin.Unit | +| ----------------------------------- | + +Detailed trace: +| ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | +| Thread 1 | +| ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | +| run(() -> kotlin.Unit): kotlin.Unit | +| failure$1.invoke() at BaseRunWithLambdaRepresentationTest$testRunWithModelChecker$failure$1.invoke(BaseTraceRepresentationTest.kt:62) | +| AtomicReferencesFromMultipleFieldsRunWithLambdaTest#1.operation() at BaseRunWithLambdaRepresentationTest$testRunWithModelChecker$failure$1.invoke(BaseTraceRepresentationTest.kt:65) | +| atomicReference1.READ: AtomicReference#1 at AtomicReferencesFromMultipleFieldsRunWithLambdaTest.operation(AtomicReferencesNamesRunWithLambdaTests.kt:97) | +| atomicReference2.READ: AtomicReference#1 at AtomicReferencesFromMultipleFieldsRunWithLambdaTest.operation(AtomicReferencesNamesRunWithLambdaTests.kt:97) | +| AtomicReference#1.get(): Node#1 at AtomicReferencesFromMultipleFieldsRunWithLambdaTest.operation(AtomicReferencesNamesRunWithLambdaTests.kt:97) | +| AtomicReference#1.compareAndSet(Node#1,Node#2): true at AtomicReferencesFromMultipleFieldsRunWithLambdaTest.operation(AtomicReferencesNamesRunWithLambdaTests.kt:97) | +| result: kotlin.Unit | +| ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | diff --git a/src/jvm/test/resources/expected_logs/atomic_references_names_trace_run_with_lambda.txt b/src/jvm/test/resources/expected_logs/atomic_references_names_trace_run_with_lambda.txt new file mode 100644 index 000000000..adc473067 --- /dev/null +++ b/src/jvm/test/resources/expected_logs/atomic_references_names_trace_run_with_lambda.txt @@ -0,0 +1,52 @@ += Invalid execution results = +| ----------------------------------- | +| Thread 1 | +| ----------------------------------- | +| run(() -> kotlin.Unit): kotlin.Unit | +| ----------------------------------- | + +The following interleaving leads to the error: +| ----------------------------------- | +| Thread 1 | +| ----------------------------------- | +| run(() -> kotlin.Unit): kotlin.Unit | +| ----------------------------------- | + +Detailed trace: +| ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | +| Thread 1 | +| ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | +| run(() -> kotlin.Unit): kotlin.Unit | +| failure$1.invoke() at BaseRunWithLambdaRepresentationTest$testRunWithModelChecker$failure$1.invoke(BaseTraceRepresentationTest.kt:62) | +| AtomicReferencesNamesRunWithLambdaTests#1.operation() at BaseRunWithLambdaRepresentationTest$testRunWithModelChecker$failure$1.invoke(BaseTraceRepresentationTest.kt:65) | +| AtomicReference#1.get(): Node#1 at AtomicReferencesNamesRunWithLambdaTests.operation(AtomicReferencesNamesRunWithLambdaTests.kt:29) | +| AtomicReference#1.compareAndSet(Node#1,Node#2): true at AtomicReferencesNamesRunWithLambdaTests.operation(AtomicReferencesNamesRunWithLambdaTests.kt:29) | +| AtomicReference#1.set(Node#3) at AtomicReferencesNamesRunWithLambdaTests.operation(AtomicReferencesNamesRunWithLambdaTests.kt:30) | +| AtomicInteger#1.get(): 3 at AtomicReferencesNamesRunWithLambdaTests.operation(AtomicReferencesNamesRunWithLambdaTests.kt:32) | +| AtomicInteger#1.compareAndSet(3,2): true at AtomicReferencesNamesRunWithLambdaTests.operation(AtomicReferencesNamesRunWithLambdaTests.kt:32) | +| AtomicInteger#1.set(3) at AtomicReferencesNamesRunWithLambdaTests.operation(AtomicReferencesNamesRunWithLambdaTests.kt:33) | +| AtomicLong#1.get(): 3 at AtomicReferencesNamesRunWithLambdaTests.operation(AtomicReferencesNamesRunWithLambdaTests.kt:35) | +| AtomicLong#1.compareAndSet(3,2): true at AtomicReferencesNamesRunWithLambdaTests.operation(AtomicReferencesNamesRunWithLambdaTests.kt:35) | +| AtomicLong#1.set(3) at AtomicReferencesNamesRunWithLambdaTests.operation(AtomicReferencesNamesRunWithLambdaTests.kt:36) | +| AtomicBoolean#1.get(): false at AtomicReferencesNamesRunWithLambdaTests.operation(AtomicReferencesNamesRunWithLambdaTests.kt:38) | +| AtomicBoolean#1.compareAndSet(false,true): true at AtomicReferencesNamesRunWithLambdaTests.operation(AtomicReferencesNamesRunWithLambdaTests.kt:38) | +| AtomicBoolean#1.set(false) at AtomicReferencesNamesRunWithLambdaTests.operation(AtomicReferencesNamesRunWithLambdaTests.kt:39) | +| AtomicReferenceArray#1[0].get(): Node#4 at AtomicReferencesNamesRunWithLambdaTests.operation(AtomicReferencesNamesRunWithLambdaTests.kt:41) | +| AtomicReferenceArray#1[0].compareAndSet(Node#4,Node#5): true at AtomicReferencesNamesRunWithLambdaTests.operation(AtomicReferencesNamesRunWithLambdaTests.kt:41) | +| AtomicReferenceArray#1[0].set(Node#6) at AtomicReferencesNamesRunWithLambdaTests.operation(AtomicReferencesNamesRunWithLambdaTests.kt:42) | +| AtomicIntegerArray#1[0].get(): 2 at AtomicReferencesNamesRunWithLambdaTests.operation(AtomicReferencesNamesRunWithLambdaTests.kt:44) | +| AtomicIntegerArray#1[0].compareAndSet(2,1): true at AtomicReferencesNamesRunWithLambdaTests.operation(AtomicReferencesNamesRunWithLambdaTests.kt:44) | +| AtomicIntegerArray#1[0].set(2) at AtomicReferencesNamesRunWithLambdaTests.operation(AtomicReferencesNamesRunWithLambdaTests.kt:45) | +| AtomicLongArray#1[0].get(): 2 at AtomicReferencesNamesRunWithLambdaTests.operation(AtomicReferencesNamesRunWithLambdaTests.kt:47) | +| AtomicLongArray#1[0].compareAndSet(2,1): true at AtomicReferencesNamesRunWithLambdaTests.operation(AtomicReferencesNamesRunWithLambdaTests.kt:47) | +| AtomicLongArray#1[0].set(2) at AtomicReferencesNamesRunWithLambdaTests.operation(AtomicReferencesNamesRunWithLambdaTests.kt:48) | +| AtomicReference#2.set(Node#7) at AtomicReferencesNamesRunWithLambdaTests.operation(AtomicReferencesNamesRunWithLambdaTests.kt:50) | +| AtomicIntegerArray#2[0].compareAndSet(1,2): false at AtomicReferencesNamesRunWithLambdaTests.operation(AtomicReferencesNamesRunWithLambdaTests.kt:51) | +| AtomicInteger#2.compareAndSet(0,2): true at AtomicReferencesNamesRunWithLambdaTests.operation(AtomicReferencesNamesRunWithLambdaTests.kt:53) | +| AtomicInteger#2.set(0) at AtomicReferencesNamesRunWithLambdaTests.operation(AtomicReferencesNamesRunWithLambdaTests.kt:54) | +| AtomicInteger#3.compareAndSet(1,2): false at AtomicReferencesNamesRunWithLambdaTests.operation(AtomicReferencesNamesRunWithLambdaTests.kt:56) | +| AtomicInteger#3.set(3) at AtomicReferencesNamesRunWithLambdaTests.operation(AtomicReferencesNamesRunWithLambdaTests.kt:57) | +| AtomicIntegerArray#3[1].compareAndSet(0,1): false at AtomicReferencesNamesRunWithLambdaTests.operation(AtomicReferencesNamesRunWithLambdaTests.kt:59) | +| AtomicIntegerArray#4[1].compareAndSet(0,1): false at AtomicReferencesNamesRunWithLambdaTests.operation(AtomicReferencesNamesRunWithLambdaTests.kt:60) | +| result: kotlin.Unit | +| ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | diff --git a/src/jvm/test/resources/expected_logs/variable_read_write_run_with_lambda.txt b/src/jvm/test/resources/expected_logs/variable_read_write_run_with_lambda.txt new file mode 100644 index 000000000..103e6f5b6 --- /dev/null +++ b/src/jvm/test/resources/expected_logs/variable_read_write_run_with_lambda.txt @@ -0,0 +1,28 @@ += Invalid execution results = +| ----------------------------------- | +| Thread 1 | +| ----------------------------------- | +| run(() -> kotlin.Unit): kotlin.Unit | +| ----------------------------------- | + +The following interleaving leads to the error: +| ----------------------------------- | +| Thread 1 | +| ----------------------------------- | +| run(() -> kotlin.Unit): kotlin.Unit | +| ----------------------------------- | + +Detailed trace: +| ----------------------------------------------------------------------------------------------------------------------------------------------------------------------- | +| Thread 1 | +| ----------------------------------------------------------------------------------------------------------------------------------------------------------------------- | +| run(() -> kotlin.Unit): kotlin.Unit | +| failure$1.invoke() at BaseRunWithLambdaRepresentationTest$testRunWithModelChecker$failure$1.invoke(BaseTraceRepresentationTest.kt:62) | +| VariableReadWriteRunWithLambdaTest#1.operation() at BaseRunWithLambdaRepresentationTest$testRunWithModelChecker$failure$1.invoke(BaseTraceRepresentationTest.kt:65) | +| x.READ: 0 at VariableReadWriteRunWithLambdaTest.operation(VariableReadWriteRunWithLambdaTest.kt:18) | +| x.WRITE(1) at VariableReadWriteRunWithLambdaTest.operation(VariableReadWriteRunWithLambdaTest.kt:18) | +| x.READ: 1 at VariableReadWriteRunWithLambdaTest.operation(VariableReadWriteRunWithLambdaTest.kt:19) | +| x.WRITE(0) at VariableReadWriteRunWithLambdaTest.operation(VariableReadWriteRunWithLambdaTest.kt:19) | +| x.READ: 0 at VariableReadWriteRunWithLambdaTest.operation(VariableReadWriteRunWithLambdaTest.kt:19) | +| result: kotlin.Unit | +| ----------------------------------------------------------------------------------------------------------------------------------------------------------------------- |