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
theory Isolation
imports Model
begin
lemma write_target:
assumes "bounded n s" "k < n"
shows "view (store s k offset byte) k = (view s k)(offset := byte)"
using prepare_view[OF assms, of k]
by (simp add: view_def store_def Let_def)
lemma write_other:
assumes inv: "invariant n s" and valid: "k < n" "j < n" and different: "j \<noteq> k"
shows "view (store s k offset byte) j = view s j"
proof -
have prepared: "invariant n (prepare s k)"
using inv by (rule prepare_invariant)
have distinct: "ptable (prepare s k) j \<noteq> ptable (prepare s k) k"
using writable_unique[of n "prepare s k" k j] prepared valid different
by (auto simp: invariant_def)
have preserved: "view (prepare s k) j = view s j"
using prepare_view[of n s j k] inv valid by (auto simp: invariant_def)
show ?thesis
using distinct preserved by (simp add: store_def view_def Let_def)
qed
theorem write_refinement:
assumes "invariant n s" "k < n" "j < n"
shows "view (store s k offset byte) j =
(if j = k then (view s k)(offset := byte) else view s j)"
using assms write_target write_other by (auto simp: invariant_def)
corollary read_after_write:
"invariant n s \<Longrightarrow> k < n \<Longrightarrow>
view (store s k offset byte) k offset = byte"
using write_refinement[of n s k k offset byte] by simp
corollary other_offset:
"invariant n s \<Longrightarrow> k < n \<Longrightarrow> address \<noteq> offset \<Longrightarrow>
view (store s k offset byte) k address = view s k address"
using write_refinement[of n s k k offset byte] by simp
definition reference_write :: "memory \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> memory" where
"reference_write m k offset byte = m(k := (m k)(offset := byte))"
definition represents :: "nat \<Rightarrow> pager \<Rightarrow> memory \<Rightarrow> bool" where
"represents n s m \<longleftrightarrow> (\<forall>k<n. view s k = m k)"
lemma represents_initial:
"represents n (initial pages contents) (\<lambda>k. contents (k mod pages))"
by (simp add: represents_def)
theorem simulation:
assumes "invariant n s" "represents n s m" "k < n"
shows "represents n (store s k offset byte) (reference_write m k offset byte)"
using assms write_refinement[of n s k]
by (auto simp: represents_def reference_write_def)
lemma prepared_exclusive:
"invariant n s \<Longrightarrow> k < n \<Longrightarrow> j < n \<Longrightarrow> j \<noteq> k \<Longrightarrow>
ptable (prepare s k) j \<noteq> ptable (prepare s k) k"
using prepare_invariant writable_unique prepare_writable
unfolding invariant_def by blast
lemma writable_no_copy:
"writable s k \<Longrightarrow> frontier (store s k offset byte) = frontier s"
by (simp add: prepare_def)
lemma readonly_one_copy:
"\<not> writable s k \<Longrightarrow> frontier (store s k offset byte) = Suc (frontier s)"
by (simp add: prepare_def)
lemma subsequent_write_no_copy:
"frontier (store (store s k a x) k b y) = frontier (store s k a x)"
by (rule writable_no_copy) simp
lemma write_writable_target [simp]: "writable (store s k offset byte) k"
by simp
lemma write_writable_other:
"j \<noteq> k \<Longrightarrow> writable (store s k offset byte) j = writable s j"
by (simp add: prepare_def)
lemma write_preserves_unallocated:
"f > frontier s \<Longrightarrow> physical (store s k offset byte) f = physical s f"
if "bounded n s" "k < n" for f s k n offset byte
using that bounded_frame[OF that]
by (auto simp: store_def prepare_def detach_def Let_def split: if_splits)
end