feat(protocol): equate fault resolution and retry with atomic stores

theory Protocol

  imports Execution

begin

definition commit :: "pager \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> pager" where

  "commit s k offset byte =

    s\<lparr>physical := (physical s)(ptable s k := (view s k)(offset := byte))\<rparr>"

definition attempt :: "pager \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> pager option" where

  "attempt s k offset byte = (if writable s k then Some (commit s k offset byte) else None)"

lemma readonly_faults:

  "\<not> writable s k \<Longrightarrow> attempt s k offset byte = None"

  by (simp add: attempt_def)

lemma writable_commits:

  "writable s k \<Longrightarrow> attempt s k offset byte = Some (store s k offset byte)"

  by (simp add: attempt_def commit_def store_def prepare_def)

lemma resolve_preserves_memory:

  "invariant n s \<Longrightarrow> j < n \<Longrightarrow> view (detach s k) j = view s j"

  using detach_view[of n s j k] by (auto simp: invariant_def)

theorem fault_retry:

  "\<not> writable s k \<Longrightarrow>

   attempt (detach s k) k offset byte = Some (store s k offset byte)"

  by (simp add: attempt_def commit_def store_def prepare_def detach_def)

theorem fault_retry_refinement:

  assumes "invariant n s" "represents n s m" "k < n" "\<not> writable s k"

  obtains t where "attempt (detach s k) k offset byte = Some t"

    "invariant n t" "represents n t (reference_write m k offset byte)"

  using assms fault_retry write_invariant simulation by blast

definition dirty :: "nat \<Rightarrow> pager \<Rightarrow> nat set" where

  "dirty n s = {k. k < n \<and> writable s k}"

lemma finite_dirty [simp]: "finite (dirty n s)"

  unfolding dirty_def by (rule finite_subset[of _ "{..<n}"]) auto

lemma dirty_initial [simp]: "dirty n (initial pages contents) = {}"

  by (auto simp: dirty_def)

lemma dirty_member [simp]: "k \<in> dirty n s \<longleftrightarrow> k < n \<and> writable s k"

  by (simp add: dirty_def)

lemma dirty_store:

  "k < n \<Longrightarrow> dirty n (store s k offset byte) = insert k (dirty n s)"

  by (auto simp: dirty_def prepare_def)

definition accounted :: "nat \<Rightarrow> nat \<Rightarrow> pager \<Rightarrow> bool" where

  "accounted pages slots s \<longleftrightarrow> frontier s = pages + card (dirty slots s)"

lemma initial_accounted: "accounted pages slots (initial pages contents)"

  by (simp add: accounted_def)

lemma store_accounted:

  assumes "accounted pages slots s" "k < slots"

  shows "accounted pages slots (store s k offset byte)"

  using assms

  by (auto simp: accounted_def dirty_store prepare_frontier card_insert_if insert_absorb)

lemma advance_accounted:

  "accounted pages slots s \<Longrightarrow> valid slots bytes a \<Longrightarrow>

   accounted pages slots (advance s a)"

  by (cases a; auto intro: store_accounted)

theorem execute_accounted:

  "accounted pages slots s \<Longrightarrow> list_all (valid slots bytes) actions \<Longrightarrow>

   accounted pages slots (execute s actions)"

  by (induction actions arbitrary: s) (auto intro: advance_accounted)

lemma dirty_card_bound: "card (dirty slots s) \<le> slots"

proof -

  have "dirty slots s \<subseteq> {..<slots}" by (auto simp: dirty_def)

  then have "card (dirty slots s) \<le> card {..<slots}"

    by (intro card_mono) auto

  then show ?thesis by simp

qed

theorem allocation_bound:

  assumes "list_all (valid slots bytes) actions"

  shows "frontier (execute (initial pages contents) actions) \<le> pages + slots"

  using execute_accounted[OF initial_accounted assms] dirty_card_bound

  unfolding accounted_def by fastforce

fun written :: "action list \<Rightarrow> nat set" where

  "written [] = {}"

| "written (Read k offset # actions) = written actions"

| "written (Write k offset byte # actions) = insert k (written actions)"

lemma writable_advance:

  "writable (advance s a) k = (writable s k \<or> k \<in> written [a])"

  by (cases a; auto simp: prepare_def)

theorem written_exactly:

  "writable (execute s actions) k = (writable s k \<or> k \<in> written actions)"

proof (induction actions arbitrary: s)

  case Nil

  then show ?case by simp

next

  case (Cons a actions)

  show ?case by (cases a) (auto simp: Cons.IH prepare_def)

qed

theorem copies_exactly:

  assumes "list_all (valid slots bytes) actions"

  shows "frontier (execute (initial pages contents) actions) =

    pages + card ({..<slots} \<inter> written actions)"

proof -

  have "dirty slots (execute (initial pages contents) actions) =

      {..<slots} \<inter> written actions"

    by (auto simp: dirty_def written_exactly)

  then show ?thesis

    using execute_accounted[OF initial_accounted assms] by (simp add: accounted_def)

qed

end

    Model

    Isolation

    Execution

    Protocol