blob: d417d594aa7aef2d0ed9f69071883dee0bf3fdbb [file] [log] [blame]
Roman Elizarova7db8ec2017-12-21 22:45:12 +03001/*
Roman Elizarov1f74a2d2018-06-29 19:19:45 +03002 * Copyright 2016-2018 JetBrains s.r.o. Use of this source code is governed by the Apache 2.0 license.
Roman Elizarova7db8ec2017-12-21 22:45:12 +03003 */
4
Roman Elizarovc43a9be2017-11-09 15:38:45 +03005package kotlinx.coroutines.experimental
6
7import com.devexperts.dxlab.lincheck.Actor
8import com.devexperts.dxlab.lincheck.Result
9import com.devexperts.dxlab.lincheck.verifier.Verifier
10import java.lang.reflect.Method
11import java.util.*
12import kotlin.coroutines.experimental.Continuation
13import kotlin.coroutines.experimental.CoroutineContext
14import kotlin.coroutines.experimental.EmptyCoroutineContext
15import kotlin.coroutines.experimental.intrinsics.COROUTINE_SUSPENDED
16import kotlin.coroutines.experimental.intrinsics.startCoroutineUninterceptedOrReturn
17
18data class OpResult(val name: String, val value: Any?) {
19 override fun toString(): String = "$name=$value"
20}
21
22private const val CS_STR = "COROUTINE_SUSPENDED"
23
24class LinTesting {
25 private val resumed = object : ThreadLocal<ArrayList<OpResult>>() {
26 override fun initialValue() = arrayListOf<OpResult>()
27 }
28
29 private inline fun wrap(block: () -> Any?): Any? =
30 try { repr(block()) }
31 catch(e: Throwable) { repr(e) }
32
33 private fun repr(e: Any?): Any? =
34 when {
35 e === COROUTINE_SUSPENDED -> CS_STR
36 e is Throwable -> e.toString()
37 else -> e
38 }
39
40 fun <T> run(name: String, block: suspend () -> T): List<OpResult> {
41 val list = resumed.get()
42 list.clear()
43 val result = arrayListOf(OpResult(name, wrap {
44 block.startCoroutineUninterceptedOrReturn(completion = object : Continuation<Any?> {
45 override val context: CoroutineContext
46 get() = EmptyCoroutineContext
47
48 override fun resume(value: Any?) {
49 resumed.get() += OpResult(name, repr(value))
50 }
51
52 override fun resumeWithException(exception: Throwable) {
53 resumed.get() += OpResult(name, repr(exception))
54 }
55 }
56 )
57 }))
58 result.addAll(list)
59 return result
60 }
61}
62
63class LinVerifier(
Sergey Mashkov62deb432017-11-09 19:50:26 +030064 actorsPerThread: List<List<Actor>>, testInstance: Any, resetMethod: Method?
Roman Elizarovc43a9be2017-11-09 15:38:45 +030065) : Verifier(actorsPerThread, testInstance, resetMethod) {
66 private val possibleResultsSet: Set<List<List<Result>>> =
67 generateAllLinearizableExecutions(actorsPerThread)
68 .map { linEx: List<Actor> ->
69 val res: List<Result> = executeActors(testInstance, linEx)
70 val actorIds = linEx.withIndex().associateBy({ it.value}, { it.index })
71 actorsPerThread.map { actors -> actors.map { actor -> res[actorIds[actor]!!] } }
72 }.toSet()
73
74 override fun verifyResults(results: List<List<Result>>) {
75 if (!valid(results)) {
76 println("\nNon-linearizable execution:")
77 printResults(results)
78 println("\nPossible linearizable executions:")
79 possibleResultsSet.forEach { possibleResults ->
80 printResults(possibleResults)
81 println()
82 }
83 throw AssertionError("Non-linearizable execution detected, see log for details")
84 }
85 }
86
87 private fun printResults(results: List<List<Result>>) {
88 results.forEachIndexed { index, res ->
89 println("Thread $index: $res")
90 }
91 println("Op map: ${results.toOpMap()}")
92 }
93
94 private fun valid(results: List<List<Result>>): Boolean =
95 (results in possibleResultsSet) || possibleResultsSet.any { matches(results, it) }
96
97 private fun matches(results: List<List<Result>>, possible: List<List<Result>>): Boolean =
98 results.toOpMap() == possible.toOpMap()
99
100 private fun List<List<Result>>.toOpMap(): Map<String, List<Any?>> {
101 val filtered = flatMap { it }.flatMap { it.resultValue }.filter { it.value != CS_STR }
102 return filtered.groupBy({ it.name }, { it.value })
103 }
104
105 private fun generateAllLinearizableExecutions(actorsPerThread: List<List<Actor>>): List<List<Actor>> {
106 val executions = ArrayList<List<Actor>>()
107 generateLinearizableExecutions0(
108 executions, actorsPerThread, ArrayList<Actor>(), IntArray(actorsPerThread.size),
109 actorsPerThread.sumBy { it.size })
110 return executions
111 }
112
113 @Suppress("UNCHECKED_CAST")
114 private fun generateLinearizableExecutions0(executions: MutableList<List<Actor>>, actorsPerThread: List<List<Actor>>,
115 currentExecution: ArrayList<Actor>, indexes: IntArray, length: Int) {
116 if (currentExecution.size == length) {
117 executions.add(currentExecution.clone() as List<Actor>)
118 return
119 }
120 for (i in indexes.indices) {
121 val actors = actorsPerThread[i]
122 if (indexes[i] == actors.size)
123 continue
124 currentExecution.add(actors[indexes[i]])
125 indexes[i]++
126 generateLinearizableExecutions0(executions, actorsPerThread, currentExecution, indexes, length)
127 indexes[i]--
128 currentExecution.removeAt(currentExecution.size - 1)
129 }
130 }
131}
132
133private val VALUE = Result::class.java.getDeclaredField("value").apply { isAccessible = true }
134
135@Suppress("UNCHECKED_CAST")
136private val Result.resultValue: List<OpResult>
137 get() = VALUE.get(this) as List<OpResult>