From be2d094d08e54af2f73d99f84530c929db2a5119 Mon Sep 17 00:00:00 2001 From: Maksim Zuev Date: Wed, 25 Nov 2020 18:38:14 +0300 Subject: [PATCH] NRL stress testing --- .../org/jetbrains/kotlinx/lincheck/Actor.kt | 7 +- .../kotlinx/lincheck/CTestConfiguration.kt | 3 +- .../jetbrains/kotlinx/lincheck/LinChecker.kt | 34 ++- .../jetbrains/kotlinx/lincheck/Reporter.kt | 27 +- .../org/jetbrains/kotlinx/lincheck/Utils.kt | 5 +- .../kotlinx/lincheck/annotations/CrashFree.kt | 26 ++ .../lincheck/annotations/Recoverable.kt | 34 +++ .../lincheck/execution/ActorGenerator.kt | 15 +- .../lincheck/execution/ExecutionResult.kt | 9 +- .../kotlinx/lincheck/nvm/CrashTransformer.kt | 151 +++++++++++ .../kotlinx/lincheck/nvm/NVMCache.kt | 50 ++++ .../kotlinx/lincheck/nvm/Persistent.kt | 71 ++++++ .../kotlinx/lincheck/nvm/Probability.kt | 50 ++++ .../lincheck/nvm/RecoverabilityTransformer.kt | 232 +++++++++++++++++ .../jetbrains/kotlinx/lincheck/nvm/crash.kt | 83 ++++++ .../lincheck/runner/ParallelThreadsRunner.kt | 76 +++++- .../RecoverableParallelThreadsRunner.kt | 41 +++ .../kotlinx/lincheck/runner/Runner.kt | 4 +- .../lincheck/strategy/stress/StressCTest.java | 2 + .../stress/StressCTestConfiguration.kt | 5 +- .../strategy/stress/StressStrategy.kt | 23 +- .../lincheck/verifier/CachedVerifier.java | 4 +- .../LincheckClassCrashFreeTest.kt | 40 +++ .../test/verifier/CustomScenarioDSL.kt | 2 +- .../verifier/linearizability/ClocksTest.kt | 8 +- .../verifier/linearizability/MSQueueTest.kt | 97 +++++++ .../test/verifier/nlr/CounterFailingTest.kt | 111 ++++++++ .../lincheck/test/verifier/nlr/CounterTest.kt | 110 ++++++++ .../test/verifier/nlr/DurableMSQueueTest.kt | 136 ++++++++++ .../test/verifier/nlr/PersistentTest.kt | 61 +++++ .../test/verifier/nlr/ReadWriteObjectTest.kt | 114 +++++++++ .../lincheck/test/verifier/nlr/SetTest.kt | 240 ++++++++++++++++++ .../test/verifier/nlr/TestAndSetTest.kt | 134 ++++++++++ 33 files changed, 1969 insertions(+), 36 deletions(-) create mode 100644 src/jvm/main/org/jetbrains/kotlinx/lincheck/annotations/CrashFree.kt create mode 100644 src/jvm/main/org/jetbrains/kotlinx/lincheck/annotations/Recoverable.kt create mode 100644 src/jvm/main/org/jetbrains/kotlinx/lincheck/nvm/CrashTransformer.kt create mode 100644 src/jvm/main/org/jetbrains/kotlinx/lincheck/nvm/NVMCache.kt create mode 100644 src/jvm/main/org/jetbrains/kotlinx/lincheck/nvm/Persistent.kt create mode 100644 src/jvm/main/org/jetbrains/kotlinx/lincheck/nvm/Probability.kt create mode 100644 src/jvm/main/org/jetbrains/kotlinx/lincheck/nvm/RecoverabilityTransformer.kt create mode 100644 src/jvm/main/org/jetbrains/kotlinx/lincheck/nvm/crash.kt create mode 100644 src/jvm/main/org/jetbrains/kotlinx/lincheck/runner/RecoverableParallelThreadsRunner.kt create mode 100644 src/jvm/test/org/jetbrains/kotlinx/lincheck/test/transformation/LincheckClassCrashFreeTest.kt create mode 100644 src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/linearizability/MSQueueTest.kt create mode 100644 src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/nlr/CounterFailingTest.kt create mode 100644 src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/nlr/CounterTest.kt create mode 100644 src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/nlr/DurableMSQueueTest.kt create mode 100644 src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/nlr/PersistentTest.kt create mode 100644 src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/nlr/ReadWriteObjectTest.kt create mode 100644 src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/nlr/SetTest.kt create mode 100644 src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/nlr/TestAndSetTest.kt diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/Actor.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/Actor.kt index 208a3fd5d..e42e00de6 100644 --- a/src/jvm/main/org/jetbrains/kotlinx/lincheck/Actor.kt +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/Actor.kt @@ -33,7 +33,7 @@ import kotlin.reflect.jvm.* */ data class Actor @JvmOverloads constructor( val method: Method, - val arguments: List, + val arguments: MutableList, val handledExceptions: List> = emptyList(), val cancelOnSuspension: Boolean = false, val allowExtraSuspension: Boolean = false, @@ -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 = emptyList() ) { init { if (promptCancellation) require(cancelOnSuspension) { @@ -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 \ No newline at end of file diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/CTestConfiguration.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/CTestConfiguration.kt index c291b8c99..bc831e643 100644 --- a/src/jvm/main/org/jetbrains/kotlinx/lincheck/CTestConfiguration.kt +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/CTestConfiguration.kt @@ -71,7 +71,8 @@ internal fun createFromTestClassAnnotations(testClass: Class<*>): List = testClass.getAnnotationsByType(ModelCheckingCTest::class.java) diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/LinChecker.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/LinChecker.kt index d1e5a2b76..46d93bc8a 100644 --- a/src/jvm/main/org/jetbrains/kotlinx/lincheck/LinChecker.kt +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/LinChecker.kt @@ -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.* @@ -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) @@ -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.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 diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/Reporter.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/Reporter.kt index 3ebcfd875..ff145d3ca 100644 --- a/src/jvm/main/org/jetbrains/kotlinx/lincheck/Reporter.kt +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/Reporter.kt @@ -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.* @@ -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) { + 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()) { @@ -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 } @@ -232,4 +247,8 @@ private fun StringBuilder.appendException(t: Throwable) { val sw = StringWriter() t.printStackTrace(PrintWriter(sw)) appendln(sw.toString()) -} \ No newline at end of file +} + +private fun StringBuilder.appendCrash(crash: CrashError) { + appendStackTrace(crash.stackTrace) +} diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/Utils.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/Utils.kt index 98933eb1f..4b19ef41f 100644 --- a/src/jvm/main/org/jetbrains/kotlinx/lincheck/Utils.kt +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/Utils.kt @@ -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), @@ -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 ) } }, diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/annotations/CrashFree.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/annotations/CrashFree.kt new file mode 100644 index 000000000..c007a0776 --- /dev/null +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/annotations/CrashFree.kt @@ -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 + * . + * #L% + */ +package org.jetbrains.kotlinx.lincheck.annotations + +@Retention(AnnotationRetention.RUNTIME) +@Target(AnnotationTarget.FUNCTION, AnnotationTarget.CONSTRUCTOR, AnnotationTarget.CLASS) +annotation class CrashFree diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/annotations/Recoverable.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/annotations/Recoverable.kt new file mode 100644 index 000000000..4d2cce7b3 --- /dev/null +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/annotations/Recoverable.kt @@ -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 + * . + * #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 = "" +) diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/execution/ActorGenerator.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/execution/ActorGenerator.kt index 3d9dc090c..dd7e40242 100644 --- a/src/jvm/main/org/jetbrains/kotlinx/lincheck/execution/ActorGenerator.kt +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/execution/ActorGenerator.kt @@ -45,20 +45,29 @@ class ActorGenerator( private val promptCancellation = cancellableOnSuspension && promptCancellation fun generate(threadId: Int): Actor { + val threadIdIndices = mutableListOf() 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 ) } diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/execution/ExecutionResult.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/execution/ExecutionResult.kt index ddcc5da87..86993bca1 100644 --- a/src/jvm/main/org/jetbrains/kotlinx/lincheck/execution/ExecutionResult.kt +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/execution/ExecutionResult.kt @@ -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 @@ -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> = emptyList() ) { constructor(initResults: List, parallelResultsWithClock: List>, postResults: List) : this(initResults, null, parallelResultsWithClock, null, postResults, null) @@ -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> get() = parallelResultsWithClock.map { it.map { r -> r.result } } // for tests diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/nvm/CrashTransformer.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/nvm/CrashTransformer.kt new file mode 100644 index 000000000..ee5138118 --- /dev/null +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/nvm/CrashTransformer.kt @@ -0,0 +1,151 @@ +/*- + * #%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 + * . + * #L% + */ +package org.jetbrains.kotlinx.lincheck.nvm + +import org.jetbrains.kotlinx.lincheck.TransformationClassLoader.ASM_API +import org.jetbrains.kotlinx.lincheck.annotations.CrashFree +import org.objectweb.asm.* +import org.objectweb.asm.commons.GeneratorAdapter +import org.objectweb.asm.commons.Method +import java.util.concurrent.atomic.AtomicInteger + +private val CRASH_FREE_TYPE = Type.getDescriptor(CrashFree::class.java) + +class CrashTransformer(cv: ClassVisitor, testClass: Class<*>) : ClassVisitor(ASM_API, cv) { + private var shouldTransform = true + private val testClassName = Type.getInternalName(testClass) + private val possibleCrashes = AtomicInteger(0) + + override fun visit( + version: Int, + access: Int, + name: String?, + signature: String?, + superName: String?, + interfaces: Array? + ) { + super.visit(version, access, name, signature, superName, interfaces) + if (name == testClassName) { + shouldTransform = false + } + } + + override fun visitAnnotation(descriptor: String?, visible: Boolean): AnnotationVisitor { + if (descriptor == CRASH_FREE_TYPE) { + shouldTransform = false + } + return super.visitAnnotation(descriptor, visible) + } + + + override fun visitMethod( + access: Int, + name: String?, + descriptor: String?, + signature: String?, + exceptions: Array? + ): MethodVisitor { + val mv = super.visitMethod(access, name, descriptor, signature, exceptions) + if (!shouldTransform) return mv + if (name == "") return mv + if (name == "") return CrashConstructorTransformer(mv, access, name, descriptor, possibleCrashes) + return CrashMethodTransformer(mv, access, name, descriptor, possibleCrashes) + } +} + +private open class CrashBaseMethodTransformer( + mv: MethodVisitor, + access: Int, + name: String?, + descriptor: String?, + private val possibleCrashes: AtomicInteger +) : GeneratorAdapter(ASM_API, mv, access, name, descriptor) { + + private val crashOwnerType = Type.getType(Crash::class.java) + private var shouldTransform = true + + protected open fun callCrash() { + if (!shouldTransform) return + Probability.totalPossibleCrashes = possibleCrashes.incrementAndGet() + super.invokeStatic(crashOwnerType, Method("possiblyCrash", "()V")) + } + + override fun visitAnnotation(descriptor: String?, visible: Boolean): AnnotationVisitor { + if (descriptor == CRASH_FREE_TYPE) { + shouldTransform = false + } + return super.visitAnnotation(descriptor, visible) + } +} + +private class CrashMethodTransformer( + mv: MethodVisitor, + access: Int, + name: String?, + descriptor: String?, + possibleCrashes: AtomicInteger +) : CrashBaseMethodTransformer(mv, access, name, descriptor, possibleCrashes) { + override fun visitCode() { + super.visitCode() + callCrash() + } + + override fun visitMethodInsn( + opcode: Int, + owner: String?, + name: String?, + descriptor: String?, + isInterface: Boolean + ) { + callCrash() + super.visitMethodInsn(opcode, owner, name, descriptor, isInterface) + } +} + +private class CrashConstructorTransformer( + mv: MethodVisitor, + access: Int, + name: String?, + descriptor: String?, + possibleCrashes: AtomicInteger +) : CrashBaseMethodTransformer(mv, access, name, descriptor, possibleCrashes) { + private var superConstructorCalled = false + + override fun visitMethodInsn( + opcode: Int, + owner: String?, + name: String?, + descriptor: String?, + isInterface: Boolean + ) { + super.visitMethodInsn(opcode, owner, name, descriptor, isInterface) + if (!superConstructorCalled && opcode == Opcodes.INVOKESPECIAL) { + superConstructorCalled = true + } + } + + override fun callCrash() { + if (superConstructorCalled) { + super.callCrash() + } + } +} diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/nvm/NVMCache.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/nvm/NVMCache.kt new file mode 100644 index 000000000..34bc3cc80 --- /dev/null +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/nvm/NVMCache.kt @@ -0,0 +1,50 @@ +/*- + * #%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 + * . + * #L% + */ +package org.jetbrains.kotlinx.lincheck.nvm + +/** Volatile cache of non-volatile memory emulation. */ +object NVMCache { + const val MAX_THREADS_NUMBER = 10 + + private val cache = Array>?>(MAX_THREADS_NUMBER) { null } + + /** Flushes all local variables of thread. */ + fun flush(threadId: Int) { + val localCache = cache[threadId] ?: return + localCache.toList().forEach { it.flush(threadId) } + } + + internal fun add(threadId: Int, variable: Persistent<*>) { + val localCache = cache[threadId] ?: hashSetOf>().also { cache[threadId] = it } + localCache.add(variable) + } + + internal fun remove(threadId: Int, variable: Persistent<*>) { + val localCache = cache[threadId] ?: return + localCache.remove(variable) + } + + internal fun crash(threadId: Int) { + val localCache = cache[threadId] ?: return + localCache.toList().forEach { it.crash(threadId) } + } +} diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/nvm/Persistent.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/nvm/Persistent.kt new file mode 100644 index 000000000..40d199b28 --- /dev/null +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/nvm/Persistent.kt @@ -0,0 +1,71 @@ +/*- + * #%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 + * . + * #L% + */ +package org.jetbrains.kotlinx.lincheck.nvm + +import org.jetbrains.kotlinx.lincheck.runner.RecoverableStateContainer + + +/** Persistent reference emulates non-volatile memory variable with volatile cache. */ +class Persistent() { + @Volatile + private var persistedValue: T? = null + + private var localValue: T? = null + + private val empty = BooleanArray(NVMCache.MAX_THREADS_NUMBER) { true } + + constructor(initialValue: T) : this() { + persistedValue = initialValue + } + + fun read(threadId: Int = RecoverableStateContainer.threadId()) = if (empty[threadId]) { + persistedValue + } else { + localValue + } + + fun write(threadId: Int = RecoverableStateContainer.threadId(), value: T) { + empty[threadId] = false + localValue = value + NVMCache.add(threadId, this) + } + + fun flush(threadId: Int = RecoverableStateContainer.threadId()) { + if (empty[threadId]) return + persistedValue = localValue + NVMCache.remove(threadId, this) + } + + fun writeAndFlush(threadId: Int = RecoverableStateContainer.threadId(), value: T) { + empty[threadId] = false + localValue = value + persistedValue = localValue + } + + internal fun crash(threadId: Int) { + if (Probability.shouldFlush()) { + flush(threadId) + } + NVMCache.remove(threadId, this) + empty[threadId] = true + } +} diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/nvm/Probability.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/nvm/Probability.kt new file mode 100644 index 000000000..55ee883a6 --- /dev/null +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/nvm/Probability.kt @@ -0,0 +1,50 @@ +/*- + * #%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 + * . + * #L% + */ +package org.jetbrains.kotlinx.lincheck.nvm + +import org.jetbrains.kotlinx.lincheck.runner.RecoverableStateContainer +import java.lang.Integer.max +import kotlin.random.Random + +object Probability { + private val random = Random(42) + + @Volatile + var totalPossibleCrashes = 0 + + @Volatile + var totalActors = 0 + + @Volatile + var expectedCrashes = 10 + + private const val RANDOM_FLUSH_PROBABILITY = 0.2 + private const val RANDOM_SYSTEM_CRASH_PROBABILITY = 0.3 + + fun shouldFlush() = bernoulli(RANDOM_FLUSH_PROBABILITY) + fun shouldCrash() = (RecoverableStateContainer.crashesCount() <= 2 * expectedCrashes) && bernoulli(singleCrashProbability()) + fun shouldSystemCrash() = bernoulli(RANDOM_SYSTEM_CRASH_PROBABILITY) + + private fun singleCrashProbability() = expectedCrashes / max(1, totalPossibleCrashes * totalActors).toDouble() + + private fun bernoulli(probability: Double) = random.nextDouble() < probability +} diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/nvm/RecoverabilityTransformer.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/nvm/RecoverabilityTransformer.kt new file mode 100644 index 000000000..f471161b7 --- /dev/null +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/nvm/RecoverabilityTransformer.kt @@ -0,0 +1,232 @@ +/*- + * #%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 + * . + * #L% + */ +package org.jetbrains.kotlinx.lincheck.nvm + +import org.jetbrains.kotlinx.lincheck.TransformationClassLoader.ASM_API +import org.jetbrains.kotlinx.lincheck.annotations.Recoverable +import org.objectweb.asm.* +import org.objectweb.asm.commons.GeneratorAdapter +import org.objectweb.asm.commons.Method +import java.lang.Integer.max + + +class RecoverabilityTransformer(cv: ClassVisitor) : ClassVisitor(ASM_API, cv) { + private lateinit var name: String + + override fun visit( + version: Int, + access: Int, + name: String?, + signature: String?, + superName: String?, + interfaces: Array? + ) { + super.visit(version, access, name, signature, superName, interfaces) + this.name = name!! + } + + + override fun visitMethod( + access: Int, + name: String?, + descriptor: String?, + signature: String?, + exceptions: Array? + ): MethodVisitor { + val mv = super.visitMethod(access, name, descriptor, signature, exceptions) + if (name == "") return RecoverableConstructorTransformer(mv, access, name, descriptor, this.name) + return RecoverableMethodTransformer(mv, access, name, descriptor, this.name) + } +} + +private val CRASH_NAME = Type.getInternalName(CrashError::class.java) + +private open class RecoverableBaseMethodTransformer( + mv: MethodVisitor, + access: Int, + name: String?, + descriptor: String?, + className: String +) : GeneratorAdapter(ASM_API, mv, access, name, descriptor) { + protected var shouldTransform = false + protected var beforeName = "" + protected var recoverName = "" + protected val tryLabel = Label() + protected val catchLabel = Label() + + private val completedVariable: Int by lazy { newLocal(Type.BOOLEAN_TYPE) } + private val classType = Type.getType("L$className;") + + /** Check whether method has [Recoverable] annotation. */ + override fun visitAnnotation(descriptor: String?, visible: Boolean): AnnotationVisitor { + val av = super.visitAnnotation(descriptor, visible) + if (descriptor != Type.getDescriptor(Recoverable::class.java)) return av + shouldTransform = true + return object : AnnotationVisitor(ASM_API, av) { + override fun visit(name: String?, value: Any?) { + super.visit(name, value) + if (name == "recoverMethod") { + recoverName = value as String + } else if (name == "beforeMethod") { + beforeName = value as String + } + } + } + } + + /** + * Call [name] method with signature [descriptor] until it completes successfully. + * @return index of local variable where result is stored or -1 in case of void return type + */ + protected fun callUntilSuccess(name: String, descriptor: String?): Int { + val (tryLabel, catchLabel, endLabel) = List(3) { Label() } + visitTryCatchBlock(tryLabel, catchLabel, catchLabel, CRASH_NAME) + + val returnType = Type.getReturnType(descriptor) + val result = if (returnType == Type.VOID_TYPE) -1 else newLocal(returnType).also { + // init result + pushDefaultValue(returnType) + storeLocal(it) + } + + push(false) + storeLocal(completedVariable) + + visitLabel(tryLabel) + + // invoke `name` method + loadThis() + loadArgs() + invokeVirtual(classType, Method(name, descriptor)) + if (returnType != Type.VOID_TYPE) { + storeLocal(result) + } + push(true) + storeLocal(completedVariable) + goTo(endLabel) + + // ignore exception, try again + visitLabel(catchLabel) + pop() + + visitLabel(endLabel) + // while not successful + loadLocal(completedVariable) + ifZCmp(EQ, tryLabel) + return result + } + + /** Push a default value of type [type] on stack. */ + private fun pushDefaultValue(type: Type) { + when (type.sort) { + Type.BOOLEAN, Type.BYTE, Type.CHAR, Type.INT -> push(0) + Type.LONG -> push(0L) + Type.DOUBLE -> push(0.0) + Type.FLOAT -> push(0.0f) + Type.ARRAY, Type.METHOD, Type.OBJECT -> visitInsn(Opcodes.ACONST_NULL) + } + } +} + + +/** + * Modifies body of method if it is marked with [Recoverable] annotation. + * Generates a call to before method(if present), wraps method body with try-catch + * and calls recover method in case of a crash. + */ +private class RecoverableMethodTransformer( + mv: MethodVisitor, + access: Int, + name: String?, + private val descriptor: String?, + className: String +) : RecoverableBaseMethodTransformer(mv, access, name, descriptor, className) { + + /** Call before if name is non-empty and wrap method body with try-catch. */ + override fun visitCode() { + super.visitCode() + if (!shouldTransform) return + visitTryCatchBlock(tryLabel, catchLabel, catchLabel, CRASH_NAME) + + if (beforeName.isNotEmpty()) { + val beforeDescriptor = Type.getMethodDescriptor(Type.VOID_TYPE, *Type.getType(descriptor).argumentTypes) + callUntilSuccess(beforeName, beforeDescriptor) + } + + visitLabel(tryLabel) + } + + /** Call recover method in case of crash. */ + override fun visitMaxs(maxStack: Int, maxLocals: Int) { + if (shouldTransform) { + visitLabel(catchLabel) + pop() + val result = callUntilSuccess(if (recoverName.isEmpty()) name else recoverName, descriptor) + if (result != -1) { + loadLocal(result) + } + returnValue() + super.visitMaxs(max(1 + maxStack, 1 + argumentTypes.size), maxLocals) + } else { + super.visitMaxs(maxStack, maxLocals) + } + } +} + +private class RecoverableConstructorTransformer( + mv: MethodVisitor, + access: Int, + name: String?, + private val descriptor: String?, + className: String +) : RecoverableBaseMethodTransformer(mv, access, name, descriptor, className) { + private var superConstructorCalled = false + + override fun visitMethodInsn( + opcode: Int, + owner: String?, + name: String?, + descriptor: String?, + isInterface: Boolean + ) { + super.visitMethodInsn(opcode, owner, name, descriptor, isInterface) + if (shouldTransform && !superConstructorCalled && opcode == Opcodes.INVOKESPECIAL) { + superConstructorCalled = true + visitTryCatchBlock(tryLabel, catchLabel, catchLabel, CRASH_NAME) + visitLabel(tryLabel) + } + } + + override fun visitMaxs(maxStack: Int, maxLocals: Int) { + if (shouldTransform) { + visitLabel(catchLabel) + pop() + if (recoverName.isEmpty()) { + goTo(tryLabel) + } else { + callUntilSuccess(recoverName, descriptor) + } + } + super.visitMaxs(maxStack, maxLocals) + } +} + diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/nvm/crash.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/nvm/crash.kt new file mode 100644 index 000000000..20fa0740f --- /dev/null +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/nvm/crash.kt @@ -0,0 +1,83 @@ +/*- + * #%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 + * . + * #L% + */ +package org.jetbrains.kotlinx.lincheck.nvm + +import kotlinx.atomicfu.atomic +import org.jetbrains.kotlinx.lincheck.runner.RecoverableStateContainer +import java.util.* +import java.util.concurrent.ConcurrentHashMap + +/** + * This exception is used to emulate system crash. + * Must be ignored by user code, namely 'catch (e: Throwable)' constructions should pass this exception. + */ +class CrashError(var actorIndex: Int = -1) : Error() + +object Crash { + /** + * Crash simulation. + * @throws CrashError + */ + private fun crash(threadId: Int) { + NVMCache.crash(threadId) + throw CrashError().also { RecoverableStateContainer.registerCrash(threadId, it) } + } + + private val threads: MutableSet = Collections.newSetFromMap(ConcurrentHashMap()) + private val waitingCont = atomic(0) + + /** + * Random crash simulation. Produces a single thread crash or a system crash. + * On a system crash a thread waits for other threads to reach this method call. + */ + @JvmStatic + fun possiblyCrash() { +// if (waitingCont.value > 0) { +// val threadId = threadId() +// awaitSystemCrash(threadId) +// crash(threadId) +// } + if (Probability.shouldCrash()) { + val threadId = RecoverableStateContainer.threadId() +// if (Probability.shouldSystemCrash()) { +// awaitSystemCrash(threadId) +// } + crash(threadId) + } + } + + private fun awaitSystemCrash(threadId: Int) { + waitingCont.incrementAndGet() + threads.add(threadId) + var threadsCount: Int + do { + threadsCount = threads.size + } while (waitingCont.value < threadsCount) + waitingCont.compareAndSet(threadsCount, 0) + } + + /** Should be called when thread finished. */ + @JvmStatic + fun exit(threadId: Int) { + threads.remove(threadId) + } +} diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/runner/ParallelThreadsRunner.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/runner/ParallelThreadsRunner.kt index 7c3ebacf1..04aab5afa 100644 --- a/src/jvm/main/org/jetbrains/kotlinx/lincheck/runner/ParallelThreadsRunner.kt +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/runner/ParallelThreadsRunner.kt @@ -23,6 +23,10 @@ package org.jetbrains.kotlinx.lincheck.runner import org.jetbrains.kotlinx.lincheck.* import org.jetbrains.kotlinx.lincheck.execution.* +import org.jetbrains.kotlinx.lincheck.nvm.CrashError +import org.jetbrains.kotlinx.lincheck.nvm.NVMCache +import org.jetbrains.kotlinx.lincheck.nvm.Probability +import org.jetbrains.kotlinx.lincheck.nvm.RecoverabilityTransformer import org.jetbrains.kotlinx.lincheck.runner.FixedActiveThreadsExecutor.TestThread import org.jetbrains.kotlinx.lincheck.runner.UseClocks.* import org.jetbrains.kotlinx.lincheck.strategy.* @@ -36,6 +40,47 @@ import kotlin.random.* private typealias SuspensionPointResultWithContinuation = AtomicReference, Continuation>> +internal enum class ExecutionState { + INIT, PARALLEL, POST +} + +object RecoverableStateContainer { + @Volatile + internal var state = ExecutionState.INIT + + @Volatile + internal var threads = 0 + + private var crashes = initCrashes() + private var executedActors = IntArray(NVMCache.MAX_THREADS_NUMBER) { -1 } + + private fun initCrashes() = Array(NVMCache.MAX_THREADS_NUMBER) { mutableListOf() } + + fun threadId(): Int = when (state) { + ExecutionState.INIT -> 0 + ExecutionState.PARALLEL -> Thread.currentThread().let { + if (it is TestThread) it.iThread + 1 else -1 + } + ExecutionState.POST -> threads + 1 + } + + internal fun registerCrash(threadId: Int, crash: CrashError) { + crash.actorIndex = executedActors[threadId] + crashes[threadId].add(crash) + } + + internal fun clearCrashes() = crashes.also { + crashes = initCrashes() + executedActors = IntArray(NVMCache.MAX_THREADS_NUMBER) { -1 } + } + + internal fun actorStarted(threadId: Int) { + executedActors[threadId]++ + } + + fun crashesCount() = crashes.sumBy { it.size } +} + /** * This runner executes parallel scenario part in different threads. * Supports running scenarios with `suspend` functions. @@ -239,8 +284,11 @@ internal open class ParallelThreadsRunner( suspensionPointResults[iThread][actorId] != NoResult || completions[iThread][actorId].resWithCont.get() != null override fun run(): InvocationResult { + Probability.totalActors = scenario.initExecution.size + scenario.parallelExecution.sumBy { it.size } + scenario.postExecution.size + beforeInit() reset() val initResults = scenario.initExecution.mapIndexed { i, initActor -> + RecoverableStateContainer.actorStarted(0) executeActor(testInstance, initActor).also { executeValidationFunctions(testInstance, validationFunctions) { functionName, exception -> val s = ExecutionScenario( @@ -253,6 +301,7 @@ internal open class ParallelThreadsRunner( } } val afterInitStateRepresentation = constructStateRepresentation() + beforeParallel(scenario.threads) try { executor.submitAndAwait(testThreadExecutions, timeoutMs) } catch (e: TimeoutException) { @@ -275,7 +324,9 @@ internal open class ParallelThreadsRunner( val afterParallelStateRepresentation = constructStateRepresentation() val dummyCompletion = Continuation(EmptyCoroutineContext) {} var postPartSuspended = false + beforePost() val postResults = scenario.postExecution.mapIndexed { i, postActor -> + RecoverableStateContainer.actorStarted(scenario.parallelExecution.size + 1) // no actors are executed after suspension of a post part val result = if (postPartSuspended) { NoResult @@ -299,11 +350,31 @@ internal open class ParallelThreadsRunner( val results = ExecutionResult( initResults, afterInitStateRepresentation, parallelResultsWithClock, afterParallelStateRepresentation, - postResults, afterPostStateRepresentation + postResults, afterPostStateRepresentation, + RecoverableStateContainer.clearCrashes().toList() ) + RecoverableStateContainer.state = ExecutionState.INIT return CompletedInvocationResult(results) } + protected fun beforeInit() { + RecoverableStateContainer.state = ExecutionState.INIT + } + + protected fun beforeParallel(threads: Int) { + RecoverableStateContainer.threads = threads + RecoverableStateContainer.state = ExecutionState.PARALLEL + } + + protected fun beforePost() { + RecoverableStateContainer.state = ExecutionState.POST + } + + override fun onActorStart(iThread: Int) { + super.onActorStart(iThread) + RecoverableStateContainer.actorStarted(iThread + 1) + } + override fun onStart(iThread: Int) { super.onStart(iThread) uninitializedThreads.decrementAndGet() // this thread has finished initialization @@ -319,7 +390,8 @@ internal open class ParallelThreadsRunner( } override fun needsTransformation() = true - override fun createTransformer(cv: ClassVisitor) = CancellabilitySupportClassTransformer(cv) + override fun createTransformer(cv: ClassVisitor): ClassVisitor = + RecoverabilityTransformer(CancellabilitySupportClassTransformer(cv)) override fun constructStateRepresentation() = stateRepresentationFunction?.let{ getMethod(testInstance, it) }?.invoke(testInstance) as String? diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/runner/RecoverableParallelThreadsRunner.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/runner/RecoverableParallelThreadsRunner.kt new file mode 100644 index 000000000..ddc756169 --- /dev/null +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/runner/RecoverableParallelThreadsRunner.kt @@ -0,0 +1,41 @@ +/*- + * #%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 + * . + * #L% + */ + +package org.jetbrains.kotlinx.lincheck.runner + +import org.jetbrains.kotlinx.lincheck.nvm.CrashTransformer +import org.jetbrains.kotlinx.lincheck.strategy.Strategy +import org.objectweb.asm.ClassVisitor +import java.lang.reflect.Method + + +internal class RecoverableParallelThreadsRunner( + strategy: Strategy, + testClass: Class<*>, + validationFunctions: List, + stateRepresentationFunction: Method?, + timeoutMs: Long, + useClocks: UseClocks +) : ParallelThreadsRunner(strategy, testClass, validationFunctions, stateRepresentationFunction, timeoutMs, useClocks) { + override fun needsTransformation() = true + override fun createTransformer(cv: ClassVisitor): ClassVisitor = CrashTransformer(super.createTransformer(cv), _testClass) +} diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/runner/Runner.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/runner/Runner.kt index ff5ffd6f6..294043944 100644 --- a/src/jvm/main/org/jetbrains/kotlinx/lincheck/runner/Runner.kt +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/runner/Runner.kt @@ -36,7 +36,7 @@ import java.io.* */ abstract class Runner protected constructor( protected val strategy: Strategy, - private val _testClass: Class<*>, // will be transformed later + protected val _testClass: Class<*>, // will be transformed later protected val validationFunctions: List, protected val stateRepresentationFunction: Method? ) : Closeable { @@ -138,7 +138,7 @@ abstract class Runner protected constructor( * Is invoked before each actor execution from the specified thread. * The invocations are inserted into the generated code. */ - fun onActorStart(iThread: Int) { + open fun onActorStart(iThread: Int) { strategy.onActorStart(iThread) } 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 eb0964309..e4e9a4fba 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 @@ -125,6 +125,8 @@ */ Class sequentialSpecification() default DummySequentialSpecification.class; + boolean addCrashes() default false; + /** * Holder annotation for {@link StressCTest}. */ 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 a81d55991..cd337d29e 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 @@ -32,12 +32,13 @@ import java.lang.reflect.* class StressCTestConfiguration(testClass: Class<*>, iterations: Int, threads: Int, actorsPerThread: Int, actorsBefore: Int, actorsAfter: Int, generatorClass: Class, verifierClass: Class, val invocationsPerIteration: Int, requireStateEquivalenceCheck: Boolean, minimizeFailedScenario: Boolean, - sequentialSpecification: Class<*>?, timeoutMs: Long + sequentialSpecification: Class<*>?, timeoutMs: Long, + val addCrashes: Boolean = false ) : CTestConfiguration(testClass, iterations, threads, actorsPerThread, actorsBefore, actorsAfter, generatorClass, verifierClass, requireStateEquivalenceCheck, minimizeFailedScenario, sequentialSpecification, timeoutMs) { override fun createStrategy(testClass: Class<*>, scenario: ExecutionScenario, validationFunctions: List, stateRepresentationMethod: Method?, verifier: Verifier) = - StressStrategy(this, testClass, scenario, validationFunctions, stateRepresentationMethod, verifier) + StressStrategy(this, testClass, scenario, validationFunctions, stateRepresentationMethod, verifier, addCrashes) companion object { const val DEFAULT_INVOCATIONS = 10000 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 265c4a276..333aa0586 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 @@ -33,20 +33,23 @@ class StressStrategy( scenario: ExecutionScenario, validationFunctions: List, stateRepresentationFunction: Method?, - private val verifier: Verifier + private val verifier: Verifier, + addCrashes: Boolean = false ) : Strategy(scenario) { private val invocations = testCfg.invocationsPerIteration - private val runner: Runner + private val runner: Runner = if (addCrashes) { + RecoverableParallelThreadsRunner( + this, testClass, validationFunctions, stateRepresentationFunction, + testCfg.timeoutMs, UseClocks.RANDOM + ) + } else { + ParallelThreadsRunner( + this, testClass, validationFunctions, stateRepresentationFunction, + testCfg.timeoutMs, UseClocks.RANDOM + ) + } init { - runner = ParallelThreadsRunner( - strategy = this, - testClass = testClass, - validationFunctions = validationFunctions, - stateRepresentationFunction = stateRepresentationFunction, - timeoutMs = testCfg.timeoutMs, - useClocks = UseClocks.RANDOM - ) try { runner.initialize() } catch (t: Throwable) { diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/verifier/CachedVerifier.java b/src/jvm/main/org/jetbrains/kotlinx/lincheck/verifier/CachedVerifier.java index 25c56b962..8bef94de6 100644 --- a/src/jvm/main/org/jetbrains/kotlinx/lincheck/verifier/CachedVerifier.java +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/verifier/CachedVerifier.java @@ -37,7 +37,9 @@ public abstract class CachedVerifier implements Verifier { @Override public boolean verifyResults(ExecutionScenario scenario, ExecutionResult results) { - boolean newResult = previousResults.computeIfAbsent(scenario, s -> new HashSet<>()).add(results); + // Stacktrace is a large object, that is useless for verification, as it is used only for report. + ExecutionResult resultWithoutCrashes = ExecutionResultKt.getWithoutCrashes(results); + boolean newResult = previousResults.computeIfAbsent(scenario, s -> new HashSet<>()).add(resultWithoutCrashes); if (!newResult) return true; return verifyResultsImpl(scenario, results); } diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/transformation/LincheckClassCrashFreeTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/transformation/LincheckClassCrashFreeTest.kt new file mode 100644 index 000000000..68e85fd84 --- /dev/null +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/transformation/LincheckClassCrashFreeTest.kt @@ -0,0 +1,40 @@ +/*- + * #%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 + * . + * #L% + */ +package org.jetbrains.kotlinx.lincheck.test.transformation + +import org.jetbrains.kotlinx.lincheck.LinChecker +import org.jetbrains.kotlinx.lincheck.annotations.Operation +import org.jetbrains.kotlinx.lincheck.strategy.stress.StressCTest +import org.jetbrains.kotlinx.lincheck.verifier.VerifierState +import org.junit.Test + +@StressCTest(addCrashes = true) +internal class LincheckClassCrashFreeTest : VerifierState() { + + @Operation + fun simple() = 42 + + @Test + fun testDoesNotThrowCrashError() = LinChecker.check(this::class.java) + + override fun extractState() = 42 +} diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/CustomScenarioDSL.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/CustomScenarioDSL.kt index c9f687099..593619f30 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/CustomScenarioDSL.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/CustomScenarioDSL.kt @@ -73,7 +73,7 @@ fun actor(function: KFunction<*>, vararg args: Any?, cancelOnSuspension: Boolean require(method.exceptionTypes.all { Throwable::class.java.isAssignableFrom(it) }) { "Not all declared exceptions are Throwable" } return Actor( method = method, - arguments = args.toList(), + arguments = args.toMutableList(), handledExceptions = (method.exceptionTypes as Array>).toList(), cancelOnSuspension = cancelOnSuspension ) diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/linearizability/ClocksTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/linearizability/ClocksTest.kt index 99579f8bc..5f8641ed3 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/linearizability/ClocksTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/linearizability/ClocksTest.kt @@ -68,12 +68,12 @@ class ClocksTestScenarioGenerator(testCfg: CTestConfiguration, testStructure: CT emptyList(), listOf( listOf( - Actor(method = ClocksTest::a.javaMethod!!, arguments = emptyList()), - Actor(method = ClocksTest::b.javaMethod!!, arguments = emptyList()) + Actor(method = ClocksTest::a.javaMethod!!, arguments = mutableListOf()), + Actor(method = ClocksTest::b.javaMethod!!, arguments = mutableListOf()) ), listOf( - Actor(method = ClocksTest::c.javaMethod!!, arguments = emptyList()), - Actor(method = ClocksTest::d.javaMethod!!, arguments = emptyList()) + Actor(method = ClocksTest::c.javaMethod!!, arguments = mutableListOf()), + Actor(method = ClocksTest::d.javaMethod!!, arguments = mutableListOf()) ) ), emptyList() diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/linearizability/MSQueueTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/linearizability/MSQueueTest.kt new file mode 100644 index 000000000..af770b210 --- /dev/null +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/linearizability/MSQueueTest.kt @@ -0,0 +1,97 @@ +/*- + * #%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 + * . + * #L% + */ +package org.jetbrains.kotlinx.lincheck.test.verifier.linearizability + +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.verifier.VerifierState +import java.util.* +import java.util.concurrent.atomic.AtomicReference + +class MSQueueTest : AbstractLincheckTest() { + private val q = MSQueue() + + @Operation + fun push(value: Int) = q.push(value) + + @Operation + fun pop() = q.pop() + + override fun > O.customize() { + sequentialSpecification(SequentialQueue::class.java) + } +} + +class SequentialQueue : VerifierState() { + private val q = ArrayDeque() + + fun push(value: Int) { + q.offer(value) + } + + fun pop() = q.poll() + fun pop(ignore: Int) = pop() + + override fun extractState() = q.toList() +} + +class MSQueue : VerifierState() { + private class Node(val next: AtomicReference> = AtomicReference>(null), val value: S) + + private val head = AtomicReference(Node(value = null)) + private val tail = AtomicReference(head.get()) + + override fun extractState(): Any { + val result = mutableListOf() + var node = head.get() + while (node.next.get() != null) { + result.add(node.next.get().value!!) + node = node.next.get() + } + return result + } + + fun push(value: T) { + val newNode = Node(value = value) + while (true) { + val tailNode = tail.get() + if (tailNode.next.compareAndSet(null, newNode)) { + tail.compareAndSet(tailNode, newNode) + return + } else { + tail.compareAndSet(tailNode, tailNode.next.get()) + } + } + } + + fun pop(): T? { + while (true) { + val h = head.get() + val next = h.next.get() ?: return null + tail.compareAndSet(h, next) + if (head.compareAndSet(h, next)) { + return next.value!! + } + } + } +} diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/nlr/CounterFailingTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/nlr/CounterFailingTest.kt new file mode 100644 index 000000000..18d2e69c9 --- /dev/null +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/nlr/CounterFailingTest.kt @@ -0,0 +1,111 @@ +/*- + * #%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 + * . + * #L% + */ +package org.jetbrains.kotlinx.lincheck.test.verifier.nlr + +import junit.framework.Assert.assertTrue +import junit.framework.Assert.fail +import org.jetbrains.kotlinx.lincheck.LinChecker +import org.jetbrains.kotlinx.lincheck.LincheckAssertionError +import org.jetbrains.kotlinx.lincheck.annotations.Operation +import org.jetbrains.kotlinx.lincheck.annotations.Param +import org.jetbrains.kotlinx.lincheck.annotations.Recoverable +import org.jetbrains.kotlinx.lincheck.nvm.NVMCache +import org.jetbrains.kotlinx.lincheck.nvm.Persistent +import org.jetbrains.kotlinx.lincheck.paramgen.ThreadIdGen +import org.jetbrains.kotlinx.lincheck.strategy.stress.StressCTest +import org.jetbrains.kotlinx.lincheck.verifier.VerifierState +import org.junit.Test + +private const val THREADS_NUMBER = 2 + + +@StressCTest( + sequentialSpecification = SequentialCounter::class, + threads = THREADS_NUMBER, + addCrashes = true +) +internal class CounterFailingTest { + private val counter = NRLFailingCounter(THREADS_NUMBER + 2) + + @Operation + fun increment(@Param(gen = ThreadIdGen::class) threadId: Int) = counter.increment(threadId) + + @Operation + fun get(@Param(gen = ThreadIdGen::class) threadId: Int) = counter.get(threadId) + + @Test + fun testFails() { + try { + LinChecker.check(this::class.java) + } catch (e: LincheckAssertionError) { + assertTrue( + "Expected invalid execution, but found: ${e.message}", + e.message!!.contains("Invalid execution result") + ) + return + } + fail("Invalid result expected") + } +} + +private class NRLFailingCounter @Recoverable constructor(threadsCount: Int) : VerifierState() { + private val R = List(threadsCount) { NRLReadWriteObject(threadsCount).also { it.write(0, 0) } } + private val Response = MutableList(threadsCount) { Persistent(0) } + private val CheckPointer = MutableList(threadsCount) { Persistent(0) } + private val CurrentValue = MutableList(threadsCount) { Persistent(0) } + + init { + NVMCache.flush(0) + } + + override fun extractState() = R.sumBy { it.read()!! } + + @Recoverable + fun get(p: Int): Int { + val returnValue = R.sumBy { it.read()!! } + Response[p].write(p, returnValue) + Response[p].flush(p) + return returnValue + } + + @Recoverable(beforeMethod = "incrementBefore", recoverMethod = "incrementRecover") + fun increment(p: Int) { + incrementImpl(p) + } + + private fun incrementImpl(p: Int) { + R[p].write(p, 1 + CurrentValue[p].read(p)!!) + CheckPointer[p].write(p, 1) + CheckPointer[p].flush(p) + } + + private fun incrementRecover(p: Int) { + if (CheckPointer[p].read(p) == 0) return incrementImpl(p) + } + + private fun incrementBefore(p: Int) { + CurrentValue[p].write(p, R[p].read()!!) + CheckPointer[p].write(p, 0) + CurrentValue[p].flush(p) + CurrentValue[p].flush(p) // should be CheckPointer[p].flush(p) + } +} diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/nlr/CounterTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/nlr/CounterTest.kt new file mode 100644 index 000000000..04e92dc16 --- /dev/null +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/nlr/CounterTest.kt @@ -0,0 +1,110 @@ +/*- + * #%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 + * . + * #L% + */ +package org.jetbrains.kotlinx.lincheck.test.verifier.nlr + +import org.jetbrains.kotlinx.lincheck.LinChecker +import org.jetbrains.kotlinx.lincheck.annotations.Operation +import org.jetbrains.kotlinx.lincheck.annotations.Param +import org.jetbrains.kotlinx.lincheck.annotations.Recoverable +import org.jetbrains.kotlinx.lincheck.nvm.NVMCache +import org.jetbrains.kotlinx.lincheck.nvm.Persistent +import org.jetbrains.kotlinx.lincheck.paramgen.ThreadIdGen +import org.jetbrains.kotlinx.lincheck.strategy.stress.StressCTest +import org.jetbrains.kotlinx.lincheck.verifier.VerifierState +import org.junit.Test + +private const val THREADS_NUMBER = 2 + +/** + * @see Nesting-Safe Recoverable Linearizability + */ +@StressCTest( + sequentialSpecification = SequentialCounter::class, + threads = THREADS_NUMBER, + addCrashes = true +) +internal class CounterTest { + private val counter = NRLCounter(THREADS_NUMBER + 2) + + @Operation + fun increment(@Param(gen = ThreadIdGen::class) threadId: Int) = counter.increment(threadId) + + @Operation + fun get(@Param(gen = ThreadIdGen::class) threadId: Int) = counter.get(threadId) + + @Test + fun test() = LinChecker.check(this::class.java) +} + +internal class SequentialCounter : VerifierState() { + private var value = 0 + + fun get(ignore: Int) = value + fun increment(ignore: Int) { + value++ + } + + override fun extractState() = value +} + +private class NRLCounter @Recoverable constructor(threadsCount: Int) : VerifierState() { + private val R = List(threadsCount) { NRLReadWriteObject(threadsCount).also { it.write(0, 0) } } + private val Response = MutableList(threadsCount) { Persistent(0) } + private val CheckPointer = MutableList(threadsCount) { Persistent(0) } + private val CurrentValue = MutableList(threadsCount) { Persistent(0) } + + init { + NVMCache.flush(0) + } + + override fun extractState() = R.sumBy { it.read()!! } + + @Recoverable + fun get(p: Int): Int { + val returnValue = R.sumBy { it.read()!! } + Response[p].write(p, returnValue) + Response[p].flush(p) + return returnValue + } + + @Recoverable(beforeMethod = "incrementBefore", recoverMethod = "incrementRecover") + fun increment(p: Int) { + incrementImpl(p) + } + + private fun incrementImpl(p: Int) { + R[p].write(p, 1 + CurrentValue[p].read(p)!!) + CheckPointer[p].write(p, 1) + CheckPointer[p].flush(p) + } + + private fun incrementRecover(p: Int) { + if (CheckPointer[p].read(p) == 0) return incrementImpl(p) + } + + private fun incrementBefore(p: Int) { + CurrentValue[p].write(p, R[p].read()!!) + CheckPointer[p].write(p, 0) + CurrentValue[p].flush(p) + CheckPointer[p].flush(p) + } +} diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/nlr/DurableMSQueueTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/nlr/DurableMSQueueTest.kt new file mode 100644 index 000000000..92a769da9 --- /dev/null +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/nlr/DurableMSQueueTest.kt @@ -0,0 +1,136 @@ +/*- + * #%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 + * . + * #L% + */ +package org.jetbrains.kotlinx.lincheck.test.verifier.nlr + +import org.jetbrains.kotlinx.lincheck.Options +import org.jetbrains.kotlinx.lincheck.annotations.Operation +import org.jetbrains.kotlinx.lincheck.annotations.Param +import org.jetbrains.kotlinx.lincheck.paramgen.ThreadIdGen +import org.jetbrains.kotlinx.lincheck.test.AbstractLincheckTest +import org.jetbrains.kotlinx.lincheck.test.verifier.linearizability.SequentialQueue +import java.util.concurrent.atomic.AtomicInteger +import java.util.concurrent.atomic.AtomicReference + +private const val THREADS_NUMBER = 2 + +/** + * @see A Persistent Lock-Free Queue for Non-Volatile Memory + */ +class DurableMSQueueTest : AbstractLincheckTest() { + private val q = DurableMSQueue(2 + THREADS_NUMBER) + + @Operation + fun push(value: Int) = q.push(value) + + @Operation + fun pop(@Param(gen = ThreadIdGen::class) threadId: Int) = q.pop(threadId) + + override fun > O.customize() { + sequentialSpecification(SequentialQueue::class.java) + threads(THREADS_NUMBER) + } +} + + +private fun flush(value: Any) { + +} + +private const val DEFAULT_DELETER = -1 + +class DurableMSQueue(threadsCount: Int) { + private class Node( + val next: AtomicReference> = AtomicReference>(null), + val value: S, + val deleter: AtomicInteger = AtomicInteger(DEFAULT_DELETER) + ) + + private val head: AtomicReference> + private val tail: AtomicReference> + private val response: MutableList + + private val empty = Any() + private val unknown = Any() + + init { + val dummy = Node(value = null) + flush(dummy) + + head = AtomicReference(dummy) + flush(head) + + + tail = AtomicReference(dummy) + flush(tail) + + response = MutableList(threadsCount) { unknown } + flush(response) + } + + fun push(value: T) { + val newNode = Node(value = value) + flush(newNode) + while (true) { + val tailNode = tail.get() + if (tailNode.next.compareAndSet(null, newNode)) { + flush(tailNode.next) + tail.compareAndSet(tailNode, newNode) + return + } else { + flush(tailNode.next) + tail.compareAndSet(tailNode, tailNode.next.get()) + } + } + } + + fun pop(p: Int): T? { + response[p] = unknown + flush(response[p]) + + while (true) { + val h = head.get() + val next = h.next.get() + if (next == null) { + response[p] = empty + flush(response[p]) + return null + } + flush(next) + tail.compareAndSet(h, next) + if (next.deleter.compareAndSet(DEFAULT_DELETER, p)) { + flush(next.deleter.get()) + response[p] = next.value!! + flush(response[p]) + head.compareAndSet(h, next) + return next.value + } else { + val deleter = next.deleter.get() + if (head.get() == h) { + flush(h.next.get().deleter) + response[deleter] = next.value!! // previous operation has completed before this operation + flush(response[deleter]) + head.compareAndSet(h, next) + } + } + } + } +} diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/nlr/PersistentTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/nlr/PersistentTest.kt new file mode 100644 index 000000000..814b85485 --- /dev/null +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/nlr/PersistentTest.kt @@ -0,0 +1,61 @@ +/*- + * #%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 + * . + * #L% + */ + +package org.jetbrains.kotlinx.lincheck.test.verifier.nlr + +import org.jetbrains.kotlinx.lincheck.LinChecker +import org.jetbrains.kotlinx.lincheck.annotations.OpGroupConfig +import org.jetbrains.kotlinx.lincheck.annotations.Operation +import org.jetbrains.kotlinx.lincheck.nvm.Persistent +import org.jetbrains.kotlinx.lincheck.strategy.stress.StressCTest +import org.jetbrains.kotlinx.lincheck.verifier.VerifierState +import org.junit.Test + +@OpGroupConfig(name = "write", nonParallel = true) +@StressCTest( + sequentialSpecification = Sequential::class +) +internal class PersistentTest { + private val x = Persistent(0) + + @Operation + fun read() = x.read() + + @Operation(group = "write") + fun write(value: Int) { + x.write(value = value) + x.flush() + } + + @Test + fun test() = LinChecker.check(this::class.java) +} + +internal class Sequential : VerifierState() { + private var x = 0 + fun read() = x + fun write(value: Int) { + x = value + } + + override fun extractState() = x +} diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/nlr/ReadWriteObjectTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/nlr/ReadWriteObjectTest.kt new file mode 100644 index 000000000..feef41062 --- /dev/null +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/nlr/ReadWriteObjectTest.kt @@ -0,0 +1,114 @@ +/*- + * #%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 + * . + * #L% + */ +package org.jetbrains.kotlinx.lincheck.test.verifier.nlr + +import org.jetbrains.kotlinx.lincheck.LinChecker +import org.jetbrains.kotlinx.lincheck.annotations.CrashFree +import org.jetbrains.kotlinx.lincheck.annotations.Operation +import org.jetbrains.kotlinx.lincheck.annotations.Param +import org.jetbrains.kotlinx.lincheck.annotations.Recoverable +import org.jetbrains.kotlinx.lincheck.nvm.NVMCache +import org.jetbrains.kotlinx.lincheck.nvm.Persistent +import org.jetbrains.kotlinx.lincheck.paramgen.ThreadIdGen +import org.jetbrains.kotlinx.lincheck.strategy.stress.StressCTest +import org.jetbrains.kotlinx.lincheck.verifier.VerifierState +import org.junit.Test + +private const val THREADS_NUMBER = 2 + + +@StressCTest( + sequentialSpecification = SequentialReadWriteObject::class, + threads = THREADS_NUMBER, + addCrashes = true +) +class ReadWriteObjectTest { + private val operationCounter = IntArray(THREADS_NUMBER + 2) { 0 } + private val rwo = NRLReadWriteObject(THREADS_NUMBER + 2) + + @CrashFree + private data class Record(val p: Int, val counter: Int, val value: Int) + + @Operation + fun read() = rwo.read()?.value + + @Operation + fun write(@Param(gen = ThreadIdGen::class) threadId: Int, value: Int) = + rwo.write(threadId, Record(threadId, operationCounter[threadId]++, value)) + + @Test + fun test() = LinChecker.check(this.javaClass) +} + +private val nullObject = Any() + +open class SequentialReadWriteObject : VerifierState() { + private var value: Int? = null + + fun read() = value + fun write(newValue: Int) { + value = newValue + } + + fun write(ignore: Int, newValue: Int) = write(newValue) + override fun extractState() = value ?: nullObject +} + +/** + * Values must be unique. + * Use (value, op) with unique op to emulate this. + * @see Nesting-Safe Recoverable Linearizability + */ +class NRLReadWriteObject(threadsCount: Int) : VerifierState() { + @Volatile + private var R: T? = null + + // (state, value) for every thread + private val S = MutableList>>(threadsCount) { Persistent(0 to null) } + + public override fun extractState() = R ?: nullObject + + @Recoverable + fun read() = R + + @Recoverable(recoverMethod = "writeRecover") + fun write(p: Int, value: T) { + writeImpl(p, value) + } + + fun writeImpl(p: Int, value: T) { + val tmp = R + S[p].write(p, 1 to tmp) + NVMCache.flush(p) + R = value + S[p].write(p, 0 to value) + NVMCache.flush(p) + } + + fun writeRecover(p: Int, value: T) { + val (flag, current) = S[p].read(p)!! + if (flag == 0 && current != value) return writeImpl(p, value) + else if (flag == 1 && current == R) return writeImpl(p, value) + S[p].write(p, 0 to value) + NVMCache.flush(p) + } +} diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/nlr/SetTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/nlr/SetTest.kt new file mode 100644 index 000000000..7d126f745 --- /dev/null +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/nlr/SetTest.kt @@ -0,0 +1,240 @@ +/*- + * #%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 + * . + * #L% + */ +package org.jetbrains.kotlinx.lincheck.test.verifier.nlr + +import kotlinx.atomicfu.atomic +import org.jetbrains.kotlinx.lincheck.LinChecker +import org.jetbrains.kotlinx.lincheck.annotations.CrashFree +import org.jetbrains.kotlinx.lincheck.annotations.Operation +import org.jetbrains.kotlinx.lincheck.annotations.Param +import org.jetbrains.kotlinx.lincheck.annotations.Recoverable +import org.jetbrains.kotlinx.lincheck.nvm.Persistent +import org.jetbrains.kotlinx.lincheck.paramgen.ThreadIdGen +import org.jetbrains.kotlinx.lincheck.strategy.stress.StressCTest +import org.jetbrains.kotlinx.lincheck.verifier.VerifierState +import org.junit.Test +import java.util.concurrent.atomic.AtomicMarkableReference + + +private const val THREADS_NUMBER = 3 + +@StressCTest( + sequentialSpecification = SequentialSet::class, + threads = THREADS_NUMBER, + addCrashes = true +) +class SetTest { + private val set = NRLSet(2 + THREADS_NUMBER) + + @Operation + fun add(@Param(gen = ThreadIdGen::class) threadId: Int, key: Int) = set.add(threadId, key) + + @Operation + fun remove(@Param(gen = ThreadIdGen::class) threadId: Int, key: Int) = set.remove(threadId, key) + + @Operation + fun contains(key: Int) = set.contains(key) + + @Test + fun test() = LinChecker.check(this::class.java) +} + +class SequentialSet : VerifierState() { + private val set = mutableSetOf() + + fun add(ignore: Int, key: Int) = set.add(key) + fun remove(ignore: Int, key: Int) = set.remove(key) + fun contains(key: Int) = set.contains(key) + + override fun extractState() = set.toList() +} + +private const val NULL_DELETER = -1 + +/** + * @see [Tracking in Order to Recover: Recoverable Lock-Free Data Structures](https://arxiv.org/pdf/1905.13600.pdf) + */ +class NRLSet> @Recoverable constructor(threadsCount: Int) { + + private inner class Node(val value: T, next: Node?) { + val next: AtomicMarkableReference = AtomicMarkableReference(next, false) + val deleter = atomic(NULL_DELETER) + } + + private inner class Info(var node: Persistent = Persistent(null)) { + var result = Persistent(null) + } + + private inner class PrevNextPair(val previous: Node?, val next: Node?) + + private val recoveryData = MutableList(threadsCount) { Persistent(null) } + private val checkPointer = Array(threadsCount) { Persistent(0) } + private val head = atomic(null) + + @Recoverable + private fun findPrevNext(value: T): PrevNextPair { + start@ while (true) { + var previous: Node? = null + var current = head.value + while (current != null) { + val isDeleted = booleanArrayOf(false) + val next = current.next[isDeleted] + if (isDeleted[0]) { + if (previous?.next?.compareAndSet(current, next, false, false) + ?: head.compareAndSet(current, next) + ) { + current = next + continue + } else { + continue@start + } + } + if (current.value >= value) { + break + } + previous = current + current = next + } + return PrevNextPair(previous, current) + } + } + + @Recoverable(beforeMethod = "addBefore", recoverMethod = "addRecover") + fun add(p: Int, value: T) = addImpl(p, value) + + private fun addImpl(p: Int, value: T): Boolean { + val newNode = recoveryData[p].read(p)!!.node.read(p)!! + while (true) { + val prevNext = findPrevNext(value) + val previous = prevNext.previous + val next = prevNext.next + if (next != null && next.value.compareTo(value) == 0) { + recoveryData[p].read(p)!!.result.write(p, false) + recoveryData[p].read(p)!!.result.flush(p) + return false + } + newNode.next[next] = false + // flush + if (previous == null) { + if (head.compareAndSet(next, newNode)) { + recoveryData[p].read(p)!!.result.write(p, true) + recoveryData[p].read(p)!!.result.flush(p) + return true + } + } else { + if (previous.next.compareAndSet(next, newNode, false, false)) { + recoveryData[p].read(p)!!.result.write(p, true) + recoveryData[p].read(p)!!.result.flush(p) + return true + } + } + } + } + + fun addBefore(p: Int, value: T) { + checkPointer[p].write(p, 0) + checkPointer[p].flush(p) + recoveryData[p].write(p, Info(Persistent(Node(value, null)))) + recoveryData[p].flush(p) + checkPointer[p].write(p, 1) + checkPointer[p].flush(p) + } + + fun addRecover(p: Int, value: T): Boolean { + if (checkPointer[p].read(p) == 0) return addImpl(p, value) + val node = recoveryData[p].read(p)!!.node.read(p)!! + val result = recoveryData[p].read(p)!!.result.read(p) + if (result != null) return result + val prevNext = findPrevNext(value) + val current = prevNext.next + if (current === node || node.next.isMarked) { + recoveryData[p].read(p)!!.result.write(p, true) + recoveryData[p].read(p)!!.result.flush(p) + return true + } + return addImpl(p, value) + } + + @Recoverable(beforeMethod = "removeBefore", recoverMethod = "removeRecover") + fun remove(p: Int, value: T) = removeImpl(p, value) + + private fun removeImpl(p: Int, value: T): Boolean { + val prevNext = findPrevNext(value) + val previous = prevNext.previous + val current = prevNext.next + if (current == null || current.value.compareTo(value) != 0) { + recoveryData[p].read(p)!!.result.write(p, false) + recoveryData[p].read(p)!!.result.flush(p) + return false + } + recoveryData[p].read(p)!!.node.write(p, current) + recoveryData[p].read(p)!!.node.flush(p) + while (!current.next.isMarked) { + val next = current.next.reference + current.next.compareAndSet(next, next, false, true) + } + val next = current.next.reference + previous?.next?.compareAndSet(current, next, false, false) ?: head.compareAndSet(current, next) + val result = current.deleter.compareAndSet(NULL_DELETER, p) + recoveryData[p].read(p)!!.result.write(p, result) + recoveryData[p].read(p)!!.result.flush(p) + return result + } + + fun removeBefore(p: Int, value: T) { + checkPointer[p].write(p, 0) + checkPointer[p].flush(p) + recoveryData[p].write(p, Info()) + recoveryData[p].flush(p) + checkPointer[p].write(p, 1) + checkPointer[p].flush(p) + } + + fun removeRecover(p: Int, value: T): Boolean { + if (checkPointer[p].read(p) == 0) return removeImpl(p, value) + val result = recoveryData[p].read(p)!!.result.read(p) + if (result != null) return result + val node = recoveryData[p].read(p)!!.node.read(p) + if (node != null && node.next.isMarked) { + node.deleter.compareAndSet(NULL_DELETER, p) + val res = node.deleter.value == p + recoveryData[p].read(p)!!.result.write(p, res) + recoveryData[p].read(p)!!.result.flush(p) + return res + } + return removeImpl(p, value) + } + + @Recoverable + operator fun contains(value: T): Boolean { + var current = head.value + val isDeleted = booleanArrayOf(false) + while (current != null && current.value <= value) { + val next = current.next[isDeleted] + if (current.value.compareTo(value) == 0 && !isDeleted[0]) { + return true + } + current = next + } + return false + } +} diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/nlr/TestAndSetTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/nlr/TestAndSetTest.kt new file mode 100644 index 000000000..20a77b32c --- /dev/null +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/nlr/TestAndSetTest.kt @@ -0,0 +1,134 @@ +/*- + * #%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 + * . + * #L% + */ + +package org.jetbrains.kotlinx.lincheck.test.verifier.nlr + +import org.jetbrains.kotlinx.lincheck.LinChecker +import org.jetbrains.kotlinx.lincheck.annotations.CrashFree +import org.jetbrains.kotlinx.lincheck.annotations.Operation +import org.jetbrains.kotlinx.lincheck.annotations.Param +import org.jetbrains.kotlinx.lincheck.annotations.Recoverable +import org.jetbrains.kotlinx.lincheck.nvm.Persistent +import org.jetbrains.kotlinx.lincheck.paramgen.ThreadIdGen +import org.jetbrains.kotlinx.lincheck.strategy.stress.StressCTest +import org.jetbrains.kotlinx.lincheck.verifier.VerifierState +import org.junit.Test +import java.util.concurrent.atomic.AtomicInteger + +private const val THREADS_NUMBER = 5 + +@StressCTest( + sequentialSpecification = SequentialTestAndSet::class, + threads = THREADS_NUMBER, + addCrashes = true, + actorsBefore = 0, + actorsPerThread = 1 +) +internal class TestAndSetTest { + private val tas = NRLTestAndSet(THREADS_NUMBER + 2) + + @Operation + fun testAndSet(@Param(gen = ThreadIdGen::class) threadId: Int) = tas.testAndSet(threadId) + + @Test + fun test() = LinChecker.check(this::class.java) +} + +internal class SequentialTestAndSet : VerifierState() { + private var value = 0 + fun testAndSet() = value.also { value = 1 } + fun testAndSet(ignore: Int) = testAndSet() + override fun extractState() = value +} + +internal class LinearizableTestAndSet : VerifierState() { + private val value = AtomicInteger(0) + + fun testAndSet() = if (value.compareAndSet(0, 1)) 0 else 1 + public override fun extractState() = value.get() +} + +/** + * @see Nesting-Safe Recoverable Linearizability + */ +class NRLTestAndSet(private val threadsCount: Int) : VerifierState() { + private val R = MutableList(threadsCount) { Persistent(0) } + private val Response = MutableList(threadsCount) { Persistent(0) } + + @Volatile + private var Winner = -1 + + @Volatile + private var Doorway = true + + // Volatile memory + private val tas = LinearizableTestAndSet() + + override fun extractState() = tas.extractState() + + @Recoverable(recoverMethod = "testAndSetRecover") + fun testAndSet(p: Int): Int { + R[p].writeAndFlush(value = 1) + val returnValue: Int + if (!Doorway) { + returnValue = 1 + } else { + R[p].writeAndFlush(value = 2) + Doorway = false + returnValue = tas.testAndSet() + if (returnValue == 0) { + Winner = p + } + } + Response[p].writeAndFlush(value = returnValue) + R[p].writeAndFlush(value = 3) + return returnValue + } + + private fun testAndSetRecover(p: Int): Int { + if (R[p].read()!! < 2) return testAndSet(p) + if (R[p].read() == 3) return Response[p].read()!! + if (Winner == -1) { + Doorway = false + R[p].writeAndFlush(value = 4) + tas.testAndSet() + for (i in 0 until p) { + wailUntil { R[i].read()!!.let { it == 0 || it == 3 } } + } + for (i in p + 1 until threadsCount) { + wailUntil { R[i].read()!!.let { it == 0 || it > 2 } } + } + if (Winner == -1) { + Winner = p + } + } + val returnValue = if (Winner == p) 0 else 1 + Response[p].writeAndFlush(value = returnValue) + R[p].writeAndFlush(value = 3) + return returnValue + } + + private inline fun wailUntil(condition: () -> Boolean) { + while (!condition()) { + } + } +}