From 1a485d5cd37ae69628bb2b0b8c4d6f822c7ab78c Mon Sep 17 00:00:00 2001 From: Maksim Zuev Date: Wed, 22 Sep 2021 17:56:59 +0300 Subject: [PATCH] NRL Operation must be Recoverable --- .../kotlinx/lincheck/nvm/CrashTransformer.kt | 24 ++----------- .../lincheck/nvm/RecoverabilityModel.kt | 25 ++++++++++--- ...SwitchesAndCrashesModelCheckingStrategy.kt | 2 +- .../lincheck/runner/ParallelThreadsRunner.kt | 1 + .../lincheck/test/nvm/PersistentTest.kt | 3 ++ .../LincheckClassCrashFreeTest.kt | 2 ++ .../transformation/crash/CrashInsertTest.kt | 1 + .../UniformDistributedCrashesTest.kt | 4 +-- .../verifier/nrl/AbstractNVMLincheckTest.kt | 1 - .../lincheck/test/verifier/nrl/CounterTest.kt | 17 ++++++--- .../test/verifier/nrl/ReadWriteObjectTest.kt | 14 +++++--- ...erableMutualExclusionWithPrimitivesTest.kt | 7 +++- .../lincheck/test/verifier/nrl/SetTest.kt | 35 +++++++++++++++---- .../test/verifier/nrl/TestAndSetTest.kt | 14 +++++--- 14 files changed, 98 insertions(+), 52 deletions(-) diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/nvm/CrashTransformer.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/nvm/CrashTransformer.kt index 792decde2..a7922b2d0 100644 --- a/src/jvm/main/org/jetbrains/kotlinx/lincheck/nvm/CrashTransformer.kt +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/nvm/CrashTransformer.kt @@ -28,9 +28,8 @@ import org.objectweb.asm.commons.GeneratorAdapter import org.objectweb.asm.commons.Method import kotlin.reflect.jvm.javaMethod -internal open class CrashEnabledVisitor(cv: ClassVisitor, testClass: Class<*>, initial: Boolean = true) : +internal open class CrashEnabledVisitor(cv: ClassVisitor, initial: Boolean = true) : ClassVisitor(ASM_API, cv) { - private val superClassNames = testClass.superClassNames() var shouldTransform = initial private set var name: String? = null @@ -48,12 +47,6 @@ internal open class CrashEnabledVisitor(cv: ClassVisitor, testClass: Class<*>, i ) { super.visit(version, access, name, signature, superName, interfaces) this.name = name - if (name in superClassNames || name !== null && - name.startsWith("org.jetbrains.kotlinx.lincheck.") && - !name.startsWith("org.jetbrains.kotlinx.lincheck.test.") - ) { - shouldTransform = false - } } override fun visitAnnotation(descriptor: String?, visible: Boolean): AnnotationVisitor { @@ -69,10 +62,7 @@ internal open class CrashEnabledVisitor(cv: ClassVisitor, testClass: Class<*>, i } } -internal class CrashTransformer( - cv: ClassVisitor, - testClass: Class<*> -) : CrashEnabledVisitor(cv, testClass) { +internal class CrashTransformer(cv: ClassVisitor) : CrashEnabledVisitor(cv) { override fun visitMethod( access: Int, name: String?, @@ -193,13 +183,3 @@ internal class CrashRethrowTransformer(cv: ClassVisitor) : ClassVisitor(ASM_API, } } } - -private fun Class<*>.superClassNames(): List { - val result = mutableListOf() - var clazz: Class<*>? = this - while (clazz !== null) { - result.add(Type.getInternalName(clazz)) - clazz = clazz.superclass - } - return result -} diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/nvm/RecoverabilityModel.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/nvm/RecoverabilityModel.kt index 4430b99fb..4c728a8ad 100644 --- a/src/jvm/main/org/jetbrains/kotlinx/lincheck/nvm/RecoverabilityModel.kt +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/nvm/RecoverabilityModel.kt @@ -20,6 +20,8 @@ package org.jetbrains.kotlinx.lincheck.nvm +import org.jetbrains.kotlinx.lincheck.annotations.Operation +import org.jetbrains.kotlinx.lincheck.annotations.Recoverable import org.jetbrains.kotlinx.lincheck.execution.ExecutionScenario import org.jetbrains.kotlinx.lincheck.verifier.Verifier import org.jetbrains.kotlinx.lincheck.verifier.linearizability.LinearizabilityVerifier @@ -76,8 +78,8 @@ private object RecoverExecutionCallback : ExecutionCallback { internal enum class StrategyRecoveryOptions { STRESS, MANAGED; - fun createCrashTransformer(cv: ClassVisitor, clazz: Class<*>): ClassVisitor = when (this) { - STRESS -> CrashRethrowTransformer(CrashTransformer(cv, clazz)) + fun createCrashTransformer(cv: ClassVisitor): ClassVisitor = when (this) { + STRESS -> CrashRethrowTransformer(CrashTransformer(cv)) MANAGED -> CrashRethrowTransformer(cv) // add crashes in ManagedStrategyTransformer } } @@ -111,6 +113,7 @@ interface RecoverabilityModel { fun defaultExpectedCrashes(): Int fun createExecutionCallback(): ExecutionCallback fun createProbabilityModel(): ProbabilityModel + fun checkTestClass(testClass: Class<*>) {} val awaitSystemCrashBeforeThrow: Boolean val verifierClass: Class @@ -151,10 +154,24 @@ private class NRLModel( override fun createTransformer(cv: ClassVisitor, clazz: Class<*>): ClassVisitor { var result: ClassVisitor = RecoverabilityTransformer(cv) if (crashes) { - result = strategyRecoveryOptions.createCrashTransformer(result, clazz) + result = strategyRecoveryOptions.createCrashTransformer(result) } return result } + + override fun checkTestClass(testClass: Class<*>) { + var clazz: Class<*>? = testClass + while (clazz !== null) { + clazz.declaredMethods.forEach { method -> + val isOperation = method.isAnnotationPresent(Operation::class.java) + val isRecoverable = method.isAnnotationPresent(Recoverable::class.java) + require(!isOperation || isRecoverable) { + "Every operation must have a Recovery annotation, but ${method.name} operation in ${clazz!!.name} class is not Recoverable." + } + } + clazz = clazz.superclass + } + } } private open class DurableModel(val strategyRecoveryOptions: StrategyRecoveryOptions) : RecoverabilityModel { @@ -171,7 +188,7 @@ private open class DurableModel(val strategyRecoveryOptions: StrategyRecoveryOpt override val verifierClass: Class get() = DurableLinearizabilityVerifier::class.java override fun createTransformerWrapper(cv: ClassVisitor, clazz: Class<*>) = DurableRecoverAllGenerator(cv, clazz) override fun createTransformer(cv: ClassVisitor, clazz: Class<*>): ClassVisitor = - strategyRecoveryOptions.createCrashTransformer(DurableOperationRecoverTransformer(cv, clazz), clazz) + strategyRecoveryOptions.createCrashTransformer(DurableOperationRecoverTransformer(cv, clazz)) } private class DetectableExecutionModel(strategyRecoveryOptions: StrategyRecoveryOptions) : diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/nvm/SwitchesAndCrashesModelCheckingStrategy.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/nvm/SwitchesAndCrashesModelCheckingStrategy.kt index b26992103..de6cca846 100644 --- a/src/jvm/main/org/jetbrains/kotlinx/lincheck/nvm/SwitchesAndCrashesModelCheckingStrategy.kt +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/nvm/SwitchesAndCrashesModelCheckingStrategy.kt @@ -50,7 +50,7 @@ internal class SwitchesAndCrashesModelCheckingStrategy( override fun createRoot(): InterleavingTreeNode = ThreadChoosingNodeWithCrashes((0 until nThreads).toList()) override fun createTransformer(cv: ClassVisitor): ClassVisitor { - val visitor = CrashEnabledVisitor(cv, testClass, recoverModel.crashes) + val visitor = CrashEnabledVisitor(cv, recoverModel.crashes) val recoverTransformer = recoverModel.createTransformer(visitor, testClass) val managedTransformer = CrashesManagedStrategyTransformer( recoverTransformer, tracePointConstructors, testCfg.guarantees, testCfg.eliminateLocalObjects, 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 39e336a3f..60525f3b3 100644 --- a/src/jvm/main/org/jetbrains/kotlinx/lincheck/runner/ParallelThreadsRunner.kt +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/runner/ParallelThreadsRunner.kt @@ -85,6 +85,7 @@ internal open class ParallelThreadsRunner( override fun initialize() { executionCallback.reset(scenario, recoverModel) super.initialize() + recoverModel.checkTestClass(testClass) testThreadExecutions = Array(scenario.threads) { t -> TestThreadExecutionGenerator.create(this, t, scenario.parallelExecution[t], completions[t], scenario.hasSuspendableActors(), recoverModel.createActorCrashHandlerGenerator()) } diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/nvm/PersistentTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/nvm/PersistentTest.kt index 21833224b..9f38f710a 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/nvm/PersistentTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/nvm/PersistentTest.kt @@ -22,6 +22,7 @@ package org.jetbrains.kotlinx.lincheck.test.nvm import org.jetbrains.kotlinx.lincheck.LinChecker import org.jetbrains.kotlinx.lincheck.annotations.Operation +import org.jetbrains.kotlinx.lincheck.annotations.Recoverable import org.jetbrains.kotlinx.lincheck.nvm.Recover import org.jetbrains.kotlinx.lincheck.nvm.api.nonVolatile import org.jetbrains.kotlinx.lincheck.strategy.stress.StressCTest @@ -33,9 +34,11 @@ internal class PersistentTest { private val x = nonVolatile(0) @Operation + @Recoverable fun read() = x.value @Operation + @Recoverable fun write(value: Int) { x.value = value x.flush() 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 index 47eecfbdf..776ad6260 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/transformation/LincheckClassCrashFreeTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/transformation/LincheckClassCrashFreeTest.kt @@ -23,6 +23,7 @@ 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.annotations.Recoverable import org.jetbrains.kotlinx.lincheck.nvm.Recover import org.jetbrains.kotlinx.lincheck.strategy.stress.StressCTest import org.jetbrains.kotlinx.lincheck.verifier.VerifierState @@ -32,6 +33,7 @@ import org.junit.Test internal class LincheckClassCrashFreeTest : VerifierState() { @Operation + @Recoverable fun simple() = 42 @Test diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/transformation/crash/CrashInsertTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/transformation/crash/CrashInsertTest.kt index 92531bd18..2e44337c1 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/transformation/crash/CrashInsertTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/transformation/crash/CrashInsertTest.kt @@ -41,6 +41,7 @@ internal class CrashInsertTest : VerifierState() { private val c = NVMClass() @Operation + @Recoverable fun foo() = c.foo() override fun extractState() = 4 diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/transformation/crash/distribution/UniformDistributedCrashesTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/transformation/crash/distribution/UniformDistributedCrashesTest.kt index 0fd2a7cd8..c799c2c6c 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/transformation/crash/distribution/UniformDistributedCrashesTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/transformation/crash/distribution/UniformDistributedCrashesTest.kt @@ -84,12 +84,12 @@ private data class CrashPosition(val iActor: Int, val line: Int) : Comparable, expectedCrashes: Int) { val n = 1_000_000 diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/nrl/AbstractNVMLincheckTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/nrl/AbstractNVMLincheckTest.kt index ea4f326fc..5c28e419f 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/nrl/AbstractNVMLincheckTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/nrl/AbstractNVMLincheckTest.kt @@ -31,7 +31,6 @@ import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.ModelChecki import org.jetbrains.kotlinx.lincheck.strategy.stress.StressOptions import org.jetbrains.kotlinx.lincheck.test.checkTraceHasNoLincheckEvents import org.junit.Test -import java.lang.IllegalStateException import java.lang.reflect.InvocationTargetException import kotlin.reflect.KClass diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/nrl/CounterTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/nrl/CounterTest.kt index 577990234..b1ce3aca7 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/nrl/CounterTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/nrl/CounterTest.kt @@ -34,6 +34,8 @@ private const val THREADS_NUMBER = 3 internal interface Counter { fun increment(threadId: Int) fun get(threadId: Int): Int + fun incrementBefore(p: Int) {} + fun incrementRecover(p: Int) {} } /** @@ -43,9 +45,13 @@ internal class CounterTest : AbstractNVMLincheckTest(Recover.NRL, THREADS_NUMBER private val counter = NRLCounter(THREADS_NUMBER + 2) @Operation + @Recoverable(beforeMethod = "incrementBefore", recoverMethod = "incrementRecover") override fun increment(@Param(gen = ThreadIdGen::class) threadId: Int) = counter.increment(threadId) + override fun incrementBefore(p: Int) = counter.incrementBefore(p) + override fun incrementRecover(p: Int) = counter.incrementRecover(p) @Operation + @Recoverable override fun get(@Param(gen = ThreadIdGen::class) threadId: Int) = counter.get(threadId) } @@ -65,10 +71,7 @@ internal open class NRLCounter(threadsCount: Int) : Counter { protected val checkPointer = MutableList(threadsCount) { nonVolatile(0) } protected val currentValue = MutableList(threadsCount) { nonVolatile(0) } - @Recoverable override fun get(threadId: Int) = r.sumBy { it.read()!! } - - @Recoverable(beforeMethod = "incrementBefore", recoverMethod = "incrementRecover") override fun increment(threadId: Int) = incrementImpl(threadId) protected open fun incrementImpl(p: Int) { @@ -76,11 +79,11 @@ internal open class NRLCounter(threadsCount: Int) : Counter { checkPointer[p].value = 1 } - protected open fun incrementRecover(p: Int) { + override fun incrementRecover(p: Int) { if (checkPointer[p].value == 0) return incrementImpl(p) } - protected open fun incrementBefore(p: Int) { + override fun incrementBefore(p: Int) { currentValue[p].value = r[p].read()!! checkPointer[p].value = 0 currentValue[p].flush() @@ -92,10 +95,14 @@ internal abstract class CounterFailingTest : AbstractNVMLincheckFailingTest(Recover.NRL, THREADS_NUMBER, SequentialCounter::class) { protected abstract val counter: Counter + @Recoverable(beforeMethod = "incrementBefore", recoverMethod = "incrementRecover") @Operation fun increment(@Param(gen = ThreadIdGen::class) threadId: Int) = counter.increment(threadId) + fun incrementBefore(p: Int) = counter.incrementBefore(p) + fun incrementRecover(p: Int) = counter.incrementRecover(p) @Operation + @Recoverable fun get(@Param(gen = ThreadIdGen::class) threadId: Int) = counter.get(threadId) } diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/nrl/ReadWriteObjectTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/nrl/ReadWriteObjectTest.kt index 14c613f22..8b25a7cbb 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/nrl/ReadWriteObjectTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/nrl/ReadWriteObjectTest.kt @@ -43,21 +43,26 @@ private const val THREADS_NUMBER = 3 interface RWO { fun read(): T? fun write(value: T, p: Int) + fun writeRecover(value: T, p: Int) {} } internal class ReadWriteObjectTest : AbstractNVMLincheckTest(Recover.NRL, THREADS_NUMBER, SequentialReadWriteObject::class) { private val rwo = NRLReadWriteObject>(THREADS_NUMBER + 2) + @Recoverable @Operation fun read() = rwo.read()?.first + @Recoverable(recoverMethod = "writeRecover") @Operation fun write( @Param(gen = ThreadIdGen::class) threadId: Int, value: Int, @Param(gen = OperationIdGen::class) operationId: Int ) = rwo.write(value to operationId, threadId) + + fun writeRecover(threadId: Int, value: Int, operationId: Int) = rwo.writeRecover(value to operationId, threadId) } private val nullObject = Any() @@ -85,10 +90,7 @@ internal open class NRLReadWriteObject(threadsCount: Int, initial: T? = null) // (state, value) for every thread protected val state = MutableList(threadsCount) { nonVolatile(0 to null as T?) } - @Recoverable override fun read(): T? = register.value - - @Recoverable(recoverMethod = "writeRecover") override fun write(value: T, p: Int) = writeImpl(value, p) protected open fun writeImpl(value: T, p: Int) { @@ -100,7 +102,7 @@ internal open class NRLReadWriteObject(threadsCount: Int, initial: T? = null) state[p].flush() } - protected open fun writeRecover(value: T, p: Int) { + override fun writeRecover(value: T, p: Int) { val (flag, current) = state[p].value if (flag == 0 && current != value) return writeImpl(value, p) else if (flag == 1 && current === register.value) return writeImpl(value, p) @@ -114,14 +116,18 @@ internal abstract class ReadWriteObjectFailingTest : protected abstract val rwo: RWO> @Operation + @Recoverable fun read() = rwo.read()?.first @Operation + @Recoverable(recoverMethod = "writeRecover") fun write( @Param(gen = ThreadIdGen::class) threadId: Int, value: Int, @Param(gen = OperationIdGen::class) operationId: Int ) = rwo.write(value to operationId, threadId) + + fun writeRecover(threadId: Int, value: Int, operationId: Int) = rwo.writeRecover(value to operationId, threadId) } internal class SmallScenarioTest : ReadWriteObjectFailingTest() { diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/nrl/RecoverableMutualExclusionWithPrimitivesTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/nrl/RecoverableMutualExclusionWithPrimitivesTest.kt index e62d20c89..c4fff52ec 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/nrl/RecoverableMutualExclusionWithPrimitivesTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/nrl/RecoverableMutualExclusionWithPrimitivesTest.kt @@ -37,8 +37,11 @@ private const val THREADS = 3 internal class RecoverableMutualExclusionWithPrimitivesTest : AbstractNVMLincheckTest(Recover.NRL, THREADS, SequentialCounter::class) { private val counter = CounterWithLock(THREADS + 2, LockWithPrimitives(THREADS + 2)) + @Recoverable(recoverMethod = "incRecover", beforeMethod = "incBefore") @Operation fun inc(@Param(gen = ThreadIdGen::class) threadId: Int): Int = counter.inc(threadId) + fun incRecover(threadId: Int) = counter.incRecover(threadId) + fun incBefore(threadId: Int) = counter.incBefore(threadId) override fun testWithStressStrategy() { println("${this::class.qualifiedName}:testWithStressStrategy test is ignored as no special atomic primitives available.") @@ -61,7 +64,6 @@ internal class CounterWithLock(threads: Int, private val lock: DurableLock) { private val cp = Array(threads) { nonVolatile(0) } private val before = Array(threads) { nonVolatile(0) } - @Recoverable(recoverMethod = "incRecover", beforeMethod = "incBefore") fun inc(threadId: Int) = incInternal(threadId) private fun incInternal(threadId: Int): Int { @@ -193,8 +195,11 @@ internal class LockWithPrimitives(threads: Int) : DurableLock { internal class MutualExclusionFailingTest : AbstractNVMLincheckFailingTest(Recover.NRL, THREADS, SequentialCounter::class, false, DeadlockWithDumpFailure::class) { private val counter = CounterWithLock(THREADS + 2, SimplestLockEver()) + @Recoverable(recoverMethod = "incRecover", beforeMethod = "incBefore") @Operation fun inc(@Param(gen = ThreadIdGen::class) threadId: Int): Int = counter.inc(threadId) + fun incRecover(threadId: Int) = counter.incRecover(threadId) + fun incBefore(threadId: Int) = counter.incBefore(threadId) override fun > O.customize() { actorsBefore(0) diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/nrl/SetTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/nrl/SetTest.kt index be4084a99..90f6d5db1 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/nrl/SetTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/nrl/SetTest.kt @@ -38,7 +38,12 @@ private const val THREADS_NUMBER = 3 internal interface RecoverableSet { fun add(p: Int, value: T): Boolean + fun addBefore(p: Int, value: T) + fun addRecover(p: Int, value: T): Boolean fun remove(p: Int, value: T): Boolean + + fun removeBefore(p: Int, value: T) + fun removeRecover(p: Int, value: T): Boolean operator fun contains(value: T): Boolean } @@ -46,13 +51,22 @@ internal interface RecoverableSet { internal class SetTest : AbstractNVMLincheckTest(Recover.NRL, THREADS_NUMBER, SequentialSet::class) { private val set = NRLSet(2 + THREADS_NUMBER) + @Recoverable(beforeMethod = "addBefore", recoverMethod = "addRecover") @Operation fun add(@Param(gen = ThreadIdGen::class) threadId: Int, @Param(name = "key") key: Int) = set.add(threadId, key) + fun addRecover(threadId: Int, key: Int) = set.addRecover(threadId, key) + fun addBefore(threadId: Int, key: Int) = set.addBefore(threadId, key) + + @Recoverable(beforeMethod = "removeBefore", recoverMethod = "removeRecover") @Operation fun remove(@Param(gen = ThreadIdGen::class) threadId: Int, @Param(name = "key") key: Int) = set.remove(threadId, key) + fun removeRecover(threadId: Int, key: Int) = set.removeRecover(threadId, key) + fun removeBefore(threadId: Int, key: Int) = set.removeBefore(threadId, key) + + @Recoverable @Operation fun contains(@Param(name = "key") key: Int) = set.contains(key) } @@ -117,7 +131,7 @@ internal open class NRLSet>(threadsCount: Int) : RecoverableSe } } - @Recoverable(beforeMethod = "addBefore", recoverMethod = "addRecover") + override fun add(p: Int, value: T) = addImpl(p, value) protected open fun addImpl(p: Int, value: T): Boolean { @@ -145,7 +159,7 @@ internal open class NRLSet>(threadsCount: Int) : RecoverableSe } } - protected open fun addBefore(p: Int, value: T) { + override fun addBefore(p: Int, value: T) { checkPointer[p].value = 0 checkPointer[p].flush() recoveryData[p].value = Info(nonVolatile(Node(value, null))) @@ -154,7 +168,7 @@ internal open class NRLSet>(threadsCount: Int) : RecoverableSe checkPointer[p].flush() } - protected open fun addRecover(p: Int, value: T): Boolean { + override fun addRecover(p: Int, value: T): Boolean { if (checkPointer[p].value == 0) return addImpl(p, value) val node = recoveryData[p].value!!.node.value!! val result = recoveryData[p].value!!.result.value @@ -168,7 +182,6 @@ internal open class NRLSet>(threadsCount: Int) : RecoverableSe return addImpl(p, value) } - @Recoverable(beforeMethod = "removeBefore", recoverMethod = "removeRecover") override fun remove(p: Int, value: T) = removeImpl(p, value) protected open fun removeImpl(p: Int, value: T): Boolean { @@ -194,7 +207,7 @@ internal open class NRLSet>(threadsCount: Int) : RecoverableSe return result } - protected open fun removeBefore(p: Int, value: T) { + override fun removeBefore(p: Int, value: T) { checkPointer[p].value = 0 checkPointer[p].flush() recoveryData[p].value = Info() @@ -203,7 +216,7 @@ internal open class NRLSet>(threadsCount: Int) : RecoverableSe checkPointer[p].flush() } - protected open fun removeRecover(p: Int, value: T): Boolean { + override fun removeRecover(p: Int, value: T): Boolean { if (checkPointer[p].value == 0) return removeImpl(p, value) val result = recoveryData[p].value!!.result.value if (result != null) return result @@ -219,7 +232,6 @@ internal open class NRLSet>(threadsCount: Int) : RecoverableSe return removeImpl(p, value) } - @Recoverable override operator fun contains(value: T): Boolean { var current = head.get() val isDeleted = booleanArrayOf(false) @@ -239,13 +251,22 @@ internal abstract class SetFailingTest : AbstractNVMLincheckFailingTest(Recover.NRL, THREADS_NUMBER, SequentialSet::class) { protected abstract val set: RecoverableSet + @Recoverable(beforeMethod = "addBefore", recoverMethod = "addRecover") @Operation fun add(@Param(gen = ThreadIdGen::class) threadId: Int, @Param(name = "key") key: Int) = set.add(threadId, key) + fun addRecover(threadId: Int, key: Int) = set.addRecover(threadId, key) + fun addBefore(threadId: Int, key: Int) = set.addBefore(threadId, key) + + @Recoverable(beforeMethod = "removeBefore", recoverMethod = "removeRecover") @Operation fun remove(@Param(gen = ThreadIdGen::class) threadId: Int, @Param(name = "key") key: Int) = set.remove(threadId, key) + fun removeRecover(threadId: Int, key: Int) = set.removeRecover(threadId, key) + fun removeBefore(threadId: Int, key: Int) = set.removeBefore(threadId, key) + + @Recoverable @Operation fun contains(@Param(name = "key") key: Int) = set.contains(key) override val expectedExceptions = listOf(NullPointerException::class) diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/nrl/TestAndSetTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/nrl/TestAndSetTest.kt index c7d2ddf5e..5c664e4b3 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/nrl/TestAndSetTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/nrl/TestAndSetTest.kt @@ -35,13 +35,17 @@ private const val THREADS_NUMBER = 5 interface TAS { fun testAndSet(threadId: Int): Int + fun testAndSetRecover(threadId: Int): Int = -1 } internal class TestAndSetTest : AbstractNVMLincheckTest(Recover.NRL, THREADS_NUMBER, SequentialTestAndSet::class) { private val tas = NRLTestAndSet(THREADS_NUMBER + 2) + @Recoverable(recoverMethod = "testAndSetRecover") @Operation fun testAndSet(@Param(gen = ThreadIdGen::class) threadId: Int) = tas.testAndSet(threadId) + + fun testAndSetRecover(threadId: Int) = tas.testAndSetRecover(threadId) override fun > O.customize() { actorsBefore(0) actorsPerThread(1) @@ -66,7 +70,7 @@ internal open class NRLTestAndSet(private val threadsCount: Int) : TAS { protected val doorway = nonVolatile(true) protected val tas = nonVolatile(0) - @Recoverable(recoverMethod = "testAndSetRecover") + override fun testAndSet(p: Int): Int { r[p].setToNVM(1) val returnValue: Int @@ -85,7 +89,7 @@ internal open class NRLTestAndSet(private val threadsCount: Int) : TAS { return returnValue } - protected open fun testAndSetRecover(p: Int): Int { + override fun testAndSetRecover(p: Int): Int { if (r[p].value < 2) return testAndSet(p) if (r[p].value == 3) return response[p].value if (winner.value == -1) { @@ -118,8 +122,11 @@ internal abstract class TestAndSetFailingTest : AbstractNVMLincheckFailingTest(Recover.NRL, THREADS_NUMBER, SequentialTestAndSet::class) { protected abstract val tas: TAS + @Recoverable(recoverMethod = "testAndSetRecover") @Operation fun testAndSet(@Param(gen = ThreadIdGen::class) threadId: Int) = tas.testAndSet(threadId) + + fun testAndSetRecover(threadId: Int) = tas.testAndSetRecover(threadId) override fun > O.customize() { actorsBefore(0) actorsPerThread(1) @@ -160,7 +167,6 @@ internal class TestAndSetFailingTest8 : TestAndSetFailingTest() { } internal class NRLFailingTestAndSet1(threadsCount: Int) : NRLTestAndSet(threadsCount) { - @Recoverable(recoverMethod = "testAndSetRecover") override fun testAndSet(p: Int): Int { r[p].setToNVM(1) val returnValue: Int @@ -287,7 +293,6 @@ internal class NRLFailingTestAndSet5(private val threadsCount: Int) : NRLTestAnd } internal class NRLFailingTestAndSet6(threadsCount: Int) : NRLTestAndSet(threadsCount) { - @Recoverable(recoverMethod = "testAndSetRecover") override fun testAndSet(p: Int): Int { r[p].setToNVM(1) val returnValue: Int @@ -308,7 +313,6 @@ internal class NRLFailingTestAndSet6(threadsCount: Int) : NRLTestAndSet(threadsC } internal class NRLFailingTestAndSet7(threadsCount: Int) : NRLTestAndSet(threadsCount) { - @Recoverable(recoverMethod = "testAndSetRecover") override fun testAndSet(p: Int): Int { r[p].setToNVM(1) val returnValue: Int