Something went wrong. Try again.
seL4 pager with proven memory isolation and frame reuse
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210theory Reuse imports Snapshotbegin
definition vacant :: "nat \<Rightarrow> pager \<Rightarrow> nat \<Rightarrow> bool" where "vacant slots s f = list_all (\<lambda>k. ptable s k \<noteq> f) [0..<slots]"
lemma vacant_iff [simp]: "vacant slots s f \<longleftrightarrow> (\<forall>k<slots. ptable s k \<noteq> f)" by (auto simp: vacant_def list_all_iff)
definition copy_frame :: "pager \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> pager" where "copy_frame s k f = s\<lparr>ptable := (ptable s)(k := f), physical := (physical s)(f := view s k), writable := (writable s)(k := True), frontier := max (frontier s) (Suc f)\<rparr>"
definition clear_slot :: "nat \<Rightarrow> pager \<Rightarrow> nat \<Rightarrow> pager" where "clear_slot pages s k = s\<lparr>ptable := (ptable s)(k := k mod pages), physical := (physical s)(ptable s k := (\<lambda>_. 0)), writable := (writable s)(k := False)\<rparr>"
definition pooled :: "nat \<Rightarrow> nat \<Rightarrow> pager \<Rightarrow> nat list \<Rightarrow> bool" where "pooled pages slots s available \<longleftrightarrow> invariant slots s \<and> private_frames pages slots s \<and> distinct available \<and> (\<forall>f\<in>set available. pages \<le> f \<and> f < frontier s \<and> vacant slots s f \<and> physical s f = (\<lambda>_. 0))"
definition reserve :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> pager \<Rightarrow> nat list \<Rightarrow> nat \<Rightarrow> (pager \<times> nat list) option" where "reserve pages slots capacity s available k = (let f = (case available of [] \<Rightarrow> frontier s | x # xs \<Rightarrow> x) in if 0 < pages \<and> k < slots \<and> \<not> writable s k \<and> pages \<le> f \<and> f < capacity \<and> vacant slots s f then Some (copy_frame s k f, tl available) else None)"
definition reclaim :: "nat \<Rightarrow> nat \<Rightarrow> pager \<Rightarrow> nat list \<Rightarrow> nat \<Rightarrow> (pager \<times> nat list) option" where "reclaim pages slots s available k = (if 0 < pages \<and> k < slots \<and> writable s k \<and> pages \<le> ptable s k \<and> ptable s k \<notin> set available \<and> list_all (\<lambda>j. j = k \<or> ptable s j \<noteq> ptable s k) [0..<slots] then Some (clear_slot pages s k, ptable s k # available) else None)"
lemma initial_pooled: "0 < pages \<Longrightarrow> pooled pages slots (initial pages contents) []" by (simp add: pooled_def initial_invariant initial_private)
lemma copy_view: "vacant slots s f \<Longrightarrow> j < slots \<Longrightarrow> view (copy_frame s k f) j = view s j" by (auto simp: view_def copy_frame_def)
lemma copy_bounded: "bounded slots s \<Longrightarrow> bounded slots (copy_frame s k f)" by (auto simp: bounded_def copy_frame_def max_def)
lemma copy_exclusive: "exclusive slots s \<Longrightarrow> vacant slots s f \<Longrightarrow> exclusive slots (copy_frame s k f)" by (auto simp: exclusive_def copy_frame_def split: if_splits)
lemma copy_invariant: "invariant slots s \<Longrightarrow> vacant slots s f \<Longrightarrow> invariant slots (copy_frame s k f)" by (simp add: invariant_def copy_bounded copy_exclusive)
lemma copy_private: "private_frames pages slots s \<Longrightarrow> pages \<le> f \<Longrightarrow> private_frames pages slots (copy_frame s k f)" by (auto simp: private_frames_def copy_frame_def max_def)
lemma copy_original: "pages \<le> f \<Longrightarrow> original < pages \<Longrightarrow> physical (copy_frame s k f) original = physical s original" by (auto simp: copy_frame_def)
lemma clear_bounded: "0 < pages \<Longrightarrow> bounded slots s \<Longrightarrow> pages \<le> frontier s \<Longrightarrow> bounded slots (clear_slot pages s k)" by (auto simp: bounded_def clear_slot_def intro: less_le_trans[OF mod_less_divisor])
lemma clear_exclusive: "0 < pages \<Longrightarrow> exclusive slots s \<Longrightarrow> private_frames pages slots s \<Longrightarrow> exclusive slots (clear_slot pages s k)" by (auto simp: exclusive_def private_frames_def clear_slot_def split: if_splits; metis mod_less_divisor not_le)
lemma clear_private: "private_frames pages slots s \<Longrightarrow> private_frames pages slots (clear_slot pages s k)" by (auto simp: private_frames_def clear_slot_def)
lemma clear_invariant: "0 < pages \<Longrightarrow> invariant slots s \<Longrightarrow> private_frames pages slots s \<Longrightarrow> invariant slots (clear_slot pages s k)" by (metis invariant_def private_frames_def clear_bounded clear_exclusive)
lemma clear_vacant: "0 < pages \<Longrightarrow> exclusive slots s \<Longrightarrow> k < slots \<Longrightarrow> writable s k \<Longrightarrow> pages \<le> ptable s k \<Longrightarrow> vacant slots (clear_slot pages s k) (ptable s k)" by (auto simp: exclusive_def clear_slot_def; metis mod_less_divisor not_le)
lemma clear_other_view: "exclusive slots s \<Longrightarrow> k < slots \<Longrightarrow> writable s k \<Longrightarrow> j < slots \<Longrightarrow> j \<noteq> k \<Longrightarrow> view (clear_slot pages s k) j = view s j" by (auto simp: exclusive_def clear_slot_def view_def)
lemma clear_target_view: "0 < pages \<Longrightarrow> pages \<le> ptable s k \<Longrightarrow> view (clear_slot pages s k) k = physical s (k mod pages)" by (auto simp: clear_slot_def view_def; metis mod_less_divisor not_le)
lemma clear_original: "pages \<le> ptable s k \<Longrightarrow> f < pages \<Longrightarrow> physical (clear_slot pages s k) f = physical s f" by (auto simp: clear_slot_def)
theorem reclaim_zero: "reclaim pages slots s available k = Some (t, remaining) \<Longrightarrow> physical t (ptable s k) = (\<lambda>_. 0)" by (auto simp: reclaim_def clear_slot_def split: if_splits)
theorem reclaim_unmapped: assumes pool: "pooled pages slots s available" and step: "reclaim pages slots s available k = Some (t, remaining)" shows "vacant slots t (ptable s k)" using pool step by (auto simp: reclaim_def pooled_def invariant_def split: if_splits; metis clear_vacant vacant_iff)
theorem reclaim_views: assumes "pooled pages slots s available" "reclaim pages slots s available k = Some (t, remaining)" "j < slots" shows "view t j = (if j = k then physical s (k mod pages) else view s j)" using assms clear_other_view clear_target_view by (auto simp: pooled_def reclaim_def invariant_def split: if_splits)
theorem reclaim_pool: assumes pool: "pooled pages slots s available" and step: "reclaim pages slots s available k = Some (t, remaining)" shows "pooled pages slots t remaining"proof - have positive: "0 < pages" and valid: "k < slots" and writable: "writable s k" and private_frame: "pages \<le> ptable s k" and fresh: "ptable s k \<notin> set available" and result: "t = clear_slot pages s k" "remaining = ptable s k # available" using step by (auto simp: reclaim_def split: if_splits) have inv: "invariant slots s" and owned: "private_frames pages slots s" using pool by (auto simp: pooled_def) have new_inv: "invariant slots t" and new_owned: "private_frames pages slots t" using clear_invariant[OF positive inv owned] clear_private[OF owned] result by auto have unused: "vacant slots t (ptable s k)" using reclaim_unmapped[OF pool step] . have clean: "physical t (ptable s k) = (\<lambda>_. 0)" using reclaim_zero[OF step] . show ?thesis using pool fresh result positive valid private_frame inv new_inv new_owned unused clean by (auto simp: pooled_def clear_slot_def bounded_def invariant_def split: if_splits; metis mod_less_divisor not_le)qed
theorem reserve_views: "reserve pages slots capacity s available k = Some (t, remaining) \<Longrightarrow> j < slots \<Longrightarrow> view t j = view s j" by (auto simp: reserve_def Let_def split: list.splits if_splits intro: copy_view)
theorem reserve_pool: assumes pool: "pooled pages slots s available" and step: "reserve pages slots capacity s available k = Some (t, remaining)" shows "pooled pages slots t remaining"proof (cases available) case Nil then have fresh: "vacant slots s (frontier s)" using pool by (auto simp: pooled_def invariant_def bounded_def) have owned: "pages \<le> frontier s" using pool by (auto simp: pooled_def private_frames_def) show ?thesis using step pool fresh owned Nil copy_invariant copy_private by (auto simp: reserve_def Let_def pooled_def split: if_splits)next case (Cons f rest) have fresh: "vacant slots s f" and owned: "pages \<le> f" and distinct: "f \<notin> set rest" using pool Cons by (auto simp: pooled_def) have result: "t = copy_frame s k f" "remaining = rest" using step Cons by (auto simp: reserve_def Let_def split: if_splits) have inv: "invariant slots t" and own: "private_frames pages slots t" using pool result fresh owned copy_invariant copy_private by (auto simp: pooled_def) show ?thesis using pool Cons distinct result inv own by (auto simp: pooled_def copy_frame_def max_def split: if_splits)qed
theorem reserve_original: "reserve pages slots capacity s available k = Some (t, remaining) \<Longrightarrow> f < pages \<Longrightarrow> physical t f = physical s f" by (auto simp: reserve_def Let_def split: list.splits if_splits intro: copy_original)
theorem reclaim_original: "reclaim pages slots s available k = Some (t, remaining) \<Longrightarrow> f < pages \<Longrightarrow> physical t f = physical s f" by (auto simp: reclaim_def split: if_splits intro: clear_original)
theorem pooled_unmapped: "pooled pages slots s available \<Longrightarrow> f \<in> set available \<Longrightarrow> j < slots \<Longrightarrow> ptable s j \<noteq> f" by (auto simp: pooled_def)
theorem pooled_clean: "pooled pages slots s available \<Longrightarrow> f \<in> set available \<Longrightarrow> physical s f offset = 0" by (auto simp: pooled_def)
theorem pooled_store: assumes "pooled pages slots s available" "k < slots" "writable s k" shows "pooled pages slots (store s k offset byte) available" using assms write_invariant[of slots s k offset byte] store_private[of pages slots s k offset byte] by (auto simp: pooled_def store_def prepare_def Let_def)
end