Skip to content

Commit

Permalink
fixes after rebase
Browse files Browse the repository at this point in the history
Signed-off-by: Evgenii Moiseenko <[email protected]>
  • Loading branch information
eupp committed Aug 17, 2023
1 parent 67ba310 commit 976d438
Show file tree
Hide file tree
Showing 7 changed files with 79 additions and 43 deletions.
15 changes: 10 additions & 5 deletions src/jvm/main/org/jetbrains/kotlinx/lincheck/Planner.kt
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,7 @@ package org.jetbrains.kotlinx.lincheck

import org.jetbrains.kotlinx.lincheck.execution.ExecutionGenerator
import org.jetbrains.kotlinx.lincheck.execution.ExecutionScenario
import org.jetbrains.kotlinx.lincheck.runner.SpinCycleFoundAndReplayRequired
import org.jetbrains.kotlinx.lincheck.strategy.LincheckFailure
import org.jetbrains.kotlinx.lincheck.strategy.Strategy
import org.jetbrains.kotlinx.lincheck.verifier.Verifier
Expand Down Expand Up @@ -52,16 +53,20 @@ fun Planner.runIterations(
val (strategy, verifier) = factory(scenario)
strategy.use {
var invocation = 0
var spinning = false
while (invocationsPlanner.shouldDoNextInvocation(invocation)) {
if (!strategy.nextInvocation()) {
if (!spinning && !strategy.nextInvocation()) {
return@trackIteration null
}
spinning = false
strategy.initializeInvocation()
tracker.trackInvocation(invocation) {
strategy.runInvocation(verifier)
}?.let {
return@trackIteration it
val failure = tracker.trackInvocation(invocation) {
val result = strategy.runInvocation()
spinning = (result is SpinCycleFoundAndReplayRequired)
strategy.verify(result, verifier)
}
if (failure != null)
return failure
invocation++
}
}
Expand Down
19 changes: 15 additions & 4 deletions src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/Strategy.kt
Original file line number Diff line number Diff line change
Expand Up @@ -35,23 +35,33 @@ abstract class Strategy protected constructor(

fun run(verifier: Verifier, planner: InvocationsPlanner, tracker: RunTracker? = null): LincheckFailure? {
var invocation = 0
var spinning = false
while (planner.shouldDoNextInvocation(invocation)) {
if (!nextInvocation()) {
if (!spinning && !nextInvocation()) {
return null
}
spinning = false
initializeInvocation()
tracker.trackInvocation(invocation) { runInvocation(verifier) }
?.let { return it }
val failure = tracker.trackInvocation(invocation) {
val result = runInvocation()
spinning = (result is SpinCycleFoundAndReplayRequired)
verify(result, verifier)
}
if (failure != null)
return failure
invocation++
}
return null
}

fun runInvocation(verifier: Verifier): LincheckFailure? = when (val result = runInvocation()) {
fun verify(result: InvocationResult, verifier: Verifier): LincheckFailure? = when (result) {
is CompletedInvocationResult ->
if (!verifier.verifyResults(scenario, result.results)) {
IncorrectResultsFailure(scenario, result.results, result.tryCollectTrace())
} else null

is SpinCycleFoundAndReplayRequired -> null

else -> result.toLincheckFailure(scenario, result.tryCollectTrace())
}

Expand Down Expand Up @@ -88,3 +98,4 @@ abstract class Strategy protected constructor(
*/
open fun onActorStart(iThread: Int) {}
}

Original file line number Diff line number Diff line change
Expand Up @@ -73,6 +73,13 @@ internal class ModelCheckingStrategy(
currentInterleaving.initialize()
}

override fun runInvocation(): InvocationResult {
return super.runInvocation().also {
if (it is SpinCycleFoundAndReplayRequired)
currentInterleaving.rollbackAfterSpinCycleFound()
}
}

override fun InvocationResult.tryCollectTrace(): Trace? = collectTrace(this)

override fun onNewSwitch(iThread: Int, mustSwitch: Boolean) {
Expand Down
Original file line number Diff line number Diff line change
@@ -1,4 +1,3 @@
@file:Suppress("unused")
/*
* Lincheck
*
Expand All @@ -9,6 +8,7 @@
* with this file, You can obtain one at http://mozilla.org/MPL/2.0/.
*/

@file:Suppress("unused", "DEPRECATION_ERROR")

package org.jetbrains.kotlinx.lincheck_test

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -27,15 +27,18 @@ class MinimizationTest {
*/
@Test
fun testWithoutMinimization() {
val options = StressOptions()
.threads(4)
.actorsPerThread(4)
.actorsBefore(4)
.actorsAfter(4)
.invocationsPerIteration(1_000)
.minimizeFailedScenario(false)
val options = LincheckOptions {
this as LincheckOptionsImpl
mode = LincheckMode.Stress
minThreads = 4
maxThreads = 4
minOperationsInThread = 4
maxOperationsInThread = 4
minimizeFailedScenario = false
tryReproduceTrace = false
}
try {
LinChecker.check(MinimizationTest::class.java, options)
options.check(MinimizationTest::class.java)
fail("Should fail with LincheckAssertionError")
} catch (error: LincheckAssertionError) {
val failedScenario = error.failure.scenario
Expand All @@ -53,14 +56,17 @@ class MinimizationTest {
*/
@Test
fun testWithMinimization() {
val options = StressOptions()
.threads(4)
.actorsPerThread(4)
.actorsBefore(4)
.actorsAfter(4)
.invocationsPerIteration(1_000)
val options = LincheckOptions {
this as LincheckOptionsImpl
mode = LincheckMode.Stress
minThreads = 4
maxThreads = 4
minOperationsInThread = 4
maxOperationsInThread = 4
tryReproduceTrace = false
}
try {
LinChecker.check(MinimizationTest::class.java, options)
options.check(MinimizationTest::class.java)
fail("Should fail with LincheckAssertionError")
} catch (error: LincheckAssertionError) {
val failedScenario = error.failure.scenario
Expand All @@ -86,14 +92,17 @@ class MinimizationWithExceptionTest {
*/
@Test
fun testWithExpectedException() {
val options = StressOptions()
.threads(4)
.actorsPerThread(4)
.actorsBefore(4)
.actorsAfter(4)
.invocationsPerIteration(1_000)
val options = LincheckOptions {
this as LincheckOptionsImpl
mode = LincheckMode.Stress
minThreads = 4
maxThreads = 4
minOperationsInThread = 4
maxOperationsInThread = 4
tryReproduceTrace = false
}
try {
LinChecker.check(IncorrectImplementationWithException::class.java, options)
options.check(IncorrectImplementationWithException::class.java)
fail("Should fail with LincheckAssertionError")
} catch (error: LincheckAssertionError) {
val failedScenario = error.failure.scenario
Expand All @@ -117,15 +126,18 @@ class MinimizationWithExceptionTest {
*/
@Test
fun testWithUnexpectedException() {
val options = StressOptions()
.threads(4)
.actorsPerThread(4)
.actorsBefore(4)
.actorsAfter(4)
.invocationsPerIteration(1_000)
.sequentialSpecification(SequentialImplementation::class.java)
val options = LincheckOptions {
this as LincheckOptionsImpl
mode = LincheckMode.Stress
minThreads = 4
maxThreads = 4
minOperationsInThread = 4
maxOperationsInThread = 4
tryReproduceTrace = false
sequentialImplementation = SequentialImplementation::class.java
}
try {
LinChecker.check(CorrectImplementationWithException::class.java, options)
options.check(CorrectImplementationWithException::class.java)
fail("Should fail with LincheckAssertionError")
} catch (error: LincheckAssertionError) {
val failedScenario = error.failure.scenario
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@
* with this file, You can obtain one at http://mozilla.org/MPL/2.0/.
*/

@file:Suppress("unused")
@file:Suppress("unused", "DEPRECATION_ERROR")

package org.jetbrains.kotlinx.lincheck_test.representation

Expand Down
Original file line number Diff line number Diff line change
@@ -1,4 +1,3 @@
@file:Suppress("UNUSED")
/*
* Lincheck
*
Expand All @@ -9,11 +8,13 @@
* with this file, You can obtain one at http://mozilla.org/MPL/2.0/.
*/

@file:Suppress("UNUSED", "DEPRECATION_ERROR")

package org.jetbrains.kotlinx.lincheck_test.representation

import org.jetbrains.kotlinx.lincheck.*
import org.jetbrains.kotlinx.lincheck.annotations.Operation
import org.jetbrains.kotlinx.lincheck.execution.*
import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.ModelCheckingOptions
import org.jetbrains.kotlinx.lincheck_test.guide.MSQueueBlocking
import org.jetbrains.kotlinx.lincheck_test.util.checkLincheckOutput
import org.junit.Test
Expand Down

0 comments on commit 976d438

Please sign in to comment.