Toy Deadlock Finder

Usage

Model

$ edit ./main.pl

You must write at least 3 predicates on the target specific part:

Predicate	Description	Example
init_locations(Ls).	Define an initial locations.	init_locations(['P0', 'Q0']).
init_vars(Vs).	Define an initial shared variables.	init_vars([0, 0]).
transit(T, L0, L1, Vs0, Vs1).	Define a transition. The transition can occure if the transition is true. It means, you can write a guard as Vs0. T Label for the transition. L0 Previous location. L1 Next location. Vs0 Preious values of shared variables. Vs1 Next values of shared variables.	transit('Foo', 'P0', 'P1', [0, M2], [1, M2]).

This is an example of a target specific part:

...

% ---- Target specific ----
init_locations(['P0', 'Q0']).
init_vars([0, 0]).

transit('Foo', 'P0', 'P1', [0, M2], [1, M2]).
transit('Bar', 'P1', 'P2', [M1, 0], [M1, 1]).

Visualize

$ ./viz-composition
strict digraph {
  P3_Q0_0_1 -> P0_Q0_0_0 [label=Foo]
  P2_Q0_1_1 -> P3_Q0_0_1 [label=Bar]
}

You can view state diagram using Graphviz facilities such as dreampuf/GraphvizOnline.

Requirements

• SWI-Prolog 8.0.2

Acknowledges

• Implement Deadlock Finder To Learn Multi-Thread Programming