1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
theory Snapshot
imports Protocol
begin
definition private_frames :: "nat \<Rightarrow> nat \<Rightarrow> pager \<Rightarrow> bool" where
"private_frames pages slots s \<longleftrightarrow> pages \<le> frontier s \<and>
(\<forall>k<slots. writable s k \<longrightarrow> pages \<le> ptable s k)"
lemma initial_private: "private_frames pages slots (initial pages contents)"
by (simp add: private_frames_def)
lemma prepare_private:
"private_frames pages slots s \<Longrightarrow> private_frames pages slots (prepare s k)"
by (auto simp: private_frames_def prepare_def split: if_splits)
lemma prepared_frame_private:
"private_frames pages slots s \<Longrightarrow> k < slots \<Longrightarrow>
pages \<le> ptable (prepare s k) k"
by (auto simp: private_frames_def prepare_def)
lemma store_private:
"private_frames pages slots s \<Longrightarrow> private_frames pages slots (store s k offset byte)"
using prepare_private[of pages slots s k]
by (simp add: private_frames_def)
lemma prepare_original:
"private_frames pages slots s \<Longrightarrow> f < pages \<Longrightarrow>
physical (prepare s k) f = physical s f"
by (auto simp: private_frames_def prepare_def detach_def)
theorem store_original:
assumes owned: "private_frames pages slots s" and valid: "k < slots" and original: "f < pages"
shows "physical (store s k offset byte) f = physical s f"
proof -
have distinct: "f \<noteq> ptable (prepare s k) k"
using prepared_frame_private[OF owned valid] original by arith
have preserved: "physical (prepare s k) f = physical s f"
using prepare_original[OF owned original] .
show ?thesis
using distinct preserved by (simp add: store_def Let_def)
qed
lemma advance_private:
"private_frames pages slots s \<Longrightarrow> private_frames pages slots (advance s a)"
by (cases a; simp add: store_private)
lemma advance_original:
"private_frames pages slots s \<Longrightarrow> valid slots bytes a \<Longrightarrow> f < pages \<Longrightarrow>
physical (advance s a) f = physical s f"
by (cases a; auto intro: store_original)
theorem execute_original:
"private_frames pages slots s \<Longrightarrow> list_all (valid slots bytes) actions \<Longrightarrow>
f < pages \<Longrightarrow> physical (execute s actions) f = physical s f"
proof (induction actions arbitrary: s)
case Nil
then show ?case by simp
next
case (Cons a actions)
have state: "private_frames pages slots (advance s a)"
using Cons.prems by (simp add: advance_private)
have tail: "physical (execute (advance s a) actions) f = physical (advance s a) f"
using Cons.IH[OF state] Cons.prems by simp
show ?case
using tail advance_original Cons.prems by auto
qed
corollary original_preserved:
"list_all (valid slots bytes) actions \<Longrightarrow> f < pages \<Longrightarrow>
physical (execute (initial pages contents) actions) f = contents f"
using execute_original[OF initial_private] by simp
definition promote :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> pager \<Rightarrow> pager" where
"promote pages slots source s =
s\<lparr>ptable := (\<lambda>k. if slots \<le> k \<and> k < slots + pages
then ptable s (source + (k - slots)) else ptable s k),
writable := (\<lambda>k. writable s k \<and> \<not> (source \<le> k \<and> k < source + pages)
\<and> \<not> (slots \<le> k \<and> k < slots + pages))\<rparr>"
lemma promotion_live_view:
"k < slots \<Longrightarrow> view (promote pages slots source s) k = view s k"
by (simp add: promote_def view_def)
lemma promotion_baseline_view:
"p < pages \<Longrightarrow>
view (promote pages slots source s) (slots + p) = view s (source + p)"
by (simp add: promote_def view_def)
lemma promotion_baseline_readonly:
"p < pages \<Longrightarrow> \<not> writable (promote pages slots source s) (slots + p)"
by (simp add: promote_def)
lemma promotion_source_readonly:
"p < pages \<Longrightarrow> \<not> writable (promote pages slots source s) (source + p)"
by (simp add: promote_def)
lemma promotion_bounded:
assumes bounds: "bounded (slots + pages) s" and source: "source + pages \<le> slots"
shows "bounded (slots + pages) (promote pages slots source s)"
proof (unfold bounded_def, intro allI impI)
fix k
assume live: "k < slots + pages"
show "ptable (promote pages slots source s) k < frontier (promote pages slots source s)"
proof (cases "slots \<le> k")
case True
have selected: "source + (k - slots) < slots + pages"
using source live True by arith
show ?thesis
using bounded_frame[OF bounds selected] live True by (simp add: promote_def)
next
case False
show ?thesis
using bounded_frame[OF bounds live] False by (simp add: promote_def)
qed
qed
lemma promotion_exclusive:
assumes owned: "exclusive (slots + pages) s" and source: "source + pages \<le> slots"
shows "exclusive (slots + pages) (promote pages slots source s)"
proof (unfold exclusive_def, intro allI impI)
fix k j
assume live: "k < slots + pages" "j < slots + pages"
and access: "writable (promote pages slots source s) k"
and sharing: "ptable (promote pages slots source s) j = ptable (promote pages slots source s) k"
have writable: "writable s k" and outside: "\<not> (source \<le> k \<and> k < source + pages)"
and old: "ptable (promote pages slots source s) k = ptable s k"
using access by (auto simp: promote_def)
show "j = k"
proof (cases "slots \<le> j")
case True
have selected: "source + (j - slots) < slots + pages"
and inside: "source \<le> source + (j - slots) \<and> source + (j - slots) < source + pages"
using source live True by arith+
have frame: "ptable s (source + (j - slots)) = ptable s k"
using sharing old live True by (simp add: promote_def)
have "source + (j - slots) = k"
using writable_unique[OF owned live(1) selected writable frame] .
then show ?thesis using inside outside by simp
next
case False
have "ptable s j = ptable s k"
using sharing old False by (simp add: promote_def)
then show ?thesis
using writable_unique[OF owned live writable] by simp
qed
qed
theorem promotion_invariant:
"invariant (slots + pages) s \<Longrightarrow> source + pages \<le> slots \<Longrightarrow>
invariant (slots + pages) (promote pages slots source s)"
by (simp add: invariant_def promotion_bounded promotion_exclusive)
theorem promotion_preserves_unselected:
assumes "k < slots" "k < source \<or> source + pages \<le> k"
shows "view (promote pages slots source s) k = view s k \<and>
writable (promote pages slots source s) k = writable s k"
using assms by (auto simp: promote_def view_def)
theorem promotion_store_preserves_unselected:
assumes inv: "invariant (slots + pages) s" and source: "source + pages \<le> slots"
and page: "p < pages" and live: "k < slots"
and unselected: "k < source \<or> source + pages \<le> k"
shows "view (store (promote pages slots source s) (source + p) offset byte) k = view s k"
proof -
have selected: "source + p < slots + pages" and other: "k \<noteq> source + p"
using source page live unselected by arith+
show ?thesis
using write_other[OF promotion_invariant[OF inv source] selected _ other] live
by (simp add: promotion_live_view)
qed
theorem promotion_store_preserves_baseline:
assumes inv: "invariant (slots + pages) s" and source: "source + pages \<le> slots"
and pages: "p < pages" "q < pages"
shows "view (store (promote pages slots source s) (source + p) offset byte) (slots + q) =
view s (source + q)"
proof -
have selected: "source + p < slots + pages" and baseline: "slots + q < slots + pages"
and other: "slots + q \<noteq> source + p"
using source pages by arith+
show ?thesis
using write_other[OF promotion_invariant[OF inv source] selected baseline other]
by (simp add: promotion_baseline_view pages)
qed
end