From 26f9906107715e7553ca7f612ff1937fb616cbd6 Mon Sep 17 00:00:00 2001 From: Evgenii Moiseenko Date: Thu, 1 Jun 2023 15:34:21 +0200 Subject: [PATCH] check planning constraints individually for model checking and stress strategy runs Signed-off-by: Evgenii Moiseenko --- .../kotlinx/lincheck/LincheckOptions.kt | 303 +++++++++++------- .../org/jetbrains/kotlinx/lincheck/Planner.kt | 28 +- .../jetbrains/kotlinx/lincheck/RunTracker.kt | 121 +++++++ .../jetbrains/kotlinx/lincheck/Statistics.kt | 45 ++- .../kotlinx/lincheck/strategy/Strategy.kt | 28 +- .../lincheck/test/AbstractLincheckTest.kt | 53 +-- 6 files changed, 390 insertions(+), 188 deletions(-) create mode 100644 src/jvm/main/org/jetbrains/kotlinx/lincheck/RunTracker.kt diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/LincheckOptions.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/LincheckOptions.kt index 29b5c06b1..153b37ad4 100644 --- a/src/jvm/main/org/jetbrains/kotlinx/lincheck/LincheckOptions.kt +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/LincheckOptions.kt @@ -26,6 +26,7 @@ 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.* @@ -76,7 +77,7 @@ interface LincheckOptions { * * @return [LincheckFailure] if some bug has been found. */ - fun runTests(testClass: Class<*>): LincheckTestingResult + fun runTests(testClass: Class<*>, tracker: RunTracker? = null): LincheckFailure? } /** @@ -96,7 +97,7 @@ fun LincheckOptions(configurationBlock: LincheckOptions.() -> Unit): LincheckOpt * @return [LincheckFailure] if some bug has been found. */ fun LincheckOptions.checkImpl(testClass: Class<*>): LincheckFailure? = - runTests(testClass).failure + runTests(testClass) /** * Runs the Lincheck test on the specified class. @@ -116,29 +117,44 @@ fun LincheckOptions.addCustomScenario(invocations: Int? = null, scenarioBuilder: fun LincheckOptions.check(testClass: KClass<*>) = check(testClass.java) // For internal tests only. -internal enum class LincheckMode { +enum class LincheckMode { Stress, ModelChecking, Hybrid } -internal class LincheckOptionsImpl : LincheckOptions { - override var testingTimeInSeconds = DEFAULT_TESTING_TIME - override var maxThreads = DEFAULT_MAX_THREADS - override var maxOperationsInThread = DEFAULT_MAX_OPERATIONS - override var verifier: Class = LinearizabilityVerifier::class.java - override var sequentialImplementation: Class<*>? = null - override var checkObstructionFreedom: Boolean = false - - internal var mode = LincheckMode.Hybrid - internal var minimizeFailedScenario = true - internal var generateRandomScenarios = true - internal var generateBeforeAndAfterParts = true - - internal var minThreads = DEFAULT_MIN_THREADS - internal var minOperationsInThread = DEFAULT_MIN_OPERATIONS +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 = (mode == LincheckMode.Hybrid), +) : LincheckOptions { + + override var testingTimeInSeconds: Long + get() = (testingTimeMs.toDouble() / 1000L).roundToLong() + set(value) { + testingTimeMs = value * 1000L + } - internal var invocationTimeoutMs = CTestConfiguration.DEFAULT_TIMEOUT_MS + private val shouldRunCustomScenarios: Boolean + get() = customScenariosOptions.size > 0 - internal val customScenariosOptions = mutableListOf() + private val shouldRunRandomScenarios: Boolean + get() = generateRandomScenarios private val shouldRunStressStrategy: Boolean get() = (mode == LincheckMode.Stress) || (mode == LincheckMode.Hybrid) @@ -146,9 +162,6 @@ internal class LincheckOptionsImpl : LincheckOptions { private val shouldRunModelCheckingStrategy: Boolean get() = (mode == LincheckMode.ModelChecking) || (mode == LincheckMode.Hybrid) - private val testingTimeMs: Long - get() = testingTimeInSeconds * 1000 - private val stressTestingTimeMs: Long get() = when (mode) { LincheckMode.Hybrid -> round(testingTimeMs * STRATEGY_SWITCH_THRESHOLD).toLong() @@ -172,106 +185,126 @@ internal class LincheckOptionsImpl : LincheckOptions { ) } - override fun runTests(testClass: Class<*>): LincheckTestingResult { - var failure: LincheckFailure? = null - var summaryStatistics = Statistics.empty + override fun runTests(testClass: Class<*>, tracker: RunTracker?): LincheckFailure? { val testStructure = CTestStructure.getFromTestClass(testClass) - if (customScenariosOptions.size > 0 && failure == null) { - val result = checkCustomScenarios(testClass, testStructure) - failure = result.failure - summaryStatistics += result.statistics + if (customScenariosOptions.size > 0) { + runCustomScenarios(testClass, testStructure, tracker)?.let { return it } } - if (generateRandomScenarios && failure == null) { - val result = checkRandomScenarios(testClass, testStructure) - failure = result.failure - summaryStatistics += result.statistics + if (generateRandomScenarios) { + runRandomScenarios(testClass, testStructure, tracker)?.let { return it } } - return LincheckTestingResult(failure, summaryStatistics) + return null } - private fun checkCustomScenarios(testClass: Class<*>, testStructure: CTestStructure): LincheckTestingResult { - var failure: LincheckFailure? = null - val stressStatistics = StatisticsTracker() - val modeCheckingStatistics = StatisticsTracker() - if (shouldRunStressStrategy && failure == null) { - checkInMode(LincheckMode.Stress, testClass, testStructure, - CustomScenariosPlanner(customScenariosOptions), - stressStatistics - )?.let { failure = it } + private fun runCustomScenarios(testClass: Class<*>, testStructure: CTestStructure, tracker: RunTracker?): LincheckFailure? { + if (shouldRunStressStrategy) { + val stressOptions = copy( + mode = LincheckMode.Stress, + generateRandomScenarios = false, + tryReproduceTrace = tryReproduceTrace + ) + stressOptions.runImpl(testClass, testStructure, tracker)?.let { + return it + } } - if (shouldRunModelCheckingStrategy && failure == null) { - checkInMode(LincheckMode.ModelChecking, testClass, testStructure, - CustomScenariosPlanner(customScenariosOptions), - modeCheckingStatistics - )?.let { failure = it } + if (shouldRunModelCheckingStrategy) { + val modelCheckingOptions = copy( + mode = LincheckMode.ModelChecking, + generateRandomScenarios = false, + tryReproduceTrace = tryReproduceTrace + ) + modelCheckingOptions.runImpl(testClass, testStructure, tracker)?.let { + return it + } } - return LincheckTestingResult(failure, stressStatistics + modeCheckingStatistics) + return null } - private fun checkRandomScenarios(testClass: Class<*>, testStructure: CTestStructure): LincheckTestingResult { - var failure: LincheckFailure? = null - val stressStatistics = StatisticsTracker() - val modeCheckingStatistics = StatisticsTracker() - if (shouldRunStressStrategy && failure == null) { - checkInMode(LincheckMode.Stress, testClass, testStructure, - createRandomScenariosPlanner(LincheckMode.Stress, testStructure, stressStatistics), - stressStatistics - )?.let { failure = it } + private fun runRandomScenarios(testClass: Class<*>, testStructure: CTestStructure, tracker: RunTracker?): LincheckFailure? { + if (shouldRunStressStrategy) { + val stressOptions = copy( + mode = LincheckMode.Stress, + testingTimeMs = stressTestingTimeMs, + customScenariosOptions = mutableListOf(), + tryReproduceTrace = tryReproduceTrace + ) + stressOptions.runImpl(testClass, testStructure, tracker)?.let { + return it + } } - if (shouldRunModelCheckingStrategy && failure == null) { - checkInMode(LincheckMode.ModelChecking, testClass, testStructure, - createRandomScenariosPlanner(LincheckMode.ModelChecking, testStructure, modeCheckingStatistics), - modeCheckingStatistics - )?.let { failure = it } + if (shouldRunModelCheckingStrategy) { + val modelCheckingOptions = copy( + mode = LincheckMode.ModelChecking, + testingTimeMs = modelCheckingTimeMs, + customScenariosOptions = mutableListOf(), + tryReproduceTrace = tryReproduceTrace + ) + modelCheckingOptions.runImpl(testClass, testStructure, tracker)?.let { + return it + } } - return LincheckTestingResult(failure, stressStatistics + modeCheckingStatistics) + return null } - private fun checkInMode( - mode: LincheckMode, - testClass: Class<*>, - testStructure: CTestStructure, - planner: Planner, - statisticsTracker: StatisticsTracker? = null - ): LincheckFailure? { - val reporter = Reporter(DEFAULT_LOG_LEVEL) - var verifier = createVerifier(testClass) - var failure = planner.runIterations(statisticsTracker) { i, scenario, invocationsPlanner -> - // 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 ((i + 1) % LinChecker.VERIFIER_REFRESH_CYCLE == 0) { - verifier = createVerifier(testClass) - } - scenario.validate() - reporter.logIteration(i + 1, scenario) - scenario.run(mode, testClass, testStructure, verifier, invocationsPlanner, statisticsTracker).also { - reporter.logIterationStatistics(planner, statisticsTracker) + 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}-${hashCode()}" + } + + private fun runImpl(testClass: Class<*>, testStructure: CTestStructure, customTracker: RunTracker? = null): LincheckFailure? { + check(mode in listOf(LincheckMode.Stress, LincheckMode.ModelChecking)) + check(shouldRunCustomScenarios xor shouldRunRandomScenarios) + return customTracker.trackRun(getRunName(testClass), this) { + val statisticsTracker = StatisticsTracker() + val reporterManager = createReporterManager(statisticsTracker) + val verifierManager = createVerifierManager(testClass) + val planner = when { + shouldRunCustomScenarios -> CustomScenariosPlanner(customScenariosOptions) + shouldRunRandomScenarios -> createRandomScenariosPlanner(mode, testStructure, statisticsTracker) + else -> throw IllegalStateException() } - } ?: return null - if (planner.minimizeFailedScenario) { - failure = failure.minimize(reporter) { - it.run(mode, testClass, testStructure, - createVerifier(testClass), - FixedInvocationsPlanner(MINIMIZATION_INVOCATIONS_COUNT) + 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) { + failure = failure.minimize(reporterManager.reporter) { + it.run( + mode, testClass, testStructure, + createVerifier(testClass), + FixedInvocationsPlanner(MINIMIZATION_INVOCATIONS_COUNT) + ) + } } - } - if (this.mode == LincheckMode.Hybrid && mode == LincheckMode.Stress) { - // 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 + // 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) } - reporter.logFailedIteration(failure) - return failure } private fun ExecutionScenario.run( @@ -282,17 +315,26 @@ internal class LincheckOptionsImpl : LincheckOptions { planner: InvocationsPlanner, statisticsTracker: StatisticsTracker? = null, ): LincheckFailure? = - createStrategy(currentMode, testClass, this, testStructure).use { + createStrategy(currentMode, testClass, testStructure, this).use { it.run(verifier, planner, statisticsTracker) } - private fun Reporter.logIterationStatistics(planner: Planner, statisticsTracker: StatisticsTracker?) { - statisticsTracker ?: return - logIterationStatistics( - statisticsTracker.currentIterationInvocationsCount, - statisticsTracker.currentIterationRunningTimeNano, - (planner.iterationsPlanner as? AdaptivePlanner)?.remainingTimeNano, - ) + private fun createReporterManager(statistics: Statistics?) = 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?) { + statistics?.apply { + reporter.logIterationStatistics( + iterationsInvocationsCount[iteration], + iterationsRunningTimeNano[iteration], + null // TODO + ) + } + } } private fun createRandomScenariosPlanner(mode: LincheckMode, testStructure: CTestStructure, statisticsTracker: StatisticsTracker): Planner = @@ -303,14 +345,9 @@ internal class LincheckOptionsImpl : LincheckOptions { maxThreads = maxThreads, maxOperations = maxOperationsInThread, generateBeforeAndAfterParts = generateBeforeAndAfterParts, - minimizeFailedScenario = minimizeFailedScenario, scenarioGenerator = RandomExecutionGenerator(testStructure, testStructure.randomProvider), statisticsTracker = statisticsTracker, - testingTimeMs = when (mode) { - LincheckMode.Stress -> stressTestingTimeMs - LincheckMode.ModelChecking -> modelCheckingTimeMs - else -> throw IllegalArgumentException() - }, + testingTimeMs = testingTimeMs, ) private fun createVerifier(testClass: Class<*>) = verifier @@ -319,11 +356,35 @@ internal class LincheckOptionsImpl : LincheckOptions { 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<*>, - scenario: ExecutionScenario, testStructure: CTestStructure, + scenario: ExecutionScenario, ): Strategy = when (mode) { LincheckMode.Stress -> StressStrategy(testClass, scenario, @@ -351,7 +412,7 @@ internal class CustomScenarioOptions( val invocations: Int, ) -private const val DEFAULT_TESTING_TIME = 5L +private const val DEFAULT_TESTING_TIME_MS = 5000L private const val DEFAULT_MIN_THREADS = 2 private const val DEFAULT_MAX_THREADS = 4 private const val DEFAULT_MIN_OPERATIONS = 2 diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/Planner.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/Planner.kt index 6c307a0b8..ba1e0ab9f 100644 --- a/src/jvm/main/org/jetbrains/kotlinx/lincheck/Planner.kt +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/Planner.kt @@ -23,13 +23,14 @@ 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 - val minimizeFailedScenario: Boolean } interface IterationsPlanner { @@ -41,16 +42,28 @@ interface InvocationsPlanner { } fun Planner.runIterations( - statisticsTracker: StatisticsTracker? = null, - block: (Int, ExecutionScenario, InvocationsPlanner) -> LincheckFailure? + tracker: RunTracker? = null, + factory: (ExecutionScenario) -> Pair, ): LincheckFailure? { scenarios.forEachIndexed { i, scenario -> if (!iterationsPlanner.shouldDoNextIteration(i)) return null - statisticsTracker.trackIteration { - block(i, scenario, invocationsPlanner)?.let { - return it + tracker.trackIteration(i, scenario) { + val (strategy, verifier) = factory(scenario) + strategy.use { + var invocation = 0 + while (invocationsPlanner.shouldDoNextInvocation(invocation)) { + tracker.trackInvocation(invocation) { + it.runInvocation(verifier) + }?.let { + return@trackIteration it + } + invocation++ + } } + return@trackIteration null + }?.let { + return it } } return null @@ -67,8 +80,6 @@ internal class CustomScenariosPlanner( override var invocationsPlanner = FixedInvocationsPlanner(0) private set - override val minimizeFailedScenario: Boolean = false - override fun shouldDoNextIteration(iteration: Int): Boolean { invocationsPlanner = FixedInvocationsPlanner(scenariosOptions[iteration].invocations) return iteration < scenariosOptions.size @@ -84,7 +95,6 @@ internal class RandomScenariosAdaptivePlanner( val minOperations: Int, val maxOperations: Int, val generateBeforeAndAfterParts: Boolean, - override val minimizeFailedScenario: Boolean, scenarioGenerator: ExecutionGenerator, statisticsTracker: StatisticsTracker, ) : Planner { 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..c7017f4be --- /dev/null +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/RunTracker.kt @@ -0,0 +1,121 @@ +/* + * 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, statistics: Statistics? = null) {} + + fun iterationStart(iteration: Int, scenario: ExecutionScenario) {} + fun iterationEnd(iteration: Int, failure: LincheckFailure? = null) {} + + fun invocationStart(invocation: Int) {} + fun invocationEnd(invocation: Int, failure: LincheckFailure? = null) {} +} + +inline fun RunTracker?.trackRun(name: String, options: LincheckOptions, + block: () -> Pair): LincheckFailure? { + this?.runStart(name, options) + try { + val (failure, statistics) = block() + this?.runEnd(name, failure, statistics) + return failure + } catch (exception: Throwable) { + // TODO: once https://github.com/JetBrains/lincheck/issues/170 is implemented, + // we can put `check(false)` here instead + this?.runEnd(name) + throw exception + } +} + +inline fun RunTracker?.trackIteration(iteration: Int, scenario: ExecutionScenario, block: () -> LincheckFailure?): LincheckFailure? { + this?.iterationStart(iteration, scenario) + try { + return block().also { + this?.iterationEnd(iteration, failure = it) + } + } catch (exception: Throwable) { + // TODO: once https://github.com/JetBrains/lincheck/issues/170 is implemented, + // we can put `check(false)` here instead + this?.iterationEnd(iteration) + throw exception + } +} + +inline fun RunTracker?.trackInvocation(invocation: Int, block: () -> LincheckFailure?): LincheckFailure? { + this?.invocationStart(invocation) + try { + return block().also { + this?.invocationEnd(invocation, failure = it) + } + } catch (exception: Throwable) { + // TODO: once https://github.com/JetBrains/lincheck/issues/170 is implemented, + // we can put `check(false)` here instead + this?.invocationEnd(invocation) + throw 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?, statistics: Statistics?) { + for (tracker in trackers) { + tracker.runEnd(name, failure, statistics) + } + } + + override fun iterationStart(iteration: Int, scenario: ExecutionScenario) { + for (tracker in trackers) { + tracker.iterationStart(iteration, scenario) + } + } + + override fun iterationEnd(iteration: Int, failure: LincheckFailure?) { + for (tracker in trackers) { + tracker.iterationEnd(iteration, failure) + } + } + + override fun invocationStart(invocation: Int) { + for (tracker in trackers) { + tracker.invocationStart(invocation) + } + } + + override fun invocationEnd(invocation: Int, failure: LincheckFailure?) { + for (tracker in trackers) { + tracker.invocationEnd(invocation, failure) + } + } + + } \ 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 index 00b9f9df6..6dcd11fbc 100644 --- a/src/jvm/main/org/jetbrains/kotlinx/lincheck/Statistics.kt +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/Statistics.kt @@ -20,6 +20,9 @@ package org.jetbrains.kotlinx.lincheck +import org.jetbrains.kotlinx.lincheck.execution.ExecutionScenario +import org.jetbrains.kotlinx.lincheck.strategy.LincheckFailure + interface Statistics { /** @@ -29,11 +32,13 @@ interface Statistics { /** * An array keeping running time of all iterations. + * TODO: refactor to function returning time of i-th iteration */ val iterationsRunningTimeNano: List /** * Array keeping number of invocations executed for each iteration + * TODO: refactor to function returning count of i-th iteration */ val iterationsInvocationsCount: List @@ -82,7 +87,7 @@ fun Statistics.averageInvocationsCount(iteration: Int): Double = fun Statistics.averageInvocationTimeNano(iteration: Int): Double = iterationsRunningTimeNano[iteration] / iterationsInvocationsCount[iteration].toDouble() -class StatisticsTracker : Statistics { +internal class StatisticsTracker : Statistics, RunTracker { override var runningTimeNano: Long = 0 private set @@ -119,43 +124,31 @@ class StatisticsTracker : Statistics { val currentIterationInvocationsCount: Int get() = iterationsInvocationsCount[iteration] - fun iterationStart() { - ++iteration + override fun iterationStart(iteration: Int, scenario: ExecutionScenario) { + check(iteration == this.iteration + 1) + ++this.iteration _iterationsRunningTimeNano.add(0) _iterationsInvocationCount.add(0) } - fun iterationEnd() { + override fun iterationEnd(iteration: Int, failure: LincheckFailure?) { invocation = -1 } - fun invocationStart() { - ++invocation + private var lastInvocationStartTimeNano = -1L + + override fun invocationStart(invocation: Int) { + check(invocation == this.invocation + 1) + ++this.invocation + lastInvocationStartTimeNano = System.nanoTime() } - fun invocationEnd(invocationTimeNano: Long) { + override fun invocationEnd(invocation: Int, failure: LincheckFailure?) { + val invocationTimeNano = System.nanoTime() - lastInvocationStartTimeNano + check(invocationTimeNano >= 0) runningTimeNano += invocationTimeNano _iterationsInvocationCount[iteration] += 1 _iterationsRunningTimeNano[iteration] += invocationTimeNano } -} - -inline fun StatisticsTracker?.trackIteration(block: () -> T): T { - this?.iterationStart() - try { - return block() - } finally { - this?.iterationEnd() - } -} - -inline fun StatisticsTracker?.trackInvocation(block: () -> T): T { - val startTimeNano = System.nanoTime() - this?.invocationStart() - try { - return block() - } finally { - this?.invocationEnd(System.nanoTime() - startTimeNano) - } } \ No newline at end of file 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 fd5eac7d3..274c01a5c 100644 --- a/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/Strategy.kt +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/Strategy.kt @@ -45,24 +45,28 @@ abstract class Strategy protected constructor( throw UnsupportedOperationException("$javaClass strategy does not transform classes") } - fun run(verifier: Verifier, planner: InvocationsPlanner, statistics: StatisticsTracker? = null): LincheckFailure? { + fun run(verifier: Verifier, planner: InvocationsPlanner, tracker: RunTracker? = null): LincheckFailure? { var invocation = 0 - while (planner.shouldDoNextInvocation(invocation++)) { - statistics.trackInvocation { - when (val result = runInvocation()) { - AllInterleavingsStudiedInvocationResult -> return null - is CompletedInvocationResult -> { - if (!verifier.verifyResults(scenario, result.results)) { - return IncorrectResultsFailure(scenario, result.results, result.tryCollectTrace()) - } - } - else -> return result.toLincheckFailure(scenario, result.tryCollectTrace()) - } + while (planner.shouldDoNextInvocation(invocation)) { + tracker.trackInvocation(invocation) { + runInvocation(verifier) + }?.let { + return it } + invocation++ } return null } + fun runInvocation(verifier: Verifier): LincheckFailure? = when (val result = runInvocation()) { + AllInterleavingsStudiedInvocationResult -> null + is CompletedInvocationResult -> + if (!verifier.verifyResults(scenario, result.results)) { + IncorrectResultsFailure(scenario, result.results, result.tryCollectTrace()) + } else null + else -> result.toLincheckFailure(scenario, result.tryCollectTrace()) + } + abstract fun runInvocation(): InvocationResult open fun InvocationResult.tryCollectTrace(): Trace? = null 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 321181bb1..494f7e0ae 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/AbstractLincheckTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/AbstractLincheckTest.kt @@ -54,33 +54,29 @@ abstract class AbstractLincheckTest( }.runTest() private fun LincheckOptions.runTest() { - val result = runTests(this@AbstractLincheckTest::class.java) - val failure = result.failure + 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)" } + checkAdaptivePlanningConstraints() } else { failure.trace?.let { checkTraceHasNoLincheckEvents(it.toString()) } assert(expectedFailures.contains(failure::class)) { "This test has failed with an unexpected error: \n $failure" } } - checkAdaptivePlanningConstraints(result) } - private fun LincheckOptions.checkAdaptivePlanningConstraints(result: LincheckTestingResult) { + private fun LincheckOptions.checkAdaptivePlanningConstraints() { this as LincheckOptionsImpl - // the failure can be detected earlier, thus it is fine if the planning constraints are violated - if (result.failure != null) - return // 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 statistics = result.statistics val randomTestingTimeNano = testingTimeInSeconds * 1_000_000_000 - val runningTimeNano = statistics.runningTimeNano + val runningTimeNano = runStatistics.values.sumOf { it.runningTimeNano } val timeDeltaNano = AdaptivePlanner.TIME_ERROR_MARGIN_NANO // check that the actual running time is close to specified time assert(abs(randomTestingTimeNano - runningTimeNano) < timeDeltaNano) { """ @@ -89,17 +85,19 @@ abstract class AbstractLincheckTest( expected: ${String.format("%.3f", randomTestingTimeNano.toDouble() / 1_000_000_000)} """.trimIndent() } - // check invocations to iterations ratio - val plannedIterations = statistics.iterationsInvocationsCount - if (plannedIterations.isEmpty()) - return - val invocationsRatio = plannedIterations.average() / plannedIterations.size - val expectedRatio = AdaptivePlanner.INVOCATIONS_TO_ITERATIONS_RATIO.toDouble() - assert(abs(invocationsRatio - expectedRatio) < expectedRatio * 0.1) { """ - Invocations to iterations ratio differs from expected: - actual: ${String.format("%.3f", invocationsRatio)} - expected: $expectedRatio - """.trimIndent() + // check invocations to iterations ratio (per each strategy run) + for (statistics in runStatistics.values) { + val plannedIterations = statistics.iterationsInvocationsCount + if (plannedIterations.isEmpty()) + return + val invocationsRatio = plannedIterations.average() / plannedIterations.size + val expectedRatio = AdaptivePlanner.INVOCATIONS_TO_ITERATIONS_RATIO.toDouble() + assert(abs(invocationsRatio - expectedRatio) < expectedRatio * 0.1) { """ + Invocations to iterations ratio differs from expected: + actual: ${String.format("%.3f", invocationsRatio)} + expected: $expectedRatio + """.trimIndent() + } } } @@ -115,6 +113,21 @@ abstract class AbstractLincheckTest( 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?, statistics: Statistics?) { + check(statistics != null) + runStatistics[name] = statistics + } + } + } private const val TIMEOUT = 100_000L