Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Minimization improvement: try to remove two operations and move operations to init and post parts #350

Merged
merged 2 commits into from
Aug 1, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
70 changes: 64 additions & 6 deletions src/jvm/main/org/jetbrains/kotlinx/lincheck/LinChecker.kt
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
Original file line number Diff line number Diff line change
@@ -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")
}
}
Loading