Minimization improvement: try to remove two operations and move opera…

…tions to init and post parts (#350)

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

@@ -215,12 +215,70 @@ private fun LincheckFailure.minimize(checkScenario: (ExecutionScenario) -> Linch
 }
 
 private fun ExecutionScenario.tryMinimize(checkScenario: (ExecutionScenario) -> LincheckFailure?): LincheckFailure? {
-    // Reversed indices to avoid conflicts with in-loop removals
-    for (i in threads.indices.reversed()) {
-        for (j in threads[i].indices.reversed()) {
-            tryMinimize(i, j)
-                ?.run(checkScenario)
-                ?.let { return it }
+    // Try to remove only one operation.
+    for (threadId in threads.indices.reversed()) {
+        for (actorId in threads[threadId].indices.reversed()) {
+            tryMinimize(threadId, actorId)?.run(checkScenario)?.let { return it }
+        }
+    }
+    // Try to remove two operations. For some data structure, such as a queue,
+    // you need to remove pairwise operations, such as enqueue(e) and dequeue(),
+    // to minimize the scenario and keep the error.
+    for (threadId1 in threads.indices.reversed()) {
+        for (actorId1 in threads[threadId1].indices.reversed()) {
+            // Try to remove two operations at once.
+            val minimizedScenario = tryMinimize(threadId1, actorId1) ?: continue
+            for (threadId2 in minimizedScenario.threads.indices.reversed()) {
+                for (actorId2 in minimizedScenario.threads[threadId2].indices.reversed()) {
+                    minimizedScenario.tryMinimize(threadId2, actorId2)?.run(checkScenario)?.let { return it }
+                }
+            }
+        }
+    }
+    // Try to move one of the first operations to the initial (pre-parallel) part.
+    parallelExecution.forEachIndexed {  threadId: Int, actors: List<Actor> ->
+        if (actors.isNotEmpty()) {
+            val newInitExecution = initExecution + actors.first()
+            val newParallelExecution = parallelExecution.mapIndexed { t: Int, it: List<Actor> ->
+                if (t == threadId) {
+                    it.drop(1)
+                } else {
+                    ArrayList(it)
+                }
+            }
+            val newPostExecution = ArrayList(postExecution)
+            val optimizedScenario = ExecutionScenario(
+                initExecution = newInitExecution,
+                parallelExecution = newParallelExecution,
+                postExecution = newPostExecution,
+                validationFunction = validationFunction
+            )
+            if (optimizedScenario.isValid) {
+                optimizedScenario.run(checkScenario)?.let { return it }
+            }
+        }
+    }
+    // Try to move one of the last operations to the post (post-parallel) part.
+    parallelExecution.forEachIndexed {  threadId: Int, actors: List<Actor> ->
+        if (actors.isNotEmpty()) {
+            val newInitExecution = ArrayList(initExecution)
+            val newParallelExecution = parallelExecution.mapIndexed { t: Int, it: List<Actor> ->
+                if (t == threadId) {
+                    it.dropLast(1)
+                } else {
+                    ArrayList(it)
+                }
+            }
+            val newPostExecution = listOf(actors.last()) + postExecution
+            val optimizedScenario = ExecutionScenario(
+                initExecution = newInitExecution,
+                parallelExecution = newParallelExecution,
+                postExecution = newPostExecution,
+                validationFunction = validationFunction
+            )
+            if (optimizedScenario.isValid) {
+                optimizedScenario.run(checkScenario)?.let { return it }
+            }
         }
     }
     return null

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

@@ -104,8 +104,7 @@ val ExecutionScenario.hasPostPartAndSuspendableActors
  *   - if it contains suspendable actors, then post part should be empty.
  */
 val ExecutionScenario.isValid: Boolean
-    get() = !isParallelPartEmpty &&
-            (!hasSuspendableActors || (!hasSuspendableActorsInInitPart && !hasPostPartAndSuspendableActors))
+    get() = !isParallelPartEmpty && !hasSuspendableActorsInInitPart && !hasPostPartAndSuspendableActors
 
 /**
  * Validates the execution scenario.

src/jvm/test/org/jetbrains/kotlinx/lincheck_test/representation/ConcurrentLinkedDequeTest.kt

@@ -0,0 +1,45 @@
+/*
+ * Lincheck
+ *
+ * Copyright (C) 2019 - 2024 JetBrains s.r.o.
+ *
+ * This Source Code Form is subject to the terms of the
+ * Mozilla Public License, v. 2.0. If a copy of the MPL was not distributed
+ * with this file, You can obtain one at http://mozilla.org/MPL/2.0/.
+ */
+
+package org.jetbrains.kotlinx.lincheck_test.representation
+
+import org.jetbrains.kotlinx.lincheck.*
+import org.jetbrains.kotlinx.lincheck.annotations.*
+import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.*
+import org.jetbrains.kotlinx.lincheck_test.util.*
+import org.junit.*
+import java.util.concurrent.*
+
+class ConcurrentLinkedDequeTest {
+    private val deque = ConcurrentLinkedDeque<Int>()
+
+    @Operation
+    fun addFirst(e: Int) = deque.addFirst(e)
+
+    @Operation
+    fun addLast(e: Int) = deque.addLast(e)
+
+    @Operation
+    fun pollFirst() = deque.pollFirst()
+
+    @Operation
+    fun pollLast() = deque.pollLast()
+
+    @Operation
+    fun peekFirst() = deque.peekFirst()
+
+    @Operation
+    fun peekLast() = deque.peekLast()
+
+    @Test
+    fun modelCheckingTest() = ModelCheckingOptions().checkImpl(this::class.java) { failure ->
+        failure.checkLincheckOutput("concurrent_linked_deque.txt")
+    }
+}