Skip to content

Commit

Permalink
NRL stress testing
Browse files Browse the repository at this point in the history
  • Loading branch information
zuevmaxim committed Nov 25, 2020
1 parent fd18c13 commit be2d094
Show file tree
Hide file tree
Showing 33 changed files with 1,969 additions and 36 deletions.
7 changes: 5 additions & 2 deletions src/jvm/main/org/jetbrains/kotlinx/lincheck/Actor.kt
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,7 @@ import kotlin.reflect.jvm.*
*/
data class Actor @JvmOverloads constructor(
val method: Method,
val arguments: List<Any?>,
val arguments: MutableList<Any?>,
val handledExceptions: List<Class<out Throwable>> = emptyList(),
val cancelOnSuspension: Boolean = false,
val allowExtraSuspension: Boolean = false,
Expand All @@ -42,7 +42,8 @@ data class Actor @JvmOverloads constructor(
val promptCancellation: Boolean = false,
// we have to specify `isSuspendable` property explicitly for transformed classes since
// `isSuspendable` implementation produces a circular dependency and, therefore, fails.
val isSuspendable: Boolean = method.isSuspendable()
val isSuspendable: Boolean = method.isSuspendable(),
val threadIdArgsIndices: List<Int> = emptyList()
) {
init {
if (promptCancellation) require(cancelOnSuspension) {
Expand All @@ -57,6 +58,8 @@ data class Actor @JvmOverloads constructor(
(if (cancelOnSuspension) "cancel" else "")

val handlesExceptions = handledExceptions.isNotEmpty()

fun setThreadId(threadId: Int) = threadIdArgsIndices.forEach { index -> arguments[index] = threadId }
}

fun Method.isSuspendable(): Boolean = kotlinFunction?.isSuspend ?: false
Original file line number Diff line number Diff line change
Expand Up @@ -71,7 +71,8 @@ internal fun createFromTestClassAnnotations(testClass: Class<*>): List<CTestConf
ann.threads, ann.actorsPerThread, ann.actorsBefore, ann.actorsAfter,
ann.generator.java, ann.verifier.java, ann.invocationsPerIteration,
ann.requireStateEquivalenceImplCheck, ann.minimizeFailedScenario,
chooseSequentialSpecification(ann.sequentialSpecification.java, testClass), DEFAULT_TIMEOUT_MS
chooseSequentialSpecification(ann.sequentialSpecification.java, testClass), DEFAULT_TIMEOUT_MS,
ann.addCrashes
)
}
val modelCheckingConfigurations: List<CTestConfiguration> = testClass.getAnnotationsByType(ModelCheckingCTest::class.java)
Expand Down
34 changes: 33 additions & 1 deletion src/jvm/main/org/jetbrains/kotlinx/lincheck/LinChecker.kt
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,9 @@ package org.jetbrains.kotlinx.lincheck
import org.jetbrains.kotlinx.lincheck.CTestConfiguration.*
import org.jetbrains.kotlinx.lincheck.annotations.*
import org.jetbrains.kotlinx.lincheck.execution.*
import org.jetbrains.kotlinx.lincheck.nvm.Probability
import org.jetbrains.kotlinx.lincheck.strategy.*
import org.jetbrains.kotlinx.lincheck.strategy.stress.StressCTestConfiguration
import org.jetbrains.kotlinx.lincheck.verifier.*
import kotlin.reflect.*

Expand Down Expand Up @@ -93,11 +95,15 @@ class LinChecker (private val testClass: Class<*>, options: Options<*, *>?) {
for (j in scenario.parallelExecution[i].indices) {
val newScenario = scenario.copy()
newScenario.parallelExecution[i].removeAt(j)
if (newScenario.parallelExecution[i].isEmpty()) newScenario.parallelExecution.removeAt(i) // remove empty thread
if (newScenario.parallelExecution[i].isEmpty()) {
newScenario.parallelExecution.removeAt(i) // remove empty thread
newScenario.setThreadIds()
}
val newFailedIteration = newScenario.tryMinimize(testCfg, verifier)
if (newFailedIteration != null) return newFailedIteration.minimize(testCfg, verifier)
}
}
scenario.setThreadIds() // reset thread ids after parallel minimization
for (i in scenario.initExecution.indices) {
val newScenario = scenario.copy()
newScenario.initExecution.removeAt(i)
Expand All @@ -110,9 +116,35 @@ class LinChecker (private val testClass: Class<*>, options: Options<*, *>?) {
val newFailedIteration = newScenario.tryMinimize(testCfg, verifier)
if (newFailedIteration != null) return newFailedIteration.minimize(testCfg, verifier)
}
if (testCfg is StressCTestConfiguration && testCfg.addCrashes && this is IncorrectResultsFailure)
return minimizeCrashes(testCfg, verifier).also { Probability.expectedCrashes = 10 }
return this
}

private fun IncorrectResultsFailure.crashesNumber() = results.crashes.sumBy { it.size }

private fun IncorrectResultsFailure.minimizeCrashes(
testCfg: CTestConfiguration,
verifier: Verifier
): LincheckFailure {
Probability.expectedCrashes--
val currentCrashesNumber = crashesNumber()
repeat(100) {
val newIteration = scenario.tryMinimize(testCfg, verifier)
if (newIteration != null
&& newIteration is IncorrectResultsFailure
&& newIteration.crashesNumber() < currentCrashesNumber
) return newIteration.minimizeCrashes(testCfg, verifier)
}
return this
}

private fun List<Actor>.setThreadId(threadId: Int) = forEach { actor -> actor.setThreadId(threadId) }
private fun ExecutionScenario.setThreadIds() {
parallelExecution.forEachIndexed { index, actors -> actors.setThreadId(index + 1) }
postExecution.setThreadId(parallelExecution.size + 1)
}

private fun ExecutionScenario.tryMinimize(testCfg: CTestConfiguration, verifier: Verifier) =
if (isValid) run(testCfg, verifier) else null

Expand Down
27 changes: 23 additions & 4 deletions src/jvm/main/org/jetbrains/kotlinx/lincheck/Reporter.kt
Original file line number Diff line number Diff line change
Expand Up @@ -24,6 +24,7 @@ package org.jetbrains.kotlinx.lincheck

import org.jetbrains.kotlinx.lincheck.LoggingLevel.*
import org.jetbrains.kotlinx.lincheck.execution.*
import org.jetbrains.kotlinx.lincheck.nvm.CrashError
import org.jetbrains.kotlinx.lincheck.runner.*
import org.jetbrains.kotlinx.lincheck.strategy.*
import org.jetbrains.kotlinx.lincheck.strategy.managed.*
Expand Down Expand Up @@ -178,13 +179,17 @@ private fun StringBuilder.appendDeadlockWithDumpFailure(failure: DeadlockWithDum
for ((t, stackTrace) in failure.threadDump) {
val threadNumber = if (t is FixedActiveThreadsExecutor.TestThread) t.iThread.toString() else "?"
appendLine("Thread-$threadNumber:")
stackTrace.map {
StackTraceElement(it.className.removePrefix(TransformationClassLoader.REMAPPED_PACKAGE_CANONICAL_NAME), it.methodName, it.fileName, it.lineNumber)
}.forEach { appendLine("\t$it") }
appendStackTrace(stackTrace)
}
return this
}

private fun StringBuilder.appendStackTrace(stackTrace: Array<StackTraceElement>) {
stackTrace.map {
StackTraceElement(it.className.removePrefix(TransformationClassLoader.REMAPPED_PACKAGE_CANONICAL_NAME), it.methodName, it.fileName, it.lineNumber)
}.forEach { appendLine("\t$it") }
}

private fun StringBuilder.appendIncorrectResultsFailure(failure: IncorrectResultsFailure): StringBuilder {
appendln("= Invalid execution results =")
if (failure.scenario.initExecution.isNotEmpty()) {
Expand Down Expand Up @@ -212,6 +217,16 @@ private fun StringBuilder.appendIncorrectResultsFailure(failure: IncorrectResult
if (failure.results.parallelResultsWithClock.flatten().any { !it.clockOnStart.empty })
appendln("\n---\nvalues in \"[..]\" brackets indicate the number of completed operations \n" +
"in each of the parallel threads seen at the beginning of the current operation\n---")
failure.results.crashes.forEachIndexed { threadId, threadCrashes ->
if (threadCrashes.isNotEmpty()) {
appendLine("\nCrashes on thread $threadId:")
threadCrashes.forEach { crash ->
val actor = if (crash.actorIndex == -1) "constructor" else "actor ${1 + crash.actorIndex}"
appendLine("Crashed inside $actor:")
appendCrash(crash)
}
}
}
return this
}

Expand All @@ -232,4 +247,8 @@ private fun StringBuilder.appendException(t: Throwable) {
val sw = StringWriter()
t.printStackTrace(PrintWriter(sw))
appendln(sw.toString())
}
}

private fun StringBuilder.appendCrash(crash: CrashError) {
appendStackTrace(crash.stackTrace)
}
5 changes: 3 additions & 2 deletions src/jvm/main/org/jetbrains/kotlinx/lincheck/Utils.kt
Original file line number Diff line number Diff line change
Expand Up @@ -232,7 +232,7 @@ internal fun ExecutionScenario.convertForLoader(loader: ClassLoader) = Execution
initExecution,
parallelExecution.map { actors ->
actors.map { a ->
val args = a.arguments.map { it.convertForLoader(loader) }
val args = a.arguments.map { it.convertForLoader(loader) }.toMutableList()
// the original `isSuspendable` is used here since `KFunction.isSuspend` fails on transformed classes
Actor(
method = a.method.convertForLoader(loader),
Expand All @@ -243,7 +243,8 @@ internal fun ExecutionScenario.convertForLoader(loader: ClassLoader) = Execution
blocking = a.blocking,
causesBlocking = a.causesBlocking,
promptCancellation = a.promptCancellation,
isSuspendable = a.isSuspendable
isSuspendable = a.isSuspendable,
threadIdArgsIndices = a.threadIdArgsIndices
)
}
},
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
/*-
* #%L
* Lincheck
* %%
* Copyright (C) 2019 - 2020 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
* <http://www.gnu.org/licenses/lgpl-3.0.html>.
* #L%
*/
package org.jetbrains.kotlinx.lincheck.annotations

@Retention(AnnotationRetention.RUNTIME)
@Target(AnnotationTarget.FUNCTION, AnnotationTarget.CONSTRUCTOR, AnnotationTarget.CLASS)
annotation class CrashFree
Original file line number Diff line number Diff line change
@@ -0,0 +1,34 @@
/*-
* #%L
* Lincheck
* %%
* Copyright (C) 2019 - 2020 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
* <http://www.gnu.org/licenses/lgpl-3.0.html>.
* #L%
*/
package org.jetbrains.kotlinx.lincheck.annotations

/**
* Marks method recoverable.
* Links this method to [recoverMethod] that should be called when this method crashes.
* [recoverMethod] must have the same signature as this method.
*/
@Retention(AnnotationRetention.RUNTIME)
@Target(AnnotationTarget.FUNCTION, AnnotationTarget.CONSTRUCTOR)
annotation class Recoverable(
val recoverMethod: String = "",
val beforeMethod: String = ""
)
Original file line number Diff line number Diff line change
Expand Up @@ -45,20 +45,29 @@ class ActorGenerator(
private val promptCancellation = cancellableOnSuspension && promptCancellation

fun generate(threadId: Int): Actor {
val threadIdIndices = mutableListOf<Int>()
val parameters = parameterGenerators
.map { it.generate() }
.map { if (it === THREAD_ID_TOKEN) threadId else it }
.mapIndexed { index, value ->
if (value === THREAD_ID_TOKEN) {
threadIdIndices.add(index)
threadId
} else {
value
}
}
val cancelOnSuspension = this.cancellableOnSuspension and DETERMINISTIC_RANDOM.nextBoolean()
val promptCancellation = cancelOnSuspension and this.promptCancellation and DETERMINISTIC_RANDOM.nextBoolean()
return Actor(
method = method,
arguments = parameters,
arguments = parameters.toMutableList(),
handledExceptions = handledExceptions,
cancelOnSuspension = cancelOnSuspension,
allowExtraSuspension = allowExtraSuspension,
blocking = blocking,
causesBlocking = causesBlocking,
promptCancellation = promptCancellation
promptCancellation = promptCancellation,
threadIdArgsIndices = threadIdIndices
)
}

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,7 @@
package org.jetbrains.kotlinx.lincheck.execution

import org.jetbrains.kotlinx.lincheck.*
import org.jetbrains.kotlinx.lincheck.nvm.CrashError

/**
* This class represents a result corresponding to
Expand Down Expand Up @@ -56,7 +57,11 @@ data class ExecutionResult(
/**
* State representation at the end of the scenario.
*/
val afterPostStateRepresentation: String?
val afterPostStateRepresentation: String?,
/**
* Crashes occurred while execution.
*/
internal val crashes: List<List<CrashError>> = emptyList()
) {
constructor(initResults: List<Result>, parallelResultsWithClock: List<List<ResultWithClock>>, postResults: List<Result>) :
this(initResults, null, parallelResultsWithClock, null, postResults, null)
Expand All @@ -71,6 +76,8 @@ val ExecutionResult.withEmptyClocks: ExecutionResult get() = ExecutionResult(
this.afterPostStateRepresentation
)

val ExecutionResult.withoutCrashes: ExecutionResult get() = if (crashes.isEmpty()) this else copy(crashes = emptyList())

val ExecutionResult.parallelResults: List<List<Result>> get() = parallelResultsWithClock.map { it.map { r -> r.result } }

// for tests
Expand Down

0 comments on commit be2d094

Please sign in to comment.