Linearizability support additionally to sequential consistency has be…

…en implemented

README.md

@@ -162,7 +162,7 @@ public class MyConcurrentTest {
 
 
 # Execution strategies
-The section above describes how to specify the operations and the initial state, whereas this section is about executing the test. Using the provided operations **lincheck** generates several random scenarios and then executes them using the specified execution strategy. At this moment stress strategy is implemented only, but some managed strategies will be added soon as well.
+The section above describes how to specify the operations and the initial state, whereas this section is about executing the test. Using the provided operations **lincheck** generates several random scenarios and then executes them using the specified execution strategy. At this moment, only stress strategy is implemented, but a model checking one will be added soon.
 
 ## Stress strategy
 The first implemented in **lincheck** execution strategy is stress testing strategy. This strategy uses the same idea as `JCStress` tool - it executes the generated scenario in parallel a lot of times in hope to hit on an interleaving which produces incorrect results. This strategy is pretty useful for finding bugs related to low-level effects (like a forgotten volatile modifier), but, unfortunately, does not guarantee any coverage. It is also recommended to use not only Intel processors with this strategy because its internal memory model is quite strong and cannot produce a lot of behaviors which are possible with ARM, for example. 
@@ -367,14 +367,14 @@ public class MyConcurrentTest {
 ```
 
 
-# Sample
-Here is a test for a not thread-safe `HashMap` with its result. It uses the default configuration and tests `put` and `get` operations only:
+# Example
+Here is a test for a not thread-safe `HashMap` with the failed scenario and the corresponding result. It uses the default configuration and tests `put` and `get` operations only:
 
 **Test class**
 
 ```java
+@StressCTest(minimizeFailedScenario = false)
 @Param(name = "key", gen = IntGen.class, conf = "1:5")
-@StressCTest
 public class HashMapLinearizabilityTest extends VerifierState {
     private HashMap<Integer, Integer> map = new HashMap<>();
 
@@ -404,15 +404,19 @@ public class HashMapLinearizabilityTest extends VerifierState {
 **Test output**
 
 ```
-= Invalid execution results: =
+= Invalid execution results =
 Init part:
-[put(1, 2): null, put(4, 6): null, get(5): null, put(3, -6): null, put(1, -8): 2]
+[put(1,2): null, put(4,6): null, get(5): null, put(3,-6): null, put(1,-8): 2]
 Parallel part:
-| get(4):     6    | put(2, 1):  null |
-| get(2):     null | put(5, 4):  null |
-| put(5, -8): null | get(3):     -6   |
-| get(3):     -6   | get(4):     6    |
-| put(3, 5):  -6   | put(1, -4): -8   |
+| get(4):    6          | put(2,1):  null       |
+| get(2):    1    [1,0] | put(5,4):  null [1,1] |
+| put(5,-8): null [2,1] | get(3):    5    [5,2] |
+| get(3):    -6   [3,1] | get(4):    6    [5,3] |
+| put(3,5):  -6   [4,1] | put(1,-4): -8   [5,4] |
 Post part:
-[put(5, -8): 4, put(5, -2): -8, get(1): -4, put(2, -8): 1, get(1): -4]
+[put(5,-8): 4, put(5,-2): -8, get(1): -4, put(2,-8): 1, get(1): -4]
+---
+values in "[..]" brackets indicate the number of completed operations 
+in each of the parallel threads seen at the beginning of the current operation
+---
 ```

lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/LinChecker.java

@@ -162,7 +162,7 @@ private ExecutionScenario copyScenario(ExecutionScenario scenario) {
 
     private void runScenario(ExecutionScenario scenario, CTestConfiguration testCfg) throws AssertionError, Exception {
         validateScenario(testCfg, scenario);
-        Verifier verifier = createVerifier(testCfg.verifierClass, scenario, testCfg.sequentialSpecification);
+        Verifier verifier = createVerifier(testCfg.verifierClass, testCfg.sequentialSpecification);
         if (testCfg.requireStateEquivalenceImplCheck) verifier.checkStateEquivalenceImplementation();
         Strategy strategy = Strategy.createStrategy(testCfg, testClass, scenario, verifier, reporter);
         strategy.run();
@@ -177,9 +177,8 @@ private void validateScenario(CTestConfiguration testCfg, ExecutionScenario scen
         }
     }
 
-    private Verifier createVerifier(Class<? extends Verifier> verifierClass, ExecutionScenario scenario,
-                                    Class<?> sequentialSpecification) throws Exception {
-        return verifierClass.getConstructor(ExecutionScenario.class, Class.class).newInstance(scenario, sequentialSpecification);
+    private Verifier createVerifier(Class<? extends Verifier> verifierClass, Class<?> sequentialSpecification) throws Exception {
+        return verifierClass.getConstructor(Class.class).newInstance(sequentialSpecification);
     }
 
     private ExecutionGenerator createExecutionGenerator(Class<? extends ExecutionGenerator> generatorClass,

lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/Reporter.kt

@@ -22,8 +22,7 @@
 
 package org.jetbrains.kotlinx.lincheck
 
-import org.jetbrains.kotlinx.lincheck.execution.ExecutionResult
-import org.jetbrains.kotlinx.lincheck.execution.ExecutionScenario
+import org.jetbrains.kotlinx.lincheck.execution.*
 import java.io.PrintStream
 
 class Reporter @JvmOverloads constructor(val logLevel: LoggingLevel, val out: PrintStream = System.out) {
@@ -71,34 +70,49 @@ private fun <T> printInColumns(groupedObjects: List<List<T>>): String {
             .joinToString(separator = "\n")
 }
 
-private class ActorWithResult(val actorRepresentation: String, val spaces: Int, val resultRepresentation: String) {
-    override fun toString(): String = actorRepresentation + ":" + " ".repeat(spaces) + resultRepresentation
+private class ActorWithResult(val actorRepresentation: String, val spacesAfterActor: Int,
+                              val resultRepresentation: String, val spacesAfterResult: Int,
+                              val clockRepresentation: String) {
+    override fun toString(): String =
+        actorRepresentation + ":" + " ".repeat(spacesAfterActor) + resultRepresentation +
+                                    " ".repeat(spacesAfterResult) + clockRepresentation
 }
 
-private fun uniteActorsAndResults(actors: List<Actor>, results: List<Result>): List<ActorWithResult> {
+private fun uniteActorsAndResultsLinear(actors: List<Actor>, results: List<Result>): List<ActorWithResult> {
     require(actors.size == results.size) {
         "Different numbers of actors and matching results found (${actors.size} != ${results.size})"
     }
-    val actorRepresentations = actors.map { it.toString() }
-    return actors.indices.map { ActorWithResult("${actors[it]}", 1, "${results[it]}") }
+    return actors.indices.map {
+        ActorWithResult("${actors[it]}", 1, "${results[it]}", 0, "")
+    }
 }
 
-private fun uniteParallelActorsAndResults(actors: List<List<Actor>>, results: List<List<Result>>): List<List<ActorWithResult>> {
+private fun uniteParallelActorsAndResults(actors: List<List<Actor>>, results: List<List<ResultWithClock>>): List<List<ActorWithResult>> {
     require(actors.size == results.size) {
         "Different numbers of threads and matching results found (${actors.size} != ${results.size})"
     }
     return actors.mapIndexed { id, threadActors -> uniteActorsAndResultsAligned(threadActors, results[id]) }
 }
 
-private fun uniteActorsAndResultsAligned(actors: List<Actor>, results: List<Result>): List<ActorWithResult> {
+private fun uniteActorsAndResultsAligned(actors: List<Actor>, results: List<ResultWithClock>): List<ActorWithResult> {
     require(actors.size == results.size) {
         "Different numbers of actors and matching results found (${actors.size} != ${results.size})"
     }
     val actorRepresentations = actors.map { it.toString() }
+    val resultRepresentations = results.map { it.result.toString() }
     val maxActorLength = actorRepresentations.map { it.length }.max()!!
-    return actorRepresentations.mapIndexed { id, actorRepr ->
-        val spaces = 1 + maxActorLength - actorRepr.length
-        ActorWithResult(actorRepr, spaces, "${results[id]}")
+    val maxResultLength = resultRepresentations.map { it.length }.max()!!
+    return actors.indices.map { i ->
+        val actorRepr = actorRepresentations[i]
+        val resultRepr = resultRepresentations[i]
+        val clock = results[i].clockOnStart
+        val spacesAfterActor = maxActorLength - actorRepr.length + 1
+        val spacesAfterResultToAlign = maxResultLength - resultRepr.length
+        if (clock.empty) {
+            ActorWithResult(actorRepr, spacesAfterActor, resultRepr, spacesAfterResultToAlign, "")
+        } else {
+            ActorWithResult(actorRepr, spacesAfterActor, resultRepr, spacesAfterResultToAlign + 1, clock.toString())
+        }
     }
 }
 
@@ -117,17 +131,20 @@ private fun StringBuilder.appendExecutionScenario(scenario: ExecutionScenario) {
 }
 
 fun StringBuilder.appendIncorrectResults(scenario: ExecutionScenario, results: ExecutionResult) {
-    appendln("= Invalid execution results: =")
+    appendln("= Invalid execution results =")
     if (scenario.initExecution.isNotEmpty()) {
         appendln("Init part:")
-        appendln(uniteActorsAndResults(scenario.initExecution, results.initResults))
+        appendln(uniteActorsAndResultsLinear(scenario.initExecution, results.initResults))
     }
     appendln("Parallel part:")
-    val parallelExecutionData = uniteParallelActorsAndResults(scenario.parallelExecution, results.parallelResults)
+    val parallelExecutionData = uniteParallelActorsAndResults(scenario.parallelExecution, results.parallelResultsWithClock)
     append(printInColumns(parallelExecutionData))
     if (scenario.postExecution.isNotEmpty()) {
         appendln()
         appendln("Post part:")
-        append(uniteActorsAndResults(scenario.postExecution, results.postResults))
+        append(uniteActorsAndResultsLinear(scenario.postExecution, results.postResults))
     }
+    if (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---")
 }

lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/Utils.kt

@@ -165,14 +165,8 @@ internal operator fun ExecutionScenario.get(threadId: Int): List<Actor> = when (
  */
 internal operator fun ExecutionResult.get(threadId: Int): List<Result> = when (threadId) {
     0 -> initResults
-    parallelResults.size + 1 -> postResults
-    else -> parallelResults[threadId - 1]
-}
-
-internal operator fun ExecutionResult.set(threadId: Int, actorId: Int, value: Result) = when (threadId) {
-    0 -> initResults[actorId] = value
-    parallelResults.size + 1 -> postResults[actorId] = value
-    else -> parallelResults[threadId - 1][actorId] = value
+    parallelResultsWithClock.size + 1 -> postResults
+    else -> parallelResultsWithClock[threadId - 1].map { it.result }
 }
 
 fun <T> CancellableContinuation<T>.cancelByLincheck() = cancel(cancellationByLincheckException)

lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/execution/ExecutionResult.kt

@@ -0,0 +1,59 @@
+/*-
+ * #%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
+ * <http://www.gnu.org/licenses/lgpl-3.0.html>.
+ * #L%
+ */
+package org.jetbrains.kotlinx.lincheck.execution
+
+import org.jetbrains.kotlinx.lincheck.*
+
+/**
+ * This class represents a result corresponding to
+ * the specified [scenario][ExecutionScenario] execution.
+ *
+ * All the result parts should have the same dimensions as the scenario.
+ */
+data class ExecutionResult(
+    /**
+     * Results of the initial sequential part of the execution.
+     * @see ExecutionScenario.initExecution
+     */
+    val initResults: List<Result>,
+    /**
+     * Results of the parallel part of the execution with the clock values at the beginning of each one.
+     * @see ExecutionScenario.parallelExecution
+     */
+    val parallelResultsWithClock: List<List<ResultWithClock>>,
+    /**
+     * Results of the last sequential part of the execution.
+     * @see ExecutionScenario.postExecution
+     */
+    val postResults: List<Result>
+)
+
+val ExecutionResult.withEmptyClocks: ExecutionResult get() = ExecutionResult(
+    this.initResults,
+    this.parallelResultsWithClock.map { it.withEmptyClock() },
+    this.postResults
+)
+
+val ExecutionResult.parallelResults: List<List<Result>> get() = parallelResultsWithClock.map { it.map { r -> r.result } }
+
+// for tests
+fun ExecutionResult.equalsIgnoringClocks(other: ExecutionResult) = this.withEmptyClocks == other.withEmptyClocks

lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/execution/HBClock.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
+ * <http://www.gnu.org/licenses/lgpl-3.0.html>.
+ * #L%
+ */
+package org.jetbrains.kotlinx.lincheck.execution
+
+import org.jetbrains.kotlinx.lincheck.Result
+
+data class HBClock(val clock: IntArray) {
+    val threads: Int get() = clock.size
+    val empty: Boolean get() = clock.all { it == 0 }
+    operator fun get(i: Int) = clock[i]
+
+    override fun toString()= clock.joinToString(prefix = "[", separator = ",", postfix = "]")
+
+    override fun equals(other: Any?): Boolean {
+        if (this === other) return true
+        if (javaClass != other?.javaClass) return false
+        other as HBClock
+        return clock.contentEquals(other.clock)
+    }
+
+    override fun hashCode() = clock.contentHashCode()
+}
+
+fun emptyClock(size: Int) = HBClock(emptyClockArray(size))
+fun emptyClockArray(size: Int) = IntArray(size) { 0 }
+
+data class ResultWithClock(val result: Result, val clockOnStart: HBClock)
+
+fun Result.withEmptyClock(threads: Int) = ResultWithClock(this, emptyClock(threads))
+fun List<Result>.withEmptyClock(threads: Int): List<ResultWithClock> = map { it.withEmptyClock(threads) }
+fun List<ResultWithClock>.withEmptyClock() = map { it.result.withEmptyClock(it.clockOnStart.threads) }