10 |
10 |
11 type_synonym memChType = "(memOp, Vals) channel" |
11 type_synonym memChType = "(memOp, Vals) channel" |
12 type_synonym memType = "(Locs \<Rightarrow> Vals) stfun" (* intention: MemLocs \<Rightarrow> MemVals *) |
12 type_synonym memType = "(Locs \<Rightarrow> Vals) stfun" (* intention: MemLocs \<Rightarrow> MemVals *) |
13 type_synonym resType = "(PrIds \<Rightarrow> Vals) stfun" |
13 type_synonym resType = "(PrIds \<Rightarrow> Vals) stfun" |
14 |
14 |
15 consts |
15 |
16 (* state predicates *) |
16 (* state predicates *) |
17 MInit :: "memType \<Rightarrow> Locs \<Rightarrow> stpred" |
17 |
18 PInit :: "resType \<Rightarrow> PrIds \<Rightarrow> stpred" |
18 definition MInit :: "memType \<Rightarrow> Locs \<Rightarrow> stpred" |
19 (* auxiliary predicates: is there a pending read/write request for |
19 where "MInit mm l == PRED mm!l = #InitVal" |
20 some process id and location/value? *) |
20 |
21 RdRequest :: "memChType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> stpred" |
21 definition PInit :: "resType \<Rightarrow> PrIds \<Rightarrow> stpred" |
22 WrRequest :: "memChType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> Vals \<Rightarrow> stpred" |
22 where "PInit rs p == PRED rs!p = #NotAResult" |
23 |
23 |
24 (* actions *) |
24 |
25 GoodRead :: "memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> action" |
25 (* auxiliary predicates: is there a pending read/write request for |
26 BadRead :: "memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> action" |
26 some process id and location/value? *) |
27 ReadInner :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> action" |
27 |
28 Read :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> action" |
28 definition RdRequest :: "memChType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> stpred" |
29 GoodWrite :: "memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> Vals \<Rightarrow> action" |
29 where "RdRequest ch p l == PRED Calling ch p \<and> (arg<ch!p> = #(read l))" |
30 BadWrite :: "memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> Vals \<Rightarrow> action" |
30 |
31 WriteInner :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> Vals \<Rightarrow> action" |
31 definition WrRequest :: "memChType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> Vals \<Rightarrow> stpred" |
32 Write :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> action" |
32 where "WrRequest ch p l v == PRED Calling ch p \<and> (arg<ch!p> = #(write l v))" |
33 MemReturn :: "memChType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> action" |
33 |
34 MemFail :: "memChType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> action" |
34 |
35 RNext :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> action" |
35 (* actions *) |
36 UNext :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> action" |
36 |
37 |
37 (* a read that doesn't raise BadArg *) |
38 (* temporal formulas *) |
38 definition GoodRead :: "memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> action" |
39 RPSpec :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> temporal" |
39 where "GoodRead mm rs p l == ACT #l \<in> #MemLoc \<and> ((rs!p)$ = $(mm!l))" |
40 UPSpec :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> temporal" |
40 |
41 MSpec :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> Locs \<Rightarrow> temporal" |
41 (* a read that raises BadArg *) |
42 IRSpec :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> temporal" |
42 definition BadRead :: "memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> action" |
43 IUSpec :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> temporal" |
43 where "BadRead mm rs p l == ACT #l \<notin> #MemLoc \<and> ((rs!p)$ = #BadArg)" |
44 |
44 |
45 RSpec :: "memChType \<Rightarrow> resType \<Rightarrow> temporal" |
45 (* the read action with l visible *) |
46 USpec :: "memChType \<Rightarrow> temporal" |
46 definition ReadInner :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> action" |
47 |
47 where "ReadInner ch mm rs p l == ACT |
48 (* memory invariant: in the paper, the invariant is hidden in the definition of |
48 $(RdRequest ch p l) |
49 the predicate S used in the implementation proof, but it is easier to verify |
49 \<and> (GoodRead mm rs p l \<or> BadRead mm rs p l) |
50 at this level. *) |
50 \<and> unchanged (rtrner ch ! p)" |
51 MemInv :: "memType \<Rightarrow> Locs \<Rightarrow> stpred" |
51 |
52 |
52 (* the read action with l quantified *) |
53 defs |
53 definition Read :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> action" |
54 MInit_def: "MInit mm l == PRED mm!l = #InitVal" |
54 where "Read ch mm rs p == ACT (\<exists>l. ReadInner ch mm rs p l)" |
55 PInit_def: "PInit rs p == PRED rs!p = #NotAResult" |
55 |
56 |
56 (* similar definitions for the write action *) |
57 RdRequest_def: "RdRequest ch p l == PRED |
57 definition GoodWrite :: "memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> Vals \<Rightarrow> action" |
58 Calling ch p \<and> (arg<ch!p> = #(read l))" |
58 where "GoodWrite mm rs p l v == |
59 WrRequest_def: "WrRequest ch p l v == PRED |
59 ACT #l \<in> #MemLoc \<and> #v \<in> #MemVal |
60 Calling ch p \<and> (arg<ch!p> = #(write l v))" |
60 \<and> ((mm!l)$ = #v) \<and> ((rs!p)$ = #OK)" |
61 (* a read that doesn't raise BadArg *) |
61 |
62 GoodRead_def: "GoodRead mm rs p l == ACT |
62 definition BadWrite :: "memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> Vals \<Rightarrow> action" |
63 #l \<in> #MemLoc \<and> ((rs!p)$ = $(mm!l))" |
63 where "BadWrite mm rs p l v == ACT |
64 (* a read that raises BadArg *) |
64 \<not> (#l \<in> #MemLoc \<and> #v \<in> #MemVal) |
65 BadRead_def: "BadRead mm rs p l == ACT |
65 \<and> ((rs!p)$ = #BadArg) \<and> unchanged (mm!l)" |
66 #l \<notin> #MemLoc \<and> ((rs!p)$ = #BadArg)" |
66 |
67 (* the read action with l visible *) |
67 definition WriteInner :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> Vals \<Rightarrow> action" |
68 ReadInner_def: "ReadInner ch mm rs p l == ACT |
68 where "WriteInner ch mm rs p l v == ACT |
69 $(RdRequest ch p l) |
69 $(WrRequest ch p l v) |
70 \<and> (GoodRead mm rs p l \<or> BadRead mm rs p l) |
70 \<and> (GoodWrite mm rs p l v \<or> BadWrite mm rs p l v) |
71 \<and> unchanged (rtrner ch ! p)" |
71 \<and> unchanged (rtrner ch ! p)" |
72 (* the read action with l quantified *) |
72 |
73 Read_def: "Read ch mm rs p == ACT (\<exists>l. ReadInner ch mm rs p l)" |
73 definition Write :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> action" |
74 |
74 where "Write ch mm rs p l == ACT (\<exists>v. WriteInner ch mm rs p l v)" |
75 (* similar definitions for the write action *) |
75 |
76 GoodWrite_def: "GoodWrite mm rs p l v == ACT |
76 |
77 #l \<in> #MemLoc \<and> #v \<in> #MemVal |
77 (* the return action *) |
78 \<and> ((mm!l)$ = #v) \<and> ((rs!p)$ = #OK)" |
78 definition MemReturn :: "memChType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> action" |
79 BadWrite_def: "BadWrite mm rs p l v == ACT |
79 where "MemReturn ch rs p == ACT |
80 \<not> (#l \<in> #MemLoc \<and> #v \<in> #MemVal) |
80 ( ($(rs!p) \<noteq> #NotAResult) |
81 \<and> ((rs!p)$ = #BadArg) \<and> unchanged (mm!l)" |
81 \<and> ((rs!p)$ = #NotAResult) |
82 WriteInner_def: "WriteInner ch mm rs p l v == ACT |
82 \<and> Return ch p (rs!p))" |
83 $(WrRequest ch p l v) |
83 |
84 \<and> (GoodWrite mm rs p l v \<or> BadWrite mm rs p l v) |
84 (* the failure action of the unreliable memory *) |
85 \<and> unchanged (rtrner ch ! p)" |
85 definition MemFail :: "memChType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> action" |
86 Write_def: "Write ch mm rs p l == ACT (\<exists>v. WriteInner ch mm rs p l v)" |
86 where "MemFail ch rs p == ACT |
87 |
87 $(Calling ch p) |
88 (* the return action *) |
88 \<and> ((rs!p)$ = #MemFailure) |
89 MemReturn_def: "MemReturn ch rs p == ACT |
89 \<and> unchanged (rtrner ch ! p)" |
90 ( ($(rs!p) \<noteq> #NotAResult) |
90 |
91 \<and> ((rs!p)$ = #NotAResult) |
91 (* next-state relations for reliable / unreliable memory *) |
92 \<and> Return ch p (rs!p))" |
92 definition RNext :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> action" |
93 |
93 where "RNext ch mm rs p == ACT |
94 (* the failure action of the unreliable memory *) |
94 ( Read ch mm rs p |
95 MemFail_def: "MemFail ch rs p == ACT |
95 \<or> (\<exists>l. Write ch mm rs p l) |
96 $(Calling ch p) |
96 \<or> MemReturn ch rs p)" |
97 \<and> ((rs!p)$ = #MemFailure) |
97 |
98 \<and> unchanged (rtrner ch ! p)" |
98 definition UNext :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> action" |
99 (* next-state relations for reliable / unreliable memory *) |
99 where "UNext ch mm rs p == ACT (RNext ch mm rs p \<or> MemFail ch rs p)" |
100 RNext_def: "RNext ch mm rs p == ACT |
100 |
101 ( Read ch mm rs p |
101 |
102 \<or> (\<exists>l. Write ch mm rs p l) |
102 (* temporal formulas *) |
103 \<or> MemReturn ch rs p)" |
103 |
104 UNext_def: "UNext ch mm rs p == ACT |
104 definition RPSpec :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> temporal" |
105 (RNext ch mm rs p \<or> MemFail ch rs p)" |
105 where "RPSpec ch mm rs p == TEMP |
106 |
106 Init(PInit rs p) |
107 RPSpec_def: "RPSpec ch mm rs p == TEMP |
107 \<and> \<box>[ RNext ch mm rs p ]_(rtrner ch ! p, rs!p) |
108 Init(PInit rs p) |
108 \<and> WF(RNext ch mm rs p)_(rtrner ch ! p, rs!p) |
109 \<and> \<box>[ RNext ch mm rs p ]_(rtrner ch ! p, rs!p) |
109 \<and> WF(MemReturn ch rs p)_(rtrner ch ! p, rs!p)" |
110 \<and> WF(RNext ch mm rs p)_(rtrner ch ! p, rs!p) |
110 |
111 \<and> WF(MemReturn ch rs p)_(rtrner ch ! p, rs!p)" |
111 definition UPSpec :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> temporal" |
112 UPSpec_def: "UPSpec ch mm rs p == TEMP |
112 where "UPSpec ch mm rs p == TEMP |
113 Init(PInit rs p) |
113 Init(PInit rs p) |
114 \<and> \<box>[ UNext ch mm rs p ]_(rtrner ch ! p, rs!p) |
114 \<and> \<box>[ UNext ch mm rs p ]_(rtrner ch ! p, rs!p) |
115 \<and> WF(RNext ch mm rs p)_(rtrner ch ! p, rs!p) |
115 \<and> WF(RNext ch mm rs p)_(rtrner ch ! p, rs!p) |
116 \<and> WF(MemReturn ch rs p)_(rtrner ch ! p, rs!p)" |
116 \<and> WF(MemReturn ch rs p)_(rtrner ch ! p, rs!p)" |
117 MSpec_def: "MSpec ch mm rs l == TEMP |
117 |
118 Init(MInit mm l) |
118 definition MSpec :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> Locs \<Rightarrow> temporal" |
119 \<and> \<box>[ \<exists>p. Write ch mm rs p l ]_(mm!l)" |
119 where "MSpec ch mm rs l == TEMP |
120 IRSpec_def: "IRSpec ch mm rs == TEMP |
120 Init(MInit mm l) |
121 (\<forall>p. RPSpec ch mm rs p) |
121 \<and> \<box>[ \<exists>p. Write ch mm rs p l ]_(mm!l)" |
122 \<and> (\<forall>l. #l \<in> #MemLoc \<longrightarrow> MSpec ch mm rs l)" |
122 |
123 IUSpec_def: "IUSpec ch mm rs == TEMP |
123 definition IRSpec :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> temporal" |
124 (\<forall>p. UPSpec ch mm rs p) |
124 where "IRSpec ch mm rs == TEMP |
125 \<and> (\<forall>l. #l \<in> #MemLoc \<longrightarrow> MSpec ch mm rs l)" |
125 (\<forall>p. RPSpec ch mm rs p) |
126 |
126 \<and> (\<forall>l. #l \<in> #MemLoc \<longrightarrow> MSpec ch mm rs l)" |
127 RSpec_def: "RSpec ch rs == TEMP (\<exists>\<exists>mm. IRSpec ch mm rs)" |
127 |
128 USpec_def: "USpec ch == TEMP (\<exists>\<exists>mm rs. IUSpec ch mm rs)" |
128 definition IUSpec :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> temporal" |
129 |
129 where "IUSpec ch mm rs == TEMP |
130 MemInv_def: "MemInv mm l == PRED #l \<in> #MemLoc \<longrightarrow> mm!l \<in> #MemVal" |
130 (\<forall>p. UPSpec ch mm rs p) |
|
131 \<and> (\<forall>l. #l \<in> #MemLoc \<longrightarrow> MSpec ch mm rs l)" |
|
132 |
|
133 definition RSpec :: "memChType \<Rightarrow> resType \<Rightarrow> temporal" |
|
134 where "RSpec ch rs == TEMP (\<exists>\<exists>mm. IRSpec ch mm rs)" |
|
135 |
|
136 definition USpec :: "memChType \<Rightarrow> temporal" |
|
137 where "USpec ch == TEMP (\<exists>\<exists>mm rs. IUSpec ch mm rs)" |
|
138 |
|
139 (* memory invariant: in the paper, the invariant is hidden in the definition of |
|
140 the predicate S used in the implementation proof, but it is easier to verify |
|
141 at this level. *) |
|
142 definition MemInv :: "memType \<Rightarrow> Locs \<Rightarrow> stpred" |
|
143 where "MemInv mm l == PRED #l \<in> #MemLoc \<longrightarrow> mm!l \<in> #MemVal" |
131 |
144 |
132 lemmas RM_action_defs = |
145 lemmas RM_action_defs = |
133 MInit_def PInit_def RdRequest_def WrRequest_def MemInv_def |
146 MInit_def PInit_def RdRequest_def WrRequest_def MemInv_def |
134 GoodRead_def BadRead_def ReadInner_def Read_def |
147 GoodRead_def BadRead_def ReadInner_def Read_def |
135 GoodWrite_def BadWrite_def WriteInner_def Write_def |
148 GoodWrite_def BadWrite_def WriteInner_def Write_def |