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 CSPProver. 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)?
 datatype Event = Eat0  Back0  End0  RD0 int  WR0
int

 Eat1  Back1  End1  RD1 int  WR1 int
  NUM int
 syntax

"_CH0" :: "Event set" ("CH0")

"_CH1" :: "Event set" ("CH1")

"_OBS" :: "Event set" ("OBS")
 translations

"CH0" == "(range RD0) Un (range WR0)"

"CH1" == "(range RD1) Un (range WR1)"
 "OBS" == "{Eat0, Back0, End0, Eat1, Back1, End1}"
 defs
FPmode_def [simp]: "FPmode == CMSmode"
 datatype
ImpName = VAR int  TH0  EAT0 int  TH1  EAT1 int
 consts

Impfun :: "ImpName => (ImpName, Event) proc"
 primrec

"Impfun (TH0) = RD0 ? n > IF (EVEN n)

THEN Eat0 > $(EAT0 n)

ELSE Back0 > $(TH0)"

"Impfun (TH1) = RD1 ? n > IF (ODD n)

THEN Eat1 > $(EAT1 n)

ELSE Back1 > $(TH1)"

"Impfun (EAT0 n) = End0 > WR0 ! (n div 2) > $(TH0)"

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

"Impfun (VAR n) = WR0 ? n > $(VAR n)

[+] WR1 ? n > $(VAR n)

[+] RD0 ! n > $(VAR n)

[+] RD1 ! n > $(VAR n)"
 defs
(overloaded)

Set_Impfun_def [simp]: "PNfun == Impfun"
 consts

Imp :: "int => (ImpName, Event) proc"
 defs
 Imp_def: "Imp == (%n. ($TH0 [CH0] $(VAR n) [CH1] $TH1)  (CH0 Un CH1))"
Fig.2. The dining mathematicians:
CSPProver 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 CSPProver: 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).
 datatype SpcName = TH0_TH1  EAT0_TH1  TH0_EAT1
 consts

Spcfun :: "SpcName => (SpcName, Event) proc"
 primrec

"Spcfun

(TH0_TH1) = ! x:OBS > IF (x = Eat0) THEN ($EAT0_TH1)

ELSE IF (x = Eat1) THEN ($TH0_EAT1)

ELSE ($TH0_TH1)"

"Spcfun

(EAT0_TH1) = ! x:(OBS  {Eat1}) > IF (x = End0)

THEN ($TH0_TH1)

ELSE ($EAT0_TH1)"

"Spcfun

(TH0_EAT1) = ! x:(OBS  {Eat0}) > IF (x = End1)

THEN ($TH0_TH1)

ELSE ($TH0_EAT1)"
 defs
(overloaded)

Set_Spcfun_def [simp]: "PNfun == Spcfun"
 consts

Spc :: "(SpcName,Event) proc"
 defs
 Spc_def: "Spc == $TH0_TH1"
Fig.3. The dining mathematicians:
CSPProver description of the specification
With CSPProver we can show that (Imp n) is a stablefailures 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 deadlockfreedom 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.