From 3bc3c600d84b11ac6ba5867126cda49b789313fe Mon Sep 17 00:00:00 2001 From: Alexander Fedorov Date: Mon, 7 Dec 2020 23:40:27 +0300 Subject: [PATCH] Add switch points into cancellation handlers (#66) --- .../org/jetbrains/kotlinx/lincheck/Utils.kt | 15 ++-- .../lincheck/runner/ParallelThreadsRunner.kt | 13 ++-- .../strategy/managed/ManagedStrategy.kt | 70 +++++++++++++++---- .../managed/ManagedStrategyTransformer.kt | 26 ------- .../lincheck/strategy/managed/TracePoint.kt | 30 +++++++- .../strategy/managed/TraceReporter.kt | 2 - .../lincheck/test/AbstractLincheckTest.kt | 10 ++- .../test/IncorrectOnCancellationTest.kt | 46 ++++++++++++ .../AFUCallRepresentationTest.kt | 2 + .../CapturedValueRepresentationTest.kt | 2 + ...CoroutineCancellationTraceReportingTest.kt | 64 +++++++++++++++++ .../representation/MethodReportingTest.kt | 3 + .../ObstructionFreedomRepresentationTest.kt | 3 + .../representation/StateRepresentationTest.kt | 3 + ...ngTest.kt => SuspendTraceReportingTest.kt} | 43 +++--------- .../SwitchAsFirstMethodEventTest.kt | 2 + .../test/representation/TraceReportingTest.kt | 6 +- .../test/representation/VerboseTraceTest.kt | 2 + 18 files changed, 250 insertions(+), 92 deletions(-) create mode 100644 src/jvm/test/org/jetbrains/kotlinx/lincheck/test/IncorrectOnCancellationTest.kt create mode 100644 src/jvm/test/org/jetbrains/kotlinx/lincheck/test/representation/CoroutineCancellationTraceReportingTest.kt rename src/jvm/test/org/jetbrains/kotlinx/lincheck/test/representation/{SuspendInterleavingReportingTest.kt => SuspendTraceReportingTest.kt} (72%) diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/Utils.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/Utils.kt index 2773f10a2..0484ae880 100644 --- a/src/jvm/main/org/jetbrains/kotlinx/lincheck/Utils.kt +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/Utils.kt @@ -190,20 +190,25 @@ internal class StoreExceptionHandler : AbstractCoroutineContextElement(Coroutine } @Suppress("INVISIBLE_REFERENCE", "INVISIBLE_MEMBER") -fun CancellableContinuation.cancelByLincheck(promptCancellation: Boolean): Boolean { +internal fun CancellableContinuation.cancelByLincheck(promptCancellation: Boolean): CancellationResult { val exceptionHandler = context[CoroutineExceptionHandler] as StoreExceptionHandler exceptionHandler.exception = null val cancelled = cancel(cancellationByLincheckException) exceptionHandler.exception?.let { throw it.cause!! // let's throw the original exception, ignoring the internal coroutines details } - if (!cancelled && promptCancellation) { - context[Job]!!.cancel() // we should always put a job into the context for prompt cancellation - return true + return when { + cancelled -> CancellationResult.CANCELLED_BEFORE_RESUMPTION + promptCancellation -> { + context[Job]!!.cancel() // we should always put a job into the context for prompt cancellation + CancellationResult.CANCELLED_AFTER_RESUMPTION + } + else -> CancellationResult.CANCELLATION_FAILED } - return cancelled } +internal enum class CancellationResult { CANCELLED_BEFORE_RESUMPTION, CANCELLED_AFTER_RESUMPTION, CANCELLATION_FAILED } + @Suppress("INVISIBLE_REFERENCE", "INVISIBLE_MEMBER") private val cancelCompletedResultMethod = DispatchedTask::class.declaredFunctions.find { it.name == "cancelCompletedResult" }!!.javaMethod!! 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 0d199b9be..34d9d9ed9 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,7 @@ package org.jetbrains.kotlinx.lincheck.runner import kotlinx.coroutines.* import org.jetbrains.kotlinx.lincheck.* +import org.jetbrains.kotlinx.lincheck.CancellationResult.* import org.jetbrains.kotlinx.lincheck.execution.* import org.jetbrains.kotlinx.lincheck.runner.FixedActiveThreadsExecutor.TestThread import org.jetbrains.kotlinx.lincheck.runner.UseClocks.* @@ -181,12 +182,11 @@ internal open class ParallelThreadsRunner( val finalResult = if (res === COROUTINE_SUSPENDED) { val t = Thread.currentThread() as TestThread val cont = t.cont.also { t.cont = null } - if (actor.cancelOnSuspension && cont !== null && cont.cancelByLincheck(actor.promptCancellation)) { + if (actor.cancelOnSuspension && cont !== null && cancelByLincheck(cont, actor.promptCancellation) != CANCELLATION_FAILED) { if (!trySetCancelledStatus(iThread, actorId)) { // already resumed, increment `completedOrSuspendedThreads` back completedOrSuspendedThreads.incrementAndGet() } - afterCoroutineCancelled(iThread) Cancelled } else waitAndInvokeFollowUp(iThread, actorId) } else createLincheckResult(res) @@ -226,14 +226,19 @@ internal open class ParallelThreadsRunner( return suspensionPointResults[iThread][actorId] } + /** + * This method is used for communication between `ParallelThreadsRunner` and `ManagedStrategy` via overriding, + * so that runner do not know about managed strategy details. + */ + internal open fun cancelByLincheck(cont: CancellableContinuation, promptCancellation: Boolean): CancellationResult = + cont.cancelByLincheck(promptCancellation) + override fun afterCoroutineSuspended(iThread: Int) { completedOrSuspendedThreads.incrementAndGet() } override fun afterCoroutineResumed(iThread: Int) {} - override fun afterCoroutineCancelled(iThread: Int) {} - // We cannot use `completionStatuses` here since // they are set _before_ the result is published. override fun isCoroutineResumed(iThread: Int, actorId: Int) = diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/ManagedStrategy.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/ManagedStrategy.kt index 9fcddcdbc..de3c70d88 100644 --- a/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/ManagedStrategy.kt +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/ManagedStrategy.kt @@ -21,7 +21,9 @@ */ package org.jetbrains.kotlinx.lincheck.strategy.managed +import kotlinx.coroutines.* import org.jetbrains.kotlinx.lincheck.* +import org.jetbrains.kotlinx.lincheck.CancellationResult.* import org.jetbrains.kotlinx.lincheck.execution.* import org.jetbrains.kotlinx.lincheck.runner.* import org.jetbrains.kotlinx.lincheck.strategy.* @@ -286,7 +288,7 @@ abstract class ManagedStrategy( if (loopDetector.visitCodeLocation(iThread, codeLocation)) { failIfObstructionFreedomIsRequired { // Log the last event that caused obstruction freedom violation - traceCollector?.passCodeLocation(codeLocation, tracePoint) + traceCollector?.passCodeLocation(tracePoint) "Obstruction-freedom is required but an active lock has been found" } checkLiveLockHappened(loopDetector.totalOperations) @@ -297,7 +299,7 @@ abstract class ManagedStrategy( val reason = if (isLoop) SwitchReason.ACTIVE_LOCK else SwitchReason.STRATEGY_SWITCH switchCurrentThread(iThread, reason) } - traceCollector?.passCodeLocation(codeLocation, tracePoint) + traceCollector?.passCodeLocation(tracePoint) // continue the operation } @@ -462,7 +464,7 @@ abstract class ManagedStrategy( internal fun beforeLockRelease(iThread: Int, codeLocation: Int, tracePoint: MonitorExitTracePoint?, monitor: Any): Boolean { if (inIgnoredSection(iThread)) return true monitorTracker.releaseMonitor(monitor) - traceCollector?.passCodeLocation(codeLocation, tracePoint) + traceCollector?.passCodeLocation(tracePoint) return false } @@ -485,7 +487,7 @@ abstract class ManagedStrategy( */ @Suppress("UNUSED_PARAMETER") internal fun afterUnpark(iThread: Int, codeLocation: Int, tracePoint: UnparkTracePoint?, thread: Any) { - traceCollector?.passCodeLocation(codeLocation, tracePoint) + traceCollector?.passCodeLocation(tracePoint) } /** @@ -515,7 +517,7 @@ abstract class ManagedStrategy( monitorTracker.notifyAll(monitor) else monitorTracker.notify(monitor) - traceCollector?.passCodeLocation(codeLocation, tracePoint) + traceCollector?.passCodeLocation(tracePoint) } /** @@ -586,7 +588,7 @@ abstract class ManagedStrategy( */ @Suppress("UNUSED_PARAMETER") internal fun beforeMethodCall(iThread: Int, codeLocation: Int, tracePoint: MethodCallTracePoint) { - if (isTestThread(iThread)) { + if (isTestThread(iThread) && !inIgnoredSection(iThread)) { check(collectTrace) { "This method should be called only when logging is enabled" } val callStackTrace = callStackTrace[iThread] val suspendedMethodStack = suspendedFunctionsStack[iThread] @@ -611,7 +613,7 @@ abstract class ManagedStrategy( * @param tracePoint the corresponding trace point for the invocation */ internal fun afterMethodCall(iThread: Int, tracePoint: MethodCallTracePoint) { - if (isTestThread(iThread)) { + if (isTestThread(iThread) && !inIgnoredSection(iThread)) { check(collectTrace) { "This method should be called only when logging is enabled" } val callStackTrace = callStackTrace[iThread] if (tracePoint.wasSuspended) { @@ -631,11 +633,26 @@ abstract class ManagedStrategy( * @param constructorId which constructor to use for creating code location * @return the created interleaving point */ - fun createTracePoint(constructorId: Int): TracePoint { + fun createTracePoint(constructorId: Int): TracePoint = doCreateTracePoint(tracePointConstructors[constructorId]) + + /** + * Creates a new [CoroutineCancellationTracePoint]. + * This method is similar to [createTracePoint] method, but also adds the new trace point to the trace. + */ + internal fun createAndLogCancellationTracePoint(): CoroutineCancellationTracePoint? { + if (collectTrace) { + val cancellationTracePoint = doCreateTracePoint(::CoroutineCancellationTracePoint) + traceCollector?.passCodeLocation(cancellationTracePoint) + return cancellationTracePoint + } + return null + } + + private fun doCreateTracePoint(constructor: (iThread: Int, actorId: Int, CallStackTrace) -> T): T { val iThread = currentThreadNumber() // use any actor id for non-test threads val actorId = if (!isTestThread(iThread)) Int.MIN_VALUE else currentActorId[iThread] - return tracePointConstructors[constructorId](iThread, actorId, callStackTrace.getOrNull(iThread)?.toList() ?: emptyList()) + return constructor(iThread, actorId, callStackTrace.getOrNull(iThread)?.toList() ?: emptyList()) } /** @@ -688,17 +705,12 @@ abstract class ManagedStrategy( _trace += FinishThreadTracePoint(iThread) } - fun passCodeLocation(codeLocation: Int, tracePoint: TracePoint?) { - // Ignore coroutine suspensions - they are processed in another place. - if (codeLocation == COROUTINE_SUSPENSION_CODE_LOCATION) return + fun passCodeLocation(tracePoint: TracePoint?) { _trace += tracePoint!! } fun addStateRepresentation(iThread: Int) { - // enter ignored section, because stateRepresentation invokes transformed method with switch points - enterIgnoredSection(iThread) val stateRepresentation = runner.constructStateRepresentation()!! - leaveIgnoredSection(iThread) // use call stack trace of the previous trace point val callStackTrace = _trace.last().callStackTrace.toList() _trace += StateRepresentationTracePoint(iThread, currentActorId[iThread], stateRepresentation, callStackTrace) @@ -743,6 +755,34 @@ private class ManagedStrategyRunner( super.afterCoroutineCancelled(iThread) managedStrategy.afterCoroutineCancelled(iThread) } + + override fun constructStateRepresentation(): String? { + // Enter ignored section, because Runner will call transformed state representation method + val iThread = managedStrategy.currentThreadNumber() + managedStrategy.enterIgnoredSection(iThread) + val stateRepresentation = super.constructStateRepresentation() + managedStrategy.leaveIgnoredSection(iThread) + return stateRepresentation + } + + override fun cancelByLincheck(cont: CancellableContinuation, promptCancellation: Boolean): CancellationResult { + // Create a cancellation trace point before `cancel`, so that cancellation trace point + // precede the events in `onCancellation` handler. + val cancellationTracePoint = managedStrategy.createAndLogCancellationTracePoint() + try { + // Call the `cancel` method. + val cancellationResult = super.cancelByLincheck(cont, promptCancellation) + // Pass the result to `cancellationTracePoint`. + cancellationTracePoint?.initializeCancellationResult(cancellationResult) + // Invoke `strategy.afterCoroutineCancelled` if the coroutine was cancelled successfully. + if (cancellationResult != CANCELLATION_FAILED) + managedStrategy.afterCoroutineCancelled(managedStrategy.currentThreadNumber()) + return cancellationResult + } catch(e: Throwable) { + cancellationTracePoint?.initializeException(e) + throw e // throw further + } + } } /** diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/ManagedStrategyTransformer.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/ManagedStrategyTransformer.kt index 20bf36494..4099aa5ad 100644 --- a/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/ManagedStrategyTransformer.kt +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/ManagedStrategyTransformer.kt @@ -91,7 +91,6 @@ internal class ManagedStrategyTransformer( mv = WaitNotifyTransformer(mname, GeneratorAdapter(mv, access, mname, desc)) mv = ParkUnparkTransformer(mname, GeneratorAdapter(mv, access, mname, desc)) mv = LocalObjectManagingTransformer(mname, GeneratorAdapter(mv, access, mname, desc)) - mv = CancellabilitySupportMethodTransformer(mname, GeneratorAdapter(mv, access, mname, desc)) mv = SharedVariableAccessMethodTransformer(mname, GeneratorAdapter(mv, access, mname, desc)) mv = TimeStubTransformer(GeneratorAdapter(mv, access, mname, desc)) mv = RandomTransformer(GeneratorAdapter(mv, access, mname, desc)) @@ -949,31 +948,6 @@ internal class ManagedStrategyTransformer( } } - /** - * Removes switch points in CancellableContinuationImpl.cancel, so that they will not be reported - * when a continuation is cancelled by lincheck - */ - private inner class CancellabilitySupportMethodTransformer(methodName: String, mv: GeneratorAdapter) : ManagedStrategyMethodVisitor(methodName, mv) { - private val isCancel = className == "kotlinx/coroutines/CancellableContinuationImpl" && - (methodName == "cancel" || methodName == "cancelCompletedResult") - - override fun visitCode() { - if (isCancel) - invokeBeforeIgnoredSectionEntering() - mv.visitCode() - } - - override fun visitInsn(opcode: Int) { - if (isCancel) { - when (opcode) { - ARETURN, DRETURN, FRETURN, IRETURN, LRETURN, RETURN -> invokeAfterIgnoredSectionLeaving() - else -> { } - } - } - mv.visitInsn(opcode) - } - } - /** * Track local objects for odd switch points elimination. * A local object is an object that can be possible viewed only from one thread. diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/TracePoint.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/TracePoint.kt index 0ee200702..e4f88546f 100644 --- a/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/TracePoint.kt +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/TracePoint.kt @@ -21,12 +21,13 @@ */ package org.jetbrains.kotlinx.lincheck.strategy.managed +import org.jetbrains.kotlinx.lincheck.* +import org.jetbrains.kotlinx.lincheck.CancellationResult.* import java.math.* -import java.util.* import kotlin.coroutines.* import kotlin.coroutines.intrinsics.* -class Trace(val trace: List, val verboseTrace: Boolean) +data class Trace(val trace: List, val verboseTrace: Boolean) /** * Essentially, a trace is a list of trace points, which represent @@ -216,6 +217,31 @@ internal class UnparkTracePoint( override fun toStringImpl(): String = "UNPARK at " + stackTraceElement.shorten() } +internal class CoroutineCancellationTracePoint( + iThread: Int, actorId: Int, + callStackTrace: CallStackTrace, +) : TracePoint(iThread, actorId, callStackTrace) { + private lateinit var cancellationResult: CancellationResult + private var exception: Throwable? = null + + fun initializeCancellationResult(cancellationResult: CancellationResult) { + this.cancellationResult = cancellationResult + } + + fun initializeException(e: Throwable) { + this.exception = e; + } + + override fun toStringImpl(): String { + if (exception != null) return "EXCEPTION WHILE CANCELLATION" + return when (cancellationResult) { + CANCELLED_BEFORE_RESUMPTION -> "CANCELLED BEFORE RESUMPTION" + CANCELLED_AFTER_RESUMPTION -> "PROMPT CANCELLED AFTER RESUMPTION" + CANCELLATION_FAILED -> "CANCELLATION ATTEMPT FAILED" + } + } +} + /** * Removes package info in the stack trace element representation. */ diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/TraceReporter.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/TraceReporter.kt index aeb61213d..492fe9af3 100644 --- a/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/TraceReporter.kt +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/TraceReporter.kt @@ -267,8 +267,6 @@ private class ActorResultNode(iThread: Int, last: TraceNode?, verboseTrace: Bool override val shouldBeExpanded: Boolean = false override fun addRepresentationTo(traceRepresentation: MutableList): TraceNode? { - if (result == Cancelled) - traceRepresentation.add(TraceEventRepresentation(iThread, traceIndentation() + "CONTINUATION CANCELLED")) if (result != null) traceRepresentation.add(TraceEventRepresentation(iThread, traceIndentation() + "result: $result")) return next diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/AbstractLincheckTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/AbstractLincheckTest.kt index ba83d3eca..632eec5b2 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/AbstractLincheckTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/AbstractLincheckTest.kt @@ -23,6 +23,7 @@ package org.jetbrains.kotlinx.lincheck.test import org.jetbrains.kotlinx.lincheck.* import org.jetbrains.kotlinx.lincheck.strategy.* +import org.jetbrains.kotlinx.lincheck.strategy.managed.* import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.ModelCheckingOptions import org.jetbrains.kotlinx.lincheck.strategy.stress.* import org.jetbrains.kotlinx.lincheck.verifier.* @@ -42,6 +43,7 @@ abstract class AbstractLincheckTest( "This test should fail, but no error has been occurred (see the logs for details)" } } else { + failure.trace?.let { checkTraceHasNoLincheckEvents(it.toString()) } assert(expectedFailures.contains(failure::class)) { "This test has failed with an unexpected error: \n $failure" } @@ -73,4 +75,10 @@ abstract class AbstractLincheckTest( } } -private const val TIMEOUT = 100_000L \ No newline at end of file +private const val TIMEOUT = 100_000L + +fun checkTraceHasNoLincheckEvents(trace: String) { + val testPackageOccurrences = trace.split("org.jetbrains.kotlinx.lincheck.test.").size - 1 + val lincheckPackageOccurrences = trace.split("org.jetbrains.kotlinx.lincheck.").size - 1 + check(testPackageOccurrences == lincheckPackageOccurrences) { "Internal Lincheck events were found in the trace" } +} \ No newline at end of file diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/IncorrectOnCancellationTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/IncorrectOnCancellationTest.kt new file mode 100644 index 000000000..3bf6b293a --- /dev/null +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/IncorrectOnCancellationTest.kt @@ -0,0 +1,46 @@ +/* + * 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 + * + */ + +package org.jetbrains.kotlinx.lincheck.test + +import kotlinx.coroutines.* +import org.jetbrains.kotlinx.lincheck.annotations.* +import org.jetbrains.kotlinx.lincheck.strategy.* + +class IncorrectOnCancellationTest : AbstractLincheckTest(IncorrectResultsFailure::class) { + @Volatile + var canEnterForbiddenSection = false + + @InternalCoroutinesApi + @Operation(cancellableOnSuspension = true) + suspend fun cancelledOp(): Int { + if (canEnterForbiddenSection) + return 42 + suspendCancellableCoroutine { cont -> + cont.invokeOnCancellation { + canEnterForbiddenSection = true + canEnterForbiddenSection = false + } + } + return 0 + } + + override fun extractState(): Any = 0 // constant state +} \ No newline at end of file diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/representation/AFUCallRepresentationTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/representation/AFUCallRepresentationTest.kt index 9df303e0a..88631ea8a 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/representation/AFUCallRepresentationTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/representation/AFUCallRepresentationTest.kt @@ -25,6 +25,7 @@ import org.jetbrains.kotlinx.lincheck.* import org.jetbrains.kotlinx.lincheck.annotations.Operation import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.* import org.jetbrains.kotlinx.lincheck.strategy.stress.* +import org.jetbrains.kotlinx.lincheck.test.* import org.jetbrains.kotlinx.lincheck.verifier.* import org.junit.* import java.util.concurrent.atomic.* @@ -65,5 +66,6 @@ class AFUCallRepresentationTest : VerifierState() { check(failure != null) { "the test should fail" } val log = StringBuilder().appendFailure(failure).toString() check("counter.compareAndSet(0,1)" in log) + checkTraceHasNoLincheckEvents(log) } } diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/representation/CapturedValueRepresentationTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/representation/CapturedValueRepresentationTest.kt index fdb95b310..d90c19ebd 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/representation/CapturedValueRepresentationTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/representation/CapturedValueRepresentationTest.kt @@ -24,6 +24,7 @@ package org.jetbrains.kotlinx.lincheck.test.representation import org.jetbrains.kotlinx.lincheck.annotations.Operation import org.jetbrains.kotlinx.lincheck.checkImpl import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.ModelCheckingOptions +import org.jetbrains.kotlinx.lincheck.test.* import org.jetbrains.kotlinx.lincheck.verifier.VerifierState import org.junit.Test @@ -68,6 +69,7 @@ class CapturedValueRepresentationTest : VerifierState() { check(" int[]@1" in log) check(" String[]@1" in log) check(" 0" in log) + checkTraceHasNoLincheckEvents(log) } override fun extractState(): Any = counter diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/representation/CoroutineCancellationTraceReportingTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/representation/CoroutineCancellationTraceReportingTest.kt new file mode 100644 index 000000000..e21f291fe --- /dev/null +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/representation/CoroutineCancellationTraceReportingTest.kt @@ -0,0 +1,64 @@ +/* + * 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 + * + */ + +package org.jetbrains.kotlinx.lincheck.test.representation + +import kotlinx.coroutines.* +import org.jetbrains.kotlinx.lincheck.* +import org.jetbrains.kotlinx.lincheck.annotations.Operation +import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.* +import org.jetbrains.kotlinx.lincheck.test.* +import org.jetbrains.kotlinx.lincheck.verifier.* +import org.junit.* + +class CoroutineCancellationTraceReportingTest : VerifierState() { + @Volatile + var correct = true + + @InternalCoroutinesApi + @Operation(cancellableOnSuspension = true) + suspend fun cancelledOp() { + suspendCancellableCoroutine { cont -> + cont.invokeOnCancellation { + correct = false + } + } + } + + @Operation + fun isAbsurd(): Boolean = correct && !correct + + override fun extractState(): Any = correct + + @Test + fun test() { + val failure = ModelCheckingOptions() + .actorsPerThread(1) + .actorsBefore(0) + .actorsAfter(0) + .verboseTrace(true) + .checkImpl(this::class.java) + checkNotNull(failure) { "the test should fail" } + val log = failure.toString() + check("CANCELLED BEFORE RESUMPTION" in log) { "The cancellation event should be reported" } + check("setCorrect(false)" in log) { "The `onCancellation` handler events should be reported" } + checkTraceHasNoLincheckEvents(log) + } +} \ No newline at end of file diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/representation/MethodReportingTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/representation/MethodReportingTest.kt index 607595191..f7c91c96b 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/representation/MethodReportingTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/representation/MethodReportingTest.kt @@ -25,6 +25,7 @@ import org.jetbrains.kotlinx.lincheck.* import org.jetbrains.kotlinx.lincheck.annotations.Operation import org.jetbrains.kotlinx.lincheck.strategy.managed.* import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.* +import org.jetbrains.kotlinx.lincheck.test.* import org.jetbrains.kotlinx.lincheck.verifier.* import org.junit.* import java.lang.StringBuilder @@ -87,6 +88,7 @@ class MethodReportingTest : VerifierState() { check("ignored" !in log) { "ignored methods should not be present in log" } check("nonPrimitiveParameter(IllegalStateException@1)" in log) check("nonPrimitiveResult(): IllegalStateException@2" in log) + checkTraceHasNoLincheckEvents(log) } } @@ -126,5 +128,6 @@ class CaughtExceptionMethodReportingTest : VerifierState() { val log = StringBuilder().appendFailure(failure).toString() check("useless" !in log) { "Due to bad call stack these accesses appear to be in the same method as thread switches" } check("badMethod(): threw NotImplementedError" in log) { "thrown exception is not shown properly" } + checkTraceHasNoLincheckEvents(log) } } \ No newline at end of file diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/representation/ObstructionFreedomRepresentationTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/representation/ObstructionFreedomRepresentationTest.kt index 03121b20a..fc0cf73c1 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/representation/ObstructionFreedomRepresentationTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/representation/ObstructionFreedomRepresentationTest.kt @@ -26,6 +26,7 @@ import org.jetbrains.kotlinx.lincheck.* import org.jetbrains.kotlinx.lincheck.annotations.Operation import org.jetbrains.kotlinx.lincheck.strategy.managed.* import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.* +import org.jetbrains.kotlinx.lincheck.test.* import org.jetbrains.kotlinx.lincheck.verifier.* import org.junit.* import java.lang.StringBuilder @@ -69,6 +70,7 @@ class ObstructionFreedomActiveLockRepresentationTest : VerifierState() { check(failure != null) { "the test should fail" } val log = StringBuilder().appendFailure(failure).toString() check("incrementAndGet" in log) { "The cause of the error should be reported" } + checkTraceHasNoLincheckEvents(log) } } @@ -96,5 +98,6 @@ class ObstructionFreedomSynchronizedRepresentationTest : VerifierState() { check(failure != null) { "the test should fail" } val log = StringBuilder().appendFailure(failure).toString() check(log.split("MONITORENTER").size - 1 == 2) { "MONITORENTER should be reported twice" } + checkTraceHasNoLincheckEvents(log) } } diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/representation/StateRepresentationTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/representation/StateRepresentationTest.kt index 2a0072a27..99c76c2a9 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/representation/StateRepresentationTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/representation/StateRepresentationTest.kt @@ -28,6 +28,7 @@ import org.jetbrains.kotlinx.lincheck.appendFailure import org.jetbrains.kotlinx.lincheck.checkImpl import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.ModelCheckingOptions import org.jetbrains.kotlinx.lincheck.strategy.stress.* +import org.jetbrains.kotlinx.lincheck.test.* import org.jetbrains.kotlinx.lincheck.verifier.VerifierState import org.junit.Test import java.lang.IllegalStateException @@ -64,6 +65,7 @@ open class ModelCheckingStateReportingTest { check("STATE: 1" in log) check("STATE: 4" in log) check(log.split("incrementAndGet(): 1").size - 1 == 1) { "A method call is logged twice in the trace" } + checkTraceHasNoLincheckEvents(log) } } @@ -97,6 +99,7 @@ class StressStateReportingTest : VerifierState() { val log = StringBuilder().appendFailure(failure).toString() check("STATE: 0" in log) check("STATE: 2" in log || "STATE: 3" in log || "STATE: 4" in log) + checkTraceHasNoLincheckEvents(log) } } diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/representation/SuspendInterleavingReportingTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/representation/SuspendTraceReportingTest.kt similarity index 72% rename from src/jvm/test/org/jetbrains/kotlinx/lincheck/test/representation/SuspendInterleavingReportingTest.kt rename to src/jvm/test/org/jetbrains/kotlinx/lincheck/test/representation/SuspendTraceReportingTest.kt index 73572bf52..933484bdb 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/representation/SuspendInterleavingReportingTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/representation/SuspendTraceReportingTest.kt @@ -26,17 +26,18 @@ import kotlinx.coroutines.sync.* import org.jetbrains.kotlinx.lincheck.* import org.jetbrains.kotlinx.lincheck.annotations.Operation import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.* +import org.jetbrains.kotlinx.lincheck.test.* import org.jetbrains.kotlinx.lincheck.verifier.* import org.junit.* -class SuspendInterleavingReportingTest : VerifierState() { +class SuspendTraceReportingTest : VerifierState() { private val lock = Mutex() private var canEnterForbiddenBlock: Boolean = false private var barStarted: Boolean = false private var counter: Int = 0 - @Operation(allowExtraSuspension = true) + @Operation(allowExtraSuspension = true, cancellableOnSuspension = false) suspend fun foo() { if (barStarted) canEnterForbiddenBlock = true lock.withLock { @@ -45,9 +46,12 @@ class SuspendInterleavingReportingTest : VerifierState() { canEnterForbiddenBlock = false } - @Operation(cancellableOnSuspension = false) + @Operation(allowExtraSuspension = true, cancellableOnSuspension = false) suspend fun bar(): Int { barStarted = true + lock.withLock { + counter++ + } if (canEnterForbiddenBlock) return -1 return 0 } @@ -69,39 +73,8 @@ class SuspendInterleavingReportingTest : VerifierState() { "suspended function should be mentioned exactly twice (once in parallel and once in parallel execution)" } check("barStarted.READ: true" in log) { "this code location after suspension should be reported" } + checkTraceHasNoLincheckEvents(log) } private fun String.numberOfOccurrences(text: String): Int = split(text).size - 1 -} - -class CancelledSuspendInterleavingReportingTest : VerifierState() { - @Volatile - var correct = true - - @InternalCoroutinesApi - @Operation(cancellableOnSuspension = true) - suspend fun cancelledOp() { - suspendCancellableCoroutine { cont -> - cont.invokeOnCancellation { - correct = false - } - } - } - - @Operation - fun isAbsurd(): Boolean = correct && !correct - - override fun extractState(): Any = correct - - @Test - fun test() { - val failure = ModelCheckingOptions() - .actorsPerThread(1) - .actorsBefore(0) - .actorsAfter(0) - .checkImpl(this::class.java) - checkNotNull(failure) { "the test should fail" } - val log = failure.toString() - check("CONTINUATION CANCELLED" in log) - } } \ No newline at end of file diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/representation/SwitchAsFirstMethodEventTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/representation/SwitchAsFirstMethodEventTest.kt index 03051f3d4..3e10fb8bd 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/representation/SwitchAsFirstMethodEventTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/representation/SwitchAsFirstMethodEventTest.kt @@ -24,6 +24,7 @@ import kotlinx.atomicfu.* import org.jetbrains.kotlinx.lincheck.* import org.jetbrains.kotlinx.lincheck.annotations.* import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.* +import org.jetbrains.kotlinx.lincheck.test.* import org.junit.* import java.lang.StringBuilder @@ -75,5 +76,6 @@ class SwitchAsFirstMethodEventTest { check("incrementAndGet" !in log) { "When the switch is lifted out of methods, there is no point at reporting this method" } + checkTraceHasNoLincheckEvents(log) } } \ No newline at end of file diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/representation/TraceReportingTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/representation/TraceReportingTest.kt index 9b7431e07..8067e130d 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/representation/TraceReportingTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/representation/TraceReportingTest.kt @@ -24,6 +24,7 @@ package org.jetbrains.kotlinx.lincheck.test.representation import org.jetbrains.kotlinx.lincheck.* import org.jetbrains.kotlinx.lincheck.annotations.Operation import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.* +import org.jetbrains.kotlinx.lincheck.test.* import org.junit.* /** @@ -83,13 +84,14 @@ class TraceReportingTest { checkNotNull(failure) { "test should fail" } val log = failure.toString() check("foo" in log) - check("canEnterForbiddenSection.WRITE(true) at TraceReportingTest.resetFlag(TraceReportingTest.kt:64)" in log) - check("canEnterForbiddenSection.WRITE(false) at TraceReportingTest.resetFlag(TraceReportingTest.kt:65)" in log) + check("canEnterForbiddenSection.WRITE(true) at TraceReportingTest.resetFlag(TraceReportingTest.kt:65)" in log) + check("canEnterForbiddenSection.WRITE(false) at TraceReportingTest.resetFlag(TraceReportingTest.kt:66)" in log) check("a.READ: 0 at TraceReportingTest.bar" in log) check("a.WRITE(1) at TraceReportingTest.bar" in log) check("a.READ: 1 at TraceReportingTest.bar" in log) check("a.WRITE(2) at TraceReportingTest.bar" in log) check("MONITORENTER at TraceReportingTest.resetFlag" in log) check("MONITOREXIT at TraceReportingTest.resetFlag" in log) + checkTraceHasNoLincheckEvents(log) } } diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/representation/VerboseTraceTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/representation/VerboseTraceTest.kt index 44d95e5f6..80819a2b1 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/representation/VerboseTraceTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/representation/VerboseTraceTest.kt @@ -23,6 +23,7 @@ package org.jetbrains.kotlinx.lincheck.test.representation import org.jetbrains.kotlinx.lincheck.* import org.jetbrains.kotlinx.lincheck.annotations.* import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.* +import org.jetbrains.kotlinx.lincheck.test.* import org.junit.* /** @@ -70,5 +71,6 @@ class VerboseTraceTest { check(" levelOneCounter" in log) check(" levelTwoEvent" in log) { "An intermediate method call was not logged or has an incorrect indentation" } check(" levelTwoCounter" in log) + checkTraceHasNoLincheckEvents(log) } } \ No newline at end of file