Skip to content

Commit

Permalink
Make ExecutionScenario immutable
Browse files Browse the repository at this point in the history
  • Loading branch information
zuevmaxim committed Oct 5, 2021
1 parent 1a485d5 commit 8c5a49c
Show file tree
Hide file tree
Showing 2 changed files with 46 additions and 50 deletions.
22 changes: 1 addition & 21 deletions src/jvm/main/org/jetbrains/kotlinx/lincheck/LinChecker.kt
Original file line number Diff line number Diff line change
Expand Up @@ -131,14 +131,7 @@ class LinChecker (private val testClass: Class<*>, options: Options<*, *>?) {
}

private fun ExecutionScenario.tryMinimize(threadId: Int, position: Int, testCfg: CTestConfiguration): LincheckFailure? {
var newScenario = this.copy()
val actors = newScenario[threadId] as MutableList<Actor>
actors.removeAt(position)
if (actors.isEmpty() && threadId != 0 && threadId != newScenario.threads + 1) {
// Also remove the empty thread
newScenario.parallelExecution.removeAt(threadId - 1)
newScenario = newScenario.setThreadIds()
}
val newScenario = this.copyWithRemovedActor(threadId, position)
return if (newScenario.isValid) {
newScenario.runTryMinimize(testCfg)
} else null
Expand Down Expand Up @@ -175,13 +168,6 @@ class LinChecker (private val testClass: Class<*>, options: Options<*, *>?) {
return result
}

private fun List<Actor>.copyWithThreadId(threadId: Int) = map { actor -> actor.copyWithThreadId(threadId) }
private fun ExecutionScenario.setThreadIds() = ExecutionScenario(
initExecution,
parallelExecution.mapIndexed { index, actors -> actors.copyWithThreadId(index + 1) },
postExecution.copyWithThreadId(parallelExecution.size + 1)
)

private fun ExecutionScenario.run(testCfg: CTestConfiguration, verifier: Verifier): LincheckFailure? =
testCfg.createStrategy(
testClass = testClass,
Expand All @@ -191,12 +177,6 @@ class LinChecker (private val testClass: Class<*>, options: Options<*, *>?) {
verifier = verifier
).run()

private fun ExecutionScenario.copy() = ExecutionScenario(
ArrayList(initExecution),
parallelExecution.map { ArrayList(it) },
ArrayList(postExecution)
)

private val ExecutionScenario.isValid: Boolean
get() = !isParallelPartEmpty &&
(!hasSuspendableActors() || (!hasSuspendableActorsInInitPart && !hasPostPartAndSuspendableActors))
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -19,22 +19,17 @@
* <http://www.gnu.org/licenses/lgpl-3.0.html>.
* #L%
*/
package org.jetbrains.kotlinx.lincheck.execution;
package org.jetbrains.kotlinx.lincheck.execution

import org.jetbrains.kotlinx.lincheck.Actor;
import org.jetbrains.kotlinx.lincheck.strategy.Strategy;

import java.util.*;
import java.util.stream.*;

import static org.jetbrains.kotlinx.lincheck.ReporterKt.appendExecutionScenario;
import org.jetbrains.kotlinx.lincheck.Actor
import org.jetbrains.kotlinx.lincheck.appendExecutionScenario

/**
* This class represents an execution scenario, which
* is generated by an {@link ExecutionGenerator} and then \
* used by a {@link Strategy} which produces an {@link ExecutionResult}.
*/
public class ExecutionScenario {
data class ExecutionScenario(
/**
* The initial sequential part of the execution.
* It helps to produce different initial states
Expand All @@ -43,45 +38,66 @@ public class ExecutionScenario {
* The initial execution part should contain only non-suspendable actors;
* otherwise, the single initial execution thread will suspend with no chance to be resumed.
*/
public final List<Actor> initExecution;
val initExecution: List<Actor>,
/**
* The parallel part of the execution, which is used
* to find an interleaving with incorrect behaviour.
*/
public final List<List<Actor>> parallelExecution;
val parallelExecution: List<List<Actor>>,
/**
* The last sequential part is used to test that
* the data structure is in some correct state.
*
* If this execution scenario contains suspendable actors, the post part should be empty;
* if not, an actor could resume a previously suspended one from the parallel execution part.
*/
public final List<Actor> postExecution;

public ExecutionScenario(List<Actor> initExecution, List<List<Actor>> parallelExecution, List<Actor> postExecution) {
this.initExecution = initExecution;
this.parallelExecution = parallelExecution;
this.postExecution = postExecution;
}
val postExecution: List<Actor>
) {

/**
* Returns the number of threads used in the parallel part of this execution.
*/
public int getThreads() {
return parallelExecution.size();
}
val threads get() = parallelExecution.size

/**
* Returns `true` if there is at least one suspendable actor in the generated scenario
*/
public boolean hasSuspendableActors() {
return Stream.concat(parallelExecution.stream().flatMap(Collection::stream), postExecution.stream()).anyMatch(Actor::isSuspendable);
}
fun hasSuspendableActors() = parallelExecution.asSequence().flatten().plus(postExecution).any(Actor::isSuspendable)


override fun toString() = StringBuilder()
.also { it.appendExecutionScenario(this) }
.toString()

@Override
public String toString() {
StringBuilder sb = new StringBuilder();
appendExecutionScenario(sb, this);
return sb.toString();
/**
* Copy the [ExecutionScenario] with the [actorId] actor of the [threadId] thread removed.
*/
fun copyWithRemovedActor(threadId: Int, actorId: Int): ExecutionScenario = when (threadId) {
0 -> copy(initExecution = initExecution.removeAt(actorId))
in 1..threads -> {
val thread = parallelExecution[threadId - 1]
if (thread.size > 1) {
copy(parallelExecution = parallelExecution.mapIndexed { id, actors -> if (id == threadId - 1) actors.removeAt(actorId) else actors })
} else {
copy(
parallelExecution = parallelExecution
.removeAt(threadId - 1)
.mapIndexed { id, actors -> actors.copyWithThreadId(id + 1) },
postExecution = postExecution.copyWithThreadId(threads)
)
}
}
threads + 1 -> copy(postExecution = postExecution.removeAt(actorId))
else -> error("Thread id is out of bounds 0..${threads}: $threadId")
}
}

/**
* Create a copy of the list without the [index] element.
*/
private fun <T> List<T>.removeAt(index: Int) = filterIndexed { i, _ -> i != index }

/**
* Copy actors list with [threadId] set as thread id.
*/
private fun List<Actor>.copyWithThreadId(threadId: Int) = map { actor -> actor.copyWithThreadId(threadId) }

0 comments on commit 8c5a49c

Please sign in to comment.