Roman Elizarov | a7db8ec | 2017-12-21 22:45:12 +0300 | [diff] [blame] | 1 | /* |
Roman Elizarov | 1f74a2d | 2018-06-29 19:19:45 +0300 | [diff] [blame] | 2 | * Copyright 2016-2018 JetBrains s.r.o. Use of this source code is governed by the Apache 2.0 license. |
Roman Elizarov | a7db8ec | 2017-12-21 22:45:12 +0300 | [diff] [blame] | 3 | */ |
| 4 | |
Roman Elizarov | c43a9be | 2017-11-09 15:38:45 +0300 | [diff] [blame] | 5 | package kotlinx.coroutines.experimental |
| 6 | |
| 7 | import com.devexperts.dxlab.lincheck.Actor |
| 8 | import com.devexperts.dxlab.lincheck.Result |
| 9 | import com.devexperts.dxlab.lincheck.verifier.Verifier |
| 10 | import java.lang.reflect.Method |
| 11 | import java.util.* |
| 12 | import kotlin.coroutines.experimental.Continuation |
| 13 | import kotlin.coroutines.experimental.CoroutineContext |
| 14 | import kotlin.coroutines.experimental.EmptyCoroutineContext |
| 15 | import kotlin.coroutines.experimental.intrinsics.COROUTINE_SUSPENDED |
| 16 | import kotlin.coroutines.experimental.intrinsics.startCoroutineUninterceptedOrReturn |
| 17 | |
| 18 | data class OpResult(val name: String, val value: Any?) { |
| 19 | override fun toString(): String = "$name=$value" |
| 20 | } |
| 21 | |
| 22 | private const val CS_STR = "COROUTINE_SUSPENDED" |
| 23 | |
| 24 | class 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 | |
| 63 | class LinVerifier( |
Sergey Mashkov | 62deb43 | 2017-11-09 19:50:26 +0300 | [diff] [blame] | 64 | actorsPerThread: List<List<Actor>>, testInstance: Any, resetMethod: Method? |
Roman Elizarov | c43a9be | 2017-11-09 15:38:45 +0300 | [diff] [blame] | 65 | ) : 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 | |
| 133 | private val VALUE = Result::class.java.getDeclaredField("value").apply { isAccessible = true } |
| 134 | |
| 135 | @Suppress("UNCHECKED_CAST") |
| 136 | private val Result.resultValue: List<OpResult> |
| 137 | get() = VALUE.get(this) as List<OpResult> |