Skip to content

Commit

Permalink
LincheckOptions, testingTime option, statistics tracking and adaptive…
Browse files Browse the repository at this point in the history 
… planning
  • Loading branch information
@eupp
eupp committed Aug 17, 2023
1 parent b148b15 commit 67ba310
Show file tree
Hide file tree
Showing 99 changed files with 2,274 additions and 824 deletions.
1 change: 1 addition & 0 deletions build.gradle.kts
View file
Original file line number Diff line number Diff line change
Expand Up @@ -93,6 +93,7 @@ tasks {
withType<Test> {
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"
Expand Down
13 changes: 6 additions & 7 deletions src/jvm/main/org/jetbrains/kotlinx/lincheck/CTestConfiguration.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.*
Expand All @@ -38,8 +36,8 @@ abstract class CTestConfiguration(
val customScenarios: List<ExecutionScenario>
) {
abstract fun createStrategy(
testClass: Class<*>, scenario: ExecutionScenario, validationFunctions: List<Method>,
stateRepresentationMethod: Method?, verifier: Verifier
testClass: Class<*>, scenario: ExecutionScenario,
validationFunctions: List<Method>, stateRepresentationMethod: Method?
): Strategy

companion object {
Expand All @@ -55,6 +53,7 @@ abstract class CTestConfiguration(
}
}

@Suppress("DEPRECATION_ERROR")
internal fun createFromTestClassAnnotations(testClass: Class<*>): List<CTestConfiguration> {
val stressConfigurations: List<CTestConfiguration> = testClass.getAnnotationsByType(StressCTest::class.java)
.map { ann: StressCTest ->
Expand All @@ -70,7 +69,7 @@ internal fun createFromTestClassAnnotations(testClass: Class<*>): List<CTestConf
invocationsPerIteration = ann.invocationsPerIteration,
minimizeFailedScenario = ann.minimizeFailedScenario,
sequentialSpecification = chooseSequentialSpecification(ann.sequentialSpecification.java, testClass),
timeoutMs = DEFAULT_TIMEOUT_MS,
timeoutMs = CTestConfiguration.DEFAULT_TIMEOUT_MS,
customScenarios = emptyList()
)
}
Expand All @@ -95,8 +94,8 @@ internal fun createFromTestClassAnnotations(testClass: Class<*>): List<CTestConf
ann.sequentialSpecification.java,
testClass
),
timeoutMs = DEFAULT_TIMEOUT_MS,
eliminateLocalObjects = DEFAULT_ELIMINATE_LOCAL_OBJECTS,
timeoutMs = CTestConfiguration.DEFAULT_TIMEOUT_MS,
eliminateLocalObjects = ManagedCTestConfiguration.DEFAULT_ELIMINATE_LOCAL_OBJECTS,
customScenarios = emptyList()
)
}
Expand Down
96 changes: 56 additions & 40 deletions src/jvm/main/org/jetbrains/kotlinx/lincheck/LinChecker.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,13 +12,16 @@ package org.jetbrains.kotlinx.lincheck
import org.jetbrains.kotlinx.lincheck.annotations.*
import org.jetbrains.kotlinx.lincheck.execution.*
import org.jetbrains.kotlinx.lincheck.strategy.*
import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.*
import org.jetbrains.kotlinx.lincheck.strategy.stress.*
import org.jetbrains.kotlinx.lincheck.verifier.*
import kotlin.reflect.*

/**
* This class runs concurrent tests.
*/
class LinChecker (private val testClass: Class<*>, options: Options<*, *>?) {
@Suppress("DEPRECATION_ERROR")
class LinChecker(private val testClass: Class<*>, options: Options<*, *>?) {
private val testStructure = CTestStructure.getFromTestClass(testClass)
private val testConfigurations: List<CTestConfiguration>
private val reporter: Reporter
Expand Down Expand Up @@ -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
}
Expand All @@ -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
}
Expand All @@ -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 {
Expand All @@ -144,18 +132,18 @@ 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:
* ```
* val options = ...
* LinChecker.check(testClass, options)
* ```
*/
@Suppress("DEPRECATION_ERROR")
fun <O : Options<O, *>> O.check(testClass: Class<*>) = LinChecker.check(testClass, this)

/**
Expand All @@ -165,6 +153,34 @@ fun <O : Options<O, *>> O.check(testClass: Class<*>) = LinChecker.check(testClas
* LinChecker.check(testClass.java, options)
* ```
*/
@Suppress("DEPRECATION_ERROR")
fun <O : Options<O, *>> O.check(testClass: KClass<*>) = this.check(testClass.java)

internal fun <O : Options<O, *>> O.checkImpl(testClass: Class<*>) = LinChecker(testClass, this).checkImpl()
@Suppress("DEPRECATION_ERROR")
internal fun <O : Options<O, *>> 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
}
Loading

0 comments on commit 67ba310

Please sign in to comment.