90 lines
3.5 KiB
Plaintext
90 lines
3.5 KiB
Plaintext
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
|