From 67ba3101544cf07d9bb9e34c83bdd10e75ab2bdb Mon Sep 17 00:00:00 2001 From: Evgeniy Moiseenko Date: Tue, 11 Apr 2023 18:38:29 +0200 Subject: [PATCH] LincheckOptions, testingTime option, statistics tracking and adaptive planning --- build.gradle.kts | 1 + .../kotlinx/lincheck/CTestConfiguration.kt | 13 +- .../jetbrains/kotlinx/lincheck/LinChecker.kt | 96 ++-- .../kotlinx/lincheck/LincheckOptions.kt | 436 ++++++++++++++++++ .../kotlinx/lincheck/LincheckTestingResult.kt | 35 ++ .../org/jetbrains/kotlinx/lincheck/Options.kt | 7 + .../org/jetbrains/kotlinx/lincheck/Planner.kt | 412 +++++++++++++++++ .../jetbrains/kotlinx/lincheck/Reporter.kt | 21 +- .../jetbrains/kotlinx/lincheck/RunTracker.kt | 149 ++++++ .../jetbrains/kotlinx/lincheck/Statistics.kt | 209 +++++++++ .../execution/ExecutionGenerator.java | 9 +- .../execution/RandomExecutionGenerator.java | 19 +- .../kotlinx/lincheck/strategy/Strategy.kt | 59 ++- .../strategy/managed/ManagedOptions.kt | 7 + .../strategy/managed/ManagedStrategy.kt | 73 ++- .../modelchecking/ModelCheckingCTest.java | 7 + .../ModelCheckingCTestConfiguration.kt | 10 +- .../modelchecking/ModelCheckingOptions.kt | 6 + .../modelchecking/ModelCheckingStrategy.kt | 61 ++- .../lincheck/strategy/stress/StressCTest.java | 9 + .../stress/StressCTestConfiguration.kt | 7 +- .../lincheck/strategy/stress/StressOptions.kt | 9 +- .../strategy/stress/StressStrategy.kt | 34 +- .../lincheck_test/AbstractLincheckTest.kt | 117 +++-- .../lincheck_test/AddCustomScenarioTest.kt | 21 +- .../lincheck_test/AlmostEmptyScenarioTest.kt | 3 +- .../lincheck_test/BlockingBehaviourTest.kt | 29 +- .../kotlinx/lincheck_test/ExceptionTest.kt | 75 ++- .../FailedScenarioMinimizationTest.kt | 0 .../lincheck_test/HangingDetectionTests.kt | 76 ++- .../IncorrectOnCancellationTest.kt | 2 + .../OperationsInAbstractClassTest.kt | 9 +- .../lincheck_test/PromptCancellationTest.kt | 13 +- .../kotlinx/lincheck_test/ThreadIdTest.kt | 2 + ...ectedExceptionInCancellationHandlerTest.kt | 14 +- .../lincheck_test/UnexpectedExceptionTest.kt | 4 + .../generator/ParamGeneratorsTests.kt | 78 ++-- .../lincheck_test/guide/BasicCounterTest.kt | 6 +- .../guide/ConcurrentLinkedDequeTest.kt | 4 +- .../guide/ConcurrentLinkedQueueTest.kt | 6 +- .../lincheck_test/guide/ConcurrentMapTest.kt | 19 +- .../lincheck_test/guide/CounterTest.kt | 25 +- .../lincheck_test/guide/MPSCQueueTest.kt | 8 +- .../guide/ObstructionFreedomViolationTest.kt | 6 +- .../AFUCallRepresentationTest.kt | 1 + .../CapturedValueRepresentationTest.kt | 14 +- .../ClocksWithExceptionsInOutputTest.kt | 23 +- ...CoroutineCancellationTraceReportingTest.kt | 14 +- .../representation/ExceptionsInOutputTest.kt | 19 +- .../ForcibleFinishExceptionInTryBlockTest.kt | 1 + .../IllegalModuleAccessOutputMessageTest.kt | 5 +- .../representation/InternalLincheckBugTest.kt | 7 +- .../representation/MethodReportingTest.kt | 19 +- .../ObstructionFreedomRepresentationTest.kt | 2 + .../representation/SpinlockEventsCutTests.kt | 80 ++-- .../representation/StateRepresentationTest.kt | 6 +- .../SuspendTraceReportingTest.kt | 15 +- .../SwitchAsFirstMethodEventTest.kt | 18 +- .../representation/ThreadDumpTest.kt | 1 + .../representation/TraceReportingTest.kt | 30 +- .../representation/ValidateFunctionTest.kt | 8 +- .../runner/CancellationHandlingTest.kt | 9 +- .../lincheck_test/runner/DeadlockTests.kt | 27 +- .../ParallelThreadsRunnerExceptionTest.kt | 4 +- .../lincheck_test/runner/RunBlockingTest.kt | 5 +- .../runner/TestThreadExecutionHelperTest.java | 4 +- .../ObstructionFreedomViolationTest.kt | 1 + .../SingletonCollectionInTraceTest.kt | 1 + .../FinalFieldReadingEliminationTest.kt | 3 + .../transformation/HashCodeStubTest.kt | 6 +- .../IgnoredGuaranteeOnExceptionTest.kt | 1 + .../transformation/IgnoredGuaranteeTest.kt | 1 + .../IterableTransformationTest.kt | 9 +- .../KotlinStdlibTransformationTest.kt | 17 +- .../LocalObjectEliminationTest.kt | 1 + .../NestedSynchronizedBlocksTest.kt | 5 +- .../RandomTransformationTest.kt | 5 +- .../transformation/SerializableValueTests.kt | 71 ++- .../transformation/Striped64SupportTest.kt | 10 +- .../transformation/TimeStubTest.kt | 3 +- ...rmInterfaceFromJUCWithRemappedClassTest.kt | 15 +- .../TransformedExceptionTests.kt | 15 +- .../transformation/WaitNotifyLockTests.kt | 9 +- .../verifier/AllowExtraSuspensionTest.kt | 20 +- .../verifier/EpsilonVerifierTest.kt | 6 +- .../verifier/SequentialSpecificationTest.kt | 4 +- .../linearizability/BufferedChannelTest.kt | 7 +- .../linearizability/ConcurrentDequeTest.kt | 4 +- .../linearizability/ConcurrentHashMapTest.kt | 7 - .../verifier/linearizability/CounterTests.kt | 3 + .../linearizability/LockBasedSetTests.kt | 2 + .../linearizability/LockFreeSetTest.kt | 13 +- .../linearizability/ManySwitchBugTest.kt | 21 +- .../linearizability/RendezvousChannelTest.kt | 8 +- .../quiescent/LockFreeTaskQueueTest.kt | 10 +- .../serializability/SerializableQueueTest.kt | 9 +- .../expected_logs/clocks_and_exceptions.txt | 99 +--- .../infinite_spin_loop_events_cut.txt | 192 ++++---- .../expected_logs/trace_reporting_empty.txt | 2 +- 99 files changed, 2274 insertions(+), 824 deletions(-) create mode 100644 src/jvm/main/org/jetbrains/kotlinx/lincheck/LincheckOptions.kt create mode 100644 src/jvm/main/org/jetbrains/kotlinx/lincheck/LincheckTestingResult.kt create mode 100644 src/jvm/main/org/jetbrains/kotlinx/lincheck/Planner.kt create mode 100644 src/jvm/main/org/jetbrains/kotlinx/lincheck/RunTracker.kt create mode 100644 src/jvm/main/org/jetbrains/kotlinx/lincheck/Statistics.kt create mode 100644 src/jvm/test/org/jetbrains/kotlinx/lincheck_test/FailedScenarioMinimizationTest.kt diff --git a/build.gradle.kts b/build.gradle.kts index f76b86292..351ec4daf 100644 --- a/build.gradle.kts +++ b/build.gradle.kts @@ -93,6 +93,7 @@ tasks { withType { maxParallelForks = 1 jvmArgs( + "-Xmx1G", "--add-opens", "java.base/jdk.internal.misc=ALL-UNNAMED", "--add-exports", "java.base/jdk.internal.util=ALL-UNNAMED", "--add-exports", "java.base/sun.security.action=ALL-UNNAMED" diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/CTestConfiguration.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/CTestConfiguration.kt index f73285787..2a1dac4db 100644 --- a/src/jvm/main/org/jetbrains/kotlinx/lincheck/CTestConfiguration.kt +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/CTestConfiguration.kt @@ -9,11 +9,9 @@ */ package org.jetbrains.kotlinx.lincheck -import org.jetbrains.kotlinx.lincheck.CTestConfiguration.Companion.DEFAULT_TIMEOUT_MS import org.jetbrains.kotlinx.lincheck.execution.* import org.jetbrains.kotlinx.lincheck.strategy.* import org.jetbrains.kotlinx.lincheck.strategy.managed.* -import org.jetbrains.kotlinx.lincheck.strategy.managed.ManagedCTestConfiguration.Companion.DEFAULT_ELIMINATE_LOCAL_OBJECTS import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.* import org.jetbrains.kotlinx.lincheck.strategy.stress.* import org.jetbrains.kotlinx.lincheck.verifier.* @@ -38,8 +36,8 @@ abstract class CTestConfiguration( val customScenarios: List ) { abstract fun createStrategy( - testClass: Class<*>, scenario: ExecutionScenario, validationFunctions: List, - stateRepresentationMethod: Method?, verifier: Verifier + testClass: Class<*>, scenario: ExecutionScenario, + validationFunctions: List, stateRepresentationMethod: Method? ): Strategy companion object { @@ -55,6 +53,7 @@ abstract class CTestConfiguration( } } +@Suppress("DEPRECATION_ERROR") internal fun createFromTestClassAnnotations(testClass: Class<*>): List { val stressConfigurations: List = testClass.getAnnotationsByType(StressCTest::class.java) .map { ann: StressCTest -> @@ -70,7 +69,7 @@ internal fun createFromTestClassAnnotations(testClass: Class<*>): List): List, options: Options<*, *>?) { +@Suppress("DEPRECATION_ERROR") +class LinChecker(private val testClass: Class<*>, options: Options<*, *>?) { private val testStructure = CTestStructure.getFromTestClass(testClass) private val testConfigurations: List private val reporter: Reporter @@ -56,7 +59,7 @@ class LinChecker (private val testClass: Class<*>, options: Options<*, *>?) { val verifier = createVerifier() val scenario = customScenarios[i] scenario.validate() - reporter.logIteration(i + 1, customScenarios.size, scenario) + reporter.logIteration(iteration = i + 1, scenario = scenario) val failure = scenario.run(this, verifier) if (failure != null) return failure } @@ -69,12 +72,18 @@ class LinChecker (private val testClass: Class<*>, options: Options<*, *>?) { // https://github.com/Kotlin/kotlinx-lincheck/issues/124 if ((i + 1) % VERIFIER_REFRESH_CYCLE == 0) verifier = createVerifier() - val scenario = exGen.nextExecution() + val scenario = exGen.nextExecution(threads, actorsPerThread, actorsBefore, actorsAfter) scenario.validate() - reporter.logIteration(i + 1 + customScenarios.size, iterations, scenario) + reporter.logIteration(iteration = i + 1 + customScenarios.size, scenario = scenario) val failure = scenario.run(this, verifier) if (failure != null) { - val minimizedFailedIteration = if (!minimizeFailedScenario) failure else failure.minimize(this) + val minimizedFailedIteration = if (minimizeFailedScenario) { + reporter.logScenarioMinimization(scenario) + failure.minimize { + it.run(this, createVerifier()) + } + } else + failure reporter.logFailedIteration(minimizedFailedIteration) return minimizedFailedIteration } @@ -84,51 +93,30 @@ class LinChecker (private val testClass: Class<*>, options: Options<*, *>?) { return null } - // Tries to minimize the specified failing scenario to make the error easier to understand. - // The algorithm is greedy: it tries to remove one actor from the scenario and checks - // whether a test with the modified one fails with error as well. If it fails, - // then the scenario has been successfully minimized, and the algorithm tries to minimize it again, recursively. - // Otherwise, if no actor can be removed so that the generated test fails, the minimization is completed. - // Thus, the algorithm works in the linear time of the total number of actors. - private fun LincheckFailure.minimize(testCfg: CTestConfiguration): LincheckFailure { - reporter.logScenarioMinimization(scenario) - var minimizedFailure = this - while (true) { - minimizedFailure = minimizedFailure.scenario.tryMinimize(testCfg) ?: break - } - return minimizedFailure - } - - private fun ExecutionScenario.tryMinimize(testCfg: CTestConfiguration): LincheckFailure? { - // Reversed indices to avoid conflicts with in-loop removals - for (i in threads.indices.reversed()) { - for (j in threads[i].indices.reversed()) { - tryMinimize(i, j) - ?.run(testCfg, testCfg.createVerifier()) - ?.let { return it } - } - } - return null - } - private fun ExecutionScenario.run(testCfg: CTestConfiguration, verifier: Verifier): LincheckFailure? = testCfg.createStrategy( testClass = testClass, scenario = this, validationFunctions = testStructure.validationFunctions, - stateRepresentationMethod = testStructure.stateRepresentation, - verifier = verifier - ).run() + stateRepresentationMethod = testStructure.stateRepresentation + ).use { + it.run(verifier, FixedInvocationsPlanner(testCfg.invocations)) + } + + private val CTestConfiguration.invocations get() = when (this) { + is ModelCheckingCTestConfiguration -> this.invocationsPerIteration + is StressCTestConfiguration -> this.invocationsPerIteration + else -> error("unexpected") + } private fun CTestConfiguration.createVerifier() = verifierClass.getConstructor(Class::class.java).newInstance(sequentialSpecification) private fun CTestConfiguration.createExecutionGenerator(randomProvider: RandomProvider) = generatorClass.getConstructor( - CTestConfiguration::class.java, CTestStructure::class.java, RandomProvider::class.java - ).newInstance(this, testStructure, randomProvider) + ).newInstance(testStructure, randomProvider) // This companion object is used for backwards compatibility. companion object { @@ -144,11 +132,10 @@ class LinChecker (private val testClass: Class<*>, options: Options<*, *>?) { LinChecker(testClass, options).check() } - private const val VERIFIER_REFRESH_CYCLE = 100 + internal const val VERIFIER_REFRESH_CYCLE = 100 } } - /** * This is a short-cut for the following code: * ``` @@ -156,6 +143,7 @@ class LinChecker (private val testClass: Class<*>, options: Options<*, *>?) { * LinChecker.check(testClass, options) * ``` */ +@Suppress("DEPRECATION_ERROR") fun > O.check(testClass: Class<*>) = LinChecker.check(testClass, this) /** @@ -165,6 +153,34 @@ fun > O.check(testClass: Class<*>) = LinChecker.check(testClas * LinChecker.check(testClass.java, options) * ``` */ +@Suppress("DEPRECATION_ERROR") fun > O.check(testClass: KClass<*>) = this.check(testClass.java) -internal fun > O.checkImpl(testClass: Class<*>) = LinChecker(testClass, this).checkImpl() \ No newline at end of file +@Suppress("DEPRECATION_ERROR") +internal fun > O.checkImpl(testClass: Class<*>) = LinChecker(testClass, this).checkImpl() + +// Tries to minimize the specified failing scenario to make the error easier to understand. +// The algorithm is greedy: it tries to remove one actor from the scenario and checks +// whether a test with the modified one fails with error as well. If it fails, +// then the scenario has been successfully minimized, and the algorithm tries to minimize it again, recursively. +// Otherwise, if no actor can be removed so that the generated test fails, the minimization is completed. +// Thus, the algorithm works in the linear time of the total number of actors. +internal fun LincheckFailure.minimize(checkScenario: (ExecutionScenario) -> LincheckFailure?): LincheckFailure { + var minimizedFailure = this + while (true) { + minimizedFailure = minimizedFailure.scenario.tryMinimize(checkScenario) ?: break + } + return minimizedFailure +} + +private fun ExecutionScenario.tryMinimize(checkScenario: (ExecutionScenario) -> LincheckFailure?): LincheckFailure? { + // Reversed indices to avoid conflicts with in-loop removals + for (i in threads.indices.reversed()) { + for (j in threads[i].indices.reversed()) { + tryMinimize(i, j) + ?.run(checkScenario) + ?.let { return it } + } + } + return null +} \ No newline at end of file diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/LincheckOptions.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/LincheckOptions.kt new file mode 100644 index 000000000..7ca7edf03 --- /dev/null +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/LincheckOptions.kt @@ -0,0 +1,436 @@ +/* + * Lincheck + * + * Copyright (C) 2019 - 2023 JetBrains s.r.o. + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU Lesser General Public License as + * published by the Free Software Foundation, either version 3 of the + * License, or (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Lesser Public License for more details. + * + * You should have received a copy of the GNU General Lesser Public + * License along with this program. If not, see + * + */ +package org.jetbrains.kotlinx.lincheck + +import org.jetbrains.kotlinx.lincheck.execution.* +import org.jetbrains.kotlinx.lincheck.strategy.* +import org.jetbrains.kotlinx.lincheck.strategy.managed.* +import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.* +import org.jetbrains.kotlinx.lincheck.strategy.stress.* +import org.jetbrains.kotlinx.lincheck.verifier.* +import org.jetbrains.kotlinx.lincheck.verifier.linearizability.* +import java.lang.IllegalStateException +import kotlin.math.* +import kotlin.reflect.* + +interface LincheckOptions { + /** + * The maximal amount of time in seconds dedicated to testing. + */ + var testingTimeInSeconds: Long + + /** + * Maximal number of threads in generated scenarios. + */ + var maxThreads: Int + + /** + * Maximal number of operations in generated scenarios. + */ + var maxOperationsInThread: Int + + /** + * The verifier class used to check consistency of the execution. + */ + var verifier: Class + + /** + * The specified class defines the sequential behavior of the testing data structure; + * it is used by [Verifier] to build a labeled transition system, + * and should have the same methods as the testing data structure. + * + * By default, the provided concurrent implementation is used in a sequential way. + */ + var sequentialImplementation: Class<*>? + + /** + * Set to `true` to check the testing algorithm for obstruction-freedom. + * It also extremely useful for lock-free and wait-free algorithms. + */ + var checkObstructionFreedom: Boolean + + /** + * Add the specified custom [scenario] additionally to the generated ones. + * If [invocations] count is specified, the scenario will be run exactly this number of times. + */ + fun addCustomScenario(scenario: ExecutionScenario, invocations: Int? = null) + + /** + * Runs the Lincheck test on the specified class. + * + * @return [LincheckFailure] if some bug has been found. + */ + fun runTests(testClass: Class<*>, tracker: RunTracker? = null): LincheckFailure? +} + +/** + * Creates new instance of LincheckOptions class. + */ +fun LincheckOptions(): LincheckOptions = LincheckOptionsImpl() + +fun LincheckOptions(configurationBlock: LincheckOptions.() -> Unit): LincheckOptions { + val options = LincheckOptionsImpl() + options.configurationBlock() + return options +} + +/** + * Runs the Lincheck test on the specified class. + * + * @return [LincheckFailure] if some bug has been found. + */ +fun LincheckOptions.checkImpl(testClass: Class<*>): LincheckFailure? = + runTests(testClass) + +/** + * Runs the Lincheck test on the specified class. + * + * @throws [LincheckAssertionError] if some bug has been found. + */ +fun LincheckOptions.check(testClass: Class<*>) { + checkImpl(testClass)?.let { throw LincheckAssertionError(it) } +} + +/** + * Add the specified custom scenario additionally to the generated ones. + */ +fun LincheckOptions.addCustomScenario(invocations: Int? = null, scenarioBuilder: DSLScenarioBuilder.() -> Unit): Unit = + addCustomScenario(scenario { scenarioBuilder() }, invocations) + +fun LincheckOptions.check(testClass: KClass<*>) = check(testClass.java) + +// For internal tests only. +enum class LincheckMode { + Stress, ModelChecking, Hybrid +} + +internal data class LincheckOptionsImpl( + /* execution time options */ + var testingTimeMs: Long = DEFAULT_TESTING_TIME_MS, + internal var invocationTimeoutMs: Long = CTestConfiguration.DEFAULT_TIMEOUT_MS, + /* random scenarios generation options */ + internal var generateRandomScenarios: Boolean = true, + override var maxThreads: Int = DEFAULT_MAX_THREADS, + internal var minThreads: Int = DEFAULT_MIN_THREADS, + override var maxOperationsInThread: Int = DEFAULT_MAX_OPERATIONS, + internal var minOperationsInThread: Int = DEFAULT_MIN_OPERATIONS, + internal var generateBeforeAndAfterParts: Boolean = true, + /* custom scenarios options */ + internal val customScenariosOptions: MutableList = mutableListOf(), + /* verification options */ + override var sequentialImplementation: Class<*>? = null, + override var verifier: Class = LinearizabilityVerifier::class.java, + override var checkObstructionFreedom: Boolean = false, + /* strategy options */ + internal var mode: LincheckMode = LincheckMode.Hybrid, + internal var minimizeFailedScenario: Boolean = true, + internal var tryReproduceTrace: Boolean = false, +) : LincheckOptions { + + override var testingTimeInSeconds: Long + get() = (testingTimeMs.toDouble() / 1000L).roundToLong() + set(value) { + testingTimeMs = value * 1000L + } + + private val shouldRunCustomScenarios: Boolean + get() = customScenariosOptions.size > 0 + + private val shouldRunRandomScenarios: Boolean + get() = generateRandomScenarios + + private val shouldRunStressStrategy: Boolean + get() = (mode == LincheckMode.Stress) || (mode == LincheckMode.Hybrid) + + private val shouldRunModelCheckingStrategy: Boolean + get() = (mode == LincheckMode.ModelChecking) || (mode == LincheckMode.Hybrid) + + private val stressTestingTimeMs: Long + get() = when (mode) { + LincheckMode.Hybrid -> round(testingTimeMs * STRATEGY_SWITCH_THRESHOLD).toLong() + LincheckMode.Stress -> testingTimeMs + LincheckMode.ModelChecking -> 0 + } + + private val modelCheckingTimeMs: Long + get() = when (mode) { + LincheckMode.Hybrid -> round(testingTimeMs * (1 - STRATEGY_SWITCH_THRESHOLD)).toLong() + LincheckMode.ModelChecking -> testingTimeMs + LincheckMode.Stress -> 0 + } + + override fun addCustomScenario(scenario: ExecutionScenario, invocations: Int?) { + customScenariosOptions.add( + CustomScenarioOptions( + scenario = scenario, + invocations = invocations ?: CUSTOM_SCENARIO_DEFAULT_INVOCATIONS_COUNT + ) + ) + } + + override fun runTests(testClass: Class<*>, tracker: RunTracker?): LincheckFailure? { + val testStructure = CTestStructure.getFromTestClass(testClass) + if (customScenariosOptions.size > 0) { + runCustomScenarios(testClass, testStructure, tracker)?.let { return it } + } + if (generateRandomScenarios) { + runRandomScenarios(testClass, testStructure, tracker)?.let { return it } + } + return null + } + + private fun runCustomScenarios(testClass: Class<*>, testStructure: CTestStructure, tracker: RunTracker?): LincheckFailure? { + if (shouldRunStressStrategy) { + val stressOptions = copy( + mode = LincheckMode.Stress, + generateRandomScenarios = false, + tryReproduceTrace = (mode == LincheckMode.Hybrid) + ) + val (failure, _) = stressOptions.runImpl(testClass, testStructure, tracker) + if (failure != null) + return failure + } + if (shouldRunModelCheckingStrategy) { + val modelCheckingOptions = copy( + mode = LincheckMode.ModelChecking, + generateRandomScenarios = false, + tryReproduceTrace = true + ) + val (failure, _) = modelCheckingOptions.runImpl(testClass, testStructure, tracker) + if (failure != null) + return failure + } + return null + } + + private fun runRandomScenarios(testClass: Class<*>, testStructure: CTestStructure, tracker: RunTracker?): LincheckFailure? { + var stressTestingTimeMs = this.stressTestingTimeMs + var modelCheckingTimeMs = this.modelCheckingTimeMs + if (shouldRunStressStrategy) { + val stressOptions = copy( + mode = LincheckMode.Stress, + testingTimeMs = stressTestingTimeMs, + customScenariosOptions = mutableListOf(), + tryReproduceTrace = (mode == LincheckMode.Hybrid) + ) + val (failure, statistics) = stressOptions.runImpl(testClass, testStructure, tracker) + if (failure != null) + return failure + modelCheckingTimeMs = testingTimeMs - (statistics.totalRunningTimeNano / 1_000_000) + } + if (shouldRunModelCheckingStrategy) { + val modelCheckingOptions = copy( + mode = LincheckMode.ModelChecking, + testingTimeMs = modelCheckingTimeMs, + customScenariosOptions = mutableListOf(), + tryReproduceTrace = true + ) + val (failure, _) = modelCheckingOptions.runImpl(testClass, testStructure, tracker) + if (failure != null) + return failure + } + return null + } + + private fun getRunName(testClass: Class<*>): String { + check(shouldRunCustomScenarios xor shouldRunRandomScenarios) + val scenariosKind = when { + shouldRunCustomScenarios -> "CustomScenarios" + shouldRunRandomScenarios -> "RandomScenarios" + else -> throw IllegalStateException() + } + return "${testClass.name}-${scenariosKind}-${mode}-${abs(hashCode())}" + } + + private fun runImpl( + testClass: Class<*>, + testStructure: CTestStructure, + customTracker: RunTracker? = null + ): Pair { + check(mode in listOf(LincheckMode.Stress, LincheckMode.ModelChecking)) + check(shouldRunCustomScenarios xor shouldRunRandomScenarios) + return customTracker.trackRun(getRunName(testClass), this) { + val statisticsTracker = StatisticsTracker() + val verifierManager = createVerifierManager(testClass) + val planner = when { + shouldRunCustomScenarios -> CustomScenariosPlanner(customScenariosOptions) + shouldRunRandomScenarios -> RandomScenariosPlanner(mode, testStructure, statisticsTracker) + else -> throw IllegalStateException() + } + val reporterManager = createReporterManager(statisticsTracker, planner) + val tracker = trackersList( + listOfNotNull( + statisticsTracker, + reporterManager, + customTracker, + ) + ) + var failure = planner.runIterations(tracker) { scenario -> + // TODO: move scenario validation to more appropriate place? + scenario.validate() + createStrategy(mode, testClass, testStructure, scenario) to verifierManager.verifier + } ?: return@trackRun (null to statisticsTracker) + // TODO: implement a minimization planner? + if (minimizeFailedScenario) { + reporterManager.reporter.logScenarioMinimization(failure.scenario) + failure = failure.minimize { + it.run( + mode, testClass, testStructure, + createVerifier(testClass), + FixedInvocationsPlanner(MINIMIZATION_INVOCATIONS_COUNT) + ) + } + } + // TODO: move to StressStrategy.collectTrace() ? + if (failure.trace == null && mode != LincheckMode.ModelChecking && tryReproduceTrace) { + // try to reproduce an error trace with model checking strategy + failure.scenario.run( + LincheckMode.ModelChecking, + testClass, testStructure, + createVerifier(testClass), + FixedInvocationsPlanner(MODEL_CHECKING_ON_ERROR_INVOCATIONS_COUNT) + )?.let { + failure = it + } + } + reporterManager.reporter.logFailedIteration(failure) + return@trackRun (failure to statisticsTracker) + } + } + + private fun ExecutionScenario.run( + currentMode: LincheckMode, + testClass: Class<*>, + testStructure: CTestStructure, + verifier: Verifier, + planner: InvocationsPlanner, + statisticsTracker: StatisticsTracker? = null, + ): LincheckFailure? = + createStrategy(currentMode, testClass, testStructure, this).use { + it.run(verifier, planner, statisticsTracker) + } + + private fun createReporterManager(statistics: Statistics?, planner: Planner) = object : RunTracker { + val reporter = Reporter(DEFAULT_LOG_LEVEL) + + override fun iterationStart(iteration: Int, scenario: ExecutionScenario) { + reporter.logIteration(iteration + 1, scenario) + } + + override fun iterationEnd(iteration: Int, failure: LincheckFailure?, exception: Throwable?) { + statistics?.apply { + reporter.logIterationStatistics( + invocations = iterationsStatistics[iteration].totalInvocationsCount, + runningTimeNano = iterationsStatistics[iteration].totalRunningTimeNano, + remainingTimeNano = (planner.iterationsPlanner as? AdaptivePlanner)?.remainingTimeNano + ) + } + } + } + + private fun RandomScenariosPlanner(mode: LincheckMode, testStructure: CTestStructure, statisticsTracker: StatisticsTracker): Planner = + RandomScenariosAdaptivePlanner( + mode = mode, + minThreads = min(minThreads, maxThreads), + minOperations = min(minOperationsInThread, maxOperationsInThread), + maxThreads = maxThreads, + maxOperations = maxOperationsInThread, + generateBeforeAndAfterParts = generateBeforeAndAfterParts, + scenarioGenerator = RandomExecutionGenerator(testStructure, testStructure.randomProvider), + statisticsTracker = statisticsTracker, + testingTimeMs = testingTimeMs, + ) + + private fun createVerifier(testClass: Class<*>) = verifier + .getConstructor(Class::class.java) + .newInstance( + chooseSequentialSpecification(sequentialImplementation, testClass) + ) + + private fun createVerifierManager(testClass: Class<*>) = object : RunTracker { + lateinit var verifier: Verifier + private set + + init { + refresh() + } + + override fun iterationStart(iteration: Int, scenario: ExecutionScenario) { + // For performance reasons, verifier re-uses LTS from previous iterations. + // This behaviour is similar to a memory leak and can potentially cause OutOfMemoryError. + // This is why we periodically create a new verifier to still have increased performance + // from re-using LTS and limit the size of potential memory leak. + // https://github.com/Kotlin/kotlinx-lincheck/issues/124 + if ((iteration + 1) % LinChecker.VERIFIER_REFRESH_CYCLE == 0) { + refresh() + } + } + + private fun refresh() { + verifier = createVerifier(testClass) + } + } + + private fun createStrategy( + mode: LincheckMode, + testClass: Class<*>, + testStructure: CTestStructure, + scenario: ExecutionScenario, + ): Strategy = when (mode) { + + LincheckMode.Stress -> StressStrategy(testClass, scenario, + testStructure.validationFunctions, + testStructure.stateRepresentation, + timeoutMs = invocationTimeoutMs, + ) + + LincheckMode.ModelChecking -> ModelCheckingStrategy(testClass, scenario, + testStructure.validationFunctions, + testStructure.stateRepresentation, + timeoutMs = invocationTimeoutMs, + checkObstructionFreedom = checkObstructionFreedom, + eliminateLocalObjects = ManagedCTestConfiguration.DEFAULT_ELIMINATE_LOCAL_OBJECTS, + hangingDetectionThreshold = ManagedCTestConfiguration.DEFAULT_HANGING_DETECTION_THRESHOLD, + guarantees = ManagedCTestConfiguration.DEFAULT_GUARANTEES, + ) + + else -> throw IllegalArgumentException() + } +} + +internal class CustomScenarioOptions( + val scenario: ExecutionScenario, + val invocations: Int, +) + +private const val DEFAULT_TESTING_TIME_MS = 5000L +private const val DEFAULT_MIN_THREADS = 2 +private const val DEFAULT_MAX_THREADS = 3 +private const val DEFAULT_MIN_OPERATIONS = 2 +private const val DEFAULT_MAX_OPERATIONS = 5 + +// in hybrid mode: testing progress threshold (in %) after which strategy switch +// from Stress to ModelChecking strategy occurs +private const val STRATEGY_SWITCH_THRESHOLD = 0.25 + +private const val CUSTOM_SCENARIO_DEFAULT_INVOCATIONS_COUNT = 10_000 +private const val MINIMIZATION_INVOCATIONS_COUNT = 10_000 +private const val MODEL_CHECKING_ON_ERROR_INVOCATIONS_COUNT = 10_000 + diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/LincheckTestingResult.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/LincheckTestingResult.kt new file mode 100644 index 000000000..bd8b8895c --- /dev/null +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/LincheckTestingResult.kt @@ -0,0 +1,35 @@ +/* + * Lincheck + * + * Copyright (C) 2019 - 2023 JetBrains s.r.o. + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU Lesser General Public License as + * published by the Free Software Foundation, either version 3 of the + * License, or (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Lesser Public License for more details. + * + * You should have received a copy of the GNU General Lesser Public + * License along with this program. If not, see + * + */ + +package org.jetbrains.kotlinx.lincheck + +import org.jetbrains.kotlinx.lincheck.strategy.LincheckFailure + +data class LincheckTestingResult( + val failure: LincheckFailure?, + val statistics: Statistics, +) { + val isSuccessful: Boolean + get() = (failure == null) + + val isFailed: Boolean + get() = (failure != null) +} + diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/Options.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/Options.kt index 8c2c5ec90..447080459 100644 --- a/src/jvm/main/org/jetbrains/kotlinx/lincheck/Options.kt +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/Options.kt @@ -7,6 +7,8 @@ * 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/. */ +@file:Suppress("DEPRECATION_ERROR", "DEPRECATION") + package org.jetbrains.kotlinx.lincheck import org.jetbrains.kotlinx.lincheck.annotations.Operation @@ -16,6 +18,11 @@ import org.jetbrains.kotlinx.lincheck.verifier.* /** * Abstract class for test options. */ +@Deprecated( + message= "Options class exposes internal API, please use LincheckOptions instead", + replaceWith=ReplaceWith("LincheckOptions"), + level=DeprecationLevel.ERROR, +) abstract class Options, CTEST : CTestConfiguration> { internal var logLevel = DEFAULT_LOG_LEVEL protected var iterations = CTestConfiguration.DEFAULT_ITERATIONS diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/Planner.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/Planner.kt new file mode 100644 index 000000000..3addafd44 --- /dev/null +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/Planner.kt @@ -0,0 +1,412 @@ +/* + * Lincheck + * + * Copyright (C) 2019 - 2023 JetBrains s.r.o. + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU Lesser General Public License as + * published by the Free Software Foundation, either version 3 of the + * License, or (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Lesser Public License for more details. + * + * You should have received a copy of the GNU General Lesser Public + * License along with this program. If not, see + * + */ + +package org.jetbrains.kotlinx.lincheck + +import org.jetbrains.kotlinx.lincheck.execution.ExecutionGenerator +import org.jetbrains.kotlinx.lincheck.execution.ExecutionScenario +import org.jetbrains.kotlinx.lincheck.strategy.LincheckFailure +import org.jetbrains.kotlinx.lincheck.strategy.Strategy +import org.jetbrains.kotlinx.lincheck.verifier.Verifier +import kotlin.math.* + +interface Planner { + val scenarios: Sequence + val iterationsPlanner: IterationsPlanner + val invocationsPlanner: InvocationsPlanner +} + +interface IterationsPlanner { + fun shouldDoNextIteration(iteration: Int): Boolean +} + +interface InvocationsPlanner { + fun shouldDoNextInvocation(invocation: Int): Boolean +} + +fun Planner.runIterations( + tracker: RunTracker? = null, + factory: (ExecutionScenario) -> Pair, +): LincheckFailure? { + scenarios.forEachIndexed { i, scenario -> + if (!iterationsPlanner.shouldDoNextIteration(i)) + return null + tracker.trackIteration(i, scenario) { + val (strategy, verifier) = factory(scenario) + strategy.use { + var invocation = 0 + while (invocationsPlanner.shouldDoNextInvocation(invocation)) { + if (!strategy.nextInvocation()) { + return@trackIteration null + } + strategy.initializeInvocation() + tracker.trackInvocation(invocation) { + strategy.runInvocation(verifier) + }?.let { + return@trackIteration it + } + invocation++ + } + } + return@trackIteration null + }?.let { + return it + } + } + return null +} + +internal class CustomScenariosPlanner( + val scenariosOptions: List, +) : Planner, IterationsPlanner { + + override val scenarios = scenariosOptions.asSequence().map { it.scenario } + + override val iterationsPlanner = this + + override var invocationsPlanner = FixedInvocationsPlanner(0) + private set + + override fun shouldDoNextIteration(iteration: Int): Boolean { + invocationsPlanner = FixedInvocationsPlanner(scenariosOptions[iteration].invocations) + return iteration < scenariosOptions.size + } + +} + +internal class RandomScenariosAdaptivePlanner( + mode: LincheckMode, + testingTimeMs: Long, + val minThreads: Int, + val maxThreads: Int, + val minOperations: Int, + val maxOperations: Int, + val generateBeforeAndAfterParts: Boolean, + scenarioGenerator: ExecutionGenerator, + statisticsTracker: StatisticsTracker, +) : Planner { + private val planner = AdaptivePlanner(mode, testingTimeMs, statisticsTracker) + override val iterationsPlanner = planner + override val invocationsPlanner = planner + + private val configurations: List> = run { + (minThreads .. maxThreads).flatMap { threads -> + (minOperations .. maxOperations).flatMap { operations -> + listOf(threads to operations) + } + } + } + + override val scenarios = sequence { + while (true) { + val n = round(planner.testingProgress * configurations.size).toInt() + .coerceAtLeast(0) + .coerceAtMost(configurations.size - 1) + val (threads, operations) = configurations[n] + yield(scenarioGenerator.nextExecution(threads, operations, + if (generateBeforeAndAfterParts) operations else 0, + if (generateBeforeAndAfterParts) operations else 0, + )) + } + } +} + +internal class FixedInvocationsPlanner(val totalInvocations: Int) : InvocationsPlanner { + override fun shouldDoNextInvocation(invocation: Int) = + invocation < totalInvocations +} + +/** + * The class for planning the work distribution during one run. + * In particular, it is responsible for the following activities: + * - measuring the time of invocations run; + * - keep the track of deadlines and remaining time; + * - adaptively adjusting number of test scenarios and invocations allocated per scenario. + */ +internal class AdaptivePlanner( + /** + * Testing mode. It is used to calculate upper/lower bounds on the number of invocations. + */ + mode: LincheckMode, + /** + * Total amount of time in milliseconds allocated for testing. + */ + testingTimeMs: Long, + /** + * Statistics tracker. + */ + val statisticsTracker: StatisticsTracker, +) : IterationsPlanner, InvocationsPlanner { + + /** + * Total amount of time in nanoseconds allocated for testing. + */ + var testingTimeNano: Long = testingTimeMs * 1_000_000 + private set + + /** + * Remaining amount of time for testing. + */ + val remainingTimeNano: Long + get() = (testingTimeNano - statisticsTracker.totalRunningTimeNano).coerceAtLeast(0) + + /** + * Testing progress: floating-point number in range [0.0 .. 1.0], + * representing a fraction of spent testing time. + */ + val testingProgress: Double + get() = (statisticsTracker.totalRunningTimeNano / testingTimeNano.toDouble()).coerceAtMost(1.0) + + /** + * Admissible time delay (in nano-seconds) for last iteration to finish, + * even if it exceeds [remainingTimeNano]. + */ + private val admissibleErrorTimeNano = TIME_ERROR_MARGIN_NANO / 2 + + /** + * Bound on the number of iterations. + * Adjusted automatically after each iteration. + */ + private var iterationsBound = INITIAL_ITERATIONS_BOUND + + /** + * Bound on the number of invocations allocated to current iteration. + * Adjusted automatically after each iteration. + */ + private var invocationsBound = INITIAL_INVOCATIONS_BOUND + + /** + * Lower bound of invocations allocated per iteration. + */ + private val invocationsLowerBound = INVOCATIONS_LOWER_BOUND + + /** + * Upper bound of invocations allocated per iteration. + */ + private val invocationsUpperBound = when (mode) { + LincheckMode.Stress -> STRESS_INVOCATIONS_UPPER_BOUND + LincheckMode.ModelChecking -> MODEL_CHECKING_INVOCATIONS_UPPER_BOUND + else -> throw IllegalArgumentException() + } + + private var currentIterationUpperTimeNano = Long.MAX_VALUE + + override fun shouldDoNextIteration(iteration: Int): Boolean { + check(iteration == statisticsTracker.iteration + 1) + if (iteration >= WARM_UP_ITERATIONS.coerceAtLeast(1)) { + adjustBounds( + // set number of completed iterations + performedIterations = statisticsTracker.iteration + 1, + // total number of performed invocations, excluding warm-up invocations + performedInvocations = statisticsTracker.invocationsCount, + // remaining time; for simplicity we do not estimate and subtract warm-up time + remainingTimeNano = remainingTimeNano, + // as an estimated average invocation time we took average invocation time on previous iteration, + // excluding warm-up invocations + averageInvocationTimeNano = with(statisticsTracker.iterationsStatistics[statisticsTracker.iteration]) { + if (invocationsCount > 0) + averageInvocationTimeNano + else + // in case when no iterations, except warm-up iterations, were performed, + // take average time on all iterations (including warm-up) as an estimate + statisticsTracker.totalRunningTimeNano.toDouble() / statisticsTracker.totalInvocationsCount + }, + ) + } + return (iteration < iterationsBound) && (remainingTimeNano > 0) + } + + override fun shouldDoNextInvocation(invocation: Int): Boolean { + check(invocation == statisticsTracker.invocation + 1) + if (invocation == 0) { + statisticsTracker.iterationWarmUpStart(statisticsTracker.iteration) + } + if (invocation == WARM_UP_INVOCATIONS_COUNT) { + statisticsTracker.iterationWarmUpEnd(statisticsTracker.iteration) + } + if (statisticsTracker.totalRunningTimeNano > testingTimeNano + admissibleErrorTimeNano) { + return false + } + if (invocation < WARM_UP_INVOCATIONS_COUNT) { + return true + } + if (statisticsTracker.currentIterationRunningTimeNano > currentIterationUpperTimeNano) { + return false + } + return (invocation < invocationsBound + statisticsTracker.currentIterationWarmUpInvocationsCount) + } + + /* + * Adjustment of remaining iteration and invocation bounds. + * This function is called after each iteration in order to adjust iterations and invocations bounds. + * + * We aim to maintain the following ratio between number of iterations and invocations: + * C = A / I + * where + * - C is a ratio constant, + * - I is a number of iterations, + * - A is a number of invocations per iteration. + * + * Note that the number of performed invocations may vary for different iterations, + * thus for A we take average number of invocations per iteration. + * A = J / I + * where + * - J is the total number of invocations performed on all iterations. + * + * Therefore, we derive the following equation: + * C = J / I^2 + * + * The adjustment function takes as arguments: + * - K --- number of performed iterations so far; + * - P --- total number of performed invocations so far; + * - T --- estimated average invocation time; + * - R --- remaining time. + * and it computes: + * - N --- number of remaining iterations; + * - M --- invocations bound for the next iteration. + * + * We have that: + * - I = K + N + * - J = P + M * N + * Therefore, to find N and M, we have to solve the following system of equations: + * + * (1) (P + M * N) / (K + N)^2 = C + * (2) M * N = R / T + * + * (note that R / T is the number of remaining invocations). + * + * By performing a rewrite M * N = R / T in the equation (1) and then applying other simplifications, + * we arrive at the following quadratic equation for N: + * + * (1') C * N^2 + 2CK * N + (C * K^2 - P - R / T) = 0 + * + * This equation can have either 0, 1, or 2 solutions. + * If it has 0 positive solutions, we take N = 0. + * If it has 2 solutions, we take N to be the maximal one. + * + * Then using the found N we determine M using equation (2): + * M = R / (T * N). + * + */ + private fun adjustBounds( + performedIterations: Int, + performedInvocations: Int, + averageInvocationTimeNano: Double, + remainingTimeNano: Long + ) { + require(averageInvocationTimeNano > 0) + if (remainingTimeNano <= 0) + return + // estimate number of remaining invocations + val remainingInvocations = floor(remainingTimeNano / averageInvocationTimeNano) + // shorter name for invocations to iterations ratio constant + val ratio = INVOCATIONS_TO_ITERATIONS_RATIO.toDouble() + // calculate remaining iterations bound + var remainingIterations = solveQuadraticEquation( + a = ratio, + b = 2 * ratio * performedIterations, + c = ratio * performedIterations * performedIterations - (performedInvocations + remainingInvocations), + default = 0.0 + ).let { round(it).toInt() }.coerceAtLeast(0) + + // if there are some iterations left, derive invocations per iteration bound by + // dividing total remaining invocations number to the number of remaining iterations + if (remainingIterations > 0) { + invocationsBound = round(remainingInvocations / remainingIterations) + .toInt() + .roundUpTo(INVOCATIONS_FACTOR) + .coerceAtLeast(invocationsLowerBound) + .coerceAtMost(invocationsUpperBound) + } + + // if there is no remaining iterations, but there is still some time left + // (more time than admissible error), + // we still can try to perform one more iteration --- + // in case of overdue it will be just aborted when the time is up; + // this additional iteration helps us to prevent the case when we finish earlier and + // do not use all allocated testing time; + // we allocate all remaining invocations to this last iteration; + // however, because in some rare cases even single invocation can take significant time + // and thus surpass the deadline, we still perform additional check + // to see if there enough time to perform at least X of additional invocations. + if (remainingIterations == 0 && + remainingTimeNano > admissibleErrorTimeNano && + averageInvocationTimeNano * invocationsLowerBound < remainingTimeNano) { + invocationsBound = remainingInvocations.toInt() + remainingIterations += 1 + } + + // finally, set the iterations bound + iterationsBound = performedIterations + remainingIterations + + // calculate upper bound on running time for the next iteration + currentIterationUpperTimeNano = if (remainingIterations > 0) + round((remainingTimeNano * PLANNED_ITERATION_TIME_ERROR_FACTOR) / remainingIterations).toLong() + else 0L + } + + companion object { + // initial iterations upper bound + private const val INITIAL_ITERATIONS_BOUND = 30 + + // number of iterations added/subtracted when we over- or under-perform the plan + private const val ITERATIONS_DELTA = 5 + + // initial number of invocations + private const val INITIAL_INVOCATIONS_BOUND = 500 + + internal const val WARM_UP_ITERATIONS = 1 + + // number of warm-up invocations + private const val WARM_UP_INVOCATIONS_COUNT = 10 + + // number of invocations should be divisible to this constant, + // that is we ensure number of invocations is always rounded up to this constant + internal const val INVOCATIONS_FACTOR = 100 + + internal const val INVOCATIONS_TO_ITERATIONS_RATIO = 100 + + internal const val INVOCATIONS_LOWER_BOUND = 100 + internal const val STRESS_INVOCATIONS_UPPER_BOUND = 1_000_000 + internal const val MODEL_CHECKING_INVOCATIONS_UPPER_BOUND = 20_000 + + private const val PLANNED_ITERATION_TIME_ERROR_FACTOR = 2.0 + + // error up to 1.5 sec --- we can try to decrease the error in the future + internal const val TIME_ERROR_MARGIN_NANO = 1_500_000_000 + } + +} + +private fun solveQuadraticEquation(a: Double, b: Double, c: Double, default: Double): Double { + val d = (b * b - 4 * a * c) + return if (d >= 0) + max( + (-b + sqrt(d)) / (2 * a), + (-b - sqrt(d)) / (2 * a), + ) + else default +} + +private fun Double.roundUpTo(c: Double) = round(this / c) * c +private fun Int.roundUpTo(c: Int) = toDouble().roundUpTo(c.toDouble()).toInt() + +private fun Double.ceilUpTo(c: Double) = ceil(this / c) * c +private fun Int.ceilUpTo(c: Int) = toDouble().ceilUpTo(c.toDouble()).toInt() \ No newline at end of file diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/Reporter.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/Reporter.kt index 04d0e0d29..65c0da872 100644 --- a/src/jvm/main/org/jetbrains/kotlinx/lincheck/Reporter.kt +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/Reporter.kt @@ -21,11 +21,17 @@ class Reporter(private val logLevel: LoggingLevel) { private val out: PrintStream = System.out private val outErr: PrintStream = System.err - fun logIteration(iteration: Int, maxIterations: Int, scenario: ExecutionScenario) = log(INFO) { - appendLine("\n= Iteration $iteration / $maxIterations =") + fun logIteration(iteration: Int, scenario: ExecutionScenario) = log(INFO) { + appendLine("\n= Iteration $iteration =") appendExecutionScenario(scenario) } + fun logIterationStatistics(invocations: Int, runningTimeNano: Long, remainingTimeNano: Long?) = log(INFO) { + val runningTime = nanoTimeToString(runningTimeNano) + val remainingString = remainingTimeNano?.let { String.format(", remaining time ${nanoTimeToString(it)}s") } ?: "" + appendLine("= Statistics: #invocations=$invocations, running time ${runningTime}s${remainingString} =") + } + fun logFailedIteration(failure: LincheckFailure) = log(INFO) { appendFailure(failure) } @@ -35,7 +41,6 @@ class Reporter(private val logLevel: LoggingLevel) { appendExecutionScenario(scenario) } - private inline fun log(logLevel: LoggingLevel, crossinline msg: StringBuilder.() -> Unit): Unit = synchronized(this) { if (this.logLevel > logLevel) return val sb = StringBuilder() @@ -45,7 +50,7 @@ class Reporter(private val logLevel: LoggingLevel) { } } -@JvmField val DEFAULT_LOG_LEVEL = WARN +@JvmField val DEFAULT_LOG_LEVEL = INFO enum class LoggingLevel { INFO, WARN } @@ -561,8 +566,8 @@ private fun StringBuilder.appendHints(hints: List) { private fun StringBuilder.appendValidationFailure(failure: ValidationFailure): StringBuilder { appendLine("= Validation function ${failure.functionName} has failed =") appendExecutionScenario(failure.scenario) - appendln() - appendln() + appendLine() + appendLine() appendException(failure.exception) return this } @@ -580,3 +585,7 @@ private fun StringBuilder.appendException(t: Throwable) { } private const val EXCEPTIONS_TRACES_TITLE = "Exception stack traces:" + + +internal fun nanoTimeToString(timeNano: Long, decimalPlaces: Int = 3) = + String.format("%.${decimalPlaces}f", timeNano.toDouble() / 1_000_000_000) \ No newline at end of file diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/RunTracker.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/RunTracker.kt new file mode 100644 index 000000000..7259b2fad --- /dev/null +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/RunTracker.kt @@ -0,0 +1,149 @@ +/* + * Lincheck + * + * Copyright (C) 2019 - 2023 JetBrains s.r.o. + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU Lesser General Public License as + * published by the Free Software Foundation, either version 3 of the + * License, or (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Lesser Public License for more details. + * + * You should have received a copy of the GNU General Lesser Public + * License along with this program. If not, see + * + */ + +package org.jetbrains.kotlinx.lincheck + +import org.jetbrains.kotlinx.lincheck.execution.ExecutionScenario +import org.jetbrains.kotlinx.lincheck.strategy.LincheckFailure + +interface RunTracker { + fun runStart(name: String, options: LincheckOptions) {} + + fun runEnd( + name: String, + failure: LincheckFailure? = null, + exception: Throwable? = null, + statistics: Statistics? = null + ) {} + + fun iterationStart(iteration: Int, scenario: ExecutionScenario) {} + + fun iterationEnd( + iteration: Int, + failure: LincheckFailure? = null, + exception: Throwable? = null, + ) {} + + fun invocationStart(invocation: Int) {} + + fun invocationEnd( + invocation: Int, + failure: LincheckFailure? = null, + exception: Throwable? = null, + ) {} + +} + +inline fun RunTracker?.trackRun( + name: String, + options: LincheckOptions, + block: () -> Pair +): Pair { + var failure: LincheckFailure? = null + var exception: Throwable? = null + var statistics: Statistics? = null + this?.runStart(name, options) + try { + return block().also { + failure = it.first + statistics = it.second + } + } catch (throwable: Throwable) { + exception = throwable + throw throwable + } finally { + this?.runEnd(name, failure, exception, statistics) + } +} + +inline fun RunTracker?.trackIteration(iteration: Int, scenario: ExecutionScenario, block: () -> LincheckFailure?): LincheckFailure? { + var failure: LincheckFailure? = null + var exception: Throwable? = null + this?.iterationStart(iteration, scenario) + try { + return block().also { + failure = it + } + } catch (throwable: Throwable) { + exception = throwable + throw throwable + } finally { + this?.iterationEnd(iteration, failure, exception) + } +} + +inline fun RunTracker?.trackInvocation(invocation: Int, block: () -> LincheckFailure?): LincheckFailure? { + var failure: LincheckFailure? = null + var exception: Throwable? = null + this?.invocationStart(invocation) + try { + return block().also { + failure = it + } + } catch (throwable: Throwable) { + exception = throwable + throw throwable + } finally { + this?.invocationEnd(invocation, failure, exception) + } +} + +fun trackersList(trackers: List): RunTracker? = + if (trackers.isEmpty()) + null + else object : RunTracker { + + override fun runStart(name: String, options: LincheckOptions) { + for (tracker in trackers) { + tracker.runStart(name, options) + } + } + + override fun runEnd(name: String, failure: LincheckFailure?, exception: Throwable?, statistics: Statistics?) { + for (tracker in trackers) { + tracker.runEnd(name, failure, exception, statistics) + } + } + + override fun iterationStart(iteration: Int, scenario: ExecutionScenario) { + for (tracker in trackers) { + tracker.iterationStart(iteration, scenario) + } + } + + override fun iterationEnd(iteration: Int, failure: LincheckFailure?, exception: Throwable?) { + for (tracker in trackers) { + tracker.iterationEnd(iteration, failure, exception) + } + } + + override fun invocationStart(invocation: Int) { + for (tracker in trackers) { + tracker.invocationStart(invocation) + } + } + + override fun invocationEnd(invocation: Int, failure: LincheckFailure?, exception: Throwable?) { + for (tracker in trackers) { + tracker.invocationEnd(invocation, failure, exception) + } + } + + } \ No newline at end of file diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/Statistics.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/Statistics.kt new file mode 100644 index 000000000..232e5cfa6 --- /dev/null +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/Statistics.kt @@ -0,0 +1,209 @@ +/* + * Lincheck + * + * Copyright (C) 2019 - 2023 JetBrains s.r.o. + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU Lesser General Public License as + * published by the Free Software Foundation, either version 3 of the + * License, or (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Lesser Public License for more details. + * + * You should have received a copy of the GNU General Lesser Public + * License along with this program. If not, see + * + */ + +package org.jetbrains.kotlinx.lincheck + +import org.jetbrains.kotlinx.lincheck.execution.ExecutionScenario +import org.jetbrains.kotlinx.lincheck.strategy.LincheckFailure + +interface Statistics { + /** + * Total running time in nanoseconds, excluding warm-up time. + */ + val runningTimeNano: Long + /** + * A list of iteration statistics. + */ + val iterationsStatistics: List +} + +interface IterationStatistics { + /** + * Running time of this iteration in nanoseconds, excluding warm-up time. + */ + val runningTimeNano: Long + + /** + * Warm-up time of this iteration in nanoseconds. + */ + val warmUpTimeNano: Long + + /** + * Number of invocations performed on this iteration, excluding warm-up invocations. + */ + val invocationsCount: Int + + /** + * Number of warm-up invocations performed on this iteration. + */ + val warmUpInvocationsCount: Int +} + +/** + * Number of performed iterations. + */ +val Statistics.iterationsCount: Int + get() = iterationsStatistics.size + +/** + * Total running time, including warm-up time. + */ +val Statistics.totalRunningTimeNano: Long + get() = runningTimeNano + warmUpTimeNano + +/** + * Total warm-up time in nanoseconds, spent on all iterations. + */ +val Statistics.warmUpTimeNano: Long + get() = iterationsStatistics.sumOf { it.warmUpTimeNano } + +/** + * Number of invocations performed on all iterations. + */ +val Statistics.invocationsCount: Int + get() = iterationsStatistics.sumOf { it.invocationsCount } + +/** + * Total number of performed invocations, including warm-up invocations + */ +val Statistics.totalInvocationsCount: Int + get() = iterationsStatistics.sumOf { it.totalInvocationsCount } + +/** + * Average number of invocations performed by iteration. + */ +val Statistics.averageInvocationsCount: Double + get() = iterationsStatistics.map { it.invocationsCount }.average() + +/** + * The average invocation time (across all iterations) in nanoseconds. + */ +val Statistics.averageInvocationTimeNano + get() = runningTimeNano.toDouble() / invocationsCount + +/** + * Total running time of this iteration in nanoseconds, including warm-up time. + */ +val IterationStatistics.totalRunningTimeNano: Long + get() = runningTimeNano + warmUpTimeNano + +/** + * Total number of invocations performed on this iteration, including warm-up invocations. + */ +val IterationStatistics.totalInvocationsCount: Int + get() = invocationsCount + warmUpInvocationsCount + +/** + * Average invocation time on given iteration. + */ +val IterationStatistics.averageInvocationTimeNano + get() = runningTimeNano.toDouble() / invocationsCount + +internal class StatisticsTracker : Statistics, RunTracker { + + override var runningTimeNano: Long = 0 + private set + + override val iterationsStatistics: List + get() = _iterationsStatistics + private val _iterationsStatistics = mutableListOf() + + private class IterationStatisticsTracker : IterationStatistics { + override var runningTimeNano: Long = 0 + override var warmUpTimeNano: Long = 0 + override var invocationsCount: Int = 0 + override var warmUpInvocationsCount: Int = 0 + } + + /** + * Current iteration number. + */ + var iteration: Int = -1 + private set + + /** + * Current invocation number within current iteration. + */ + var invocation: Int = -1 + private set + + /** + * Running time of current iteration. + */ + val currentIterationRunningTimeNano: Long + get() = iterationsStatistics[iteration].runningTimeNano + + /** + * Number of invocations in current iteration. + */ + val currentIterationInvocationsCount: Int + get() = iterationsStatistics[iteration].invocationsCount + + val currentIterationWarmUpInvocationsCount: Int + get() = iterationsStatistics[iteration].warmUpInvocationsCount + + // flag indicating that next invocations should be considered warm-up + private var warmUpFlag: Boolean = false + + override fun iterationStart(iteration: Int, scenario: ExecutionScenario) { + check(iteration == this.iteration + 1) + ++this.iteration + _iterationsStatistics.add(IterationStatisticsTracker()) + warmUpFlag = false + } + + override fun iterationEnd(iteration: Int, failure: LincheckFailure?, exception: Throwable?) { + invocation = -1 + } + + private var lastInvocationStartTimeNano = -1L + + override fun invocationStart(invocation: Int) { + check(invocation == this.invocation + 1) + ++this.invocation + lastInvocationStartTimeNano = System.nanoTime() + } + + override fun invocationEnd(invocation: Int, failure: LincheckFailure?, exception: Throwable?) { + val invocationTimeNano = System.nanoTime() - lastInvocationStartTimeNano + check(invocationTimeNano >= 0) + if (warmUpFlag) { + _iterationsStatistics[iteration].warmUpTimeNano += invocationTimeNano + _iterationsStatistics[iteration].warmUpInvocationsCount += 1 + } else { + _iterationsStatistics[iteration].runningTimeNano += invocationTimeNano + _iterationsStatistics[iteration].invocationsCount += 1 + runningTimeNano += invocationTimeNano + } + } + + fun iterationWarmUpStart(iteration: Int) { + check(iteration == this.iteration) + check(iterationsStatistics[this.iteration].warmUpTimeNano == 0L) + warmUpFlag = true + } + + fun iterationWarmUpEnd(iteration: Int) { + check(iteration == this.iteration) + warmUpFlag = false + } + +} + diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/execution/ExecutionGenerator.java b/src/jvm/main/org/jetbrains/kotlinx/lincheck/execution/ExecutionGenerator.java index 04a8a1c36..a045a63e8 100644 --- a/src/jvm/main/org/jetbrains/kotlinx/lincheck/execution/ExecutionGenerator.java +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/execution/ExecutionGenerator.java @@ -21,11 +21,9 @@ * All implementations should have the same constructor as {@link ExecutionGenerator} has. */ public abstract class ExecutionGenerator { - protected final CTestConfiguration testConfiguration; protected final CTestStructure testStructure; - protected ExecutionGenerator(CTestConfiguration testConfiguration, CTestStructure testStructure) { - this.testConfiguration = testConfiguration; + protected ExecutionGenerator(CTestStructure testStructure) { this.testStructure = testStructure; } @@ -36,5 +34,8 @@ protected ExecutionGenerator(CTestConfiguration testConfiguration, CTestStructur * If the current test contains suspendable operations, the initial part of an execution * should not contain suspendable actors and the post part should be empty. */ - public abstract ExecutionScenario nextExecution(); + public abstract ExecutionScenario nextExecution( + int threads, int operationsPerThread, + int operationsInInitPart, int operationsInPostPart + ); } diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/execution/RandomExecutionGenerator.java b/src/jvm/main/org/jetbrains/kotlinx/lincheck/execution/RandomExecutionGenerator.java index 1267fe942..76a8a6795 100644 --- a/src/jvm/main/org/jetbrains/kotlinx/lincheck/execution/RandomExecutionGenerator.java +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/execution/RandomExecutionGenerator.java @@ -25,18 +25,21 @@ public class RandomExecutionGenerator extends ExecutionGenerator { private final Random random; - public RandomExecutionGenerator(CTestConfiguration testConfiguration, CTestStructure testStructure, RandomProvider randomProvider) { - super(testConfiguration, testStructure); + public RandomExecutionGenerator(CTestStructure testStructure, RandomProvider randomProvider) { + super(testStructure); random = randomProvider.createRandom(); } @Override - public ExecutionScenario nextExecution() { + public ExecutionScenario nextExecution( + int threads, int operationsPerThread, + int operationsInInitPart, int operationsInPostPart + ) { // Create init execution part List validActorGeneratorsForInit = testStructure.actorGenerators.stream() .filter(ag -> !ag.getUseOnce() && !ag.isSuspendable()).collect(Collectors.toList()); List initExecution = new ArrayList<>(); - for (int i = 0; i < testConfiguration.getActorsBefore() && !validActorGeneratorsForInit.isEmpty(); i++) { + for (int i = 0; i < operationsInInitPart && !validActorGeneratorsForInit.isEmpty(); i++) { ActorGenerator ag = validActorGeneratorsForInit.get(random.nextInt(validActorGeneratorsForInit.size())); initExecution.add(ag.generate(0, random)); } @@ -51,9 +54,9 @@ public ExecutionScenario nextExecution() { List> parallelExecution = new ArrayList<>(); List threadGens = new ArrayList<>(); - for (int t = 0; t < testConfiguration.getThreads(); t++) { + for (int t = 0; t < threads; t++) { parallelExecution.add(new ArrayList<>()); - threadGens.add(new ThreadGen(t, testConfiguration.getActorsPerThread())); + threadGens.add(new ThreadGen(t, operationsPerThread)); } for (int i = 0; i < nonParallelGroups.size(); i++) { threadGens.get(i % threadGens.size()).nonParallelActorGenerators @@ -89,9 +92,9 @@ public ExecutionScenario nextExecution() { List leftActorGenerators = new ArrayList<>(parallelGroup); for (ThreadGen threadGen : tgs2) leftActorGenerators.addAll(threadGen.nonParallelActorGenerators); - for (int i = 0; i < testConfiguration.getActorsAfter() && !leftActorGenerators.isEmpty(); i++) { + for (int i = 0; i < operationsInPostPart && !leftActorGenerators.isEmpty(); i++) { ActorGenerator agen = getActorGenFromGroup(leftActorGenerators, random.nextInt(leftActorGenerators.size())); - postExecution.add(agen.generate(testConfiguration.getThreads() + 1, random)); + postExecution.add(agen.generate(threads + 1, random)); } } else { postExecution = Collections.emptyList(); diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/Strategy.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/Strategy.kt index 558da9926..c8feac4c3 100644 --- a/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/Strategy.kt +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/Strategy.kt @@ -9,9 +9,13 @@ */ package org.jetbrains.kotlinx.lincheck.strategy -import org.jetbrains.kotlinx.lincheck.execution.ExecutionScenario -import org.jetbrains.kotlinx.lincheck.runner.ExecutionPart +import org.jetbrains.kotlinx.lincheck.* +import org.jetbrains.kotlinx.lincheck.execution.* +import org.jetbrains.kotlinx.lincheck.runner.* +import org.jetbrains.kotlinx.lincheck.strategy.managed.* +import org.jetbrains.kotlinx.lincheck.verifier.* import org.objectweb.asm.ClassVisitor +import java.io.Closeable /** * Implementation of this class describes how to run the generated execution. @@ -22,13 +26,60 @@ import org.objectweb.asm.ClassVisitor */ abstract class Strategy protected constructor( val scenario: ExecutionScenario -) { +) : Closeable { open fun needsTransformation() = false + open fun createTransformer(cv: ClassVisitor): ClassVisitor { throw UnsupportedOperationException("$javaClass strategy does not transform classes") } - abstract fun run(): LincheckFailure? + fun run(verifier: Verifier, planner: InvocationsPlanner, tracker: RunTracker? = null): LincheckFailure? { + var invocation = 0 + while (planner.shouldDoNextInvocation(invocation)) { + if (!nextInvocation()) { + return null + } + initializeInvocation() + tracker.trackInvocation(invocation) { runInvocation(verifier) } + ?.let { return it } + invocation++ + } + return null + } + + fun runInvocation(verifier: Verifier): LincheckFailure? = when (val result = runInvocation()) { + is CompletedInvocationResult -> + if (!verifier.verifyResults(scenario, result.results)) { + IncorrectResultsFailure(scenario, result.results, result.tryCollectTrace()) + } else null + else -> result.toLincheckFailure(scenario, result.tryCollectTrace()) + } + + /** + * Sets the internal state of strategy to run next invocation. + * + * @returns true if there is next invocation to run, false if all invocations have been studied. + */ + open fun nextInvocation(): Boolean = true + + /** + * Initializes the invocation. + * Should be called before each call to [runInvocation]. + */ + open fun initializeInvocation() {} + + /** + * Runs the current invocation and returns its result. + * For deterministic strategies, consecutive calls to [runInvocation] + * (without intervening [nextInvocation] calls) should run the same invocation, leading to the same results. + * + * Should be called after [initializeInvocation] and only if previous call to [nextInvocation] returned `true`. + */ + abstract fun runInvocation(): InvocationResult + + open fun InvocationResult.tryCollectTrace(): Trace? = null + + override fun close() {} open fun beforePart(part: ExecutionPart) {} diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/ManagedOptions.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/ManagedOptions.kt index 8e07bcae0..df76a7415 100644 --- a/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/ManagedOptions.kt +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/ManagedOptions.kt @@ -7,6 +7,8 @@ * 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/. */ +@file:Suppress("DEPRECATION_ERROR") + package org.jetbrains.kotlinx.lincheck.strategy.managed import org.jetbrains.kotlinx.lincheck.* @@ -20,6 +22,11 @@ import java.util.* /** * Common options for all managed strategies. */ +@Deprecated( + message="Please use `LincheckOptions` instead, which combines stress testing and model checking", + replaceWith=ReplaceWith("LincheckOptions"), + level=DeprecationLevel.ERROR, +) abstract class ManagedOptions, CTEST : CTestConfiguration> : Options() { protected var invocationsPerIteration = DEFAULT_INVOCATIONS protected var checkObstructionFreedom = DEFAULT_CHECK_OBSTRUCTION_FREEDOM diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/ManagedStrategy.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/ManagedStrategy.kt index c62badff5..7bcf735f2 100644 --- a/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/ManagedStrategy.kt +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/ManagedStrategy.kt @@ -33,10 +33,13 @@ import kotlin.collections.set abstract class ManagedStrategy( private val testClass: Class<*>, scenario: ExecutionScenario, - private val verifier: Verifier, private val validationFunctions: List, private val stateRepresentationFunction: Method?, - private val testCfg: ManagedCTestConfiguration + private val timeoutMs: Long, + private val checkObstructionFreedom: Boolean, + private val eliminateLocalObjects: Boolean, + private val hangingDetectionThreshold: Int, + private val guarantees: List, ) : Strategy(scenario), Closeable { // The number of parallel threads. protected val nThreads: Int = scenario.nThreads @@ -65,7 +68,7 @@ abstract class ManagedStrategy( // Ihe number of entered but not left (yet) blocks that should be ignored by the strategy analysis for each thread. private val ignoredSectionDepth = IntArray(nThreads) { 0 } // Detector of loops or hangs (i.e. active locks). - protected val loopDetector: LoopDetector = LoopDetector(testCfg.hangingDetectionThreshold) + protected val loopDetector: LoopDetector = LoopDetector(hangingDetectionThreshold) // Tracker of acquisitions and releases of monitors. private lateinit var monitorTracker: MonitorTracker @@ -111,13 +114,19 @@ abstract class ManagedStrategy( } private fun createRunner(): ManagedStrategyRunner = - ManagedStrategyRunner(this, testClass, validationFunctions, stateRepresentationFunction, testCfg.timeoutMs, UseClocks.ALWAYS) + ManagedStrategyRunner(this, + testClass, + validationFunctions, + stateRepresentationFunction, + timeoutMs, + UseClocks.ALWAYS + ) override fun createTransformer(cv: ClassVisitor): ClassVisitor = ManagedStrategyTransformer( cv = cv, tracePointConstructors = tracePointConstructors, - guarantees = testCfg.guarantees, - eliminateLocalObjects = testCfg.eliminateLocalObjects, + guarantees = guarantees, + eliminateLocalObjects = eliminateLocalObjects, collectStateRepresentation = collectStateRepresentation, constructTraceRepresentation = collectTrace, codeLocationIdProvider = codeLocationIdProvider @@ -126,17 +135,10 @@ abstract class ManagedStrategy( override fun needsTransformation(): Boolean = true fun useBytecodeCache(): Boolean = - !collectTrace && testCfg.eliminateLocalObjects && (testCfg.guarantees == ManagedCTestConfiguration.DEFAULT_GUARANTEES) - - override fun run(): LincheckFailure? = runImpl().also { close() } + !collectTrace && eliminateLocalObjects && (guarantees == ManagedCTestConfiguration.DEFAULT_GUARANTEES) // == STRATEGY INTERFACE METHODS == - /** - * This method implements the strategy logic. - */ - protected abstract fun runImpl(): LincheckFailure? - /** * This method is invoked before every thread context switch. * @param iThread current thread that is about to be switched @@ -157,9 +159,10 @@ abstract class ManagedStrategy( protected abstract fun chooseThread(iThread: Int): Int /** - * Returns all data to the initial state. + * Resets all internal data to the initial state and initialized next invocation to be run. */ - protected open fun initializeInvocation() { + override fun initializeInvocation() { + super.initializeInvocation() finished.fill(false) isSuspended.fill(false) currentActorId.fill(-1) @@ -172,25 +175,22 @@ abstract class ManagedStrategy( ManagedStrategyStateHolder.setState(runner.classLoader, this, testClass) } - // == BASIC STRATEGY METHODS == - /** - * Checks whether the [result] is a failing one or is [CompletedInvocationResult] - * but the verification fails, and return the corresponding failure. - * Returns `null` if the result is correct. + * Runs the next invocation with the same [scenario][ExecutionScenario]. */ - protected fun checkResult(result: InvocationResult): LincheckFailure? = when (result) { - is CompletedInvocationResult -> { - if (verifier.verifyResults(scenario, result.results)) null - else IncorrectResultsFailure(scenario, result.results, collectTrace(result)) - } - else -> result.toLincheckFailure(scenario, collectTrace(result)) + override fun runInvocation(): InvocationResult { + val result = runner.run() + // Has strategy already determined the invocation result? + suddenInvocationResult?.let { return it } + return result } + // == BASIC STRATEGY METHODS == + /** * Re-runs the last invocation to collect its trace. */ - private fun collectTrace(failingResult: InvocationResult): Trace? { + fun collectTrace(failingResult: InvocationResult): Trace? { val detectedByStrategy = suddenInvocationResult != null val canCollectTrace = when { detectedByStrategy -> true // ObstructionFreedomViolationInvocationResult or UnexpectedExceptionInvocationResult @@ -212,7 +212,7 @@ abstract class ManagedStrategy( runner = createRunner() ManagedStrategyStateHolder.setState(runner.classLoader, this, testClass) runner.initialize() - + initializeInvocation() loopDetector.enableReplayMode( failDueToDeadlockInTheEnd = failingResult is DeadlockInvocationResult || failingResult is ObstructionFreedomViolationInvocationResult ) @@ -232,19 +232,8 @@ abstract class ManagedStrategy( return Trace(traceCollector!!.trace) } - /** - * Runs the next invocation with the same [scenario][ExecutionScenario]. - */ - protected fun runInvocation(): InvocationResult { - initializeInvocation() - val result = runner.run() - // Has strategy already determined the invocation result? - suddenInvocationResult?.let { return it } - return result - } - private fun failIfObstructionFreedomIsRequired(lazyMessage: () -> String) { - if (testCfg.checkObstructionFreedom && !curActorIsBlocking && !concurrentActorCausesBlocking) { + if (checkObstructionFreedom && !curActorIsBlocking && !concurrentActorCausesBlocking) { suddenInvocationResult = ObstructionFreedomViolationInvocationResult(lazyMessage()) // Forcibly finish the current execution by throwing an exception. throw ForcibleExecutionFinishException @@ -256,7 +245,7 @@ abstract class ManagedStrategy( private val concurrentActorCausesBlocking: Boolean get() = currentActorId.mapIndexed { iThread, actorId -> - if (iThread != currentThread && !finished[iThread]) + if (iThread != currentThread && actorId >= 0 && !finished[iThread]) scenario.threads[iThread][actorId] else null }.filterNotNull().any { it.causesBlocking } diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/modelchecking/ModelCheckingCTest.java b/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/modelchecking/ModelCheckingCTest.java index eb826294c..2df6f745d 100644 --- a/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/modelchecking/ModelCheckingCTest.java +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/modelchecking/ModelCheckingCTest.java @@ -10,6 +10,7 @@ package org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking; import kotlin.Deprecated; +import kotlin.DeprecationLevel; import org.jetbrains.kotlinx.lincheck.*; import org.jetbrains.kotlinx.lincheck.annotations.Operation; import org.jetbrains.kotlinx.lincheck.execution.*; @@ -22,11 +23,17 @@ /** * This annotation configures concurrent test using {@link ModelCheckingStrategy managed} strategy. + * + * @deprecated use {@link LincheckOptions} instead. */ @Retention(RetentionPolicy.RUNTIME) @Target(ElementType.TYPE) @Repeatable(ModelCheckingCTest.ModelCheckingCTests.class) @Inherited +@Deprecated( + message = "Please use `LincheckOptions` instead", + level = DeprecationLevel.ERROR +) public @interface ModelCheckingCTest { /** * The number of different test scenarios to be executed diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/modelchecking/ModelCheckingCTestConfiguration.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/modelchecking/ModelCheckingCTestConfiguration.kt index 5df794002..ebaf877fe 100644 --- a/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/modelchecking/ModelCheckingCTestConfiguration.kt +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/modelchecking/ModelCheckingCTestConfiguration.kt @@ -9,6 +9,7 @@ */ package org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking +import org.jetbrains.kotlinx.lincheck.* import org.jetbrains.kotlinx.lincheck.execution.* import org.jetbrains.kotlinx.lincheck.strategy.* import org.jetbrains.kotlinx.lincheck.strategy.managed.* @@ -43,7 +44,10 @@ class ModelCheckingCTestConfiguration(testClass: Class<*>, iterations: Int, thre eliminateLocalObjects = eliminateLocalObjects, customScenarios = customScenarios ) { - override fun createStrategy(testClass: Class<*>, scenario: ExecutionScenario, validationFunctions: List, - stateRepresentationMethod: Method?, verifier: Verifier): Strategy - = ModelCheckingStrategy(this, testClass, scenario, validationFunctions, stateRepresentationMethod, verifier) + override fun createStrategy(testClass: Class<*>, scenario: ExecutionScenario, + validationFunctions: List, stateRepresentationMethod: Method?): Strategy = + ModelCheckingStrategy(testClass, scenario, + validationFunctions, stateRepresentationMethod, + timeoutMs, checkObstructionFreedom, eliminateLocalObjects, hangingDetectionThreshold, guarantees, + ) } diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/modelchecking/ModelCheckingOptions.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/modelchecking/ModelCheckingOptions.kt index 54cebd4ea..ab03515c2 100644 --- a/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/modelchecking/ModelCheckingOptions.kt +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/modelchecking/ModelCheckingOptions.kt @@ -15,6 +15,12 @@ import org.jetbrains.kotlinx.lincheck.strategy.managed.* /** * Options for [model checking][ModelCheckingStrategy] strategy. */ +@Deprecated( + message="Please use `LincheckOptions` instead, which combines stress testing and model checking", + replaceWith=ReplaceWith("LincheckOptions"), + level=DeprecationLevel.ERROR, +) +@Suppress("DEPRECATION_ERROR") class ModelCheckingOptions : ManagedOptions() { override fun createTestConfigurations(testClass: Class<*>): ModelCheckingCTestConfiguration { return ModelCheckingCTestConfiguration( diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/modelchecking/ModelCheckingStrategy.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/modelchecking/ModelCheckingStrategy.kt index 80f2f2894..d4a1baf55 100644 --- a/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/modelchecking/ModelCheckingStrategy.kt +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/modelchecking/ModelCheckingStrategy.kt @@ -9,6 +9,7 @@ */ package org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking +import org.jetbrains.kotlinx.lincheck.* import org.jetbrains.kotlinx.lincheck.execution.* import org.jetbrains.kotlinx.lincheck.runner.* import org.jetbrains.kotlinx.lincheck.strategy.* @@ -33,17 +34,24 @@ import kotlin.random.* * than the number of all possible interleavings on the current depth level. */ internal class ModelCheckingStrategy( - testCfg: ModelCheckingCTestConfiguration, - testClass: Class<*>, - scenario: ExecutionScenario, - validationFunctions: List, - stateRepresentation: Method?, - verifier: Verifier -) : ManagedStrategy(testClass, scenario, verifier, validationFunctions, stateRepresentation, testCfg) { - // The number of invocations that the strategy is eligible to use to search for an incorrect execution. - private val maxInvocations = testCfg.invocationsPerIteration - // The number of already used invocations. - private var usedInvocations = 0 + testClass: Class<*>, + scenario: ExecutionScenario, + validationFunctions: List, + stateRepresentationFunction: Method?, + timeoutMs: Long, + checkObstructionFreedom: Boolean, + eliminateLocalObjects: Boolean, + hangingDetectionThreshold: Int, + guarantees: List, +) : ManagedStrategy(testClass, scenario, + validationFunctions, + stateRepresentationFunction, + timeoutMs, + checkObstructionFreedom, + eliminateLocalObjects, + hangingDetectionThreshold, + guarantees, +) { // The maximum number of thread switch choices that strategy should perform // (increases when all the interleavings with the current depth are studied). private var maxNumberOfSwitches = 0 @@ -54,23 +62,19 @@ internal class ModelCheckingStrategy( // The interleaving that will be studied on the next invocation. private lateinit var currentInterleaving: Interleaving - override fun runImpl(): LincheckFailure? { - currentInterleaving = root.nextInterleaving() ?: return null - while (usedInvocations < maxInvocations) { - // run invocation and check its results - val invocationResult = runInvocation() - if (suddenInvocationResult is SpinCycleFoundAndReplayRequired) { - currentInterleaving.rollbackAfterSpinCycleFound() - continue - } - usedInvocations++ - checkResult(invocationResult)?.let { return it } - // get new unexplored interleaving - currentInterleaving = root.nextInterleaving() ?: break - } - return null + override fun nextInvocation(): Boolean { + currentInterleaving = root.nextInterleaving() + ?: return false + return true + } + + override fun initializeInvocation() { + super.initializeInvocation() + currentInterleaving.initialize() } + override fun InvocationResult.tryCollectTrace(): Trace? = collectTrace(this) + override fun onNewSwitch(iThread: Int, mustSwitch: Boolean) { if (mustSwitch) { // Create new execution position if this is a forced switch. @@ -89,11 +93,6 @@ internal class ModelCheckingStrategy( return currentInterleaving.isSwitchPosition() } - override fun initializeInvocation() { - currentInterleaving.initialize() - super.initializeInvocation() - } - override fun beforePart(part: ExecutionPart) { val nextThread = when (part) { ExecutionPart.INIT -> 0 diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/stress/StressCTest.java b/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/stress/StressCTest.java index efecc4d63..5876cefe7 100644 --- a/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/stress/StressCTest.java +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/stress/StressCTest.java @@ -10,7 +10,10 @@ package org.jetbrains.kotlinx.lincheck.strategy.stress; +import kotlin.Deprecated; +import kotlin.DeprecationLevel; import org.jetbrains.kotlinx.lincheck.CTestConfiguration; +import org.jetbrains.kotlinx.lincheck.LincheckOptions; import org.jetbrains.kotlinx.lincheck.annotations.Operation; import org.jetbrains.kotlinx.lincheck.execution.ExecutionGenerator; import org.jetbrains.kotlinx.lincheck.execution.ExecutionScenario; @@ -23,11 +26,17 @@ /** * This annotation configures concurrent test using stress strategy. + * + * @deprecated use {@link LincheckOptions} instead. */ @Retention(RetentionPolicy.RUNTIME) @Target(ElementType.TYPE) @Repeatable(StressCTest.StressCTests.class) @Inherited +@Deprecated( + message = "Please use `LincheckOptions` instead", + level = DeprecationLevel.ERROR +) public @interface StressCTest { /** * The number of different test scenarios to be executed diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/stress/StressCTestConfiguration.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/stress/StressCTestConfiguration.kt index d561d28d5..3f0d9608f 100644 --- a/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/stress/StressCTestConfiguration.kt +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/stress/StressCTestConfiguration.kt @@ -11,6 +11,7 @@ package org.jetbrains.kotlinx.lincheck.strategy.stress import org.jetbrains.kotlinx.lincheck.* import org.jetbrains.kotlinx.lincheck.execution.* +import org.jetbrains.kotlinx.lincheck.strategy.* import org.jetbrains.kotlinx.lincheck.verifier.* import java.lang.reflect.* @@ -36,9 +37,9 @@ class StressCTestConfiguration( timeoutMs = timeoutMs, customScenarios = customScenarios ) { - override fun createStrategy(testClass: Class<*>, scenario: ExecutionScenario, validationFunctions: List, - stateRepresentationMethod: Method?, verifier: Verifier) = - StressStrategy(this, testClass, scenario, validationFunctions, stateRepresentationMethod, verifier) + override fun createStrategy(testClass: Class<*>, scenario: ExecutionScenario, + validationFunctions: List, stateRepresentationMethod: Method?): Strategy = + StressStrategy(testClass, scenario, validationFunctions, stateRepresentationMethod, timeoutMs) companion object { const val DEFAULT_INVOCATIONS = 10000 diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/stress/StressOptions.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/stress/StressOptions.kt index 582b4c932..12bb8b5e3 100644 --- a/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/stress/StressOptions.kt +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/stress/StressOptions.kt @@ -9,12 +9,17 @@ */ package org.jetbrains.kotlinx.lincheck.strategy.stress -import org.jetbrains.kotlinx.lincheck.Options -import org.jetbrains.kotlinx.lincheck.chooseSequentialSpecification +import org.jetbrains.kotlinx.lincheck.* /** * Options for [stress][StressStrategy] strategy. */ +@Deprecated( + message="Please use LincheckOptions class instead, which implements automated strategy selection", + replaceWith=ReplaceWith("LincheckOptions"), + level=DeprecationLevel.ERROR, +) +@Suppress("DEPRECATION_ERROR") open class StressOptions : Options() { private var invocationsPerIteration = StressCTestConfiguration.DEFAULT_INVOCATIONS diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/stress/StressStrategy.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/stress/StressStrategy.kt index 1f8bf0cf9..0c600f1de 100644 --- a/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/stress/StressStrategy.kt +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/stress/StressStrategy.kt @@ -9,22 +9,22 @@ */ package org.jetbrains.kotlinx.lincheck.strategy.stress +import org.jetbrains.kotlinx.lincheck.* import org.jetbrains.kotlinx.lincheck.execution.* import org.jetbrains.kotlinx.lincheck.runner.* import org.jetbrains.kotlinx.lincheck.strategy.* +import org.jetbrains.kotlinx.lincheck.strategy.managed.* import org.jetbrains.kotlinx.lincheck.verifier.* import java.lang.reflect.* -class StressStrategy( - testCfg: StressCTestConfiguration, +internal class StressStrategy( testClass: Class<*>, scenario: ExecutionScenario, validationFunctions: List, stateRepresentationFunction: Method?, - private val verifier: Verifier + timeoutMs: Long, ) : Strategy(scenario) { - private val invocations = testCfg.invocationsPerIteration - private val runner: Runner + private val runner: ParallelThreadsRunner init { runner = ParallelThreadsRunner( @@ -32,7 +32,7 @@ class StressStrategy( testClass = testClass, validationFunctions = validationFunctions, stateRepresentationFunction = stateRepresentationFunction, - timeoutMs = testCfg.timeoutMs, + timeoutMs = timeoutMs, useClocks = UseClocks.RANDOM ) try { @@ -43,19 +43,13 @@ class StressStrategy( } } - override fun run(): LincheckFailure? { - runner.use { - // Run invocations - for (invocation in 0 until invocations) { - when (val ir = runner.run()) { - is CompletedInvocationResult -> { - if (!verifier.verifyResults(scenario, ir.results)) - return IncorrectResultsFailure(scenario, ir.results) - } - else -> return ir.toLincheckFailure(scenario) - } - } - return null - } + override fun runInvocation(): InvocationResult { + return runner.run() + } + + override fun InvocationResult.tryCollectTrace(): Trace? = null + + override fun close() { + runner.close() } } \ No newline at end of file diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/AbstractLincheckTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/AbstractLincheckTest.kt index c213cb5ce..badcf6bd4 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/AbstractLincheckTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/AbstractLincheckTest.kt @@ -11,25 +11,46 @@ package org.jetbrains.kotlinx.lincheck_test import org.jetbrains.kotlinx.lincheck.* import org.jetbrains.kotlinx.lincheck.strategy.* -import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.ModelCheckingOptions -import org.jetbrains.kotlinx.lincheck.strategy.stress.* -import org.jetbrains.kotlinx.lincheck.verifier.* -import org.jetbrains.kotlinx.lincheck_test.util.* +import org.jetbrains.kotlinx.lincheck.verifier.VerifierState import org.junit.* +import kotlin.math.* import kotlin.reflect.* +import org.jetbrains.kotlinx.lincheck_test.util.* abstract class AbstractLincheckTest( - private vararg val expectedFailures: KClass + private vararg val expectedFailures: KClass, ) : VerifierState() { - open fun > O.customize() {} - override fun extractState(): Any = System.identityHashCode(this) - private fun > O.runInternalTest() { - val failure: LincheckFailure? = checkImpl(this@AbstractLincheckTest::class.java) - if (failure === null) { + @Test(timeout = TIMEOUT) + fun testWithStressStrategy(): Unit = LincheckOptions { + this as LincheckOptionsImpl + mode = LincheckMode.Stress + configure() + }.runTest() + + @Test(timeout = TIMEOUT) + fun testWithModelCheckingStrategy(): Unit = LincheckOptions { + this as LincheckOptionsImpl + mode = LincheckMode.ModelChecking + configure() + }.runTest() + + @Test(timeout = TIMEOUT) + fun testWithHybridStrategy(): Unit = LincheckOptions { + this as LincheckOptionsImpl + mode = LincheckMode.Hybrid + configure() + }.runTest() + + private fun LincheckOptions.runTest() { + val failure = runTests(this@AbstractLincheckTest::class.java, tracker = runTracker) + if (failure == null) { assert(expectedFailures.isEmpty()) { "This test should fail, but no error has been occurred (see the logs for details)" } + if (testPlanningConstraints) { + checkAdaptivePlanningConstraints() + } } else { failure.trace?.let { checkTraceHasNoLincheckEvents(it.toString()) } assert(expectedFailures.contains(failure::class)) { @@ -38,29 +59,69 @@ abstract class AbstractLincheckTest( } } - @Test(timeout = TIMEOUT) - fun testWithStressStrategy(): Unit = StressOptions().run { - invocationsPerIteration(5_000) - commonConfiguration() - runInternalTest() + private fun LincheckOptions.checkAdaptivePlanningConstraints() { + this as LincheckOptionsImpl + // if we tested only custom scenarios, then return + if (!generateRandomScenarios) + return + // we expect test to run only custom or only random scenarios + check(customScenariosOptions.size == 0) + val randomTestingTimeNano = testingTimeInSeconds * 1_000_000_000 + val runningTimeNano = runStatistics.values.sumOf { it.totalRunningTimeNano } + val timeDeltaNano = AdaptivePlanner.TIME_ERROR_MARGIN_NANO + // check that the actual running time is close to specified time + assert(abs(randomTestingTimeNano - runningTimeNano) < timeDeltaNano) { """ + Testing time is beyond expected bounds: + actual: ${String.format("%.3f", runningTimeNano.toDouble() / 1_000_000_000)} + expected: ${String.format("%.3f", randomTestingTimeNano.toDouble() / 1_000_000_000)} + """.trimIndent() + } + // check invocations to iterations ratio (per each strategy run) + for ((runName, statistics) in runStatistics.entries) { + if (statistics.iterationsStatistics.isEmpty()) + return + val invocationsRatio = statistics.averageInvocationsCount / statistics.iterationsCount + val expectedRatio = AdaptivePlanner.INVOCATIONS_TO_ITERATIONS_RATIO.toDouble() + val ratioError = 0.30 + assert(abs(invocationsRatio - expectedRatio) < expectedRatio * ratioError) { """ + Invocations to iterations ratio differs from expected. + actual: ${String.format("%.3f", invocationsRatio)} + expected: $expectedRatio + run name: $runName + """.trimIndent() + } + } } - @Test(timeout = TIMEOUT) - fun testWithModelCheckingStrategy(): Unit = ModelCheckingOptions().run { - invocationsPerIteration(1_000) - commonConfiguration() - runInternalTest() + private fun LincheckOptionsImpl.configure() { + testingTimeInSeconds = 10 + maxThreads = 3 + maxOperationsInThread = 2 + minimizeFailedScenario = false + customize() } - private fun > O.commonConfiguration(): Unit = run { - iterations(30) - actorsBefore(2) - threads(3) - actorsPerThread(2) - actorsAfter(2) - minimizeFailedScenario(false) - customize() + internal open fun LincheckOptionsImpl.customize() {} + + internal open val testPlanningConstraints: Boolean = true + + override fun extractState(): Any = System.identityHashCode(this) + + private val runOptions = mutableMapOf() + private val runStatistics = mutableMapOf() + + private val runTracker = object : RunTracker { + + override fun runStart(name: String, options: LincheckOptions) { + runOptions[name] = options + } + + override fun runEnd(name: String, failure: LincheckFailure?, exception: Throwable?, statistics: Statistics?) { + check(statistics != null) + runStatistics[name] = statistics + } } + } private const val TIMEOUT = 100_000L \ No newline at end of file diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/AddCustomScenarioTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/AddCustomScenarioTest.kt index 15a128540..3dc76d33d 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/AddCustomScenarioTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/AddCustomScenarioTest.kt @@ -12,7 +12,6 @@ package org.jetbrains.kotlinx.lincheck_test import org.jetbrains.kotlinx.lincheck.* import org.jetbrains.kotlinx.lincheck.strategy.* -import org.jetbrains.kotlinx.lincheck.strategy.stress.* import org.junit.* class AddCustomScenarioTest { @@ -31,29 +30,31 @@ class AddCustomScenarioTest { @Test fun stressTest1() { - val failure = StressOptions() - .iterations(0) - .addCustomScenario(scenario { + val failure = LincheckOptions { + this as LincheckOptionsImpl + generateRandomScenarios = false + addCustomScenario { parallel { thread { actor(::t1) } thread { actor(::t2) } } - }) - .checkImpl(this::class.java) + } + }.checkImpl(this::class.java) assert(failure is IncorrectResultsFailure) } @Test fun stressTest2() { - val failure = StressOptions() - .iterations(0) - .addCustomScenario { + val failure = LincheckOptions { + this as LincheckOptionsImpl + generateRandomScenarios = false + addCustomScenario { parallel { thread { actor(::t1) } thread { actor(::t2) } } } - .checkImpl(this::class.java) + }.checkImpl(this::class.java) assert(failure is IncorrectResultsFailure) } } \ No newline at end of file diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/AlmostEmptyScenarioTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/AlmostEmptyScenarioTest.kt index 9627115bd..775163155 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/AlmostEmptyScenarioTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/AlmostEmptyScenarioTest.kt @@ -12,11 +12,12 @@ package org.jetbrains.kotlinx.lincheck_test import org.jetbrains.kotlinx.lincheck.LinChecker import org.jetbrains.kotlinx.lincheck.LincheckAssertionError import org.jetbrains.kotlinx.lincheck.annotations.Operation -import org.jetbrains.kotlinx.lincheck.strategy.stress.StressCTest +import org.jetbrains.kotlinx.lincheck.strategy.stress.* import org.junit.Assert.* import org.junit.Test import java.util.concurrent.ThreadLocalRandom +@Suppress("DEPRECATION_ERROR") @StressCTest(iterations = 1, requireStateEquivalenceImplCheck = false, actorsBefore = 1, actorsAfter = 1, threads = 3) class AlmostEmptyScenarioTest { @Operation(runOnce = true) diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/BlockingBehaviourTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/BlockingBehaviourTest.kt index f45099a34..d78d2d43e 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/BlockingBehaviourTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/BlockingBehaviourTest.kt @@ -22,12 +22,15 @@ class BlockingOperationTest { fun blocking(): Unit = synchronized(this) {} @Test - fun test() = ModelCheckingOptions() - .checkObstructionFreedom() - .verifier(EpsilonVerifier::class.java) - .actorsBefore(0) - .actorsAfter(0) - .check(this::class) + fun test() = LincheckOptions { + (this as LincheckOptionsImpl) + mode = LincheckMode.ModelChecking + testingTimeInSeconds = 1 + verifier = EpsilonVerifier::class.java + checkObstructionFreedom = true + generateBeforeAndAfterParts = false + }.check(this::class) + } class CausesBlockingOperationTest { @@ -45,11 +48,11 @@ class CausesBlockingOperationTest { } @Test - fun test() = ModelCheckingOptions() - .checkObstructionFreedom() - .verifier(EpsilonVerifier::class.java) - .iterations(20) - .actorsBefore(0) - .actorsAfter(0) - .check(this::class) + fun test() = LincheckOptions { + (this as LincheckOptionsImpl) + mode = LincheckMode.ModelChecking + verifier = EpsilonVerifier::class.java + checkObstructionFreedom = true + generateBeforeAndAfterParts = false + }.check(this::class) } \ No newline at end of file diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/ExceptionTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/ExceptionTest.kt index 292748ac7..bbb39a676 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/ExceptionTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/ExceptionTest.kt @@ -21,22 +21,19 @@ class ExceptionInParallelPartTest : AbstractLincheckTest(IncorrectResultsFailure throw IllegalStateException() } - val scenario = scenario { - parallel { - thread { - actor(::exception) - } - thread { - actor(::exception) + override fun LincheckOptionsImpl.customize() { + addCustomScenario { + parallel { + thread { + actor(::exception) + } + thread { + actor(::exception) + } } } - } - - override fun > O.customize() { - iterations(0) - addCustomScenario(scenario) - minimizeFailedScenario(false) - sequentialSpecification(ExceptionTestSequentialImplementation::class.java) + generateRandomScenarios = false + sequentialImplementation = ExceptionTestSequentialImplementation::class.java } } @@ -51,22 +48,19 @@ class ExceptionInInitPartTest : AbstractLincheckTest(IncorrectResultsFailure::cl @Operation fun idle() {} - val scenario = scenario { - initial { - actor(ExceptionInInitPartTest::exception) - } - parallel { - thread { - actor(ExceptionInInitPartTest::idle) + override fun LincheckOptionsImpl.customize() { + addCustomScenario { + initial { + actor(ExceptionInInitPartTest::exception) + } + parallel { + thread { + actor(ExceptionInInitPartTest::idle) + } } } - } - - override fun > O.customize() { - iterations(0) - addCustomScenario(scenario) - minimizeFailedScenario(false) - sequentialSpecification(ExceptionTestSequentialImplementation::class.java) + generateRandomScenarios = false + sequentialImplementation = ExceptionTestSequentialImplementation::class.java } } @@ -81,22 +75,19 @@ class ExceptionInPostPartTest : AbstractLincheckTest(IncorrectResultsFailure::cl @Operation fun idle() {} - val scenario = scenario { - parallel { - thread { - actor(ExceptionInPostPartTest::idle) + override fun LincheckOptionsImpl.customize() { + addCustomScenario { + parallel { + thread { + actor(ExceptionInPostPartTest::idle) + } + } + post { + actor(ExceptionInPostPartTest::exception) } } - post { - actor(ExceptionInPostPartTest::exception) - } - } - - override fun > O.customize() { - iterations(0) - addCustomScenario(scenario) - minimizeFailedScenario(false) - sequentialSpecification(ExceptionTestSequentialImplementation::class.java) + generateRandomScenarios = false + sequentialImplementation = ExceptionTestSequentialImplementation::class.java } } diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/FailedScenarioMinimizationTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/FailedScenarioMinimizationTest.kt new file mode 100644 index 000000000..e69de29bb diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/HangingDetectionTests.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/HangingDetectionTests.kt index fc2eb1e89..5b49278da 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/HangingDetectionTests.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/HangingDetectionTests.kt @@ -12,6 +12,7 @@ package org.jetbrains.kotlinx.lincheck_test import org.jetbrains.kotlinx.lincheck.* import org.jetbrains.kotlinx.lincheck.annotations.* import org.jetbrains.kotlinx.lincheck.strategy.* +import org.jetbrains.kotlinx.lincheck.verifier.EpsilonVerifier class HangingInParallelPartTest : AbstractLincheckTest(DeadlockWithDumpFailure::class) { @@ -20,22 +21,19 @@ class HangingInParallelPartTest : AbstractLincheckTest(DeadlockWithDumpFailure:: while (true) {} } - val scenario = scenario { - parallel { - thread { - actor(::hang) - } - thread { - actor(::hang) + override fun LincheckOptionsImpl.customize() { + addCustomScenario { + parallel { + thread { + actor(::hang) + } + thread { + actor(::hang) + } } } - } - - override fun > O.customize() { - addCustomScenario(scenario) - iterations(0) - minimizeFailedScenario(false) - invocationTimeout(100) + generateRandomScenarios = false + invocationTimeoutMs = 100 } } @@ -50,22 +48,19 @@ class HangingInInitPartTest : AbstractLincheckTest(DeadlockWithDumpFailure::clas @Operation fun idle() {} - val scenario = scenario { - initial { - actor(::hang) - } - parallel { - thread { - actor(::idle) + override fun LincheckOptionsImpl.customize() { + addCustomScenario { + initial { + actor(::hang) + } + parallel { + thread { + actor(::idle) + } } } - } - - override fun > O.customize() { - addCustomScenario(scenario) - iterations(0) - minimizeFailedScenario(false) - invocationTimeout(100) + generateRandomScenarios = false + invocationTimeoutMs = 100 } } @@ -80,22 +75,21 @@ class HangingInPostPartTest : AbstractLincheckTest(DeadlockWithDumpFailure::clas @Operation fun idle() {} - val scenario = scenario { - parallel { - thread { - actor(::idle) + override fun LincheckOptionsImpl.customize() { + addCustomScenario { + parallel { + thread { + actor(::idle) + } + } + post { + actor(::hang) } } - post { - actor(::hang) - } + generateRandomScenarios = false + invocationTimeoutMs = 100 } - override fun > O.customize() { - addCustomScenario(scenario) - iterations(0) - minimizeFailedScenario(false) - invocationTimeout(100) - } + override fun extractState(): Any = System.identityHashCode(this) } \ No newline at end of file diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/IncorrectOnCancellationTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/IncorrectOnCancellationTest.kt index 7417e5191..2f5b7016a 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/IncorrectOnCancellationTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/IncorrectOnCancellationTest.kt @@ -33,4 +33,6 @@ class IncorrectOnCancellationTest : AbstractLincheckTest(IncorrectResultsFailure } override fun extractState(): Any = 0 // constant state + + override val testPlanningConstraints: Boolean = false } \ No newline at end of file diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/OperationsInAbstractClassTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/OperationsInAbstractClassTest.kt index 1e2ed0bbf..c19566bea 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/OperationsInAbstractClassTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/OperationsInAbstractClassTest.kt @@ -16,13 +16,18 @@ import org.junit.* import java.lang.AssertionError import kotlin.random.* -@StressCTest(iterations = 1, minimizeFailedScenario = false, requireStateEquivalenceImplCheck = false) class OperationsInAbstractClassTest : AbstractTestClass() { @Operation fun goodOperation() = 10 @Test(expected = AssertionError::class) - fun test(): Unit = LinChecker.check(this::class.java) + fun test(): Unit = LincheckOptions { + this as LincheckOptionsImpl + mode = LincheckMode.Stress + testingTimeInSeconds = 1 + minimizeFailedScenario = false + tryReproduceTrace = false + }.check(this::class.java) } open class AbstractTestClass { diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/PromptCancellationTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/PromptCancellationTest.kt index 5476b268b..cb5da57ed 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/PromptCancellationTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/PromptCancellationTest.kt @@ -14,7 +14,6 @@ import kotlinx.atomicfu.* import kotlinx.coroutines.* import org.jetbrains.kotlinx.lincheck.* import org.jetbrains.kotlinx.lincheck.annotations.* -import org.jetbrains.kotlinx.lincheck.annotations.Operation import org.jetbrains.kotlinx.lincheck.paramgen.* import org.jetbrains.kotlinx.lincheck.strategy.* import kotlin.coroutines.* @@ -64,13 +63,13 @@ abstract class AbstractPromptCancellationTest( return returnResult } - override fun > O.customize() { - actorsBefore(0) - threads(2) - actorsPerThread(1) - actorsAfter(0) - sequentialSpecification?.let { sequentialSpecification(it.java) } + override fun LincheckOptionsImpl.customize() { + this@AbstractPromptCancellationTest.sequentialSpecification?.let { + sequentialImplementation = it.java + } } + + override val testPlanningConstraints: Boolean = false } class CorrectPromptCancellationTest : AbstractPromptCancellationTest() diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/ThreadIdTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/ThreadIdTest.kt index 4b8d640f4..f040b0b37 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/ThreadIdTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/ThreadIdTest.kt @@ -30,4 +30,6 @@ class ThreadIdTest : AbstractLincheckTest() { } override fun extractState() = balances.toList() to counter.value + + override val testPlanningConstraints: Boolean = false } diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/UnexpectedExceptionInCancellationHandlerTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/UnexpectedExceptionInCancellationHandlerTest.kt index 2326ce9a7..23e2a0804 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/UnexpectedExceptionInCancellationHandlerTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/UnexpectedExceptionInCancellationHandlerTest.kt @@ -24,14 +24,14 @@ class UnexpectedExceptionInCancellationHandlerTest: AbstractLincheckTest(Unexpec } } - override fun > O.customize() { - iterations(100) - actorsBefore(0) - actorsAfter(0) - threads(1) - actorsPerThread(1) - sequentialSpecification(UnexpectedExceptionInCancellationHandlerTestSequential::class.java) + override fun LincheckOptionsImpl.customize() { + maxThreads = 1 + maxOperationsInThread = 1 + generateBeforeAndAfterParts = false + sequentialImplementation = UnexpectedExceptionInCancellationHandlerTestSequential::class.java } + + override val testPlanningConstraints: Boolean = false } class UnexpectedExceptionInCancellationHandlerTestSequential() { diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/UnexpectedExceptionTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/UnexpectedExceptionTest.kt index c974c0dcb..094f0b160 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/UnexpectedExceptionTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/UnexpectedExceptionTest.kt @@ -30,6 +30,8 @@ class UnexpectedExceptionTest : AbstractLincheckTest(UnexpectedExceptionFailure: } override fun extractState(): Any = canEnterForbiddenSection + + override val testPlanningConstraints: Boolean = false } class CoroutineResumedWithUnexpectedExceptionTest : AbstractLincheckTest(UnexpectedExceptionFailure::class) { @@ -42,4 +44,6 @@ class CoroutineResumedWithUnexpectedExceptionTest : AbstractLincheckTest(Unexpec } override fun extractState(): Any = 0 // constant state + + override val testPlanningConstraints: Boolean = false } diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/generator/ParamGeneratorsTests.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/generator/ParamGeneratorsTests.kt index 902cf1580..946fe9ee4 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/generator/ParamGeneratorsTests.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/generator/ParamGeneratorsTests.kt @@ -11,14 +11,13 @@ package org.jetbrains.kotlinx.lincheck_test.generator -import junit.framework.Assert.assertTrue import org.jetbrains.kotlinx.lincheck.* 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.paramgen.StringGen -import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.ModelCheckingOptions import org.junit.Test +import junit.framework.Assert.assertTrue import org.jetbrains.kotlinx.lincheck.paramgen.* import org.jetbrains.kotlinx.lincheck_test.verifier.linearizability.SpinLockBasedSet import org.junit.Assert.* @@ -42,7 +41,10 @@ class GeneratorSeedTest { } @Test(expected = LincheckAssertionError::class) - fun test() = ModelCheckingOptions().check(this::class) + fun test() = LincheckOptions { + this as LincheckOptionsImpl + mode = LincheckMode.ModelChecking + }.check(this::class) } @@ -56,7 +58,10 @@ class MethodParameterGenerationTestWithBothParametersAnnotated { throwInternalExceptionIfParamsNotEquals(first, second) @Test(expected = LincheckAssertionError::class) - fun test() = ModelCheckingOptions().check(this::class) + fun test() = LincheckOptions { + this as LincheckOptionsImpl + mode = LincheckMode.ModelChecking + }.check(this::class) } @@ -71,7 +76,10 @@ class MethodParameterGenerationTestWithFirstParameterAnnotated { fun operation(@Param(name = "key") first: Int, second: Int) = throwInternalExceptionIfParamsNotEquals(first, second) @Test(expected = LincheckAssertionError::class) - fun test() = ModelCheckingOptions().check(this::class) + fun test() = LincheckOptions { + this as LincheckOptionsImpl + mode = LincheckMode.ModelChecking + }.check(this::class) } @@ -85,7 +93,10 @@ class MethodParameterGenerationTestWithSecondParameterAnnotated { fun operation(first: Int, @Param(name = "key") second: Int) = throwInternalExceptionIfParamsNotEquals(first, second) @Test(expected = LincheckAssertionError::class) - fun test() = ModelCheckingOptions().check(this::class) + fun test() = LincheckOptions { + this as LincheckOptionsImpl + mode = LincheckMode.ModelChecking + }.check(this::class) } @@ -97,7 +108,10 @@ class MethodParameterGenerationTest { fun operation(first: Int, second: Int) = throwInternalExceptionIfParamsNotEquals(first, second) @Test(expected = LincheckAssertionError::class) - fun test() = ModelCheckingOptions().check(this::class) + fun test() = LincheckOptions { + this as LincheckOptionsImpl + mode = LincheckMode.ModelChecking + }.check(this::class) } @@ -147,11 +161,12 @@ class ParamGeneratorResetBetweenScenariosTest { @Test fun test() { - ModelCheckingOptions() - .threads(2) - .actorsPerThread(5) - .iterations(30) - .check(this::class) + LincheckOptions { + this as LincheckOptionsImpl + mode = LincheckMode.ModelChecking + maxThreads = 2 + maxOperationsInThread = 5 + }.check(this::class) } @Operation @@ -240,10 +255,12 @@ class NamedEnumParamGeneratorTest { } @Test(expected = LincheckAssertionError::class) - fun test() = ModelCheckingOptions() - .checkObstructionFreedom(true) - .minimizeFailedScenario(false) - .check(this::class) + fun test() = LincheckOptions { + this as LincheckOptionsImpl + mode = LincheckMode.ModelChecking + checkObstructionFreedom = true + minimizeFailedScenario = false + }.check(this::class) enum class OperationType { ADD, @@ -269,10 +286,12 @@ class UnnamedEnumParamGeneratorTest() { } @Test(expected = LincheckAssertionError::class) - fun test() = ModelCheckingOptions() - .checkObstructionFreedom(true) - .minimizeFailedScenario(false) - .check(this::class) + fun test() = LincheckOptions { + this as LincheckOptionsImpl + mode = LincheckMode.ModelChecking + checkObstructionFreedom = true + minimizeFailedScenario = false + }.check(this::class) enum class OperationType { ADD, @@ -293,10 +312,12 @@ class EnumParamWithoutAnnotationGeneratorTest: BaseEnumSetTest() { } @Test(expected = LincheckAssertionError::class) - fun test() = ModelCheckingOptions() - .checkObstructionFreedom(true) - .minimizeFailedScenario(false) - .check(this::class) + fun test() = LincheckOptions { + this as LincheckOptionsImpl + mode = LincheckMode.ModelChecking + checkObstructionFreedom = true + minimizeFailedScenario = false + }.check(this::class) } abstract class BaseEnumSetTest { @@ -327,7 +348,9 @@ class MultipleTypesAssociatedWithNamedEnumParameterGeneratorTest { @Test fun test() { - val exception = assertThrows(IllegalStateException::class.java) { ModelCheckingOptions().check(this::class) } + val exception = assertThrows(IllegalStateException::class.java) { + LincheckOptions().check(this::class) + } assertEquals( "Enum param gen with name type can't be associated with two different types: FirstEnum and SecondEnum", exception.message @@ -349,7 +372,10 @@ class EnumsWithWhitespacesInNameConfigurationTest { @Operation fun operation(@Param(name = "type") param: WeirdEnum) = 0 @Test - fun test() = ModelCheckingOptions().check(this::class) + fun test() = LincheckOptions { + this as LincheckOptionsImpl + mode = LincheckMode.ModelChecking + }.check(this::class) enum class WeirdEnum { `FIRST OPTION`, diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/guide/BasicCounterTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/guide/BasicCounterTest.kt index 0bc49478e..d549d926d 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/guide/BasicCounterTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/guide/BasicCounterTest.kt @@ -36,9 +36,5 @@ class BasicCounterTest { //@Test // TODO: Please, uncomment me and comment the line below to run the test and get the output @Test(expected = AssertionError::class) - fun stressTest() = StressOptions().check(this::class) // the magic button - - //@Test // TODO: Please, uncomment me and comment the line below to run the test and get the output - @Test(expected = AssertionError::class) - fun modelCheckingTest() = ModelCheckingOptions().check(this::class) + fun lincheckTest() = LincheckOptions().check(this::class) // the magic button } \ No newline at end of file diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/guide/ConcurrentLinkedDequeTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/guide/ConcurrentLinkedDequeTest.kt index 812a5e4b5..03961d30e 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/guide/ConcurrentLinkedDequeTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/guide/ConcurrentLinkedDequeTest.kt @@ -39,5 +39,7 @@ class ConcurrentLinkedDequeTest { //@Test // TODO: Please, uncomment me and comment the line below to run the test and get the output @Test(expected = AssertionError::class) - fun modelCheckingTest() = ModelCheckingOptions().check(this::class) + fun lincheckTest() = LincheckOptions { + testingTimeInSeconds = 30 + }.check(this::class) } diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/guide/ConcurrentLinkedQueueTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/guide/ConcurrentLinkedQueueTest.kt index cd4c06fd7..ce08a41e6 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/guide/ConcurrentLinkedQueueTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/guide/ConcurrentLinkedQueueTest.kt @@ -27,9 +27,9 @@ class ConcurrentLinkedQueueTest { fun poll(): Int? = s.poll() @Test - fun stressTest() = StressOptions() - .sequentialSpecification(SequentialQueue::class.java) - .check(this::class) + fun lincheckTest() = LincheckOptions { + sequentialImplementation = SequentialQueue::class.java + }.check(this::class) } class SequentialQueue { diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/guide/ConcurrentMapTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/guide/ConcurrentMapTest.kt index 2fb3c2337..1d3714005 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/guide/ConcurrentMapTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/guide/ConcurrentMapTest.kt @@ -12,7 +12,6 @@ package org.jetbrains.kotlinx.lincheck_test.guide import org.jetbrains.kotlinx.lincheck.* import org.jetbrains.kotlinx.lincheck.annotations.* -import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.* import org.junit.* import java.util.concurrent.* @@ -24,13 +23,11 @@ class ConcurrentHashMapTest { //@Test // TODO: Please, uncomment me and comment the line below to run the test and get the output @Test(expected = AssertionError::class) - fun modelCheckingTest() = ModelCheckingOptions() - .actorsBefore(1) - .actorsPerThread(1) - .actorsAfter(0) - .minimizeFailedScenario(false) - .checkObstructionFreedom(true) - .check(this::class) + fun lincheckTest() = LincheckOptions { + maxThreads = 2 + maxOperationsInThread = 1 + checkObstructionFreedom = true + }.check(this::class) } class ConcurrentSkipListMapTest { @@ -40,7 +37,7 @@ class ConcurrentSkipListMapTest { public fun put(key: Int, value: Int) = map.put(key, value) @Test - fun modelCheckingTest() = ModelCheckingOptions() - .checkObstructionFreedom(true) - .check(this::class) + fun lincheckTest() = LincheckOptions { + checkObstructionFreedom = true + }.check(this::class) } diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/guide/CounterTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/guide/CounterTest.kt index 78e57f13c..e4b4daf5c 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/guide/CounterTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/guide/CounterTest.kt @@ -12,8 +12,6 @@ package org.jetbrains.kotlinx.lincheck_test.guide import org.jetbrains.kotlinx.lincheck.* import org.jetbrains.kotlinx.lincheck.annotations.* -import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.* -import org.jetbrains.kotlinx.lincheck.strategy.stress.* import org.junit.* class CounterTest { @@ -30,23 +28,8 @@ class CounterTest { //@Test // TODO: Please, uncomment me and comment the line below to run the test and get the output @Test(expected = AssertionError::class) - fun stressTest() = StressOptions() // stress testing options - .actorsBefore(2) // number of operations before the parallel part - .threads(2) // number of threads in the parallel part - .actorsPerThread(2) // number of operations in each thread of the parallel part - .actorsAfter(1) // number of operations after the parallel part - .iterations(100) // generate 100 random concurrent scenarios - .invocationsPerIteration(1000) // run each generated scenario 1000 times - .check(this::class) // run the test - - //@Test // TODO: Please, uncomment me and comment the line below to run the test and get the output - @Test(expected = AssertionError::class) - fun modelCheckingTest() = ModelCheckingOptions() - .actorsBefore(2) // number of operations before the parallel part - .threads(2) // number of threads in the parallel part - .actorsPerThread(2) // number of operations in each thread of the parallel part - .actorsAfter(1) // number of operations after the parallel part - .iterations(100) // generate 100 random concurrent scenarios - .invocationsPerIteration(1000) // run each generated scenario 1000 times - .check(this::class) + fun lincheckTest() = LincheckOptions { + maxThreads = 2 + maxOperationsInThread = 2 + }.check(this::class) } \ No newline at end of file diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/guide/MPSCQueueTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/guide/MPSCQueueTest.kt index 742eaf613..cf22ba216 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/guide/MPSCQueueTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/guide/MPSCQueueTest.kt @@ -30,8 +30,8 @@ class MPSCQueueTest { public fun peek(): Int? = queue.peek() @Test - fun stressTest() = StressOptions().check(this::class) - - @Test - fun modelCheckingTest() = ModelCheckingOptions().check(this::class) + fun lincheckTest() = LincheckOptions { + maxThreads = 2 + maxOperationsInThread = 5 + }.check(this::class) } \ No newline at end of file diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/guide/ObstructionFreedomViolationTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/guide/ObstructionFreedomViolationTest.kt index 789b64057..8afdb4e53 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/guide/ObstructionFreedomViolationTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/guide/ObstructionFreedomViolationTest.kt @@ -63,7 +63,7 @@ class ObstructionFreedomViolationTest { //@Test // TODO: Please, uncomment me and comment the line below to run the test and get the output @Test(expected = AssertionError::class) - fun runModelCheckingTest() = ModelCheckingOptions() - .checkObstructionFreedom(true) - .check(this::class) + fun lincheckTest() = LincheckOptions { + checkObstructionFreedom = true + }.check(this::class) } \ No newline at end of file diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/AFUCallRepresentationTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/AFUCallRepresentationTest.kt index 0b97253c7..3ca25599a 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/AFUCallRepresentationTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/AFUCallRepresentationTest.kt @@ -44,6 +44,7 @@ class AFUCallRepresentationTest : VerifierState() { override fun extractState(): Any = counter @Test + @Suppress("DEPRECATION_ERROR") fun test() { val options = ModelCheckingOptions() .actorsPerThread(1) diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/CapturedValueRepresentationTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/CapturedValueRepresentationTest.kt index ae70b643e..5be99256c 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/CapturedValueRepresentationTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/CapturedValueRepresentationTest.kt @@ -9,10 +9,12 @@ */ package org.jetbrains.kotlinx.lincheck_test.representation +import org.jetbrains.kotlinx.lincheck.LincheckMode +import org.jetbrains.kotlinx.lincheck.LincheckOptions +import org.jetbrains.kotlinx.lincheck.LincheckOptionsImpl import org.jetbrains.kotlinx.lincheck.annotations.Operation import org.jetbrains.kotlinx.lincheck.checkImpl import org.jetbrains.kotlinx.lincheck.verifier.VerifierState -import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.ModelCheckingOptions import org.jetbrains.kotlinx.lincheck_test.util.checkLincheckOutput import org.junit.Test @@ -44,10 +46,12 @@ class CapturedValueRepresentationTest : VerifierState() { } @Test - fun test() = ModelCheckingOptions().apply { - actorsAfter(0) - actorsBefore(0) - actorsPerThread(1) + fun test() = LincheckOptions { + this as LincheckOptionsImpl + maxThreads = 2 + maxOperationsInThread = 1 + generateBeforeAndAfterParts = false + mode = LincheckMode.ModelChecking } .checkImpl(this::class.java) .checkLincheckOutput("captured_value.txt") diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/ClocksWithExceptionsInOutputTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/ClocksWithExceptionsInOutputTest.kt index 659887b33..701dba32d 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/ClocksWithExceptionsInOutputTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/ClocksWithExceptionsInOutputTest.kt @@ -10,9 +10,9 @@ package org.jetbrains.kotlinx.lincheck_test.representation +import org.jetbrains.kotlinx.lincheck.* +import org.jetbrains.kotlinx.lincheck.LincheckOptionsImpl import org.jetbrains.kotlinx.lincheck.annotations.Operation -import org.jetbrains.kotlinx.lincheck.checkImpl -import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.* import org.jetbrains.kotlinx.lincheck_test.util.* import org.junit.Test @@ -34,9 +34,22 @@ class ClocksWithExceptionsInOutputTest { fun operation2() = check(!canEnterForbiddenSection) { "Violating exception" } @Test - fun `should add stackTrace to output`() = ModelCheckingOptions().apply { - actorsPerThread(2) - minimizeFailedScenario(false) + fun `should add stackTrace to output`() = LincheckOptions { + this as LincheckOptionsImpl + mode = LincheckMode.ModelChecking + addCustomScenario { + parallel { + thread { + actor(::operation1) + actor(::operation1) + } + thread { + actor(::operation2) + } + } + } + generateRandomScenarios = false + minimizeFailedScenario = false } .checkImpl(this::class.java) .checkLincheckOutput("clocks_and_exceptions.txt") diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/CoroutineCancellationTraceReportingTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/CoroutineCancellationTraceReportingTest.kt index 4dd581581..94189f5aa 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/CoroutineCancellationTraceReportingTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/CoroutineCancellationTraceReportingTest.kt @@ -11,9 +11,11 @@ package org.jetbrains.kotlinx.lincheck_test.representation import kotlinx.coroutines.* +import org.jetbrains.kotlinx.lincheck.LincheckMode +import org.jetbrains.kotlinx.lincheck.LincheckOptions +import org.jetbrains.kotlinx.lincheck.LincheckOptionsImpl import org.jetbrains.kotlinx.lincheck.annotations.Operation import org.jetbrains.kotlinx.lincheck.checkImpl -import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.ModelCheckingOptions import org.jetbrains.kotlinx.lincheck.verifier.* import org.jetbrains.kotlinx.lincheck_test.util.* import org.junit.* @@ -38,10 +40,12 @@ class CoroutineCancellationTraceReportingTest : VerifierState() { override fun extractState(): Any = correct @Test - fun test() = ModelCheckingOptions().apply { - actorsPerThread(1) - actorsBefore(0) - actorsAfter(0) + fun test() = LincheckOptions { + this as LincheckOptionsImpl + maxThreads = 2 + maxOperationsInThread = 1 + generateBeforeAndAfterParts = false + mode = LincheckMode.ModelChecking } .checkImpl(this::class.java) .checkLincheckOutput( "coroutine_cancellation.txt") diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/ExceptionsInOutputTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/ExceptionsInOutputTest.kt index a8ce0eaf6..6c0cf6099 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/ExceptionsInOutputTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/ExceptionsInOutputTest.kt @@ -10,8 +10,9 @@ package org.jetbrains.kotlinx.lincheck_test.representation +import org.jetbrains.kotlinx.lincheck.* +import org.jetbrains.kotlinx.lincheck.LincheckOptionsImpl import org.jetbrains.kotlinx.lincheck.annotations.Operation -import org.jetbrains.kotlinx.lincheck.checkImpl import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.* import org.jetbrains.kotlinx.lincheck_test.util.* import org.junit.Test @@ -32,8 +33,20 @@ class ExceptionsInOutputTest { fun operation2() = check(!canEnterForbiddenSection) { "Violating exception" } @Test - fun `should add stackTrace to output`() = ModelCheckingOptions().apply { - actorsBefore(2) + fun `should add stackTrace to output`() = LincheckOptions { + this as LincheckOptionsImpl + addCustomScenario { + parallel { + thread { + actor(::operation1) + } + thread { + actor(::operation2) + } + } + } + generateRandomScenarios = false + mode = LincheckMode.ModelChecking } .checkImpl(this::class.java) .checkLincheckOutput("exceptions_in_output.txt") diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/ForcibleFinishExceptionInTryBlockTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/ForcibleFinishExceptionInTryBlockTest.kt index 8b282629d..50ac9f26a 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/ForcibleFinishExceptionInTryBlockTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/ForcibleFinishExceptionInTryBlockTest.kt @@ -34,6 +34,7 @@ class ForcibleFinishExceptionInTryBlockTest { } @Test + @Suppress("DEPRECATION_ERROR") fun test() { val options = ModelCheckingOptions() .actorsPerThread(1) diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/IllegalModuleAccessOutputMessageTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/IllegalModuleAccessOutputMessageTest.kt index 986479450..1298ad50d 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/IllegalModuleAccessOutputMessageTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/IllegalModuleAccessOutputMessageTest.kt @@ -41,7 +41,10 @@ class IllegalModuleAccessOutputMessageTest { } @Test - fun test() = ModelCheckingOptions() + fun test() = LincheckOptions { + this as LincheckOptionsImpl + mode = LincheckMode.ModelChecking + } .checkImpl(this::class.java) .checkLincheckOutput("illegal_module_access.txt") } \ No newline at end of file diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/InternalLincheckBugTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/InternalLincheckBugTest.kt index 90bfd76b1..923e3dd29 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/InternalLincheckBugTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/InternalLincheckBugTest.kt @@ -39,8 +39,11 @@ class InternalLincheckBugTest { } @Test - fun `should add stackTrace to output`() = ModelCheckingOptions().apply { - actorsPerThread(2) + fun `should add stackTrace to output`() = LincheckOptions { + this as LincheckOptionsImpl + maxThreads = 2 + maxOperationsInThread = 2 + mode = LincheckMode.ModelChecking } .checkImpl(this::class.java) .checkLincheckOutput("internal_bug_report.txt") diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/MethodReportingTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/MethodReportingTest.kt index 0b83b1830..beda58c68 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/MethodReportingTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/MethodReportingTest.kt @@ -62,6 +62,7 @@ class MethodReportingTest : VerifierState() { override fun extractState(): Any = a @Test + @Suppress("DEPRECATION_ERROR") fun test() { val options = ModelCheckingOptions() .actorsPerThread(1) @@ -107,10 +108,20 @@ class CaughtExceptionMethodReportingTest : VerifierState() { override fun extractState(): Any = counter @Test - fun test() = ModelCheckingOptions().apply { - actorsPerThread(1) - actorsBefore(0) - actorsAfter(0) + fun test() = LincheckOptions { + this as LincheckOptionsImpl + addCustomScenario { + parallel { + thread { + actor(::operation) + } + thread { + actor(::operation) + } + } + } + mode = LincheckMode.ModelChecking + generateRandomScenarios = false } .checkImpl(this::class.java) .checkLincheckOutput("method_reporting.txt") diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/ObstructionFreedomRepresentationTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/ObstructionFreedomRepresentationTest.kt index 48887aa86..0ab256fc5 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/ObstructionFreedomRepresentationTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/ObstructionFreedomRepresentationTest.kt @@ -48,6 +48,7 @@ class ObstructionFreedomActiveLockRepresentationTest : VerifierState() { override fun extractState(): Any = counter.get() @Test + @Suppress("DEPRECATION_ERROR") fun test() = ModelCheckingOptions() .actorsPerThread(1) .actorsBefore(0) @@ -72,6 +73,7 @@ class ObstructionFreedomSynchronizedRepresentationTest : VerifierState() { override fun extractState(): Any = counter @Test + @Suppress("DEPRECATION_ERROR") fun test() = ModelCheckingOptions().apply { actorsPerThread(1) actorsBefore(0) diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/SpinlockEventsCutTests.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/SpinlockEventsCutTests.kt index bb537fa95..adc2d5ef5 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/SpinlockEventsCutTests.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/SpinlockEventsCutTests.kt @@ -14,7 +14,6 @@ package org.jetbrains.kotlinx.lincheck_test.representation import org.jetbrains.kotlinx.lincheck.* import org.jetbrains.kotlinx.lincheck.annotations.Operation import org.jetbrains.kotlinx.lincheck.execution.* -import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.ModelCheckingOptions import org.jetbrains.kotlinx.lincheck_test.guide.MSQueueBlocking import org.jetbrains.kotlinx.lincheck_test.util.checkLincheckOutput import org.junit.Test @@ -36,8 +35,22 @@ class ObstructionFreedomViolationEventsCutTest { fun dequeue(): Int? = q.dequeue() @Test - fun runModelCheckingTest() = ModelCheckingOptions() - .checkObstructionFreedom(true) + fun runModelCheckingTest() = LincheckOptions { + this as LincheckOptionsImpl + mode = LincheckMode.ModelChecking + checkObstructionFreedom = true + addCustomScenario { + parallel { + thread { + actor(::enqueue, 1) + } + thread { + actor(::enqueue, -1) + } + } + } + generateRandomScenarios = false + } .checkImpl(this::class.java) .checkLincheckOutput("obstruction_freedom_violation_events_cut.txt") @@ -162,8 +175,14 @@ abstract class AbstractSpinLivelockTest { abstract fun meaninglessActions() @Test - fun testWithModelCheckingStrategy() = ModelCheckingOptions() - .minimizeFailedScenario(false) + fun testWithModelCheckingStrategy() = LincheckOptions { + this as LincheckOptionsImpl + mode = LincheckMode.ModelChecking + maxThreads = 2 + minOperationsInThread = 5 + maxOperationsInThread = 5 + minimizeFailedScenario = false + } .checkImpl(this::class.java) .checkLincheckOutput(outputFileName) } @@ -196,41 +215,28 @@ class SpinlockInIncorrectResultsWithClocksTest { fun d(): Int = 0 // cannot return 0, should fail @Test - fun test() = ModelCheckingOptions() - .executionGenerator(ClocksTestScenarioGenerator::class.java) - .iterations(1) - .sequentialSpecification(ClocksTestSequential::class.java) - .minimizeFailedScenario(false) + fun test() = LincheckOptions { + this as LincheckOptionsImpl + mode = LincheckMode.ModelChecking + addCustomScenario { + parallel { + thread { + actor(::a) + actor(::b) + } + thread { + actor(::c) + actor(::d) + } + } + } + generateRandomScenarios = false + minimizeFailedScenario = false + sequentialImplementation = ClocksTestSequential::class.java + } .checkImpl(this::class.java) .checkLincheckOutput("spin_lock_in_incorrect_results_failure.txt") - - /** - * @param randomProvider is required by scenario generator contract - */ - @Suppress("UNUSED_PARAMETER") - class ClocksTestScenarioGenerator( - testCfg: CTestConfiguration, - testStructure: CTestStructure, - randomProvider: RandomProvider - ) : ExecutionGenerator(testCfg, testStructure) { - override fun nextExecution() = ExecutionScenario( - emptyList(), - listOf( - listOf( - Actor(method = SpinlockInIncorrectResultsWithClocksTest::a.javaMethod!!, arguments = emptyList()), - Actor(method = SpinlockInIncorrectResultsWithClocksTest::b.javaMethod!!, arguments = emptyList()) - ), - listOf( - Actor(method = SpinlockInIncorrectResultsWithClocksTest::c.javaMethod!!, arguments = emptyList()), - Actor(method = SpinlockInIncorrectResultsWithClocksTest::d.javaMethod!!, arguments = emptyList()) - ) - ), - emptyList() - ) - - } - class ClocksTestSequential { private var x = 0 diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/StateRepresentationTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/StateRepresentationTest.kt index 019343873..0b7bbc6dc 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/StateRepresentationTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/StateRepresentationTest.kt @@ -13,8 +13,8 @@ import org.jetbrains.kotlinx.lincheck.annotations.Operation import org.jetbrains.kotlinx.lincheck.annotations.StateRepresentation import org.jetbrains.kotlinx.lincheck.appendFailure import org.jetbrains.kotlinx.lincheck.checkImpl -import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.ModelCheckingOptions import org.jetbrains.kotlinx.lincheck.strategy.stress.* +import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.* import org.jetbrains.kotlinx.lincheck.strategy.IncorrectResultsFailure import org.jetbrains.kotlinx.lincheck_test.util.* import org.jetbrains.kotlinx.lincheck.verifier.VerifierState @@ -40,6 +40,7 @@ open class ModelCheckingStateReportingTest { fun stateRepresentation() = counter.toString() @Test + @Suppress("DEPRECATION_ERROR") fun test() = ModelCheckingOptions().apply { actorsPerThread(1) actorsBefore(0) @@ -70,6 +71,7 @@ class StressStateReportingTest : VerifierState() { fun stateRepresentation() = counter.toString() @Test + @Suppress("DEPRECATION_ERROR") fun test() { val options = StressOptions() .actorsPerThread(1) @@ -107,6 +109,7 @@ class TwoStateRepresentationFunctionsTest : VerifierState() { fun stateRepresentation2() = counter.toString() @Test(expected = IllegalStateException::class) + @Suppress("DEPRECATION_ERROR") fun test() { ModelCheckingOptions() .actorsPerThread(1) @@ -133,6 +136,7 @@ class NonDeterministicStateRepresentationTest() { fun stateRepresentation() = "(${counter.get()}, ${Any()})" @Test + @Suppress("DEPRECATION_ERROR") fun test() { val options = ModelCheckingOptions() .actorsPerThread(1) diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/SuspendTraceReportingTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/SuspendTraceReportingTest.kt index d76c53c35..718f19207 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/SuspendTraceReportingTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/SuspendTraceReportingTest.kt @@ -10,9 +10,9 @@ package org.jetbrains.kotlinx.lincheck_test.representation import kotlinx.coroutines.sync.* +import org.jetbrains.kotlinx.lincheck.* +import org.jetbrains.kotlinx.lincheck.LincheckOptionsImpl import org.jetbrains.kotlinx.lincheck.annotations.Operation -import org.jetbrains.kotlinx.lincheck.checkImpl -import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.ModelCheckingOptions import org.jetbrains.kotlinx.lincheck_test.util.* import org.jetbrains.kotlinx.lincheck.verifier.* import org.junit.* @@ -46,10 +46,13 @@ class SuspendTraceReportingTest : VerifierState() { override fun extractState(): Any = counter @Test - fun test() = ModelCheckingOptions().apply { - actorsPerThread(1) - actorsBefore(0) - actorsAfter(0) + fun test() = LincheckOptions { + this as LincheckOptionsImpl + mode = LincheckMode.ModelChecking + maxThreads = 2 + maxOperationsInThread = 1 + generateBeforeAndAfterParts = false + testingTimeInSeconds = 10 } .checkImpl(this::class.java) .checkLincheckOutput("suspend_trace_reporting.txt") diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/SwitchAsFirstMethodEventTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/SwitchAsFirstMethodEventTest.kt index 2bee6e632..89a659b14 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/SwitchAsFirstMethodEventTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/SwitchAsFirstMethodEventTest.kt @@ -49,10 +49,20 @@ class SwitchAsFirstMethodEventTest { private fun incAndGetImpl() = counter.incrementAndGet() @Test - fun test() = ModelCheckingOptions().apply { - actorsPerThread(1) - actorsBefore(0) - actorsAfter(0) + fun test() = LincheckOptions { + this as LincheckOptionsImpl + addCustomScenario { + parallel { + thread { + actor(::incTwiceAndGet) + } + thread { + actor(::incTwiceAndGet) + } + } + } + mode = LincheckMode.ModelChecking + generateRandomScenarios = false } .checkImpl(this::class.java) .checkLincheckOutput("switch_as_first_method_event.txt") diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/ThreadDumpTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/ThreadDumpTest.kt index a23f1b4f0..9104ce661 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/ThreadDumpTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/ThreadDumpTest.kt @@ -20,6 +20,7 @@ import org.junit.* */ class ThreadDumpTest { @Test + @Suppress("DEPRECATION_ERROR") fun test() { val iterations = 30 repeat(iterations) { diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/TraceReportingTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/TraceReportingTest.kt index 271b38348..748b80b94 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/TraceReportingTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/TraceReportingTest.kt @@ -11,7 +11,6 @@ package org.jetbrains.kotlinx.lincheck_test.representation import org.jetbrains.kotlinx.lincheck.* import org.jetbrains.kotlinx.lincheck.annotations.Operation -import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.* import org.jetbrains.kotlinx.lincheck_test.util.* import org.junit.* @@ -63,8 +62,9 @@ class TraceReportingTest { @Test fun test() { - val failure = ModelCheckingOptions().apply { - iterations(0) + val failure = LincheckOptions { + this as LincheckOptionsImpl + mode = LincheckMode.ModelChecking addCustomScenario { parallel { thread { @@ -75,6 +75,7 @@ class TraceReportingTest { } } } + generateRandomScenarios = false }.checkImpl(this::class.java) failure.checkLincheckOutput("trace_reporting.txt") checkTraceHasNoLincheckEvents(failure.toString()) @@ -95,9 +96,10 @@ class TraceReportingTest { @Test fun testInitPostParts() { - val failure = ModelCheckingOptions() - .iterations(0) - .addCustomScenario { + val failure = LincheckOptions { + this as LincheckOptionsImpl + mode = LincheckMode.ModelChecking + addCustomScenario { initial { actor(::enterInit) } @@ -113,7 +115,9 @@ class TraceReportingTest { actor(::enterPost) } } - .checkImpl(this::class.java) + generateRandomScenarios = false + minimizeFailedScenario = false + }.checkImpl(this::class.java) failure.checkLincheckOutput("trace_reporting_init_post_parts.txt") checkTraceHasNoLincheckEvents(failure.toString()) } @@ -125,17 +129,19 @@ class TraceReportingTest { @Test fun testEmptyTrace() { - val failure = ModelCheckingOptions() - .iterations(0) - .addCustomScenario { + val failure = LincheckOptions { + this as LincheckOptionsImpl + mode = LincheckMode.ModelChecking + addCustomScenario { parallel { thread { actor(::notImplemented) } } } - .sequentialSpecification(EmptySequentialImplementation::class.java) - .checkImpl(this::class.java) + generateRandomScenarios = false + sequentialImplementation = EmptySequentialImplementation::class.java + }.checkImpl(this::class.java) failure.checkLincheckOutput("trace_reporting_empty.txt") } diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/ValidateFunctionTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/ValidateFunctionTest.kt index 67e79b69e..7aecb0309 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/ValidateFunctionTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/ValidateFunctionTest.kt @@ -9,10 +9,9 @@ */ package org.jetbrains.kotlinx.lincheck_test.representation +import org.jetbrains.kotlinx.lincheck.* import org.jetbrains.kotlinx.lincheck.annotations.* import org.jetbrains.kotlinx.lincheck.annotations.Operation -import org.jetbrains.kotlinx.lincheck.checkImpl -import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.* import org.jetbrains.kotlinx.lincheck_test.util.* import org.jetbrains.kotlinx.lincheck.verifier.* import org.junit.* @@ -39,7 +38,9 @@ class ValidateFunctionTest : VerifierState() { } @Test - fun test() = ModelCheckingOptions().apply { + fun test() = LincheckOptions { + this as LincheckOptionsImpl + mode = LincheckMode.ModelChecking addCustomScenario { initial { actor(::inc) @@ -53,6 +54,7 @@ class ValidateFunctionTest : VerifierState() { actor(::inc) } } + generateRandomScenarios = false } .checkImpl(this::class.java) .checkLincheckOutput("validation_function_failure.txt") diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/runner/CancellationHandlingTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/runner/CancellationHandlingTest.kt index 6ef7e2be8..0a019ffee 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/runner/CancellationHandlingTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/runner/CancellationHandlingTest.kt @@ -33,11 +33,12 @@ class CancellationHandlingTest : AbstractLincheckTest() { (cont as CancellableContinuation).cancel() } - override fun > O.customize() { - actorsBefore(0) - actorsAfter(0) - iterations(1) + override fun LincheckOptionsImpl.customize() { + generateBeforeAndAfterParts = false } + + override val testPlanningConstraints = false + } private val CANCELLED = Any() diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/runner/DeadlockTests.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/runner/DeadlockTests.kt index 382649a85..1f99f78ea 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/runner/DeadlockTests.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/runner/DeadlockTests.kt @@ -38,12 +38,12 @@ class DeadlockOnSynchronizedTest : AbstractLincheckTest(DeadlockWithDumpFailure: } } - override fun > O.customize() { - minimizeFailedScenario(false) - invocationTimeout(200) + override fun LincheckOptionsImpl.customize() { + invocationTimeoutMs = 200 + generateBeforeAndAfterParts = false } - override fun extractState(): Any = counter + override val testPlanningConstraints = false } class DeadlockOnSynchronizedWaitTest : AbstractLincheckTest(DeadlockWithDumpFailure::class) { @@ -56,13 +56,12 @@ class DeadlockOnSynchronizedWaitTest : AbstractLincheckTest(DeadlockWithDumpFail } } - override fun > O.customize() { - actorsBefore(0) - minimizeFailedScenario(false) - invocationTimeout(200) + override fun LincheckOptionsImpl.customize() { + invocationTimeoutMs = 200 + generateBeforeAndAfterParts = false } - override fun extractState(): Any = 0 // constant + override val testPlanningConstraints = false } class LiveLockTest : AbstractLincheckTest(DeadlockWithDumpFailure::class) { @@ -84,13 +83,13 @@ class LiveLockTest : AbstractLincheckTest(DeadlockWithDumpFailure::class) { } } - override fun extractState(): Any = counter - - override fun > O.customize() { - minimizeFailedScenario(false) - invocationTimeout(200) + override fun LincheckOptionsImpl.customize() { + invocationTimeoutMs = 200 + generateBeforeAndAfterParts = false } + override val testPlanningConstraints = false + private fun AtomicBoolean.withSpinLock(block: () -> Int): Int { while (!this.compareAndSet(false, true)); val result = block() diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/runner/ParallelThreadsRunnerExceptionTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/runner/ParallelThreadsRunnerExceptionTest.kt index e43672740..9491b674f 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/runner/ParallelThreadsRunnerExceptionTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/runner/ParallelThreadsRunnerExceptionTest.kt @@ -180,6 +180,6 @@ class ParallelThreadExecutionExceptionsTest { } } -fun mockStrategy(scenario: ExecutionScenario) = object : Strategy(scenario) { - override fun run(): LincheckFailure? = error("Not yet implemented") +private fun mockStrategy(scenario: ExecutionScenario) = object : Strategy(scenario) { + override fun runInvocation(): InvocationResult = error("Not yet implemented") } \ No newline at end of file diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/runner/RunBlockingTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/runner/RunBlockingTest.kt index c196d515a..dd4ca2103 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/runner/RunBlockingTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/runner/RunBlockingTest.kt @@ -32,8 +32,5 @@ class RunBlockingTest : AbstractLincheckTest() { override fun extractState() = Unit - override fun > O.customize() { - minimizeFailedScenario(false) - iterations(1) - } + override val testPlanningConstraints = false } diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/runner/TestThreadExecutionHelperTest.java b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/runner/TestThreadExecutionHelperTest.java index a7d527111..187cc703a 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/runner/TestThreadExecutionHelperTest.java +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/runner/TestThreadExecutionHelperTest.java @@ -10,6 +10,7 @@ package org.jetbrains.kotlinx.lincheck_test.runner; +import org.jetbrains.annotations.NotNull; import org.jetbrains.kotlinx.lincheck.*; import org.jetbrains.kotlinx.lincheck.execution.*; import org.jetbrains.kotlinx.lincheck.runner.*; @@ -28,8 +29,9 @@ public class TestThreadExecutionHelperTest { public void setUp() { ExecutionScenario scenario = new ExecutionScenario(emptyList(), emptyList(), emptyList()); Strategy strategy = new Strategy(scenario) { + @NotNull @Override - public LincheckFailure run() { + public InvocationResult runInvocation() { throw new UnsupportedOperationException(); } }; diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/strategy/modelchecking/ObstructionFreedomViolationTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/strategy/modelchecking/ObstructionFreedomViolationTest.kt index 9ffbd2df4..28e3f699f 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/strategy/modelchecking/ObstructionFreedomViolationTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/strategy/modelchecking/ObstructionFreedomViolationTest.kt @@ -26,6 +26,7 @@ class ObstructionFreedomViolationTest : VerifierState() { fun get(): Int = synchronized(this) { c } @Test + @Suppress("DEPRECATION_ERROR") fun test() { val options = ModelCheckingOptions() .checkObstructionFreedom() diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/strategy/modelchecking/SingletonCollectionInTraceTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/strategy/modelchecking/SingletonCollectionInTraceTest.kt index e7801c84a..abae6d5bb 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/strategy/modelchecking/SingletonCollectionInTraceTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/strategy/modelchecking/SingletonCollectionInTraceTest.kt @@ -39,6 +39,7 @@ class SingletonCollectionInTraceTest { } @Test + @Suppress("DEPRECATION_ERROR") fun modelCheckingTest() { val failure = ModelCheckingOptions() .iterations(1) diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/transformation/FinalFieldReadingEliminationTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/transformation/FinalFieldReadingEliminationTest.kt index a9a52a9e7..f083d511d 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/transformation/FinalFieldReadingEliminationTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/transformation/FinalFieldReadingEliminationTest.kt @@ -7,6 +7,8 @@ * 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/. */ +@file:Suppress("DEPRECATION_ERROR") + package org.jetbrains.kotlinx.lincheck_test.transformation import org.jetbrains.kotlinx.lincheck.LinChecker @@ -23,6 +25,7 @@ import java.io.Serializable * Otherwise, this test fails by timeout since * the number of invocations is set to [Int.MAX_VALUE]. */ +@Suppress("DEPRECATION_ERROR") @ModelCheckingCTest(actorsBefore = 0, actorsAfter = 0, actorsPerThread = 50, invocationsPerIteration = Int.MAX_VALUE, iterations = 50, minimizeFailedScenario = false) class FinalFieldReadingEliminationTest : VerifierState() { val primitiveValue: Int = 32 diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/transformation/HashCodeStubTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/transformation/HashCodeStubTest.kt index 921a34fb0..d3c09c49b 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/transformation/HashCodeStubTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/transformation/HashCodeStubTest.kt @@ -19,7 +19,6 @@ import org.junit.* * Checks that [Object.hashCode] is replaced with a deterministic * implementations in the model checking mode. */ -@ModelCheckingCTest(iterations = 50, invocationsPerIteration = 1000) class HashCodeStubTest : VerifierState() { @Volatile private var a: Any = Any() @@ -37,7 +36,10 @@ class HashCodeStubTest : VerifierState() { @Test fun test() { - LinChecker.check(this::class.java) + LincheckOptions { + this as LincheckOptionsImpl + mode = LincheckMode.ModelChecking + }.check(this::class.java) } override fun extractState(): Any = 0 // constant state diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/transformation/IgnoredGuaranteeOnExceptionTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/transformation/IgnoredGuaranteeOnExceptionTest.kt index 7fe4b8c1a..d8dcbbda6 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/transformation/IgnoredGuaranteeOnExceptionTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/transformation/IgnoredGuaranteeOnExceptionTest.kt @@ -34,6 +34,7 @@ class IgnoredGuaranteeOnExceptionTest : VerifierState() { private fun badMethod(): Int = TODO() @Test + @Suppress("DEPRECATION_ERROR") fun test() { val options = ModelCheckingOptions().addGuarantee(forClasses(this.javaClass.name).methods("badMethod").ignore()) val failure = options.checkImpl(this.javaClass) diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/transformation/IgnoredGuaranteeTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/transformation/IgnoredGuaranteeTest.kt index 01946a6f9..548f8191c 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/transformation/IgnoredGuaranteeTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/transformation/IgnoredGuaranteeTest.kt @@ -26,6 +26,7 @@ import org.junit.* * If the ignored method is not processed properly, this test fails * by timeout since the number of invocations is set to Int.MAX_VALUE. */ +@Suppress("DEPRECATION_ERROR") @ModelCheckingCTest(actorsBefore = 0, actorsAfter = 0, actorsPerThread = 100, invocationsPerIteration = Int.MAX_VALUE, iterations = 50) class IgnoredGuaranteeTest : VerifierState() { var value: Int = 0 diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/transformation/IterableTransformationTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/transformation/IterableTransformationTest.kt index f5660c2b3..0414476c3 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/transformation/IterableTransformationTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/transformation/IterableTransformationTest.kt @@ -9,9 +9,9 @@ */ package org.jetbrains.kotlinx.lincheck_test.transformation -import org.jetbrains.kotlinx.lincheck.LinChecker +import org.jetbrains.kotlinx.lincheck.* +import org.jetbrains.kotlinx.lincheck.LincheckOptionsImpl 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.junit.Test @@ -19,7 +19,6 @@ import org.junit.Test * Tests that java.lang.Iterable is transformed and * iterator() method returns transformed java.util.Iterator */ -@ModelCheckingCTest(iterations = 1, actorsBefore = 1, actorsAfter = 1, actorsPerThread = 1) class IterableTransformationTest : VerifierState() { private var sum = 0 @@ -33,7 +32,9 @@ class IterableTransformationTest : VerifierState() { @Test fun test() { - LinChecker.check(this::class.java) + LincheckOptions { + testingTimeInSeconds = 1 + }.check(this::class) } override fun extractState(): Any = 0 // constant state diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/transformation/KotlinStdlibTransformationTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/transformation/KotlinStdlibTransformationTest.kt index 5a5c23992..ae226ba35 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/transformation/KotlinStdlibTransformationTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/transformation/KotlinStdlibTransformationTest.kt @@ -9,9 +9,9 @@ */ package org.jetbrains.kotlinx.lincheck_test.transformation -import org.jetbrains.kotlinx.lincheck.Options -import org.jetbrains.kotlinx.lincheck.annotations.Operation -import org.jetbrains.kotlinx.lincheck_test.AbstractLincheckTest +import org.jetbrains.kotlinx.lincheck.* +import org.jetbrains.kotlinx.lincheck.annotations.* +import org.jetbrains.kotlinx.lincheck_test.* /** * This test checks that some methods in kotlin stdlib related to @@ -52,8 +52,15 @@ class KotlinStdlibTransformationTest : AbstractLincheckTest() { intProgression.toSet() } - override fun > O.customize() { - iterations(1) + override fun LincheckOptionsImpl.customize() { + generateRandomScenarios = false + addCustomScenario { + parallel { + thread { + actor(::operation) + } + } + } } override fun extractState(): Any = 0 // constant state diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/transformation/LocalObjectEliminationTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/transformation/LocalObjectEliminationTest.kt index 12e4ae59d..ab42002a7 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/transformation/LocalObjectEliminationTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/transformation/LocalObjectEliminationTest.kt @@ -22,6 +22,7 @@ import org.junit.* * this test fails by timeout since the number of * invocations is set to [Int.MAX_VALUE]. */ +@Suppress("DEPRECATION_ERROR") @ModelCheckingCTest(actorsBefore = 0, actorsAfter = 0, actorsPerThread = 50, invocationsPerIteration = Int.MAX_VALUE, iterations = 50) class LocalObjectEliminationTest : VerifierState() { @Operation diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/transformation/NestedSynchronizedBlocksTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/transformation/NestedSynchronizedBlocksTest.kt index 6d3a65978..b92e28aed 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/transformation/NestedSynchronizedBlocksTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/transformation/NestedSynchronizedBlocksTest.kt @@ -18,7 +18,6 @@ import org.junit.* /** * This test checks that transformed code supports reentrant synchronized locking. */ -@ModelCheckingCTest(iterations = 1) class NestedSynchronizedBlocksTest : VerifierState() { private var counter = 0 @@ -31,7 +30,9 @@ class NestedSynchronizedBlocksTest : VerifierState() { @Test fun test() { - LinChecker.check(this::class.java) + LincheckOptions { + testingTimeInSeconds = 1 + }.check(this::class) } override fun extractState(): Any = counter diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/transformation/RandomTransformationTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/transformation/RandomTransformationTest.kt index bc83ffe2d..0b01edb51 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/transformation/RandomTransformationTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/transformation/RandomTransformationTest.kt @@ -21,7 +21,6 @@ import java.util.concurrent.* * Checks that [Random] and [ThreadLocalRandom] are replaced * with deterministic implementations in the model checking mode. */ -@ModelCheckingCTest(iterations = 50, invocationsPerIteration = 1000) class RandomTransformationTest : VerifierState() { @Volatile private var a: Any = Any() @@ -46,7 +45,9 @@ class RandomTransformationTest : VerifierState() { @Test fun test() { - LinChecker.check(this::class.java) + LincheckOptions { + testingTimeInSeconds = 1 + }.check(this::class) } override fun extractState(): Any = 0 // constant state diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/transformation/SerializableValueTests.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/transformation/SerializableValueTests.kt index bacc63590..a766296ac 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/transformation/SerializableValueTests.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/transformation/SerializableValueTests.kt @@ -25,13 +25,12 @@ class SerializableResultTest : AbstractLincheckTest() { @Operation fun getAndSet(key: Int) = counter.getAndSet(ValueHolder(key)) - override fun extractState(): Any = counter.get().value - - override fun > O.customize() { - iterations(1) - actorsBefore(0) - actorsAfter(0) + override fun LincheckOptionsImpl.customize() { + testingTimeInSeconds = 1 + generateBeforeAndAfterParts = false } + + override val testPlanningConstraints: Boolean = false } class SerializableJavaUtilResultTest : AbstractLincheckTest() { @@ -40,13 +39,12 @@ class SerializableJavaUtilResultTest : AbstractLincheckTest() { @Operation fun get(key: Int) = value - override fun extractState(): Any = value - - override fun > O.customize() { - iterations(1) - actorsBefore(0) - actorsAfter(0) + override fun LincheckOptionsImpl.customize() { + testingTimeInSeconds = 1 + generateBeforeAndAfterParts = false } + + override val testPlanningConstraints: Boolean = false } class SerializableJavaUtilResultIncorrectTest : AbstractLincheckTest(IncorrectResultsFailure::class) { @@ -58,13 +56,7 @@ class SerializableJavaUtilResultIncorrectTest : AbstractLincheckTest(IncorrectRe return value } - override fun extractState(): Any = value - - override fun > O.customize() { - iterations(1) - actorsBefore(0) - actorsAfter(0) - } + override val testPlanningConstraints: Boolean = false } class SerializableNullResultTest { @@ -88,13 +80,12 @@ class SerializableParameterTest : AbstractLincheckTest() { @Operation fun operation(@Param(name = "key") key: ValueHolder): Int = counter.addAndGet(key.value) - override fun extractState(): Any = counter.get() - - override fun > O.customize() { - iterations(1) - actorsBefore(0) - actorsAfter(0) + override fun LincheckOptionsImpl.customize() { + testingTimeInSeconds = 1 + generateBeforeAndAfterParts = false } + + override val testPlanningConstraints: Boolean = false } @Param(name = "key", gen = ValueHolderGen::class) @@ -107,13 +98,7 @@ class SerializableParameterIncorrectTest : AbstractLincheckTest(IncorrectResults return counter } - override fun extractState(): Any = counter - - override fun > O.customize() { - iterations(1) - actorsBefore(0) - actorsAfter(0) - } + override val testPlanningConstraints: Boolean = false } class ValueHolderGen(randomProvider: RandomProvider, conf: String) : ParameterGenerator { @@ -125,13 +110,12 @@ class SerializableJavaUtilParameterTest : AbstractLincheckTest() { @Operation fun operation(@Param(name = "key") key: List): Int = key[0] + key.sum() - override fun extractState(): Any = 0 // constant state - - override fun > O.customize() { - iterations(1) - actorsBefore(0) - actorsAfter(0) + override fun LincheckOptionsImpl.customize() { + testingTimeInSeconds = 1 + generateBeforeAndAfterParts = false } + + override val testPlanningConstraints: Boolean = false } class JavaUtilGen(randomProvider: RandomProvider, conf: String) : ParameterGenerator> { @@ -145,13 +129,12 @@ class SerializableNullParameterTest : AbstractLincheckTest() { @Operation fun operation(@Param(name = "key") key: List?): Int = key?.sum() ?: 0 - override fun extractState(): Any = 0 // constant state - - override fun > O.customize() { - iterations(1) - actorsBefore(0) - actorsAfter(0) + override fun LincheckOptionsImpl.customize() { + testingTimeInSeconds = 1 + generateBeforeAndAfterParts = false } + + override val testPlanningConstraints: Boolean = false } class NullGen(randomProvider: RandomProvider, conf: String) : ParameterGenerator?> { diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/transformation/Striped64SupportTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/transformation/Striped64SupportTest.kt index 3bdd8d3c7..696b275a3 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/transformation/Striped64SupportTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/transformation/Striped64SupportTest.kt @@ -13,7 +13,6 @@ package org.jetbrains.kotlinx.lincheck_test.transformation import org.jetbrains.kotlinx.lincheck.* import org.jetbrains.kotlinx.lincheck.annotations.* import org.jetbrains.kotlinx.lincheck.strategy.* -import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.* import org.junit.* import java.util.concurrent.atomic.* @@ -31,9 +30,12 @@ class Striped64SupportTest { @Test fun test() { - val failure = ModelCheckingOptions() - .minimizeFailedScenario(false) - .checkImpl(this::class.java) + val failure = LincheckOptions { + this as LincheckOptionsImpl + mode = LincheckMode.ModelChecking + testingTimeInSeconds = 10 + minimizeFailedScenario = false + }.checkImpl(this::class.java) assert(failure is IncorrectResultsFailure) { "This test should fail with IncorrectResultsFailure, but another error has been detected:\n$failure" } diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/transformation/TimeStubTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/transformation/TimeStubTest.kt index d4ff0d02e..10a9fb3e5 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/transformation/TimeStubTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/transformation/TimeStubTest.kt @@ -19,7 +19,6 @@ import org.junit.* * Checks that [System.nanoTime] and [System.currentTimeMillis] are * replaced with deterministic implementations in the model checking mode. */ -@ModelCheckingCTest(iterations = 30, invocationsPerIteration = 1000) class TimeStubTest : VerifierState() { @Volatile private var a: Any = Any() @@ -44,7 +43,7 @@ class TimeStubTest : VerifierState() { @Test fun test() { - LinChecker.check(this::class.java) + LincheckOptions().check(this::class) } override fun extractState(): Any = 0 // constant state diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/transformation/TransformInterfaceFromJUCWithRemappedClassTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/transformation/TransformInterfaceFromJUCWithRemappedClassTest.kt index 75749b809..6f3b231e7 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/transformation/TransformInterfaceFromJUCWithRemappedClassTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/transformation/TransformInterfaceFromJUCWithRemappedClassTest.kt @@ -24,11 +24,14 @@ class TransformInterfaceFromJUCWithRemappedClassTest : AbstractLincheckTest() { @Operation fun op() = q.poll(100, TimeUnit.DAYS) - override fun > O.customize() { - iterations(1) - actorsBefore(0) - threads(1) - actorsPerThread(1) - actorsAfter(0) + override fun LincheckOptionsImpl.customize() { + generateRandomScenarios = false + addCustomScenario { + parallel { + thread { + actor(::op) + } + } + } } } diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/transformation/TransformedExceptionTests.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/transformation/TransformedExceptionTests.kt index f9836df3a..e155841e7 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/transformation/TransformedExceptionTests.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/transformation/TransformedExceptionTests.kt @@ -9,8 +9,7 @@ */ package org.jetbrains.kotlinx.lincheck_test.transformation -import org.jetbrains.kotlinx.lincheck.InternalLincheckTestUnexpectedException -import org.jetbrains.kotlinx.lincheck.Options +import org.jetbrains.kotlinx.lincheck.* import org.jetbrains.kotlinx.lincheck.annotations.Operation import org.jetbrains.kotlinx.lincheck.strategy.* import org.jetbrains.kotlinx.lincheck_test.AbstractLincheckTest @@ -19,11 +18,13 @@ class ExpectedTransformedExceptionTest : AbstractLincheckTest() { @Operation fun operation(): Unit = throw CustomException() - override fun > O.customize() { - iterations(1) + override fun LincheckOptionsImpl.customize() { + testingTimeInSeconds = 1 } override fun extractState(): Any = 0 // constant state + + override val testPlanningConstraints: Boolean = false } class UnexpectedTransformedExceptionTest : AbstractLincheckTest(UnexpectedExceptionFailure::class) { @@ -39,7 +40,13 @@ class UnexpectedTransformedExceptionTest : AbstractLincheckTest(UnexpectedExcept return 0 } + override fun LincheckOptionsImpl.customize() { + testingTimeInSeconds = 1 + } + override fun extractState(): Any = 0 // constant state + + override val testPlanningConstraints: Boolean = false } internal class CustomException : Throwable() diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/transformation/WaitNotifyLockTests.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/transformation/WaitNotifyLockTests.kt index 728b2aa98..2d69a0f96 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/transformation/WaitNotifyLockTests.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/transformation/WaitNotifyLockTests.kt @@ -10,14 +10,12 @@ package org.jetbrains.kotlinx.lincheck_test.transformation -import org.jetbrains.kotlinx.lincheck.LinChecker +import org.jetbrains.kotlinx.lincheck.* 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.junit.Test // tests wait/notify support in model checking strategy -@ModelCheckingCTest(iterations = 30) class WaitNotifyLockTest : VerifierState() { private var counter = 0 private val lock = WaitNotifyLock() @@ -29,12 +27,11 @@ class WaitNotifyLockTest : VerifierState() { @Test fun test() { - LinChecker.check(this::class.java) + LincheckOptions().check(this::class) } } // tests wait/notify support under lock re-entrance in model checking strategy -@ModelCheckingCTest(iterations = 30) class NestedWaitNotifyLockTest : VerifierState() { private var counter = 0 private val lock = NestedWaitNotifyLock() @@ -46,7 +43,7 @@ class NestedWaitNotifyLockTest : VerifierState() { @Test fun test() { - LinChecker.check(this::class.java) + LincheckOptions().check(this::class) } } diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/verifier/AllowExtraSuspensionTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/verifier/AllowExtraSuspensionTest.kt index 7baab0365..f3fc8b19b 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/verifier/AllowExtraSuspensionTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/verifier/AllowExtraSuspensionTest.kt @@ -31,9 +31,11 @@ class AllowExtraSuspensionCorrectTest : AbstractLincheckTest() { @Operation suspend fun dec() = counter.getAndDecrement() - override fun > O.customize() { - sequentialSpecification(CounterSequential::class.java) + override fun LincheckOptionsImpl.customize() { + sequentialImplementation = CounterSequential::class.java } + + override val testPlanningConstraints: Boolean = false } class AllowExtraSuspensionIncorrectTest : AbstractLincheckTest(IncorrectResultsFailure::class) { @@ -48,9 +50,11 @@ class AllowExtraSuspensionIncorrectTest : AbstractLincheckTest(IncorrectResultsF @Operation suspend fun dec() = counter.getAndDecrement() - override fun > O.customize() { - sequentialSpecification(CounterSequential::class.java) + override fun LincheckOptionsImpl.customize() { + sequentialImplementation = CounterSequential::class.java } + + override val testPlanningConstraints: Boolean = false } // One of the operations should always succeed without suspension @@ -73,13 +77,7 @@ class OnlyExtraSuspensionsHaveToBeAtomicTest : AbstractLincheckTest() { suspendCancellableCoroutine { } } - override fun > O.customize() { - iterations(10) - actorsBefore(0) - threads(2) - actorsPerThread(3) - actorsAfter(0) - } + override val testPlanningConstraints: Boolean = false } class CounterSequential : VerifierState() { diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/verifier/EpsilonVerifierTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/verifier/EpsilonVerifierTest.kt index fe19b33c9..2d5cc0472 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/verifier/EpsilonVerifierTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/verifier/EpsilonVerifierTest.kt @@ -15,7 +15,6 @@ import org.jetbrains.kotlinx.lincheck.strategy.stress.* import org.jetbrains.kotlinx.lincheck.verifier.* import org.junit.* -@StressCTest(iterations = 5, threads = 2, actorsPerThread = 2, verifier = EpsilonVerifier::class) class EpsilonVerifierTest : VerifierState() { private var i = 0 @@ -23,7 +22,10 @@ class EpsilonVerifierTest : VerifierState() { fun incAndGet() = i++ // non-atomic! @Test - fun test() = LinChecker.check(EpsilonVerifierTest::class.java) + fun test() = LincheckOptions { + testingTimeInSeconds = 1 + verifier = EpsilonVerifier::class.java + }.check(EpsilonVerifierTest::class.java) override fun extractState() = i } diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/verifier/SequentialSpecificationTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/verifier/SequentialSpecificationTest.kt index bc649818f..00f0a6a21 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/verifier/SequentialSpecificationTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/verifier/SequentialSpecificationTest.kt @@ -25,8 +25,8 @@ class SequentialSpecificationTest : AbstractLincheckTest(IncorrectResultsFailure @Operation fun get() = c.get() + 1 - override fun > O.customize() { - sequentialSpecification(CorrectCounter::class.java) + override fun LincheckOptionsImpl.customize() { + sequentialImplementation = CorrectCounter::class.java } } diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/verifier/linearizability/BufferedChannelTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/verifier/linearizability/BufferedChannelTest.kt index 999247979..b280ef9d0 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/verifier/linearizability/BufferedChannelTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/verifier/linearizability/BufferedChannelTest.kt @@ -33,8 +33,11 @@ class BufferedChannelTest : AbstractLincheckTest() { @Operation fun offer(@Param(name = "value") value: Int) = c.trySend(value).isSuccess - override fun > O.customize() { - sequentialSpecification(SequentiaBuffered2IntChannel::class.java) + override fun LincheckOptionsImpl.customize() { + // increase testing time because currently BufferedChannelTest performs poorly, + // thus often leading to a small number of iterations + testingTimeInSeconds = 30 + sequentialImplementation = SequentiaBuffered2IntChannel::class.java } } diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/verifier/linearizability/ConcurrentDequeTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/verifier/linearizability/ConcurrentDequeTest.kt index 4315ae5f1..b3398d2a5 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/verifier/linearizability/ConcurrentDequeTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/verifier/linearizability/ConcurrentDequeTest.kt @@ -33,7 +33,7 @@ class ConcurrentDequeTest : AbstractLincheckTest() { override fun extractState() = deque.toList() - override fun > O.customize() { - iterations(100) // more iterations, because stress strategy not always finds the bug quickly + override fun LincheckOptionsImpl.customize() { + testingTimeInSeconds = 30 // more time, because stress strategy not always finds the bug quickly } } diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/verifier/linearizability/ConcurrentHashMapTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/verifier/linearizability/ConcurrentHashMapTest.kt index 5c546cfac..c2619d6b3 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/verifier/linearizability/ConcurrentHashMapTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/verifier/linearizability/ConcurrentHashMapTest.kt @@ -29,11 +29,4 @@ class ConcurrentHashMapTest : AbstractLincheckTest() { @Operation fun remove(@Param(name = "key") key: Int) = map.remove(key) - override fun extractState(): Any = map - - override fun > O.customize() { - // To obtain rare interleaving with `fullAddCount` method - if (this is ModelCheckingOptions) - invocationsPerIteration(10000) - } } \ No newline at end of file diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/verifier/linearizability/CounterTests.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/verifier/linearizability/CounterTests.kt index 4ebb46994..75de03c13 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/verifier/linearizability/CounterTests.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/verifier/linearizability/CounterTests.kt @@ -23,6 +23,9 @@ abstract class AbstractCounterTest( fun incAndGet(): Int = counter.incAndGet() override fun extractState(): Any = counter.get() + + // counter tests have small number of interleavings + override val testPlanningConstraints: Boolean = false } class CounterCorrectTest : AbstractCounterTest(CounterCorrect()) diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/verifier/linearizability/LockBasedSetTests.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/verifier/linearizability/LockBasedSetTests.kt index e6bca4c58..bcf620174 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/verifier/linearizability/LockBasedSetTests.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/verifier/linearizability/LockBasedSetTests.kt @@ -9,6 +9,7 @@ */ package org.jetbrains.kotlinx.lincheck_test.verifier.linearizability +import org.jetbrains.kotlinx.lincheck.LincheckOptionsImpl import org.jetbrains.kotlinx.lincheck.annotations.* import org.jetbrains.kotlinx.lincheck.paramgen.IntGen import org.jetbrains.kotlinx.lincheck_test.* @@ -28,6 +29,7 @@ abstract class AbstractSetTest(private val set: Set) : AbstractLincheckTest() { operator fun contains(@Param(name = "key") key: Int): Boolean = set.contains(key) override fun extractState(): Any = (1..5).map { set.contains(it) } + } class SpinLockSetTest : AbstractSetTest(SpinLockBasedSet()) diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/verifier/linearizability/LockFreeSetTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/verifier/linearizability/LockFreeSetTest.kt index cc1ca9b14..2287f8b39 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/verifier/linearizability/LockFreeSetTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/verifier/linearizability/LockFreeSetTest.kt @@ -12,7 +12,6 @@ package org.jetbrains.kotlinx.lincheck_test.verifier.linearizability import kotlinx.atomicfu.* import org.jetbrains.kotlinx.lincheck.* -import org.jetbrains.kotlinx.lincheck.strategy.stress.* import org.junit.* class LockFreeSetTest { @@ -35,12 +34,12 @@ class LockFreeSetTest { } } } - - StressOptions() - .addCustomScenario(scenario) - .invocationsPerIteration(1000000) - .iterations(0) - .check(LockFreeSet::class) + LincheckOptions { + this as LincheckOptionsImpl + mode = LincheckMode.Stress + generateRandomScenarios = false + addCustomScenario(scenario, invocations = 1_000_000) + }.check(LockFreeSet::class) } } diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/verifier/linearizability/ManySwitchBugTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/verifier/linearizability/ManySwitchBugTest.kt index d9fe6787a..b71e11dfa 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/verifier/linearizability/ManySwitchBugTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/verifier/linearizability/ManySwitchBugTest.kt @@ -12,7 +12,6 @@ package org.jetbrains.kotlinx.lincheck_test.verifier.linearizability import org.jetbrains.kotlinx.lincheck.* import org.jetbrains.kotlinx.lincheck.annotations.* import org.jetbrains.kotlinx.lincheck.strategy.* -import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.* import org.junit.* /** @@ -54,11 +53,21 @@ class ManySwitchBugTest { @Test fun test() { - val failure = ModelCheckingOptions() - .actorsAfter(0) - .actorsBefore(0) - .actorsPerThread(1) - .checkImpl(this::class.java) + val failure = LincheckOptions { + this as LincheckOptionsImpl + mode = LincheckMode.ModelChecking + generateRandomScenarios = false + addCustomScenario { + parallel { + thread { + actor(::foo) + } + thread { + actor(::bar) + } + } + } + }.checkImpl(this::class.java) check(failure is IncorrectResultsFailure) { "The test should fail" } } } diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/verifier/linearizability/RendezvousChannelTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/verifier/linearizability/RendezvousChannelTest.kt index 3dd6872d3..f9154cf1e 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/verifier/linearizability/RendezvousChannelTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/verifier/linearizability/RendezvousChannelTest.kt @@ -34,9 +34,11 @@ class RendezvousChannelTest : AbstractLincheckTest() { @Operation fun close() = ch.close() - override fun > O.customize() { - sequentialSpecification(SequentialRendezvousIntChannel::class.java) - iterations(10) + override fun LincheckOptionsImpl.customize() { + // increase testing time because currently RendezvousChannelTest performs poorly, + // thus often leading to a small number of iterations + testingTimeInSeconds = 30 + sequentialImplementation = SequentialRendezvousIntChannel::class.java } } diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/verifier/quiescent/LockFreeTaskQueueTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/verifier/quiescent/LockFreeTaskQueueTest.kt index 432f2b160..0cd09e953 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/verifier/quiescent/LockFreeTaskQueueTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/verifier/quiescent/LockFreeTaskQueueTest.kt @@ -32,13 +32,7 @@ class LockFreeTaskQueueTest : AbstractLincheckTest() { @Operation fun close() = q.close() - override fun > O.customize() { - actorsBefore(2) - actorsAfter(2) - threads(2) - actorsPerThread(3) - verifier(QuiescentConsistencyVerifier::class.java) + override fun LincheckOptionsImpl.customize() { + verifier = QuiescentConsistencyVerifier::class.java } - - override fun extractState() = q.map { it } to q.isClosed() } \ No newline at end of file diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/verifier/serializability/SerializableQueueTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/verifier/serializability/SerializableQueueTest.kt index d2f54e579..cb5d70ab7 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/verifier/serializability/SerializableQueueTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/verifier/serializability/SerializableQueueTest.kt @@ -25,12 +25,9 @@ class SerializableQueueTest : AbstractLincheckTest() { @Operation fun poll(): Int? = q.poll() - override fun > O.customize() { - actorsBefore(0) - actorsAfter(0) - actorsPerThread(2) - verifier(SerializabilityVerifier::class.java) - sequentialSpecification(SequentialIntQueue::class.java) + override fun LincheckOptionsImpl.customize() { + verifier = SerializabilityVerifier::class.java + sequentialImplementation = SequentialIntQueue::class.java } } diff --git a/src/jvm/test/resources/expected_logs/clocks_and_exceptions.txt b/src/jvm/test/resources/expected_logs/clocks_and_exceptions.txt index 2485dd909..a0e9e54fd 100644 --- a/src/jvm/test/resources/expected_logs/clocks_and_exceptions.txt +++ b/src/jvm/test/resources/expected_logs/clocks_and_exceptions.txt @@ -2,24 +2,10 @@ | ----------------------------------------------------------------------- | | Thread 1 | Thread 2 | | ----------------------------------------------------------------------- | -| operation2(): void | | -| operation1(): void | | -| operation1(): void | | -| operation2(): void | | -| operation2(): void | | -| ----------------------------------------------------------------------- | | operation1(): void | operation2(): IllegalStateException #1 [1,0] | -| operation1(): void [1,0] | operation1(): void [1,1] | -| ----------------------------------------------------------------------- | -| operation1(): void | | -| operation1(): void | | -| operation1(): void | | -| operation2(): void | | -| operation1(): void | | +| operation1(): void [1,0] | | | ----------------------------------------------------------------------- | ---- -All operations above the horizontal line | ----- | happen before those below the line --- Values in "[..]" brackets indicate the number of completed operations in each of the parallel threads seen at the beginning of the current operation @@ -31,24 +17,13 @@ The following interleaving leads to the error: | ----------------------------------------------------------------------------------------------------------------------------------------------------------------------- | | Thread 1 | Thread 2 | | ----------------------------------------------------------------------------------------------------------------------------------------------------------------------- | -| operation2() | | -| operation1() | | -| operation1() | | -| operation2() | | -| operation2() | | | operation1() | | | operation1() | | | canEnterForbiddenSection.WRITE(true) at ClocksWithExceptionsInOutputTest.operation1(ClocksWithExceptionsInOutputTest.kt:29) | | | switch | | | | operation2(): IllegalStateException #1 | -| | operation1() | | canEnterForbiddenSection.WRITE(false) at ClocksWithExceptionsInOutputTest.operation1(ClocksWithExceptionsInOutputTest.kt:30) | | | result: void | | -| operation1() | | -| operation1() | | -| operation1() | | -| operation2() | | -| operation1() | | | ----------------------------------------------------------------------------------------------------------------------------------------------------------------------- | Exception stack traces: @@ -56,59 +31,19 @@ Exception stack traces: at org.jetbrains.kotlinx.lincheck_test.representation.ClocksWithExceptionsInOutputTest.operation2(ClocksWithExceptionsInOutputTest.kt:34) Detailed trace: -| --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | -| Thread 1 | Thread 2 | -| --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | -| operation2() | | -| canEnterForbiddenSection.READ: false at ClocksWithExceptionsInOutputTest.operation2(ClocksWithExceptionsInOutputTest.kt:34) | | -| result: void | | -| operation1() | | -| canEnterForbiddenSection.WRITE(true) at ClocksWithExceptionsInOutputTest.operation1(ClocksWithExceptionsInOutputTest.kt:29) | | -| canEnterForbiddenSection.WRITE(false) at ClocksWithExceptionsInOutputTest.operation1(ClocksWithExceptionsInOutputTest.kt:30) | | -| result: void | | -| operation1() | | -| canEnterForbiddenSection.WRITE(true) at ClocksWithExceptionsInOutputTest.operation1(ClocksWithExceptionsInOutputTest.kt:29) | | -| canEnterForbiddenSection.WRITE(false) at ClocksWithExceptionsInOutputTest.operation1(ClocksWithExceptionsInOutputTest.kt:30) | | -| result: void | | -| operation2() | | -| canEnterForbiddenSection.READ: false at ClocksWithExceptionsInOutputTest.operation2(ClocksWithExceptionsInOutputTest.kt:34) | | -| result: void | | -| operation2() | | -| canEnterForbiddenSection.READ: false at ClocksWithExceptionsInOutputTest.operation2(ClocksWithExceptionsInOutputTest.kt:34) | | -| result: void | | -| operation1() | | -| canEnterForbiddenSection.WRITE(true) at ClocksWithExceptionsInOutputTest.operation1(ClocksWithExceptionsInOutputTest.kt:29) | | -| canEnterForbiddenSection.WRITE(false) at ClocksWithExceptionsInOutputTest.operation1(ClocksWithExceptionsInOutputTest.kt:30) | | -| result: void | | -| operation1() | | -| canEnterForbiddenSection.WRITE(true) at ClocksWithExceptionsInOutputTest.operation1(ClocksWithExceptionsInOutputTest.kt:29) | | -| switch | | -| | operation2(): IllegalStateException #1 | -| | canEnterForbiddenSection.READ: true at ClocksWithExceptionsInOutputTest.operation2(ClocksWithExceptionsInOutputTest.kt:34) | -| | result: IllegalStateException #1 | -| | operation1() | -| | canEnterForbiddenSection.WRITE(true) at ClocksWithExceptionsInOutputTest.operation1(ClocksWithExceptionsInOutputTest.kt:29) | -| | canEnterForbiddenSection.WRITE(false) at ClocksWithExceptionsInOutputTest.operation1(ClocksWithExceptionsInOutputTest.kt:30) | -| | result: void | -| canEnterForbiddenSection.WRITE(false) at ClocksWithExceptionsInOutputTest.operation1(ClocksWithExceptionsInOutputTest.kt:30) | | -| result: void | | -| operation1() | | -| canEnterForbiddenSection.WRITE(true) at ClocksWithExceptionsInOutputTest.operation1(ClocksWithExceptionsInOutputTest.kt:29) | | -| canEnterForbiddenSection.WRITE(false) at ClocksWithExceptionsInOutputTest.operation1(ClocksWithExceptionsInOutputTest.kt:30) | | -| result: void | | -| operation1() | | -| canEnterForbiddenSection.WRITE(true) at ClocksWithExceptionsInOutputTest.operation1(ClocksWithExceptionsInOutputTest.kt:29) | | -| canEnterForbiddenSection.WRITE(false) at ClocksWithExceptionsInOutputTest.operation1(ClocksWithExceptionsInOutputTest.kt:30) | | -| result: void | | -| operation1() | | -| canEnterForbiddenSection.WRITE(true) at ClocksWithExceptionsInOutputTest.operation1(ClocksWithExceptionsInOutputTest.kt:29) | | -| canEnterForbiddenSection.WRITE(false) at ClocksWithExceptionsInOutputTest.operation1(ClocksWithExceptionsInOutputTest.kt:30) | | -| result: void | | -| operation2() | | -| canEnterForbiddenSection.READ: false at ClocksWithExceptionsInOutputTest.operation2(ClocksWithExceptionsInOutputTest.kt:34) | | -| result: void | | -| operation1() | | -| canEnterForbiddenSection.WRITE(true) at ClocksWithExceptionsInOutputTest.operation1(ClocksWithExceptionsInOutputTest.kt:29) | | -| canEnterForbiddenSection.WRITE(false) at ClocksWithExceptionsInOutputTest.operation1(ClocksWithExceptionsInOutputTest.kt:30) | | -| result: void | | -| --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | +| ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | +| Thread 1 | Thread 2 | +| ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | +| operation1() | | +| canEnterForbiddenSection.WRITE(true) at ClocksWithExceptionsInOutputTest.operation1(ClocksWithExceptionsInOutputTest.kt:29) | | +| canEnterForbiddenSection.WRITE(false) at ClocksWithExceptionsInOutputTest.operation1(ClocksWithExceptionsInOutputTest.kt:30) | | +| result: void | | +| operation1() | | +| canEnterForbiddenSection.WRITE(true) at ClocksWithExceptionsInOutputTest.operation1(ClocksWithExceptionsInOutputTest.kt:29) | | +| switch | | +| | operation2(): IllegalStateException #1 | +| | canEnterForbiddenSection.READ: true at ClocksWithExceptionsInOutputTest.operation2(ClocksWithExceptionsInOutputTest.kt:34) | +| | result: IllegalStateException #1 | +| canEnterForbiddenSection.WRITE(false) at ClocksWithExceptionsInOutputTest.operation1(ClocksWithExceptionsInOutputTest.kt:30) | | +| result: void | | +| ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | diff --git a/src/jvm/test/resources/expected_logs/infinite_spin_loop_events_cut.txt b/src/jvm/test/resources/expected_logs/infinite_spin_loop_events_cut.txt index 2e70f8a83..8d2e4a287 100644 --- a/src/jvm/test/resources/expected_logs/infinite_spin_loop_events_cut.txt +++ b/src/jvm/test/resources/expected_logs/infinite_spin_loop_events_cut.txt @@ -23,103 +23,103 @@ The following interleaving leads to the error: -| --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | -| Thread 1 | Thread 2 | -| --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | -| one() | | -| one() | | -| one() | | -| one() | | -| two() | | -| | two() | -| | two() | -| | two() | -| | one() | -| | compareAndSet(false,true): true at AbstractSpinLivelockTest.one(SpinlockEventsCutTests.kt:135) | -| | compareAndSet(false,true): true at AbstractSpinLivelockTest.one(SpinlockEventsCutTests.kt:138) | -| | switch | -| two() | | -| compareAndSet(false,true): false at AbstractSpinLivelockTest.two(SpinlockEventsCutTests.kt:149) | | -| meaninglessActions() at AbstractSpinLivelockTest.two(SpinlockEventsCutTests.kt:150) | | -| /* The following events repeat infinitely: */ | | -| get(): false at SpinlockEventsCutInfiniteLoopTest.meaninglessActions(SpinlockEventsCutTests.kt:87) | | -| set(true) at SpinlockEventsCutInfiniteLoopTest.meaninglessActions(SpinlockEventsCutTests.kt:88) | | -| switch (reason: active lock detected) | | -| | set(false) at AbstractSpinLivelockTest.one(SpinlockEventsCutTests.kt:141) | -| | set(false) at AbstractSpinLivelockTest.one(SpinlockEventsCutTests.kt:142) | -| | one() | -| /* The following events repeat infinitely: */ | | -| get(): true at SpinlockEventsCutInfiniteLoopTest.meaninglessActions(SpinlockEventsCutTests.kt:87) | | -| set(false) at SpinlockEventsCutInfiniteLoopTest.meaninglessActions(SpinlockEventsCutTests.kt:88) | | -| switch (reason: active lock detected) | | -| --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | +| ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | +| Thread 1 | Thread 2 | +| ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | +| one() | | +| one() | | +| one() | | +| one() | | +| two() | | +| | two() | +| | two() | +| | two() | +| | one() | +| | compareAndSet(false,true): true at AbstractSpinLivelockTest.one(SpinlockEventsCutTests.kt:148) | +| | compareAndSet(false,true): true at AbstractSpinLivelockTest.one(SpinlockEventsCutTests.kt:151) | +| | switch | +| two() | | +| compareAndSet(false,true): false at AbstractSpinLivelockTest.two(SpinlockEventsCutTests.kt:162) | | +| meaninglessActions() at AbstractSpinLivelockTest.two(SpinlockEventsCutTests.kt:163) | | +| /* The following events repeat infinitely: */ | | +| get(): false at SpinlockEventsCutInfiniteLoopTest.meaninglessActions(SpinlockEventsCutTests.kt:100) | | +| set(true) at SpinlockEventsCutInfiniteLoopTest.meaninglessActions(SpinlockEventsCutTests.kt:101) | | +| switch (reason: active lock detected) | | +| | set(false) at AbstractSpinLivelockTest.one(SpinlockEventsCutTests.kt:154) | +| | set(false) at AbstractSpinLivelockTest.one(SpinlockEventsCutTests.kt:155) | +| | one() | +| /* The following events repeat infinitely: */ | | +| get(): true at SpinlockEventsCutInfiniteLoopTest.meaninglessActions(SpinlockEventsCutTests.kt:100) | | +| set(false) at SpinlockEventsCutInfiniteLoopTest.meaninglessActions(SpinlockEventsCutTests.kt:101) | | +| switch (reason: active lock detected) | | +| ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | All unfinished threads are in deadlock Detailed trace: -| --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | -| Thread 1 | Thread 2 | -| --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | -| one() | | -| compareAndSet(false,true): true at AbstractSpinLivelockTest.one(SpinlockEventsCutTests.kt:135) | | -| compareAndSet(false,true): true at AbstractSpinLivelockTest.one(SpinlockEventsCutTests.kt:138) | | -| set(false) at AbstractSpinLivelockTest.one(SpinlockEventsCutTests.kt:141) | | -| set(false) at AbstractSpinLivelockTest.one(SpinlockEventsCutTests.kt:142) | | -| one() | | -| compareAndSet(false,true): true at AbstractSpinLivelockTest.one(SpinlockEventsCutTests.kt:135) | | -| compareAndSet(false,true): true at AbstractSpinLivelockTest.one(SpinlockEventsCutTests.kt:138) | | -| set(false) at AbstractSpinLivelockTest.one(SpinlockEventsCutTests.kt:141) | | -| set(false) at AbstractSpinLivelockTest.one(SpinlockEventsCutTests.kt:142) | | -| one() | | -| compareAndSet(false,true): true at AbstractSpinLivelockTest.one(SpinlockEventsCutTests.kt:135) | | -| compareAndSet(false,true): true at AbstractSpinLivelockTest.one(SpinlockEventsCutTests.kt:138) | | -| set(false) at AbstractSpinLivelockTest.one(SpinlockEventsCutTests.kt:141) | | -| set(false) at AbstractSpinLivelockTest.one(SpinlockEventsCutTests.kt:142) | | -| one() | | -| compareAndSet(false,true): true at AbstractSpinLivelockTest.one(SpinlockEventsCutTests.kt:135) | | -| compareAndSet(false,true): true at AbstractSpinLivelockTest.one(SpinlockEventsCutTests.kt:138) | | -| set(false) at AbstractSpinLivelockTest.one(SpinlockEventsCutTests.kt:141) | | -| set(false) at AbstractSpinLivelockTest.one(SpinlockEventsCutTests.kt:142) | | -| two() | | -| compareAndSet(false,true): true at AbstractSpinLivelockTest.two(SpinlockEventsCutTests.kt:149) | | -| compareAndSet(false,true): true at AbstractSpinLivelockTest.two(SpinlockEventsCutTests.kt:152) | | -| set(false) at AbstractSpinLivelockTest.two(SpinlockEventsCutTests.kt:155) | | -| set(false) at AbstractSpinLivelockTest.two(SpinlockEventsCutTests.kt:156) | | -| | two() | -| | compareAndSet(false,true): true at AbstractSpinLivelockTest.two(SpinlockEventsCutTests.kt:149) | -| | compareAndSet(false,true): true at AbstractSpinLivelockTest.two(SpinlockEventsCutTests.kt:152) | -| | set(false) at AbstractSpinLivelockTest.two(SpinlockEventsCutTests.kt:155) | -| | set(false) at AbstractSpinLivelockTest.two(SpinlockEventsCutTests.kt:156) | -| | two() | -| | compareAndSet(false,true): true at AbstractSpinLivelockTest.two(SpinlockEventsCutTests.kt:149) | -| | compareAndSet(false,true): true at AbstractSpinLivelockTest.two(SpinlockEventsCutTests.kt:152) | -| | set(false) at AbstractSpinLivelockTest.two(SpinlockEventsCutTests.kt:155) | -| | set(false) at AbstractSpinLivelockTest.two(SpinlockEventsCutTests.kt:156) | -| | two() | -| | compareAndSet(false,true): true at AbstractSpinLivelockTest.two(SpinlockEventsCutTests.kt:149) | -| | compareAndSet(false,true): true at AbstractSpinLivelockTest.two(SpinlockEventsCutTests.kt:152) | -| | set(false) at AbstractSpinLivelockTest.two(SpinlockEventsCutTests.kt:155) | -| | set(false) at AbstractSpinLivelockTest.two(SpinlockEventsCutTests.kt:156) | -| | one() | -| | compareAndSet(false,true): true at AbstractSpinLivelockTest.one(SpinlockEventsCutTests.kt:135) | -| | compareAndSet(false,true): true at AbstractSpinLivelockTest.one(SpinlockEventsCutTests.kt:138) | -| | switch | -| two() | | -| compareAndSet(false,true): false at AbstractSpinLivelockTest.two(SpinlockEventsCutTests.kt:149) | | -| meaninglessActions() at AbstractSpinLivelockTest.two(SpinlockEventsCutTests.kt:150) | | -| /* The following events repeat infinitely: */ | | -| get(): false at SpinlockEventsCutInfiniteLoopTest.meaninglessActions(SpinlockEventsCutTests.kt:87) | | -| set(true) at SpinlockEventsCutInfiniteLoopTest.meaninglessActions(SpinlockEventsCutTests.kt:88) | | -| switch (reason: active lock detected) | | -| | set(false) at AbstractSpinLivelockTest.one(SpinlockEventsCutTests.kt:141) | -| | set(false) at AbstractSpinLivelockTest.one(SpinlockEventsCutTests.kt:142) | -| | one() | -| | compareAndSet(false,true): true at AbstractSpinLivelockTest.one(SpinlockEventsCutTests.kt:135) | -| | compareAndSet(false,true): true at AbstractSpinLivelockTest.one(SpinlockEventsCutTests.kt:138) | -| | set(false) at AbstractSpinLivelockTest.one(SpinlockEventsCutTests.kt:141) | -| | set(false) at AbstractSpinLivelockTest.one(SpinlockEventsCutTests.kt:142) | -| /* The following events repeat infinitely: */ | | -| get(): true at SpinlockEventsCutInfiniteLoopTest.meaninglessActions(SpinlockEventsCutTests.kt:87) | | -| set(false) at SpinlockEventsCutInfiniteLoopTest.meaninglessActions(SpinlockEventsCutTests.kt:88) | | -| switch (reason: active lock detected) | | -| --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | +| ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | +| Thread 1 | Thread 2 | +| ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | +| one() | | +| compareAndSet(false,true): true at AbstractSpinLivelockTest.one(SpinlockEventsCutTests.kt:148) | | +| compareAndSet(false,true): true at AbstractSpinLivelockTest.one(SpinlockEventsCutTests.kt:151) | | +| set(false) at AbstractSpinLivelockTest.one(SpinlockEventsCutTests.kt:154) | | +| set(false) at AbstractSpinLivelockTest.one(SpinlockEventsCutTests.kt:155) | | +| one() | | +| compareAndSet(false,true): true at AbstractSpinLivelockTest.one(SpinlockEventsCutTests.kt:148) | | +| compareAndSet(false,true): true at AbstractSpinLivelockTest.one(SpinlockEventsCutTests.kt:151) | | +| set(false) at AbstractSpinLivelockTest.one(SpinlockEventsCutTests.kt:154) | | +| set(false) at AbstractSpinLivelockTest.one(SpinlockEventsCutTests.kt:155) | | +| one() | | +| compareAndSet(false,true): true at AbstractSpinLivelockTest.one(SpinlockEventsCutTests.kt:148) | | +| compareAndSet(false,true): true at AbstractSpinLivelockTest.one(SpinlockEventsCutTests.kt:151) | | +| set(false) at AbstractSpinLivelockTest.one(SpinlockEventsCutTests.kt:154) | | +| set(false) at AbstractSpinLivelockTest.one(SpinlockEventsCutTests.kt:155) | | +| one() | | +| compareAndSet(false,true): true at AbstractSpinLivelockTest.one(SpinlockEventsCutTests.kt:148) | | +| compareAndSet(false,true): true at AbstractSpinLivelockTest.one(SpinlockEventsCutTests.kt:151) | | +| set(false) at AbstractSpinLivelockTest.one(SpinlockEventsCutTests.kt:154) | | +| set(false) at AbstractSpinLivelockTest.one(SpinlockEventsCutTests.kt:155) | | +| two() | | +| compareAndSet(false,true): true at AbstractSpinLivelockTest.two(SpinlockEventsCutTests.kt:162) | | +| compareAndSet(false,true): true at AbstractSpinLivelockTest.two(SpinlockEventsCutTests.kt:165) | | +| set(false) at AbstractSpinLivelockTest.two(SpinlockEventsCutTests.kt:168) | | +| set(false) at AbstractSpinLivelockTest.two(SpinlockEventsCutTests.kt:169) | | +| | two() | +| | compareAndSet(false,true): true at AbstractSpinLivelockTest.two(SpinlockEventsCutTests.kt:162) | +| | compareAndSet(false,true): true at AbstractSpinLivelockTest.two(SpinlockEventsCutTests.kt:165) | +| | set(false) at AbstractSpinLivelockTest.two(SpinlockEventsCutTests.kt:168) | +| | set(false) at AbstractSpinLivelockTest.two(SpinlockEventsCutTests.kt:169) | +| | two() | +| | compareAndSet(false,true): true at AbstractSpinLivelockTest.two(SpinlockEventsCutTests.kt:162) | +| | compareAndSet(false,true): true at AbstractSpinLivelockTest.two(SpinlockEventsCutTests.kt:165) | +| | set(false) at AbstractSpinLivelockTest.two(SpinlockEventsCutTests.kt:168) | +| | set(false) at AbstractSpinLivelockTest.two(SpinlockEventsCutTests.kt:169) | +| | two() | +| | compareAndSet(false,true): true at AbstractSpinLivelockTest.two(SpinlockEventsCutTests.kt:162) | +| | compareAndSet(false,true): true at AbstractSpinLivelockTest.two(SpinlockEventsCutTests.kt:165) | +| | set(false) at AbstractSpinLivelockTest.two(SpinlockEventsCutTests.kt:168) | +| | set(false) at AbstractSpinLivelockTest.two(SpinlockEventsCutTests.kt:169) | +| | one() | +| | compareAndSet(false,true): true at AbstractSpinLivelockTest.one(SpinlockEventsCutTests.kt:148) | +| | compareAndSet(false,true): true at AbstractSpinLivelockTest.one(SpinlockEventsCutTests.kt:151) | +| | switch | +| two() | | +| compareAndSet(false,true): false at AbstractSpinLivelockTest.two(SpinlockEventsCutTests.kt:162) | | +| meaninglessActions() at AbstractSpinLivelockTest.two(SpinlockEventsCutTests.kt:163) | | +| /* The following events repeat infinitely: */ | | +| get(): false at SpinlockEventsCutInfiniteLoopTest.meaninglessActions(SpinlockEventsCutTests.kt:100) | | +| set(true) at SpinlockEventsCutInfiniteLoopTest.meaninglessActions(SpinlockEventsCutTests.kt:101) | | +| switch (reason: active lock detected) | | +| | set(false) at AbstractSpinLivelockTest.one(SpinlockEventsCutTests.kt:154) | +| | set(false) at AbstractSpinLivelockTest.one(SpinlockEventsCutTests.kt:155) | +| | one() | +| | compareAndSet(false,true): true at AbstractSpinLivelockTest.one(SpinlockEventsCutTests.kt:148) | +| | compareAndSet(false,true): true at AbstractSpinLivelockTest.one(SpinlockEventsCutTests.kt:151) | +| | set(false) at AbstractSpinLivelockTest.one(SpinlockEventsCutTests.kt:154) | +| | set(false) at AbstractSpinLivelockTest.one(SpinlockEventsCutTests.kt:155) | +| /* The following events repeat infinitely: */ | | +| get(): true at SpinlockEventsCutInfiniteLoopTest.meaninglessActions(SpinlockEventsCutTests.kt:100) | | +| set(false) at SpinlockEventsCutInfiniteLoopTest.meaninglessActions(SpinlockEventsCutTests.kt:101) | | +| switch (reason: active lock detected) | | +| ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | All unfinished threads are in deadlock diff --git a/src/jvm/test/resources/expected_logs/trace_reporting_empty.txt b/src/jvm/test/resources/expected_logs/trace_reporting_empty.txt index 26a0a98de..e0034c15c 100644 --- a/src/jvm/test/resources/expected_logs/trace_reporting_empty.txt +++ b/src/jvm/test/resources/expected_logs/trace_reporting_empty.txt @@ -18,7 +18,7 @@ The following interleaving leads to the error: Exception stack traces: #1: kotlin.NotImplementedError: An operation is not implemented. - at org.jetbrains.kotlinx.lincheck_test.representation.TraceReportingTest.notImplemented(TraceReportingTest.kt:123) + at org.jetbrains.kotlinx.lincheck_test.representation.TraceReportingTest.notImplemented(TraceReportingTest.kt:126) Detailed trace: | ---------------------------------------- |