README.md

Toy Deadlock Detector

This package aims to provide a DSL to represent processes as finite state machines and their concurrent composition. A detector traverses all possible states of the concurrent system, and reports on deadlocks, namely states in which no process can take the next step. Also, the package provides Graphviz style outputs, so you can intuitively view the state space of your system.

Example: Dining Philosophers Problem

The dining philosophers problem is one of the best-known examples of concurrent programming. In this model, some philosophers are sitting on a round table and forks are served between each philosopher. A pasta bawl is also served at the centre of the table, but philosophers have to hold both of left/right forks to help themselves. Here the philosophers are analogues of processes/threads, and the forks are that of shared resources.

In a naive implementation of this setting, for example, all philosophers act as following:

1. Pick up the fork on the left side
2. Pick up the fork on the right side
3. Eat the pasta
4. Put down the fork on the right side
5. Put down the fork on the left side

When multiple philosophers act like this concurrently, as you noticed, it results in a deadlock. Let's model the situation and detect the deadlocked state by this package.

As the simplest case, assume that only two philosophers sitting on the table. We define two processes P1, P2 to represent the philosophers, and two shared variables f1, f2 for forks. The fork f1 is on P1's left side, and the f2 is on his right side.

package main

import (
	"fmt"
	"os"

	"github.com/y-taka-23/ddsv-go/deadlock"
	"github.com/y-taka-23/ddsv-go/deadlock/rule"
	"github.com/y-taka-23/ddsv-go/deadlock/rule/do"
	"github.com/y-taka-23/ddsv-go/deadlock/rule/vars"
	"github.com/y-taka-23/ddsv-go/deadlock/rule/when"
)

func main() {

	philo := func(me int, left, right vars.Name) deadlock.Process {
		return deadlock.NewProcess().
			EnterAt("0").
			// Pick up the fork on his left side
			Define(rule.At("0").Only(when.Var(left).Is(0)).
				Let("up_l", do.Set(me).ToVar(left)).MoveTo("1")).
			// Pick up the fork on his right side
			Define(rule.At("1").Only(when.Var(right).Is(0)).
				Let("up_r", do.Set(me).ToVar(right)).MoveTo("2")).
			// Put down the fork on his right side
			Define(rule.At("2").Only(when.Var(right).Is(me)).
				Let("down_r", do.Set(0).ToVar(right)).MoveTo("3")).
			// Put down the fork on his left side
			Define(rule.At("3").Only(when.Var(left).Is(me)).
				Let("down_l", do.Set(0).ToVar(left)).MoveTo("0"))
	}

	system := deadlock.NewSystem().
		Declare(vars.Shared{"f1": 0, "f2": 0}).
		Register("P1", philo(1, "f1", "f2")).
		Register("P2", philo(1, "f2", "f1"))

	report, err := deadlock.NewDetector().Detect(system)
	if err != nil {
		fmt.Fprintln(os.Stderr, err)
	}

	_, err = deadlock.NewPrinter(os.Stdout).Print(report)
	if err != nil {
		fmt.Fprintln(os.Stderr, err)
	}

}

The red arrows show you an error trace from the initial state (blue) to a deadlock (red.) In the error firstly P1 gets f1 (P1.up_l) then P2 gets f2 (P2.up_l.) At the deadlock, P1 waits f2 and P2 waits f1 respectively forever.

Then, how can we solve the deadlock problem? One idea is to let philosophers put down his first fork if his second fork is occupied by another philosopher, and try again. Add the following lines in the definition of philo. Run the detector again, and you see the deadlock state disappears.

// Discard the fork in his left side
Define(rule.At("1").Only(when.Var(right).IsNot(0)).
	Let("down_l", do.Set(0).ToVar(left)).MoveTo("0")).

More examples are demonstrated in the examples directory. Check it out!

Acknowledgements

• Learn about multi-thread programming by DIY deadlock detector by @hatsugai