# The dining mathematicians

last updated 2023.08.03
[ Isobe > CSP-Prover > The dining mathematicians ]
In model checking, the dining mathematicians (e.g.  [Clarke2001]) are considered as a benchmark. The main difference to the famous dining philosophers is that mathematicians can count! Here, we use the dining mathematicians as an example involving both, infinite systems of equations (i.e. infinite state systems) as well as unbounded nondeterminism.

The dining mathematicians are a classical mutual exclusion problem: There are two mathematicians living at the same place, whose life is focused on two activities, namely thinking (TH0 and TH1, respectively) and eating (EAT0 and EAT1, respectively), see Fig.1. As they have a strong disliking for each other, they never want to eat at the same time. To ensure this, they agreed to the following protocol. They both have access to a common variable (VAR n) storing integer values. If the stored integer (n) is even, the first mathematician is allowed to start eating. When finished, the first mathematician sets the stored value to (n/2). A similar procedure holds for the second mathematician, where the check is if the value of the stored variable is odd, and the value written back after eating is (3n+1).

Fig.1. the Dining Mathematicians.

The dining mathematicians are a classical mutual exclusion problem: There are two mathematicians living at the same place, whose life is focused on two activities, namely thinking (TH0 and TH1, respectively) and eating (EAT0 and EAT1, respectively), see Fig.1. As they have a strong disliking for each other, they never want to eat at the same time. To ensure this, they agreed to the following protocol. They both have access to a common variable (VAR n) storing integer values. If the stored integer (n) is even, the first mathematician is allowed to start eating. When finished, the first mathematician sets the stored value to (n/2). A similar procedure holds for the second mathematician, where the check is if the value of the stored variable is odd, and the value written back after eating is (3n+1).

Fig.2 shows this implementation described in CSP-Prover. Here, each of the process definitions (EAT0 n), (EAT1 n), and (VAR n) describes infinitely many equations. The question is: does this now precisely described implementation exclude the situation where both mathematicians eat together? Or, on a more formal level: has this implementation a trace where Eat1 appears between consecutive communications Eat0 and End0 (and vice versa)?

1. datatype Event = Eat0 | Back0 | End0 | RD0 int | WR0 int
2.                | Eat1 | Back1 | End1 | RD1 int | WR1 int
3.                | NUM int

4. syntax
5.   "_CH0" :: "Event set" ("CH0")
6.   "_CH1" :: "Event set" ("CH1")
7.   "_OBS" :: "Event set" ("OBS")

8. translations
9.   "CH0" == "(range RD0) Un (range WR0)"
10.   "CH1" == "(range RD1) Un (range WR1)"
11.   "OBS" == "{Eat0, Back0, End0, Eat1, Back1, End1}"

12. defs FPmode_def [simp]: "FPmode == CMSmode"

13. datatype ImpName = VAR int | TH0 | EAT0 int | TH1 | EAT1 int

14. consts
15.   Impfun :: "ImpName => (ImpName, Event) proc"

16. primrec
17.   "Impfun   (TH0) = RD0 ? n -> IF (EVEN n)
18.                                   THEN Eat0  -> \$(EAT0 n)
19.                                   ELSE Back0 -> \$(TH0)"

20.   "Impfun   (TH1) = RD1 ? n -> IF (ODD n)
21.                                   THEN Eat1  -> \$(EAT1 n)
22.                                   ELSE Back1 -> \$(TH1)"

23.   "Impfun (EAT0 n) = End0 -> WR0 ! (n div 2) -> \$(TH0)"

24.   "Impfun (EAT1 n) = End1 -> WR1 ! (3 * n + 1) -> \$(TH1)"

25.   "Impfun (VAR n) = WR0 ? n -> \$(VAR n)
26.                    [+] WR1 ? n -> \$(VAR n)
27.                    [+] RD0 ! n -> \$(VAR n)
28.                    [+] RD1 ! n -> \$(VAR n)"

30.   Set_Impfun_def [simp]: "PNfun == Impfun"

31. consts
32.   Imp :: "int => (ImpName, Event) proc"

33. defs
34.   Imp_def: "Imp == (%n. (\$TH0 |[CH0]| \$(VAR n) |[CH1]| \$TH1) -- (CH0 Un CH1))"

Fig.2. The dining mathematicians: CSP-Prover description of the concrete implementation

The classical argument in analysing this implementation is to provide an abstraction of the dining mathematicians, which clearly has the desired exclusion property. Fig.3 shows such a specification described in CSP-Prover: it consists only of three states, which stand for the situations `both mathematicians think' TH0_TH1 and `one mathematician eats while the other is thinking' (EAT0_TH1 and TH0_EAT1, respectively). The CSP operator ! x:X -> P(x) makes an (internal) choice between the events of X and then proceeds with the process P which can depend on the chosen value of x. Starting in state TH0_TH1 with an observation Eat0, the event Eat1 is excluded from the possible communications till an End0 appears (and vice versa for Eat1, Eat0, and End1).

1. datatype SpcName = TH0_TH1 | EAT0_TH1 | TH0_EAT1

2. consts
3.   Spcfun :: "SpcName => (SpcName, Event) proc"

4. primrec
5.    "Spcfun
6.       (TH0_TH1)  = ! x:OBS -> IF (x = Eat0) THEN (\$EAT0_TH1)
7.                                  ELSE IF (x = Eat1) THEN (\$TH0_EAT1)
8.                                                     ELSE (\$TH0_TH1)"

9.    "Spcfun
10.       (EAT0_TH1) = ! x:(OBS - {Eat1}) -> IF (x = End0)
11.                                             THEN (\$TH0_TH1)
12.                                             ELSE (\$EAT0_TH1)"

13.    "Spcfun
14.       (TH0_EAT1) = ! x:(OBS - {Eat0}) -> IF (x = End1)
15.                                             THEN (\$TH0_TH1)
16.                                             ELSE (\$TH0_EAT1)"

18.   Set_Spcfun_def [simp]: "PNfun == Spcfun"

19. consts
20.   Spc :: "(SpcName,Event) proc"

21. defs
22.   Spc_def: "Spc == \$TH0_TH1"

Fig.3. The dining mathematicians: CSP-Prover description of the specification

With CSP-Prover we can show that (Imp n) is a stable-failures refinement of Spc for any integer n, thus `ALL n. Spc <=F Imp n'. As Spc is a sequential process, this refinement result also establishes deadlock-freedom of (Imp n). The theory files for this proof are given as follows:

DM1_Imp_def.thy  : defines Imp
DM2_para.thy     : expands parallel operators in Imp
DM3_hide.thy     : expands hiding operators in Imp
DM4_Spc_def.thy  : defines Spc
DM5_Spc_Imp.thy  : proves Spc <=F Imp

References

[Clarke2001] E. M. Clarke and H. Schlingloff. Handbook of Automated Reasoning. Elsevier Science, 2001.