Deadlock detector first implementation.

ddsv.kt

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)