Skip to content

Instantly share code, notes, and snippets.

@ryohji

ryohji/ddsv.kt

Created Oct 19, 2019
Embed
What would you like to do?
Deadlock detector first implementation.
package app
fun main() {
val rules: List<Rule> = listOf(
object : Rule {
override val name = "read"
override fun applicable(shared: Shared, thread: Thread) = thread.ir == Location.P0
override fun convert(shared: Shared, thread: Thread) = shared to Local(Location.P1, shared.x)
},
object : Rule {
override val name = "increment"
override fun applicable(shared: Shared, thread: Thread) = thread.ir == Location.P1
override fun convert(shared: Shared, thread: Thread) = shared to Local(Location.P2, (thread as Local).t + 1)
},
object : Rule {
override val name = "write"
override fun applicable(shared: Shared, thread: Thread) = thread.ir == Location.P2
override fun convert(shared: Shared, thread: Thread) = Shared((thread as Local).t) to Local(Location.EXIT, thread.t)
}
)
val initialState = listOf(Shared(0), Local(Location.P0, 0), Local(Location.P0, 0), Local(Location.P0, 0))
buildGraph(rules, initialState).let { buildDot(initialState, it) }.let { println(it) }
}
fun buildGraph(rules: List<Rule>, initialState: List<Variable>): Map<State, Set<Pair<String, State>>> {
val graph = mutableMapOf<State, Set<Pair<String, State>>>()
val frontier: MutableList<State> = mutableListOf(initialState)
while (frontier.isNotEmpty()) {
val s = frontier.first().also { frontier.removeAt(0) } // pop front
val shared = s.first() as Shared
val threads = s.drop(1).map { it as Thread }
val checked = graph.keys + s
val end = graph[s]?.toMutableSet() ?: mutableSetOf()
threads
.mapIndexed { index, local ->
rules.mapNotNull { rule -> rule.apply(shared, local)?.let { (index to rule.name) to it } }
}
.flatten()
.map {
val (indexAndRule, sharedAndLocal) = it
val (index, rule) = indexAndRule
(listOf(sharedAndLocal.first) + swapAt(index, threads, sharedAndLocal.second))
.also { newState -> end += rule to newState }
}
.filterNot { it in checked }
.let { frontier += it } // breadth first search
graph[s] = end
}
return graph
}
fun buildDot(initial: State, graph: Map<State, Set<Pair<String, State>>>): String {
val states = graph.keys
val nodes = states.mapIndexed { index: Int, vars: State ->
val attr = if (graph.getValue(vars).isEmpty()) "filled" else if (vars == initial) "bold" else "solid"
"$index [label=\"${vars.joinToString("\\n")}\" style=$attr]"
}.joinToString(";\n ")
val edges = graph.entries.flatMap {
val start = states.indexOf(it.key)
it.value.map { arrow ->
val (name, state) = arrow
val end = states.indexOf(state)
"$start -> $end [label=\"$name\"]"
}
}.joinToString(";\n ")
return "digraph {\n $nodes;\n $edges;\n}"
}
enum class Location { P0, P1, P2, EXIT }
interface Variable
typealias State = List<Variable>
data class Shared(var x: Int) : Variable
interface Thread : Variable { val ir: Location }
data class Local(override val ir: Location, val t: Int) : Thread
interface Rule {
val name: String
fun applicable(shared: Shared, thread: Thread): Boolean
fun convert(shared: Shared, thread: Thread): Pair<Shared, Thread>
}
fun Rule.apply(shared: Shared, thread: Thread) = if (applicable(shared, thread)) {
convert(shared, thread)
} else {
null
}
private fun <T> swapAt(n: Int, list: List<T>, item: T): List<T> = list.take(n) + item + list.drop(n + 1)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.