The Kit offers several different algorithms for proving deadlock-freeness of a system. In this chapter we show by means of Dekker's mutex algorithm specified as CFA (see Modelling a system as CFA) how one can apply the different methods for deadlock-checking. The Kit returns a deadlocking execution sequence if there is any.

• Using the deadlock-checker of PEP:

First we use the deadlock-checker from PEP. Type the following line:

check cfa:pep-dl dekker.cfa

The following output should be printed on your screen (the exact amount of time depends on the speed of your system, of course):

Time needed: 0.010000 seconds
Result: YES.

• Using the deadlock-checker of PROD:

Next we try the deadlock-checker of PROD. Type:

check cfa:prod-dl dekker.cfa

The following output should be printed on your screen:

Time needed: 1.830000 seconds
Result: YES.

• Using the deadlock-checker of SMV:

The deadlock-checker of SMV can be invoked by typing:

check cfa:smv-dl dekker.cfa

The following output should be printed on your screen:

Time needed: 0.010000 seconds
Result: YES.

• Using the deadlock-checker of Mcsmodels:

The deadlock-checker of Mcsmodels can be invoked by typing:

check cfa:mcs-dl dekker.cfa

The following output should be printed on your screen:

Time needed: 0.010000 seconds
Result: YES.

• Using the deadlock-checker of CLP:

The deadlock-checker of CLP can be invoked by typing:

check cfa:clp-dl dekker.cfa

The following output should be printed on your screen:

Time needed: 0.010000 seconds
Result: YES.

It works successfully, and now we are sure that the specified system is deadlock-free.

Violating the deadlock-freeness

Now we change the system in such a way that the property of deadlock-freeness is violated. For the modified CFA specification see here. The counterexamples produced by the Kit are deadlocking execution sequences.

• Using the deadlock-checker of PEP:

check cfa:pep-dl dekker_deadlock.cfa

The following output should be printed on your screen:

Time needed: 0.020000 seconds
Result: NO.
Counterexample:
dek2: B1 [ flag2=0 --> flag2=1 ] B2
dek1: A1 [ flag1=0 --> flag1=1 ] A2
dek2: B2 [ turn=1, flag1=1 --> turn=1, flag1=1 ] B5

• Using the deadlock-checker of PROD:

check cfa:prod-dl dekker_deadlock.cfa

The following output should be printed on your screen:

Time needed: 2.090000 seconds
Result: NO.
Counterexample:
dek1: A1 [ flag1=0 --> flag1=1 ] A2
dek1: A2 [ flag2=0 --> flag2=0 ] A3
dek2: B1 [ flag2=0 --> flag2=1 ] B2
dek1: A3 [ turn=1 --> turn=2 ] A4
dek1: A4 [ flag1=1 --> flag1=0 ] A1
dek2: B2 [ flag1=0 --> flag1=0 ] B3
dek1: A1 [ flag1=0 --> flag1=1 ] A2
dek1: A2 [ turn=2, flag2=1 --> turn=2, flag2=1 ] A6
dek2: B3 [ turn=2 --> turn=1 ] B4
dek2: B4 [ flag2=1 --> flag2=0 ] B1
dek2: B1 [ flag2=0 --> flag2=1 ] B2
dek2: B2 [ turn=1, flag1=1 --> turn=1, flag1=1 ] B5
dek1: A6 [ flag1=1 --> flag1=0 ] A7
dek1: A7 [ turn=1 --> turn=1 ] A8
dek1: A8 [ flag1=0 --> flag1=1 ] A2

• Using the deadlock-checker of SMV:

check cfa:smv-dl dekker_deadlock.cfa

The following output should be printed on your screen:

Time needed: 0.020000 seconds
Result: NO.
Counterexample:
dek1: A1 [ flag1=0 --> flag1=1 ] A2
dek2: B1 [ flag2=0 --> flag2=1 ] B2
dek2: B2 [ turn=1, flag1=1 --> turn=1, flag1=1 ] B5

• Using the deadlock-checker of Mcsmodels:

check cfa:mcs-dl dekker_deadlock.cfa

The following output should be printed on your screen:

Time needed: 0.030000 seconds
Result: NO.
Counterexample:
dek2: B1 [ flag2=0 --> flag2=1 ] B2
dek1: A1 [ flag1=0 --> flag1=1 ] A2
dek2: B2 [ turn=1, flag1=1 --> turn=1, flag1=1 ] B5

• Using the deadlock-checker of CLP:

check cfa:clp-dl dekker_deadlock.cfa

The following output should be printed on your screen:

Time needed: 0.010000 seconds
Result: NO.
Counterexample:
dek2: B1 [ flag2=0 --> flag2=1 ] B2
dek1: A1 [ flag1=0 --> flag1=1 ] A2
dek2: B2 [ turn=1, flag1=1 --> turn=1, flag1=1 ] B5