Skip to content

Commit

Permalink
Add tests
Browse files Browse the repository at this point in the history
  • Loading branch information
@dmitrii-artuhov
dmitrii-artuhov committed Dec 17, 2024
1 parent a9844ea commit 9e0d1fa
Show file tree
Hide file tree
Showing 9 changed files with 308 additions and 3 deletions.
10 changes: 7 additions & 3 deletions src/jvm/main/org/jetbrains/kotlinx/lincheck/Lincheck.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -25,15 +27,16 @@ 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.
* @param block lambda which body will be a target for the interleavings exploration.
*/
@JvmStatic
fun <R> verifyWithModelChecker(
invocations: Int = 1,
invocations: Int = ManagedCTestConfiguration.DEFAULT_INVOCATIONS,
verifierClass: Class<out Verifier>? = null,
block: () -> R
): LincheckFailure? {
val scenario = scenario {
Expand All @@ -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()

Expand Down
24 changes: 24 additions & 0 deletions ...est/org/jetbrains/kotlinx/lincheck_test/representation/ArrayReadWriteRunWithLambdaTest.kt
View file
Original file line number Diff line number Diff line change
@@ -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]
}
}
104 changes: 104 additions & 0 deletions ...jetbrains/kotlinx/lincheck_test/representation/AtomicReferencesNamesRunWithLambdaTests.kt
View file
Original file line number Diff line number Diff line change
@@ -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<Node>
private var atomicReference2: AtomicReference<Node>

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)

}


19 changes: 19 additions & 0 deletions ...vm/test/org/jetbrains/kotlinx/lincheck_test/representation/BaseTraceRepresentationTest.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
}
21 changes: 21 additions & 0 deletions .../org/jetbrains/kotlinx/lincheck_test/representation/VariableReadWriteRunWithLambdaTest.kt
View file
Original file line number Diff line number Diff line change
@@ -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
}
}
26 changes: 26 additions & 0 deletions src/jvm/test/resources/expected_logs/array_read_write_run_with_lambda.txt
View file
Original file line number Diff line number Diff line change
@@ -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 |
| -------------------------------------------------------------------------------------------------------------------------------------------------------------------- |
27 changes: 27 additions & 0 deletions .../test/resources/expected_logs/atomic_references_name_two_fields_trace_run_with_lambda.txt
View file
Original file line number Diff line number Diff line change
@@ -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 |
| ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- |
Loading

0 comments on commit 9e0d1fa

Please sign in to comment.