|
1 (* Title: HOL/UNITY/Mutex.thy |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1998 University of Cambridge |
|
5 |
|
6 Based on "A Family of 2-Process Mutual Exclusion Algorithms" by J Misra |
|
7 *) |
|
8 |
|
9 Mutex = Update + UNITY + Traces + SubstAx + |
|
10 |
|
11 (*WE NEED A GENERAL TREATMENT OF NUMBERS!!*) |
|
12 syntax |
|
13 "3" :: nat ("3") |
|
14 "4" :: nat ("4") |
|
15 |
|
16 translations |
|
17 "3" == "Suc 2" |
|
18 "4" == "Suc 3" |
|
19 |
|
20 |
|
21 (*program variables*) |
|
22 datatype pvar = PP | MM | NN | UU | VV |
|
23 |
|
24 (*No booleans; instead True=1 and False=0*) |
|
25 types state = pvar => nat |
|
26 |
|
27 constdefs |
|
28 cmd0 :: "[pvar,pvar] => (state*state) set" |
|
29 "cmd0 u m == {(s,s'). s' = s[u|->1][m|->1] & s m = 0}" |
|
30 |
|
31 cmd1u :: "(state*state) set" |
|
32 "cmd1u == {(s,s'). s' = s[PP|-> s VV][MM|->2] & s MM = 1}" |
|
33 |
|
34 cmd1v :: "(state*state) set" |
|
35 "cmd1v == {(s,s'). s' = s[PP|-> 1 - s UU][NN|->2] & s NN = 1}" |
|
36 |
|
37 (*Put pv=0 for u's program and pv=1 for v's program*) |
|
38 cmd2 :: "[nat,pvar] => (state*state) set" |
|
39 "cmd2 pv m == {(s,s'). s' = s[m|->3] & s PP = pv & s m = 2}" |
|
40 |
|
41 cmd3 :: "[pvar,pvar] => (state*state) set" |
|
42 "cmd3 u m == {(s,s'). s' = s[u|->0][m|->4] & s m = 3}" |
|
43 |
|
44 (*Put pv=1 for u's program and pv=0 for v's program*) |
|
45 cmd4 :: "[nat,pvar] => (state*state) set" |
|
46 "cmd4 pv m == {(s,s'). s' = s[PP|->pv][m|->0] & s m = 4}" |
|
47 |
|
48 mutex :: "(state*state) set set" |
|
49 "mutex == {id, |
|
50 cmd0 UU MM, cmd0 VV NN, |
|
51 cmd1u, cmd1v, |
|
52 cmd2 0 MM, cmd2 1 NN, |
|
53 cmd3 UU MM, cmd3 VV NN, |
|
54 cmd4 1 MM, cmd4 0 NN}" |
|
55 |
|
56 MInit :: "state set" |
|
57 "MInit == {s. s PP < 2 & s UU = 0 & s VV = 0 & s MM = 0 & s NN = 0}" |
|
58 |
|
59 boolVars :: "state set" |
|
60 "boolVars == {s. s PP<2 & s UU < 2 & s VV < 2}" |
|
61 |
|
62 (*Put pv=0 for u's program and pv=1 for v's program*) |
|
63 invariant :: "[nat,pvar,pvar] => state set" |
|
64 "invariant pv u m == {s. ((s u=1) = (1 <= s m & s m <= 3)) & |
|
65 (s m = 3 --> s PP = pv)}" |
|
66 |
|
67 bad_invariant :: "[nat,pvar,pvar] => state set" |
|
68 "bad_invariant pv u m == {s. ((s u=1) = (1 <= s m & s m <= 3)) & |
|
69 (3 <= s m & s m <= 4 --> s PP = pv)}" |
|
70 |
|
71 |
|
72 |
|
73 |
|
74 end |