Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Single Lincheck options class with testingTime(..) option #158

Open
wants to merge 5 commits into
base: develop
Choose a base branch
from
Open

Single Lincheck options class with testingTime(..) option #158

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
67ba310
LincheckOptions, testingTime option, statistics tracking and adaptive…
eupp Apr 11, 2023
976d438
fixes after rebase
eupp Aug 17, 2023
2ba1eec
rework Planner and RunTracker APIs, add possibility to run scenarios …
eupp Aug 18, 2023
9b82278
add possibility to track in the statistics each invocation running time
eupp Aug 30, 2023
8745be7
slightly rework warm-up invocations management API
eupp Aug 30, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions build.gradle.kts
View file
Open in desktop
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
Open in desktop
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
Open in desktop
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