Roman Elizarov | a7db8ec | 2017-12-21 22:45:12 +0300 | [diff] [blame] | 1 | /* |
| 2 | * Copyright 2016-2017 JetBrains s.r.o. |
| 3 | * |
| 4 | * Licensed under the Apache License, Version 2.0 (the "License"); |
| 5 | * you may not use this file except in compliance with the License. |
| 6 | * You may obtain a copy of the License at |
| 7 | * |
| 8 | * http://www.apache.org/licenses/LICENSE-2.0 |
| 9 | * |
| 10 | * Unless required by applicable law or agreed to in writing, software |
| 11 | * distributed under the License is distributed on an "AS IS" BASIS, |
| 12 | * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. |
| 13 | * See the License for the specific language governing permissions and |
| 14 | * limitations under the License. |
| 15 | */ |
| 16 | |
Roman Elizarov | c43a9be | 2017-11-09 15:38:45 +0300 | [diff] [blame] | 17 | package kotlinx.coroutines.experimental |
| 18 | |
| 19 | import com.devexperts.dxlab.lincheck.Actor |
| 20 | import com.devexperts.dxlab.lincheck.Result |
| 21 | import com.devexperts.dxlab.lincheck.verifier.Verifier |
| 22 | import java.lang.reflect.Method |
| 23 | import java.util.* |
| 24 | import kotlin.coroutines.experimental.Continuation |
| 25 | import kotlin.coroutines.experimental.CoroutineContext |
| 26 | import kotlin.coroutines.experimental.EmptyCoroutineContext |
| 27 | import kotlin.coroutines.experimental.intrinsics.COROUTINE_SUSPENDED |
| 28 | import kotlin.coroutines.experimental.intrinsics.startCoroutineUninterceptedOrReturn |
| 29 | |
| 30 | data class OpResult(val name: String, val value: Any?) { |
| 31 | override fun toString(): String = "$name=$value" |
| 32 | } |
| 33 | |
| 34 | private const val CS_STR = "COROUTINE_SUSPENDED" |
| 35 | |
| 36 | class LinTesting { |
| 37 | private val resumed = object : ThreadLocal<ArrayList<OpResult>>() { |
| 38 | override fun initialValue() = arrayListOf<OpResult>() |
| 39 | } |
| 40 | |
| 41 | private inline fun wrap(block: () -> Any?): Any? = |
| 42 | try { repr(block()) } |
| 43 | catch(e: Throwable) { repr(e) } |
| 44 | |
| 45 | private fun repr(e: Any?): Any? = |
| 46 | when { |
| 47 | e === COROUTINE_SUSPENDED -> CS_STR |
| 48 | e is Throwable -> e.toString() |
| 49 | else -> e |
| 50 | } |
| 51 | |
| 52 | fun <T> run(name: String, block: suspend () -> T): List<OpResult> { |
| 53 | val list = resumed.get() |
| 54 | list.clear() |
| 55 | val result = arrayListOf(OpResult(name, wrap { |
| 56 | block.startCoroutineUninterceptedOrReturn(completion = object : Continuation<Any?> { |
| 57 | override val context: CoroutineContext |
| 58 | get() = EmptyCoroutineContext |
| 59 | |
| 60 | override fun resume(value: Any?) { |
| 61 | resumed.get() += OpResult(name, repr(value)) |
| 62 | } |
| 63 | |
| 64 | override fun resumeWithException(exception: Throwable) { |
| 65 | resumed.get() += OpResult(name, repr(exception)) |
| 66 | } |
| 67 | } |
| 68 | ) |
| 69 | })) |
| 70 | result.addAll(list) |
| 71 | return result |
| 72 | } |
| 73 | } |
| 74 | |
| 75 | class LinVerifier( |
Sergey Mashkov | 62deb43 | 2017-11-09 19:50:26 +0300 | [diff] [blame] | 76 | actorsPerThread: List<List<Actor>>, testInstance: Any, resetMethod: Method? |
Roman Elizarov | c43a9be | 2017-11-09 15:38:45 +0300 | [diff] [blame] | 77 | ) : Verifier(actorsPerThread, testInstance, resetMethod) { |
| 78 | private val possibleResultsSet: Set<List<List<Result>>> = |
| 79 | generateAllLinearizableExecutions(actorsPerThread) |
| 80 | .map { linEx: List<Actor> -> |
| 81 | val res: List<Result> = executeActors(testInstance, linEx) |
| 82 | val actorIds = linEx.withIndex().associateBy({ it.value}, { it.index }) |
| 83 | actorsPerThread.map { actors -> actors.map { actor -> res[actorIds[actor]!!] } } |
| 84 | }.toSet() |
| 85 | |
| 86 | override fun verifyResults(results: List<List<Result>>) { |
| 87 | if (!valid(results)) { |
| 88 | println("\nNon-linearizable execution:") |
| 89 | printResults(results) |
| 90 | println("\nPossible linearizable executions:") |
| 91 | possibleResultsSet.forEach { possibleResults -> |
| 92 | printResults(possibleResults) |
| 93 | println() |
| 94 | } |
| 95 | throw AssertionError("Non-linearizable execution detected, see log for details") |
| 96 | } |
| 97 | } |
| 98 | |
| 99 | private fun printResults(results: List<List<Result>>) { |
| 100 | results.forEachIndexed { index, res -> |
| 101 | println("Thread $index: $res") |
| 102 | } |
| 103 | println("Op map: ${results.toOpMap()}") |
| 104 | } |
| 105 | |
| 106 | private fun valid(results: List<List<Result>>): Boolean = |
| 107 | (results in possibleResultsSet) || possibleResultsSet.any { matches(results, it) } |
| 108 | |
| 109 | private fun matches(results: List<List<Result>>, possible: List<List<Result>>): Boolean = |
| 110 | results.toOpMap() == possible.toOpMap() |
| 111 | |
| 112 | private fun List<List<Result>>.toOpMap(): Map<String, List<Any?>> { |
| 113 | val filtered = flatMap { it }.flatMap { it.resultValue }.filter { it.value != CS_STR } |
| 114 | return filtered.groupBy({ it.name }, { it.value }) |
| 115 | } |
| 116 | |
| 117 | private fun generateAllLinearizableExecutions(actorsPerThread: List<List<Actor>>): List<List<Actor>> { |
| 118 | val executions = ArrayList<List<Actor>>() |
| 119 | generateLinearizableExecutions0( |
| 120 | executions, actorsPerThread, ArrayList<Actor>(), IntArray(actorsPerThread.size), |
| 121 | actorsPerThread.sumBy { it.size }) |
| 122 | return executions |
| 123 | } |
| 124 | |
| 125 | @Suppress("UNCHECKED_CAST") |
| 126 | private fun generateLinearizableExecutions0(executions: MutableList<List<Actor>>, actorsPerThread: List<List<Actor>>, |
| 127 | currentExecution: ArrayList<Actor>, indexes: IntArray, length: Int) { |
| 128 | if (currentExecution.size == length) { |
| 129 | executions.add(currentExecution.clone() as List<Actor>) |
| 130 | return |
| 131 | } |
| 132 | for (i in indexes.indices) { |
| 133 | val actors = actorsPerThread[i] |
| 134 | if (indexes[i] == actors.size) |
| 135 | continue |
| 136 | currentExecution.add(actors[indexes[i]]) |
| 137 | indexes[i]++ |
| 138 | generateLinearizableExecutions0(executions, actorsPerThread, currentExecution, indexes, length) |
| 139 | indexes[i]-- |
| 140 | currentExecution.removeAt(currentExecution.size - 1) |
| 141 | } |
| 142 | } |
| 143 | } |
| 144 | |
| 145 | private val VALUE = Result::class.java.getDeclaredField("value").apply { isAccessible = true } |
| 146 | |
| 147 | @Suppress("UNCHECKED_CAST") |
| 148 | private val Result.resultValue: List<OpResult> |
| 149 | get() = VALUE.get(this) as List<OpResult> |