Repository files navigation

This package aims to provide a DSL to represent processes asfinite 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 providesGraphviz style outputs, so you can intuitively view the state space of your system.

Thedining 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 adeadlock. 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 processesP1,P2 to represent the philosophers, and two shared variablesf1,f2 for forks. The forkf1 is onP1's left side, and thef2 is on his right side.

package mainimport ("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")funcmain() {philo:=func(meint,left,right vars.Name) deadlock.Process {returndeadlock.NewProcess().EnterAt("0").// Pick up the fork on his left sideDefine(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 sideDefine(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 sideDefine(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 sideDefine(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)iferr!=nil {fmt.Fprintln(os.Stderr,err)}_,err=deadlock.NewPrinter(os.Stdout).Print(report)iferr!=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 firstlyP1 getsf1 (P1.up_l) thenP2 getsf2 (P2.up_l.) At the deadlock,P1 waitsf2 andP2 waitsf1 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 ofphilo. Run the detector again, and you see the deadlock state disappears.

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

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

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