author | wenzelm |
Wed, 07 Sep 2005 20:22:39 +0200 | |
changeset 17309 | c43ed29bd197 |
parent 11703 | 6e5de8d4290a |
child 21624 | 6f79647cf536 |
permissions | -rw-r--r-- |
3807 | 1 |
(* |
2 |
File: Memory.thy |
|
17309 | 3 |
ID: $Id$ |
3807 | 4 |
Author: Stephan Merz |
5 |
Copyright: 1997 University of Munich |
|
6 |
||
7 |
Theory Name: Memory |
|
8 |
Logic Image: TLA |
|
9 |
||
10 |
RPC-Memory example: Memory specification |
|
11 |
*) |
|
12 |
||
17309 | 13 |
theory Memory |
14 |
imports MemoryParameters ProcedureInterface |
|
15 |
begin |
|
3807 | 16 |
|
17 |
types |
|
6255 | 18 |
memChType = "(memOp, Vals) channel" |
3807 | 19 |
memType = "(Locs => Vals) stfun" (* intention: MemLocs => MemVals *) |
20 |
resType = "(PrIds => Vals) stfun" |
|
21 |
||
22 |
consts |
|
23 |
(* state predicates *) |
|
24 |
MInit :: "memType => Locs => stpred" |
|
25 |
PInit :: "resType => PrIds => stpred" |
|
26 |
(* auxiliary predicates: is there a pending read/write request for |
|
27 |
some process id and location/value? *) |
|
28 |
RdRequest :: "memChType => PrIds => Locs => stpred" |
|
29 |
WrRequest :: "memChType => PrIds => Locs => Vals => stpred" |
|
30 |
||
31 |
(* actions *) |
|
32 |
GoodRead :: "memType => resType => PrIds => Locs => action" |
|
33 |
BadRead :: "memType => resType => PrIds => Locs => action" |
|
34 |
ReadInner :: "memChType => memType => resType => PrIds => Locs => action" |
|
35 |
Read :: "memChType => memType => resType => PrIds => action" |
|
36 |
GoodWrite :: "memType => resType => PrIds => Locs => Vals => action" |
|
37 |
BadWrite :: "memType => resType => PrIds => Locs => Vals => action" |
|
38 |
WriteInner :: "memChType => memType => resType => PrIds => Locs => Vals => action" |
|
39 |
Write :: "memChType => memType => resType => PrIds => Locs => action" |
|
40 |
MemReturn :: "memChType => resType => PrIds => action" |
|
41 |
MemFail :: "memChType => resType => PrIds => action" |
|
42 |
RNext :: "memChType => memType => resType => PrIds => action" |
|
43 |
UNext :: "memChType => memType => resType => PrIds => action" |
|
44 |
||
45 |
(* temporal formulas *) |
|
46 |
RPSpec :: "memChType => memType => resType => PrIds => temporal" |
|
47 |
UPSpec :: "memChType => memType => resType => PrIds => temporal" |
|
48 |
MSpec :: "memChType => memType => resType => Locs => temporal" |
|
49 |
IRSpec :: "memChType => memType => resType => temporal" |
|
50 |
IUSpec :: "memChType => memType => resType => temporal" |
|
51 |
||
52 |
RSpec :: "memChType => resType => temporal" |
|
53 |
USpec :: "memChType => temporal" |
|
54 |
||
55 |
(* memory invariant: in the paper, the invariant is hidden in the definition of |
|
17309 | 56 |
the predicate S used in the implementation proof, but it is easier to verify |
3807 | 57 |
at this level. *) |
58 |
MemInv :: "memType => Locs => stpred" |
|
59 |
||
17309 | 60 |
defs |
61 |
MInit_def: "MInit mm l == PRED mm!l = #InitVal" |
|
62 |
PInit_def: "PInit rs p == PRED rs!p = #NotAResult" |
|
3807 | 63 |
|
17309 | 64 |
RdRequest_def: "RdRequest ch p l == PRED |
6255 | 65 |
Calling ch p & (arg<ch!p> = #(read l))" |
17309 | 66 |
WrRequest_def: "WrRequest ch p l v == PRED |
6255 | 67 |
Calling ch p & (arg<ch!p> = #(write l v))" |
3807 | 68 |
(* a read that doesn't raise BadArg *) |
17309 | 69 |
GoodRead_def: "GoodRead mm rs p l == ACT |
6255 | 70 |
#l : #MemLoc & ((rs!p)$ = $(mm!l))" |
3807 | 71 |
(* a read that raises BadArg *) |
17309 | 72 |
BadRead_def: "BadRead mm rs p l == ACT |
6255 | 73 |
#l ~: #MemLoc & ((rs!p)$ = #BadArg)" |
3807 | 74 |
(* the read action with l visible *) |
17309 | 75 |
ReadInner_def: "ReadInner ch mm rs p l == ACT |
3807 | 76 |
$(RdRequest ch p l) |
6255 | 77 |
& (GoodRead mm rs p l | BadRead mm rs p l) |
78 |
& unchanged (rtrner ch ! p)" |
|
3807 | 79 |
(* the read action with l quantified *) |
17309 | 80 |
Read_def: "Read ch mm rs p == ACT (EX l. ReadInner ch mm rs p l)" |
3807 | 81 |
|
82 |
(* similar definitions for the write action *) |
|
17309 | 83 |
GoodWrite_def: "GoodWrite mm rs p l v == ACT |
6255 | 84 |
#l : #MemLoc & #v : #MemVal |
85 |
& ((mm!l)$ = #v) & ((rs!p)$ = #OK)" |
|
17309 | 86 |
BadWrite_def: "BadWrite mm rs p l v == ACT |
6255 | 87 |
~ (#l : #MemLoc & #v : #MemVal) |
88 |
& ((rs!p)$ = #BadArg) & unchanged (mm!l)" |
|
17309 | 89 |
WriteInner_def: "WriteInner ch mm rs p l v == ACT |
3807 | 90 |
$(WrRequest ch p l v) |
6255 | 91 |
& (GoodWrite mm rs p l v | BadWrite mm rs p l v) |
92 |
& unchanged (rtrner ch ! p)" |
|
17309 | 93 |
Write_def: "Write ch mm rs p l == ACT (EX v. WriteInner ch mm rs p l v)" |
3807 | 94 |
|
95 |
(* the return action *) |
|
17309 | 96 |
MemReturn_def: "MemReturn ch rs p == ACT |
6255 | 97 |
( ($(rs!p) ~= #NotAResult) |
98 |
& ((rs!p)$ = #NotAResult) |
|
99 |
& Return ch p (rs!p))" |
|
100 |
||
3807 | 101 |
(* the failure action of the unreliable memory *) |
17309 | 102 |
MemFail_def: "MemFail ch rs p == ACT |
3807 | 103 |
$(Calling ch p) |
6255 | 104 |
& ((rs!p)$ = #MemFailure) |
105 |
& unchanged (rtrner ch ! p)" |
|
106 |
(* next-state relations for reliable / unreliable memory *) |
|
17309 | 107 |
RNext_def: "RNext ch mm rs p == ACT |
6255 | 108 |
( Read ch mm rs p |
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
6255
diff
changeset
|
109 |
| (EX l. Write ch mm rs p l) |
6255 | 110 |
| MemReturn ch rs p)" |
17309 | 111 |
UNext_def: "UNext ch mm rs p == ACT |
6255 | 112 |
(RNext ch mm rs p | MemFail ch rs p)" |
3807 | 113 |
|
17309 | 114 |
RPSpec_def: "RPSpec ch mm rs p == TEMP |
6255 | 115 |
Init(PInit rs p) |
116 |
& [][ RNext ch mm rs p ]_(rtrner ch ! p, rs!p) |
|
117 |
& WF(RNext ch mm rs p)_(rtrner ch ! p, rs!p) |
|
118 |
& WF(MemReturn ch rs p)_(rtrner ch ! p, rs!p)" |
|
17309 | 119 |
UPSpec_def: "UPSpec ch mm rs p == TEMP |
6255 | 120 |
Init(PInit rs p) |
121 |
& [][ UNext ch mm rs p ]_(rtrner ch ! p, rs!p) |
|
122 |
& WF(RNext ch mm rs p)_(rtrner ch ! p, rs!p) |
|
123 |
& WF(MemReturn ch rs p)_(rtrner ch ! p, rs!p)" |
|
17309 | 124 |
MSpec_def: "MSpec ch mm rs l == TEMP |
6255 | 125 |
Init(MInit mm l) |
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
6255
diff
changeset
|
126 |
& [][ EX p. Write ch mm rs p l ]_(mm!l)" |
17309 | 127 |
IRSpec_def: "IRSpec ch mm rs == TEMP |
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
6255
diff
changeset
|
128 |
(ALL p. RPSpec ch mm rs p) |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
6255
diff
changeset
|
129 |
& (ALL l. #l : #MemLoc --> MSpec ch mm rs l)" |
17309 | 130 |
IUSpec_def: "IUSpec ch mm rs == TEMP |
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
6255
diff
changeset
|
131 |
(ALL p. UPSpec ch mm rs p) |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
6255
diff
changeset
|
132 |
& (ALL l. #l : #MemLoc --> MSpec ch mm rs l)" |
3807 | 133 |
|
17309 | 134 |
RSpec_def: "RSpec ch rs == TEMP (EEX mm. IRSpec ch mm rs)" |
135 |
USpec_def: "USpec ch == TEMP (EEX mm rs. IUSpec ch mm rs)" |
|
3807 | 136 |
|
17309 | 137 |
MemInv_def: "MemInv mm l == PRED #l : #MemLoc --> mm!l : #MemVal" |
138 |
||
139 |
ML {* use_legacy_bindings (the_context ()) *} |
|
140 |
||
3807 | 141 |
end |