Add validation mechanism

README.md

@@ -140,6 +140,31 @@ Thus, **lincheck** can test that the testing data structure is correct even with
 This sequential specification class should have the same methods as the testing data structure.
 The specification class can be defined via `sequentialSpecification` parameter in both `Options` instances and the corresponding annotations.
 
+## Validation functions
+It is possible in **lincheck** to add the validation of the testing data structure invariants,
+which is implemented via functions that can be executed multiple times during execution
+when there is no running operation in an intermediate state (e.g., in the stress mode
+they are invoked after each of the init and post part operations and after the whole parallel part).
+Thus, these functions should not modify the data structure.
+
+Validation functions should be marked with `@Validate` annotation, should not have arguments,
+and should not return anything (in other words, the returning type is `void`).
+In case the testing data structure is in an invalid state, they should throw exceptions
+(`AssertionError` or `IllegalStateException` are the preferable ones).
+
+```kotlin
+class MyLockFreeListTest {
+  private val list = MyLockFreeList<Int>()  
+
+  @Validate 
+  fun checkNoRemovedNodesInTheList() = check(!list.hasRemovedNodes()) {
+    "The list contains logically removed nodes while all the operations are completed: $list"
+  }
+
+  ...
+}
+```
+
 ## Run test
 In order to run a test, `LinChecker.check(...)` method should be executed with the provided test class as a parameter. Then **lincheck** looks at execution strategies to be used, which can be provided using annotations or options (see [Configuration via options](#configuration-via-options) for details), and runs a test with each of provided strategies. If an error is found, an `AssertionError` is thrown and the detailed error information is printed to the standard output. It is recommended to use **JUnit** or similar testing library to run `LinChecker.check(...)` method. 
 

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

@@ -31,6 +31,7 @@
 import org.jetbrains.kotlinx.lincheck.verifier.Verifier;
 import org.jetbrains.kotlinx.lincheck.verifier.linearizability.LinearizabilityVerifier;
 
+import java.lang.reflect.*;
 import java.util.Arrays;
 import java.util.List;
 import java.util.stream.Collectors;
@@ -81,7 +82,8 @@ protected CTestConfiguration(Class<?> testClass, int iterations, int threads, in
         this.sequentialSpecification = sequentialSpecification;
     }
 
-    protected abstract Strategy createStrategy(Class<?> testClass, ExecutionScenario scenario, Verifier verifier);
+    protected abstract Strategy createStrategy(Class<?> testClass, ExecutionScenario scenario,
+                                               List<Method> validationFunctions, Verifier verifier);
 
     static List<CTestConfiguration> createFromTestClassAnnotations(Class<?> testClass) {
         Stream<StressCTestConfiguration> stressConfigurations = Arrays.stream(testClass.getAnnotationsByType(StressCTest.class))

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

@@ -22,9 +22,7 @@
  * #L%
  */
 
-import org.jetbrains.kotlinx.lincheck.annotations.OpGroupConfig;
-import org.jetbrains.kotlinx.lincheck.annotations.Operation;
-import org.jetbrains.kotlinx.lincheck.annotations.Param;
+import org.jetbrains.kotlinx.lincheck.annotations.*;
 import org.jetbrains.kotlinx.lincheck.execution.ActorGenerator;
 import org.jetbrains.kotlinx.lincheck.paramgen.*;
 import org.jetbrains.kotlinx.lincheck.strategy.stress.StressCTest;
@@ -47,10 +45,12 @@
 public class CTestStructure {
     public final List<ActorGenerator> actorGenerators;
     public final List<OperationGroup> operationGroups;
+    public final List<Method> validationFunctions;
 
-    private CTestStructure(List<ActorGenerator> actorGenerators, List<OperationGroup> operationGroups) {
+    private CTestStructure(List<ActorGenerator> actorGenerators, List<OperationGroup> operationGroups, List<Method> validationFunctions) {
         this.actorGenerators = actorGenerators;
         this.operationGroups = operationGroups;
+        this.validationFunctions = validationFunctions;
     }
 
     /**
@@ -60,18 +60,21 @@ public static CTestStructure getFromTestClass(Class<?> testClass) {
         Map<String, ParameterGenerator<?>> namedGens = new HashMap<>();
         Map<String, OperationGroup> groupConfigs = new HashMap<>();
         List<ActorGenerator> actorGenerators = new ArrayList<>();
+        List<Method> validationFunctions = new ArrayList<>();
         Class<?> clazz = testClass;
         while (clazz != null) {
-            readTestStructureFromClass(clazz, namedGens, groupConfigs, actorGenerators);
+            readTestStructureFromClass(clazz, namedGens, groupConfigs, actorGenerators, validationFunctions);
             clazz = clazz.getSuperclass();
         }
         // Create StressCTest class configuration
-        return new CTestStructure(actorGenerators, new ArrayList<>(groupConfigs.values()));
+        return new CTestStructure(actorGenerators, new ArrayList<>(groupConfigs.values()), validationFunctions);
     }
 
     private static void readTestStructureFromClass(Class<?> clazz, Map<String, ParameterGenerator<?>> namedGens,
                                                    Map<String, OperationGroup> groupConfigs,
-                                                   List<ActorGenerator> actorGenerators) {
+                                                   List<ActorGenerator> actorGenerators,
+                                                   List<Method> validationFunctions
+    ) {
         // Read named parameter paramgen (declared for class)
         for (Param paramAnn : clazz.getAnnotationsByType(Param.class)) {
             if (paramAnn.name().isEmpty()) {
@@ -115,6 +118,11 @@ private static void readTestStructureFromClass(Class<?> clazz, Map<String, Param
                     operationGroup.actors.add(actorGenerator);
                 }
             }
+            if (m.isAnnotationPresent(Validate.class)) {
+                if (m.getParameterCount() != 0)
+                    throw new IllegalStateException("Validation function " + m.getName() + " should not have parameters");
+                validationFunctions.add(m);
+            }
         }
     }
 

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

@@ -116,7 +116,7 @@ class LinChecker (private val testClass: Class<*>, options: Options<*, *>?) {
         if (isValid) run(testCfg, verifier) else null
 
     private fun ExecutionScenario.run(testCfg: CTestConfiguration, verifier: Verifier): LincheckFailure? {
-        val strategy = testCfg.createStrategy(testClass, this, verifier)
+        val strategy = testCfg.createStrategy(testClass, this, testStructure.validationFunctions, verifier)
         return strategy.run()
     }
 

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

@@ -121,13 +121,15 @@ private fun uniteActorsAndResultsAligned(actors: List<Actor>, results: List<Resu
     }
 }
 
-private fun StringBuilder.appendExecutionScenario(scenario: ExecutionScenario) {
+internal fun StringBuilder.appendExecutionScenario(scenario: ExecutionScenario) {
     if (scenario.initExecution.isNotEmpty()) {
         appendln("Execution scenario (init part):")
         appendln(scenario.initExecution)
     }
-    appendln("Execution scenario (parallel part):")
-    append(printInColumns(scenario.parallelExecution))
+    if (scenario.parallelExecution.isNotEmpty()) {
+        appendln("Execution scenario (parallel part):")
+        append(printInColumns(scenario.parallelExecution))
+    }
     if (scenario.parallelExecution.isNotEmpty()) {
         appendln()
         appendln("Execution scenario (post part):")
@@ -140,14 +142,13 @@ internal fun StringBuilder.appendFailure(failure: LincheckFailure): StringBuilde
         is IncorrectResultsFailure -> appendIncorrectResultsFailure(failure)
         is DeadlockWithDumpFailure -> appendDeadlockWithDumpFailure(failure)
         is UnexpectedExceptionFailure -> appendUnexpectedExceptionFailure(failure)
+        is ValidationFailure -> appendValidationFailure(failure)
     }
 
 private fun StringBuilder.appendUnexpectedExceptionFailure(failure: UnexpectedExceptionFailure): StringBuilder {
     appendln("= The execution failed with an unexpected exception =")
     appendExecutionScenario(failure.scenario)
-    val sw = StringWriter()
-    failure.exception.printStackTrace(PrintWriter(sw))
-    appendln(sw.toString())
+    appendException(failure.exception)
     return this
 }
 
@@ -183,4 +184,17 @@ private fun StringBuilder.appendIncorrectResultsFailure(failure: IncorrectResult
         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---")
     return this
+}
+
+private fun StringBuilder.appendValidationFailure(failure: ValidationFailure): StringBuilder {
+    appendln("= Validation function ${failure.functionName} has been failed =")
+    appendExecutionScenario(failure.scenario)
+    appendException(failure.exception)
+    return this
+}
+
+private fun StringBuilder.appendException(t: Throwable) {
+    val sw = StringWriter()
+    t.printStackTrace(PrintWriter(sw))
+    appendln(sw.toString())
 }

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

@@ -72,14 +72,14 @@ internal fun executeActor(testInstance: Any, actor: Actor) = executeActor(testIn
  * Executes the specified actor on the sequential specification instance and returns its result.
  */
 internal fun executeActor(
-    specification: Any,
+    instance: Any,
     actor: Actor,
     completion: Continuation<Any?>?
 ): Result {
     try {
-        val m = getMethod(specification, actor)
+        val m = getMethod(instance, actor.method)
         val args = if (actor.isSuspendable) actor.arguments + completion else actor.arguments
-        val res = m.invoke(specification, *args.toTypedArray())
+        val res = m.invoke(instance, *args.toTypedArray())
         return if (m.returnType.isAssignableFrom(Void.TYPE)) VoidResult else createLincheckResult(res)
     } catch (invE: Throwable) {
         val eClass = (invE.cause ?: invE).javaClass.normalize()
@@ -98,16 +98,37 @@ internal fun executeActor(
     }
 }
 
+internal inline fun executeValidationFunctions(instance: Any, validationFunctions: List<Method>,
+                                        onError: (functionName: String, exception: Throwable) -> Unit) {
+    for (f in validationFunctions) {
+        val validationException = executeValidationFunction(instance, f)
+        if (validationException != null) {
+            onError(f.name, validationException)
+            return
+        }
+    }
+}
+
+private fun executeValidationFunction(instance: Any, validationFunction: Method): Throwable? {
+    val m = getMethod(instance, validationFunction)
+    try {
+        m.invoke(instance)
+    } catch (e: Throwable) {
+        return e
+    }
+    return null
+}
+
 internal fun <T> Class<T>.normalize() = LinChecker::class.java.classLoader.loadClass(name) as Class<T>
 
 private val methodsCache = WeakHashMap<Class<*>, WeakHashMap<Method, WeakReference<Method>>>()
 
-private fun getMethod(instance: Any, actor: Actor): Method {
+private fun getMethod(instance: Any, method: Method): Method {
     val methods = methodsCache.computeIfAbsent(instance.javaClass) { WeakHashMap() }
-    return methods[actor.method]?.get() ?: run {
-        val method = instance.javaClass.getMethod(actor.method.name, *actor.method.parameterTypes)
-        methods[actor.method] = WeakReference(method)
-        method
+    return methods[method]?.get() ?: run {
+        val m = instance.javaClass.getMethod(method.name, *method.parameterTypes)
+        methods[method] = WeakReference(m)
+        m
     }
 }
 

src/main/java/org/jetbrains/kotlinx/lincheck/annotations/Validate.kt

@@ -0,0 +1,41 @@
+/*-
+ * #%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.annotations
+
+import kotlin.annotation.AnnotationRetention.*
+import kotlin.annotation.AnnotationTarget.*
+
+/**
+ * It is possible in **lincheck** to add the validation of the testing data structure invariants,
+ * which is implemented via functions that can be executed multiple times during execution
+ * when there is no running operation in an intermediate state (e.g., in the stress mode
+ * they are invoked after each of the init and post part operations and after the whole parallel part).
+ * Thus, these functions should not modify the data structure.
+ *
+ * Validation functions should be marked with this annotation, should not have arguments,
+ * and should not return anything (in other words, the returning type is `void`).
+ * In case the testing data structure is in an invalid state, they should throw exceptions
+ * ([AssertionError] or [IllegalStateException] are the preferable ones).
+ */
+@Retention(RUNTIME)
+@Target(FUNCTION)
+annotation class Validate

src/main/java/org/jetbrains/kotlinx/lincheck/execution/ExecutionScenario.java

@@ -28,6 +28,7 @@
 import java.util.stream.*;
 
 import static org.jetbrains.kotlinx.lincheck.ActorKt.isSuspendable;
+import static org.jetbrains.kotlinx.lincheck.ReporterKt.appendExecutionScenario;
 
 /**
  * This class represents an execution scenario, which
@@ -77,4 +78,11 @@ public int getThreads() {
     public boolean hasSuspendableActors() {
         return Stream.concat(parallelExecution.stream().flatMap(Collection::stream), postExecution.stream()).anyMatch(actor -> isSuspendable(actor.getMethod()));
     }
+
+    @Override
+    public String toString() {
+        StringBuilder sb = new StringBuilder();
+        appendExecutionScenario(sb, this);
+        return sb.toString();
+    }
 }

src/main/java/org/jetbrains/kotlinx/lincheck/runner/InvocationResult.kt

@@ -47,4 +47,10 @@ class DeadlockInvocationResult(
  */
 class UnexpectedExceptionInvocationResult(
     val exception: Throwable
+) : InvocationResult()
+
+class ValidationFailureInvocationResult(
+    val scenario: ExecutionScenario,
+    val functionName: String,
+    val exception: Throwable
 ) : InvocationResult()

src/main/java/org/jetbrains/kotlinx/lincheck/runner/ParallelThreadsRunner.kt

@@ -26,6 +26,7 @@ import org.jetbrains.kotlinx.lincheck.*
 import org.jetbrains.kotlinx.lincheck.execution.*
 import org.jetbrains.kotlinx.lincheck.strategy.*
 import org.objectweb.asm.*
+import java.lang.reflect.*
 import java.util.concurrent.*
 import java.util.concurrent.Executors.*
 import java.util.concurrent.atomic.*
@@ -44,8 +45,9 @@ private typealias SuspensionPointResultWithContinuation = AtomicReference<Pair<k
 open class ParallelThreadsRunner(
     strategy: Strategy,
     testClass: Class<*>,
+    validationFunctions: List<Method>,
     waits: List<IntArray>?
-) : Runner(strategy, testClass) {
+) : Runner(strategy, testClass, validationFunctions) {
     private lateinit var testInstance: Any
     private val executor = newFixedThreadPool(scenario.threads, ParallelThreadsRunner::TestThread)
 
@@ -192,7 +194,18 @@ open class ParallelThreadsRunner(
 
     override fun run(): InvocationResult {
         reset()
-        val initResults = scenario.initExecution.map { initActor -> executeActor(testInstance, initActor) }
+        val initResults = scenario.initExecution.mapIndexed { i, initActor ->
+            executeActor(testInstance, initActor).also {
+                executeValidationFunctions(testInstance, validationFunctions) { functionName, exception ->
+                    val s = ExecutionScenario(
+                        scenario.initExecution.subList(0, i + 1),
+                        emptyList(),
+                        emptyList()
+                    )
+                    return ValidationFailureInvocationResult(s, functionName, exception)
+                }
+            }
+        }
         testThreadExecutions.map { executor.submit(it) }.forEach { future ->
             try {
                 future.get(10, TimeUnit.SECONDS)
@@ -206,16 +219,35 @@ open class ParallelThreadsRunner(
         val parallelResultsWithClock = testThreadExecutions.map { ex ->
             ex.results.zip(ex.clocks).map { ResultWithClock(it.first, HBClock(it.second)) }
         }
+        executeValidationFunctions(testInstance, validationFunctions) { functionName, exception ->
+            val s = ExecutionScenario(
+                scenario.initExecution,
+                scenario.parallelExecution,
+                emptyList()
+            )
+            return ValidationFailureInvocationResult(s, functionName, exception)
+        }
         val dummyCompletion = Continuation<Any?>(EmptyCoroutineContext) {}
         var postPartSuspended = false
-        val postResults = scenario.postExecution.map { postActor ->
+        val postResults = scenario.postExecution.mapIndexed { i, postActor ->
             // no actors are executed after suspension of a post part
-            if (postPartSuspended) {
+            val result = if (postPartSuspended) {
                 NoResult
             } else {
                 // post part may contain suspendable actors if there aren't any in the parallel part, invoke with dummy continuation
-                executeActor(testInstance, postActor, dummyCompletion).also { postPartSuspended = it.wasSuspended }
+                executeActor(testInstance, postActor, dummyCompletion).also {
+                    postPartSuspended = it.wasSuspended
+                }
+            }
+            executeValidationFunctions(testInstance, validationFunctions) { functionName, exception ->
+                val s = ExecutionScenario(
+                    scenario.initExecution,
+                    scenario.parallelExecution,
+                    scenario.postExecution.subList(0, i + 1)
+                )
+                return ValidationFailureInvocationResult(s, functionName, exception)
             }
+            result
         }
         val results = ExecutionResult(initResults, parallelResultsWithClock, postResults)
         return CompletedInvocationResult(results)