New model checker algorithm

bootstrap/src/sun/nio/ch/lincheck/EventTracker.java

@@ -31,23 +31,30 @@ public interface EventTracker {
 
     void beforeNewObjectCreation(String className);
     void afterNewObjectCreation(Object obj);
+    void afterObjectInitialization(Object obj);
 
-    boolean beforeReadField(Object obj, String className, String fieldName, int codeLocation,
+    boolean beforeReadField(Object obj, String className, String fieldName, String typeDescriptor, int codeLocation,
                             boolean isStatic, boolean isFinal);
-    boolean beforeReadArrayElement(Object array, int index, int codeLocation);
+    boolean beforeReadArrayElement(Object array, int index, String typeDescriptor, int codeLocation);
     void afterRead(Object value);
 
-    boolean beforeWriteField(Object obj, String className, String fieldName, Object value, int codeLocation,
+    Object interceptReadResult();
+
+    boolean beforeWriteField(Object obj, String className, String fieldName, String typeDescriptor, Object value, int codeLocation,
                              boolean isStatic, boolean isFinal);
-    boolean beforeWriteArrayElement(Object array, int index, Object value, int codeLocation);
+    boolean beforeWriteArrayElement(Object array, int index, String typeDescriptor, Object value, int codeLocation);
     void afterWrite();
 
     void afterReflectiveSetter(Object receiver, Object value);
 
-    void beforeMethodCall(Object owner, String className, String methodName, int codeLocation, int methodId, Object[] params);
+    void onArrayCopy(Object srcArray, int srcPos, Object dstArray, int dstPos, int length);
+
+    boolean beforeMethodCall(Object owner, String className, String methodName, int codeLocation, int methodId, Object[] params);
     void onMethodCallReturn(Object result);
     void onMethodCallException(Throwable t);
 
+    Object interceptMethodCallResult();
+
     Random getThreadLocalRandom();
     int randomNextInt();
 

bootstrap/src/sun/nio/ch/lincheck/Injections.java

@@ -186,20 +186,24 @@ public static boolean isRandom(Object any) {
      *
      * @return whether the trace point was created
      */
-    public static boolean beforeReadField(Object obj, String className, String fieldName, int codeLocation,
+    public static boolean beforeReadField(Object obj, String className, String fieldName, String typeDescriptor, int codeLocation,
                                           boolean isStatic, boolean isFinal) {
         if (!isStatic && obj == null) return false; // Ignore, NullPointerException will be thrown
-        return getEventTracker().beforeReadField(obj, className, fieldName, codeLocation, isStatic, isFinal);
+        return getEventTracker().beforeReadField(obj, className, fieldName, typeDescriptor, codeLocation, isStatic, isFinal);
     }
 
     /**
      * Called from the instrumented code before any array cell read.
      *
      * @return whether the trace point was created
      */
-    public static boolean beforeReadArray(Object array, int index, int codeLocation) {
+    public static boolean beforeReadArray(Object array, int index, String typeDescriptor, int codeLocation) {
         if (array == null) return false; // Ignore, NullPointerException will be thrown
-        return getEventTracker().beforeReadArrayElement(array, index, codeLocation);
+        return getEventTracker().beforeReadArrayElement(array, index, typeDescriptor, codeLocation);
+    }
+
+    public static Object interceptReadResult() {
+        return getEventTracker().interceptReadResult();
     }
 
     /**
@@ -214,20 +218,20 @@ public static void afterRead(Object value) {
      *
      * @return whether the trace point was created
      */
-    public static boolean beforeWriteField(Object obj, String className, String fieldName, Object value, int codeLocation,
+    public static boolean beforeWriteField(Object obj, String className, String fieldName, String typeDescriptor, Object value, int codeLocation,
                                            boolean isStatic, boolean isFinal) {
         if (!isStatic && obj == null) return false; // Ignore, NullPointerException will be thrown
-        return getEventTracker().beforeWriteField(obj, className, fieldName, value, codeLocation, isStatic, isFinal);
+        return getEventTracker().beforeWriteField(obj, className, fieldName, typeDescriptor, value, codeLocation, isStatic, isFinal);
     }
 
     /**
      * Called from the instrumented code before any array cell write.
      *
      * @return whether the trace point was created
      */
-    public static boolean beforeWriteArray(Object array, int index, Object value, int codeLocation) {
+    public static boolean beforeWriteArray(Object array, int index, String typeDescriptor, Object value, int codeLocation) {
         if (array == null) return false; // Ignore, NullPointerException will be thrown
-        return getEventTracker().beforeWriteArrayElement(array, index, value, codeLocation);
+        return getEventTracker().beforeWriteArrayElement(array, index, typeDescriptor, value, codeLocation);
     }
 
     /**
@@ -250,13 +254,27 @@ public static void afterReflectiveSetter(Object receiver, Object value) {
         getEventTracker().afterReflectiveSetter(receiver, value);
     }
 
+    public static void onArrayCopy(Object srcArray, int srcPos, Object dstArray, int dstPos, int length) {
+        getEventTracker().onArrayCopy(srcArray, srcPos, dstArray, dstPos, length);
+    }
+
     /**
      * Called from the instrumented code before any method call.
      *
      * @param owner is `null` for public static methods.
+     * @return true if the method result should be intercepted. TODO: revisit this API decision
      */
-    public static void beforeMethodCall(Object owner, String className, String methodName, int codeLocation, int methodId, Object[] params) {
-        getEventTracker().beforeMethodCall(owner, className, methodName, codeLocation, methodId, params);
+    public static boolean beforeMethodCall(Object owner, String className, String methodName, int codeLocation, int methodId, Object[] params) {
+        return getEventTracker().beforeMethodCall(owner, className, methodName, codeLocation, methodId, params);
+    }
+
+    /**
+     * Intercepts the result of a method call.
+     *
+     * @return The intercepted result of the method call.
+     */
+    public static Object interceptMethodCallResult() {
+        return getEventTracker().interceptMethodCallResult();
     }
 
     /**
@@ -294,6 +312,10 @@ public static void afterNewObjectCreation(Object obj) {
         getEventTracker().afterNewObjectCreation(obj);
     }
 
+    public static void afterObjectInitialization(Object obj) {
+        getEventTracker().afterObjectInitialization(obj);
+    }
+
     /**
      * Called from the instrumented code to replace [java.lang.Object.hashCode] method call with some
      * deterministic value.

build.gradle.kts

@@ -26,7 +26,7 @@ repositories {
 kotlin {
     @OptIn(ExperimentalKotlinGradlePluginApi::class)
     compilerOptions {
-        allWarningsAsErrors = true
+        // allWarningsAsErrors = true
     }
 
     jvm {
@@ -119,7 +119,16 @@ tasks {
         if (instrumentAllClasses.toBoolean()) {
             systemProperty("lincheck.instrumentAllClasses", "true")
         }
-        val extraArgs = mutableListOf<String>()
+        val extraArgs = mutableListOf<String>(
+            // flags to import Unsafe module;
+            // it is used in some tests to check handling of unsafe APIs by Lincheck
+            "--add-opens", "java.base/jdk.internal.misc=ALL-UNNAMED",
+            "--add-exports", "java.base/jdk.internal.util=ALL-UNNAMED",
+        )
+        val useExperimentalModelChecking: String by project
+        if (useExperimentalModelChecking.toBoolean()) {
+            extraArgs.add("-Dlincheck.useExperimentalModelChecking=true")
+        }
         val withEventIdSequentialCheck: String by project
         if (withEventIdSequentialCheck.toBoolean()) {
             extraArgs.add("-Dlincheck.debug.withEventIdSequentialCheck=true")
@@ -157,6 +166,8 @@ tasks {
             ideaActive -> 10
             else -> 0
         }
+        // temporarily ignore representation tests, because they are unsupported in the new strategy
+        // exclude("org/jetbrains/kotlinx/lincheck_test/representation")
     }
 
     val jvmTestIsolated = register<Test>("jvmTestIsolated") {

gradle.properties

@@ -18,6 +18,7 @@ lastCopyrightYear=2023
 jdkToolchainVersion=17
 runAllTestsInSeparateJVMs=false
 instrumentAllClasses=false
+useExperimentalModelChecking=false
 withEventIdSequentialCheck=false
 
 kotlinVersion=1.9.21

src/jvm/main/org/jetbrains/kotlinx/lincheck/CTestConfiguration.kt

@@ -102,7 +102,8 @@ internal fun createFromTestClassAnnotations(testClass: Class<*>): List<CTestConf
                         testClass
                     ),
                     timeoutMs = DEFAULT_TIMEOUT_MS,
-                    customScenarios = emptyList()
+                    customScenarios = emptyList(),
+                    experimentalModelChecking = false,
                 )
             }
     return stressConfigurations + modelCheckingConfigurations

src/jvm/main/org/jetbrains/kotlinx/lincheck/ObjectTraverser.kt

@@ -21,9 +21,7 @@
 package org.jetbrains.kotlinx.lincheck
 
 import org.jetbrains.kotlinx.lincheck.strategy.managed.ObjectLabelFactory.getObjectNumber
-import org.jetbrains.kotlinx.lincheck.util.readFieldViaUnsafe
-import sun.misc.Unsafe
-import java.lang.reflect.Field
+import org.jetbrains.kotlinx.lincheck.util.*
 import java.lang.reflect.Modifier
 import java.math.BigDecimal
 import java.math.BigInteger
@@ -115,23 +113,6 @@ private fun enumerateObjects(obj: Any, processedObjects: MutableSet<Any>, object
     }
 }
 
-private fun readField(obj: Any?, field: Field): Any? {
-    if (!field.type.isPrimitive) {
-        return readFieldViaUnsafe(obj, field, Unsafe::getObject)
-    }
-    return when (field.type) {
-        Boolean::class.javaPrimitiveType    -> readFieldViaUnsafe(obj, field, Unsafe::getBoolean)
-        Byte::class.javaPrimitiveType       -> readFieldViaUnsafe(obj, field, Unsafe::getByte)
-        Char::class.javaPrimitiveType       -> readFieldViaUnsafe(obj, field, Unsafe::getChar)
-        Short::class.javaPrimitiveType      -> readFieldViaUnsafe(obj, field, Unsafe::getShort)
-        Int::class.javaPrimitiveType        -> readFieldViaUnsafe(obj, field, Unsafe::getInt)
-        Long::class.javaPrimitiveType       -> readFieldViaUnsafe(obj, field, Unsafe::getLong)
-        Double::class.javaPrimitiveType     -> readFieldViaUnsafe(obj, field, Unsafe::getDouble)
-        Float::class.javaPrimitiveType      -> readFieldViaUnsafe(obj, field, Unsafe::getFloat)
-        else                                -> error("No more types expected")
-    }
-}
-
 private fun isAtomic(value: Any?): Boolean {
     if (value == null) return false
     return value.javaClass.canonicalName.let {

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

@@ -45,7 +45,7 @@ class Reporter(private val logLevel: LoggingLevel) {
     }
 }
 
-@JvmField val DEFAULT_LOG_LEVEL = WARN
+@JvmField val DEFAULT_LOG_LEVEL = INFO
 enum class LoggingLevel {
     INFO, WARN
 }

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

@@ -182,7 +182,7 @@ internal fun <T> CancellableContinuation<T>.cancelByLincheck(promptCancellation:
     }
 }
 
-internal enum class CancellationResult { CANCELLED_BEFORE_RESUMPTION, CANCELLED_AFTER_RESUMPTION, CANCELLATION_FAILED }
+enum class CancellationResult { CANCELLED_BEFORE_RESUMPTION, CANCELLED_AFTER_RESUMPTION, CANCELLATION_FAILED }
 
 /**
  * Returns `true` if the continuation was cancelled by [CancellableContinuation.cancel].
@@ -233,17 +233,21 @@ internal val Class<*>.allDeclaredFieldWithSuperclasses get(): List<Field> {
 @Suppress("DEPRECATION")
 internal fun findFieldNameByOffset(targetType: Class<*>, offset: Long): String? {
     // Extract the private offset value and find the matching field.
-    for (field in targetType.declaredFields) {
+    for (field in targetType.allDeclaredFieldWithSuperclasses) {
         try {
             if (Modifier.isNative(field.modifiers)) continue
-            val fieldOffset = if (Modifier.isStatic(field.modifiers)) UnsafeHolder.UNSAFE.staticFieldOffset(field)
-            else UnsafeHolder.UNSAFE.objectFieldOffset(field)
-            if (fieldOffset == offset) return field.name
+            val fieldOffset =
+                if (Modifier.isStatic(field.modifiers))
+                    UnsafeHolder.UNSAFE.staticFieldOffset(field)
+                else
+                    UnsafeHolder.UNSAFE.objectFieldOffset(field)
+            if (fieldOffset == offset) {
+                return field.name
+            }
         } catch (t: Throwable) {
             t.printStackTrace()
         }
     }
-
     return null // Field not found
 }
 

src/jvm/main/org/jetbrains/kotlinx/lincheck/execution/HBClock.kt

@@ -13,15 +13,32 @@ 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]
 
+    fun set(other: HBClock) {
+        check(clock.size == other.clock.size)
+        for (i in clock.indices) {
+            clock[i] = other.clock[i]
+        }
+    }
+
+    fun reset() {
+        for (i in clock.indices) {
+            clock[i] = 0
+        }
+    }
+
     /**
      * Checks whether the clock contains information for any thread
      * excluding the one this clock is associated with.
      */
     fun isEmpty(clockThreadId: Int) = clock.filterIndexed { t, _ -> t != clockThreadId }.all { it == 0 }
 
+    fun copy(): HBClock {
+        return HBClock(clock.copyOf())
+    }
+
     override fun toString() = clock.joinToString(prefix = "[", separator = ",", postfix = "]")
 
     override fun equals(other: Any?): Boolean {

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

@@ -11,6 +11,7 @@ package org.jetbrains.kotlinx.lincheck.runner
 
 import org.jetbrains.kotlinx.lincheck.execution.*
 import org.jetbrains.kotlinx.lincheck.strategy.managed.ManagedStrategy
+import org.jetbrains.kotlinx.lincheck.strategy.managed.eventstructure.consistency.Inconsistency
 
 /**
  * Represents results for invocations, see [Runner.run].
@@ -65,7 +66,29 @@ class ObstructionFreedomViolationInvocationResult(
     val results: ExecutionResult
 ) : InvocationResult()
 
+class InconsistentInvocationResult(
+    val inconsistency: Inconsistency
+) : InvocationResult()
+
+/**
+ * Invocation is aborted due to one of the threads reaching
+ * the bound on the number of spin-loop iterations.
+ */
+class SpinLoopBoundInvocationResult : InvocationResult()
+
 /**
  * Indicates that spin-cycle has been found for the first time and replay of current interleaving is required.
  */
-data object SpinCycleFoundAndReplayRequired: InvocationResult()
+data object SpinCycleFoundAndReplayRequired: InvocationResult()
+
+fun InvocationResult.isAbortedInvocation(): Boolean =
+    when (this) {
+        is ManagedDeadlockInvocationResult,
+        is RunnerTimeoutInvocationResult,
+        is SpinLoopBoundInvocationResult,
+        is UnexpectedExceptionInvocationResult,
+        is ObstructionFreedomViolationInvocationResult,
+        is InconsistentInvocationResult
+             -> true
+        else -> false
+    }