Theory Proofs_Basis
theory Proofs_Basis
imports
Model
"HOL-Library.Simps_Case_Conv"
begin
declare subst_all [simp del] [[simproc del: defined_all]]
section‹ Proofs Basis \label{sec:proofs-basis}›
text‹
Extra HOL.
›
lemma Set_bind_insert[simp]:
"Set.bind (insert a A) B = B a ∪ (Set.bind A B)"
by (auto simp: Set.bind_def)
lemma option_bind_invE[elim]:
"⟦ Option.bind f g = None; ⋀a. ⟦ f = Some a; g a = None ⟧ ⟹ Q; f = None ⟹ Q ⟧ ⟹ Q"
"⟦ Option.bind f g = Some x; ⋀a. ⟦ f = Some a; g a = Some x ⟧ ⟹ Q ⟧ ⟹ Q"
by (case_tac [!] f) simp_all
lemmas conj_explode = conj_imp_eq_imp_imp
text‹
Tweak the default simpset:
▪ "not in dom" as a premise negates the goal
▪ we always want to execute suffix
▪ we try to make simplification rules about @{const ‹fun_upd›} more stable
›
declare dom_def[simp]
declare suffix_to_prefix[simp]
declare map_option.compositionality[simp]
declare o_def[simp]
declare Option.Option.option.set_map[simp]
declare bind_image[simp]
declare fun_upd_apply[simp del]
declare fun_upd_same[simp]
declare fun_upd_other[simp]
declare gc_phase.case_cong[cong]
declare mem_store_action.case_cong[cong]
declare process_name.case_cong[cong]
declare hs_phase.case_cong[cong]
declare hs_type.case_cong[cong]
declare if_split_asm[split]
text‹
Collect the component definitions. Inline everything. This is what the proofs work on.
Observe we lean heavily on locales.
›
context gc
begin
lemmas all_com_defs =
handshake_done_def handshake_init_def handshake_noop_def handshake_get_roots_def handshake_get_work_def
mark_object_fn_def
lemmas com_def2 = com_def[simplified all_com_defs append.simps if_True if_False]
intern_com com_def2
end
context mut_m
begin
lemmas all_com_defs =
mut_m.handshake_def mut_m.store_def
mark_object_fn_def
lemmas com_def2 = mut_m.com_def[simplified all_com_defs append.simps if_True if_False]
intern_com com_def2
end
context sys
begin
lemmas all_com_defs =
sys.alloc_def sys.free_def sys.mem_TSO_def sys.handshake_def
lemmas com_def2 = com_def[simplified all_com_defs append.simps if_True if_False]
intern_com com_def2
end
lemmas all_com_interned_defs = gc.com_interned mut_m.com_interned sys.com_interned
named_theorems inv "Location-sensitive invariant definitions"
named_theorems nie "Non-interference elimination rules"
subsection‹ Model-specific functions and predicates ›
text‹
We define a pile of predicates and accessor functions for the
process's local states. One might hope that a more sophisticated
approach would automate all of this (cf \<^citet>‹"DBLP:journals/entcs/SchirmerW09"›).
›
abbreviation prefixed :: "location ⇒ location set" where
"prefixed p ≡ { l . prefix p l }"
abbreviation suffixed :: "location ⇒ location set" where
"suffixed p ≡ { l . suffix p l }"
abbreviation "is_mw_Mark w ≡ ∃r fl. w = mw_Mark r fl"
abbreviation "is_mw_Mutate w ≡ ∃r f r'. w = mw_Mutate r f r'"
abbreviation "is_mw_Mutate_Payload w ≡ ∃r f pl. w = mw_Mutate_Payload r f pl"
abbreviation "is_mw_fA w ≡ ∃fl. w = mw_fA fl"
abbreviation "is_mw_fM w ≡ ∃fl. w = mw_fM fl"
abbreviation "is_mw_Phase w ≡ ∃ph. w = mw_Phase ph"
abbreviation (input) pred_in_W :: "'ref ⇒ 'mut process_name ⇒ ('field, 'mut, 'payload, 'ref) lsts_pred" (infix "in'_W" 50) where
"r in_W p ≡ λs. r ∈ W (s p)"
abbreviation (input) pred_in_ghost_honorary_grey :: "'ref ⇒ 'mut process_name ⇒ ('field, 'mut, 'payload, 'ref) lsts_pred" (infix "in'_ghost'_honorary'_grey" 50) where
"r in_ghost_honorary_grey p ≡ λs. r ∈ ghost_honorary_grey (s p)"
abbreviation "gc_cas_mark s ≡ cas_mark (s gc)"
abbreviation "gc_fM s ≡ fM (s gc)"
abbreviation "gc_field s ≡ field (s gc)"
abbreviation "gc_field_set s ≡ field_set (s gc)"
abbreviation "gc_mark s ≡ mark (s gc)"
abbreviation "gc_mut s ≡ mut (s gc)"
abbreviation "gc_muts s ≡ muts (s gc)"
abbreviation "gc_phase s ≡ phase (s gc)"
abbreviation "gc_tmp_ref s ≡ tmp_ref (s gc)"
abbreviation "gc_ghost_honorary_grey s ≡ ghost_honorary_grey (s gc)"
abbreviation "gc_ref s ≡ ref (s gc)"
abbreviation "gc_refs s ≡ refs (s gc)"
abbreviation "gc_the_ref ≡ the ∘ gc_ref"
abbreviation "gc_W s ≡ W (s gc)"
abbreviation at_gc :: "location ⇒ ('field, 'mut, 'payload, 'ref) lsts_pred ⇒ ('field, 'mut, 'payload, 'ref) gc_pred" where
"at_gc l P ≡ at gc l ❙⟶ LSTP P"
abbreviation atS_gc :: "location set ⇒ ('field, 'mut, 'payload, 'ref) lsts_pred ⇒ ('field, 'mut, 'payload, 'ref) gc_pred" where
"atS_gc ls P ≡ atS gc ls ❙⟶ LSTP P"
context mut_m
begin
abbreviation at_mut :: "location ⇒ ('field, 'mut, 'payload, 'ref) lsts_pred ⇒ ('field, 'mut, 'payload, 'ref) gc_pred" where
"at_mut l P ≡ at (mutator m) l ❙⟶ LSTP P"
abbreviation atS_mut :: "location set ⇒ ('field, 'mut, 'payload, 'ref) lsts_pred ⇒ ('field, 'mut, 'payload, 'ref) gc_pred" where
"atS_mut ls P ≡ atS (mutator m) ls ❙⟶ LSTP P"
abbreviation "mut_cas_mark s ≡ cas_mark (s (mutator m))"
abbreviation "mut_field s ≡ field (s (mutator m))"
abbreviation "mut_fM s ≡ fM (s (mutator m))"
abbreviation "mut_ghost_honorary_grey s ≡ ghost_honorary_grey (s (mutator m))"
abbreviation "mut_ghost_hs_phase s ≡ ghost_hs_phase (s (mutator m))"
abbreviation "mut_ghost_honorary_root s ≡ ghost_honorary_root (s (mutator m))"
abbreviation "mut_hs_pending s ≡ mutator_hs_pending (s (mutator m))"
abbreviation "mut_hs_type s ≡ hs_type (s (mutator m))"
abbreviation "mut_mark s ≡ mark (s (mutator m))"
abbreviation "mut_new_ref s ≡ new_ref (s (mutator m))"
abbreviation "mut_phase s ≡ phase (s (mutator m))"
abbreviation "mut_ref s ≡ ref (s (mutator m))"
abbreviation "mut_tmp_ref s ≡ tmp_ref (s (mutator m))"
abbreviation "mut_the_new_ref ≡ the ∘ mut_new_ref"
abbreviation "mut_the_ref ≡ the ∘ mut_ref"
abbreviation "mut_refs s ≡ refs (s (mutator m))"
abbreviation "mut_roots s ≡ roots (s (mutator m))"
abbreviation "mut_W s ≡ W (s (mutator m))"
end
abbreviation sys_heap :: "('field, 'mut, 'payload, 'ref) lsts ⇒ 'ref ⇒ ('field, 'payload, 'ref) object option" where "sys_heap s ≡ heap (s sys)"
abbreviation "sys_fA s ≡ fA (s sys)"
abbreviation "sys_fM s ≡ fM (s sys)"
abbreviation "sys_ghost_honorary_grey s ≡ ghost_honorary_grey (s sys)"
abbreviation "sys_ghost_hs_in_sync m s ≡ ghost_hs_in_sync (s sys) m"
abbreviation "sys_ghost_hs_phase s ≡ ghost_hs_phase (s sys)"
abbreviation "sys_hs_pending m s ≡ hs_pending (s sys) m"
abbreviation "sys_hs_type s ≡ hs_type (s sys)"
abbreviation "sys_mem_store_buffers p s ≡ mem_store_buffers (s sys) p"
abbreviation "sys_mem_lock s ≡ mem_lock (s sys)"
abbreviation "sys_phase s ≡ phase (s sys)"
abbreviation "sys_W s ≡ W (s sys)"
abbreviation atS_sys :: "location set ⇒ ('field, 'mut, 'payload, 'ref) lsts_pred ⇒ ('field, 'mut, 'payload, 'ref) gc_pred" where
"atS_sys ls P ≡ atS sys ls ❙⟶ LSTP P"
text‹Projections on TSO buffers.›
abbreviation (input) "tso_unlocked s ≡ mem_lock (s sys) = None"
abbreviation (input) "tso_locked_by p s ≡ mem_lock (s sys) = Some p"
abbreviation (input) "tso_pending p P s ≡ filter P (mem_store_buffers (s sys) p)"
abbreviation (input) "tso_pending_store p w s ≡ w ∈ set (mem_store_buffers (s sys) p)"
abbreviation (input) "tso_pending_fA p ≡ tso_pending p is_mw_fA"
abbreviation (input) "tso_pending_fM p ≡ tso_pending p is_mw_fM"
abbreviation (input) "tso_pending_mark p ≡ tso_pending p is_mw_Mark"
abbreviation (input) "tso_pending_mw_mutate p ≡ tso_pending p is_mw_Mutate"
abbreviation (input) "tso_pending_mutate p ≡ tso_pending p (is_mw_Mutate ❙∨ is_mw_Mutate_Payload)"
abbreviation (input) "tso_pending_phase p ≡ tso_pending p is_mw_Phase"
abbreviation (input) "tso_no_pending_marks ≡ ❙∀p. LIST_NULL (tso_pending_mark p)"
text‹
A somewhat-useful abstraction of the heap, following l4.verified,
which asserts that there is an object at the given reference with the
given property. In some sense this encodes a three-valued logic.
›
definition obj_at :: "(('field, 'payload, 'ref) object ⇒ bool) ⇒ 'ref ⇒ ('field, 'mut, 'payload, 'ref) lsts_pred" where
"obj_at P r ≡ λs. case sys_heap s r of None ⇒ False | Some obj ⇒ P obj"
abbreviation (input) valid_ref :: "'ref ⇒ ('field, 'mut, 'payload, 'ref) lsts_pred" where
"valid_ref r ≡ obj_at ⟨True⟩ r"
definition valid_null_ref :: "'ref option ⇒ ('field, 'mut, 'payload, 'ref) lsts_pred" where
"valid_null_ref r ≡ case r of None ⇒ ⟨True⟩ | Some r' ⇒ valid_ref r'"
abbreviation pred_points_to :: "'ref ⇒ 'ref ⇒ ('field, 'mut, 'payload, 'ref) lsts_pred" (infix "points'_to" 51) where
"x points_to y ≡ λs. obj_at (λobj. y ∈ ran (obj_fields obj)) x s"
text‹
We use Isabelle's standard transitive-reflexive closure to define
reachability through the heap.
›
definition reaches :: "'ref ⇒ 'ref ⇒ ('field, 'mut, 'payload, 'ref) lsts_pred" (infix "reaches" 51) where
"x reaches y = (λs. (λx y. (x points_to y) s)⇧*⇧* x y)"
text‹
The predicate ‹obj_at_field_on_heap› asserts that @{term ‹valid_ref r›}
and if ‹f› is a field of the object referred to by ‹r› then it it satisfies ‹P›.
›
definition obj_at_field_on_heap :: "('ref ⇒ bool) ⇒ 'ref ⇒ 'field ⇒ ('field, 'mut, 'payload, 'ref) lsts_pred" where
"obj_at_field_on_heap P r f ≡ λs.
case map_option obj_fields (sys_heap s r) of
None ⇒ False
| Some fs ⇒ (case fs f of None ⇒ True
| Some r' ⇒ P r')"
subsection‹Object colours›
text‹
We adopt the classical tricolour scheme for object colours due to
\<^citet>‹"DBLP:journals/cacm/DijkstraLMSS78"›, but
tweak it somewhat in the presence of worklists and TSO. Intuitively:
\begin{description}
\item[White] potential garbage, not yet reached
\item[Grey] reached, presumed live, a source of possible new references (work)
\item[Black] reached, presumed live, not a source of new references
\end{description}
In this particular setting we use the following interpretation:
\begin{description}
\item[White:] not marked
\item[Grey:] on a worklist or @{const ‹ghost_honorary_grey›}
\item[Black:] marked and not on a worklist
\end{description}
Note that this allows the colours to overlap: an object being marked
may be white (on the heap) and in @{const "ghost_honorary_grey"} for
some process, i.e. grey.
›
abbreviation marked :: "'ref ⇒ ('field, 'mut, 'payload, 'ref) lsts_pred" where
"marked r s ≡ obj_at (λobj. obj_mark obj = sys_fM s) r s"
definition white :: "'ref ⇒ ('field, 'mut, 'payload, 'ref) lsts_pred" where
"white r s ≡ obj_at (λobj. obj_mark obj ≠ sys_fM s) r s"
definition WL :: "'mut process_name ⇒ ('field, 'mut, 'payload, 'ref) lsts ⇒ 'ref set" where
"WL p = (λs. W (s p) ∪ ghost_honorary_grey (s p))"
definition grey :: "'ref ⇒ ('field, 'mut, 'payload, 'ref) lsts_pred" where
"grey r = (❙∃p. ⟨r⟩ ❙∈ WL p)"
definition black :: "'ref ⇒ ('field, 'mut, 'payload, 'ref) lsts_pred" where
"black r ≡ marked r ❙∧ ❙¬grey r"
text‹ These demonstrate the overlap in colours. ›
lemma colours_distinct[dest]:
"black r s ⟹ ¬grey r s"
"black r s ⟹ ¬white r s"
"grey r s ⟹ ¬black r s"
"white r s ⟹ ¬black r s"
by (auto simp: black_def white_def obj_at_def split: option.splits)
lemma marked_imp_black_or_grey:
"marked r s ⟹ black r s ∨ grey r s"
"¬ white r s ⟹ ¬ valid_ref r s ∨ black r s ∨ grey r s"
by (auto simp: black_def grey_def white_def obj_at_def split: option.splits)
text‹
In some phases the heap is monochrome.
›
definition black_heap :: "('field, 'mut, 'payload, 'ref) lsts_pred" where
"black_heap = (❙∀r. valid_ref r ❙⟶ black r)"
definition white_heap :: "('field, 'mut, 'payload, 'ref) lsts_pred" where
"white_heap = (❙∀r. valid_ref r ❙⟶ white r)"
definition no_black_refs :: "('field, 'mut, 'payload, 'ref) lsts_pred" where
"no_black_refs = (❙∀r. ❙¬black r)"
definition no_grey_refs :: "('field, 'mut, 'payload, 'ref) lsts_pred" where
"no_grey_refs = (❙∀r. ❙¬grey r)"
subsection‹Reachability›
text‹
We treat pending TSO heap mutations as extra mutator roots.
›
abbreviation store_refs :: "('field, 'payload, 'ref) mem_store_action ⇒ 'ref set" where
"store_refs w ≡ case w of mw_Mutate r f r' ⇒ {r} ∪ Option.set_option r' | mw_Mutate_Payload r f pl ⇒ {r} | _ ⇒ {}"
definition (in mut_m) tso_store_refs :: "('field, 'mut, 'payload, 'ref) lsts ⇒ 'ref set" where
"tso_store_refs = (λs. ⋃w ∈ set (sys_mem_store_buffers (mutator m) s). store_refs w)"
abbreviation (in mut_m) root :: "'ref ⇒ ('field, 'mut, 'payload, 'ref) lsts_pred" where
"root x ≡ ⟨x⟩ ❙∈ mut_roots ❙∪ mut_ghost_honorary_root ❙∪ tso_store_refs"
definition (in mut_m) reachable :: "'ref ⇒ ('field, 'mut, 'payload, 'ref) lsts_pred" where
"reachable y = (❙∃x. root x ❙∧ x reaches y)"
definition grey_reachable :: "'ref ⇒ ('field, 'mut, 'payload, 'ref) lsts_pred" where
"grey_reachable y = (❙∃g. grey g ❙∧ g reaches y)"
subsection‹ Sundry detritus ›
lemmas eq_imp_simps =
eq_imp_def
all_conj_distrib
split_paired_All split_def fst_conv snd_conv prod_eq_iff
conj_explode
simp_thms
lemma p_not_sys:
"p ≠ sys ⟷ p = gc ∨ (∃m. p = mutator m)"
by (cases p) simp_all
lemma (in mut_m') m'm[iff]: "m' ≠ m"
using mm' by blast
text‹ obj at ›
lemma obj_at_cong[cong]:
"⟦⋀obj. sys_heap s r = Some obj ⟹ P obj = P' obj; r = r'; s = s'⟧
⟹ obj_at P r s ⟷ obj_at P' r' s'"
unfolding obj_at_def by (simp cong: option.case_cong)
lemma obj_at_split:
"Q (obj_at P r s) = ((sys_heap s r = None ⟶ Q False) ∧ (∀obj. sys_heap s r = Some obj ⟶ Q (P obj)))"
by (simp add: obj_at_def split: option.splits)
lemma obj_at_split_asm:
"Q (obj_at P r s) = (¬ ((sys_heap s r = None ∧ ¬Q False) ∨ (∃obj. sys_heap s r = Some obj ∧ ¬ Q (P obj))))"
by (simp add: obj_at_def split: option.splits)
lemmas obj_at_splits = obj_at_split obj_at_split_asm
lemma obj_at_eq_imp:
"eq_imp (λ(_::unit) s. map_option P (sys_heap s r))
(obj_at P r)"
by (simp add: eq_imp_def obj_at_def split: option.splits)
lemmas obj_at_fun_upd[simp] = eq_imp_fun_upd[OF obj_at_eq_imp, simplified eq_imp_simps]
lemma obj_at_simps:
"obj_at (λobj. P obj ∧ Q obj) r s ⟷ obj_at P r s ∧ obj_at Q r s"
by (simp_all split: obj_at_splits)
text‹ obj at field on heap ›
lemma obj_at_field_on_heap_cong[cong]:
"⟦⋀r' obj. ⟦sys_heap s r = Some obj; obj_fields obj f = Some r'⟧⟹ P r' = P' r'; r = r'; f = f'; s = s'⟧
⟹ obj_at_field_on_heap P r f s ⟷ obj_at_field_on_heap P' r' f' s'"
unfolding obj_at_field_on_heap_def by (simp cong: option.case_cong)
lemma obj_at_field_on_heap_split:
"Q (obj_at_field_on_heap P r f s) ⟷ ((sys_heap s r = None ⟶ Q False)
∧ (∀obj. sys_heap s r = Some obj ∧ obj_fields obj f = None ⟶ Q True)
∧ (∀r' obj. sys_heap s r = Some obj ∧ obj_fields obj f = Some r' ⟶ Q (P r')))"
by (simp add: obj_at_field_on_heap_def split: option.splits)
lemma obj_at_field_on_heap_split_asm:
"Q (obj_at_field_on_heap P r f s) ⟷ (¬ ((sys_heap s r = None ∧ ¬Q False)
∨ (∃obj. sys_heap s r = Some obj ∧ obj_fields obj f = None ∧ ¬ Q True)
∨ (∃r' obj. sys_heap s r = Some obj ∧ obj_fields obj f = Some r' ∧ ¬ Q (P r'))))"
by (simp add: obj_at_field_on_heap_def split: option.splits)
lemmas obj_at_field_on_heap_splits = obj_at_field_on_heap_split obj_at_field_on_heap_split_asm
lemma obj_at_field_on_heap_eq_imp:
"eq_imp (λ(_::unit) s. sys_heap s r)
(obj_at_field_on_heap P r f)"
by (simp add: eq_imp_def obj_at_field_on_heap_def)
lemmas obj_at_field_on_heap_fun_upd[simp] = eq_imp_fun_upd[OF obj_at_field_on_heap_eq_imp, simplified eq_imp_simps]
lemma obj_at_field_on_heap_imp_valid_ref[elim]:
"obj_at_field_on_heap P r f s ⟹ valid_ref r s"
"obj_at_field_on_heap P r f s ⟹ valid_null_ref (Some r) s"
by (auto simp: obj_at_field_on_heap_def valid_null_ref_def split: obj_at_splits option.splits)
lemma obj_at_field_on_heapE[elim]:
"⟦ obj_at_field_on_heap P r f s; sys_heap s' r = sys_heap s r; ⋀r'. P r' ⟹ P' r' ⟧
⟹ obj_at_field_on_heap P' r f s'"
by (simp add: obj_at_field_on_heap_def split: option.splits)
lemma valid_null_ref_eq_imp:
"eq_imp (λ(_::unit) s. Option.bind r (map_option ⟨True⟩ ∘ sys_heap s))
(valid_null_ref r)"
by (simp add: eq_imp_def obj_at_def valid_null_ref_def split: option.splits)
lemmas valid_null_ref_fun_upd[simp] = eq_imp_fun_upd[OF valid_null_ref_eq_imp, simplified]
lemma valid_null_ref_simps[simp]:
"valid_null_ref None s"
"valid_null_ref (Some r) s ⟷ valid_ref r s"
unfolding valid_null_ref_def by simp_all
text‹Derive simplification rules from ‹case› expressions›
simps_of_case hs_step_simps[simp]: hs_step_def (splits: hs_phase.split)
simps_of_case do_load_action_simps[simp]: fun_cong[OF do_load_action_def[simplified atomize_eq]] (splits: mem_load_action.split)
simps_of_case do_store_action_simps[simp]: fun_cong[OF do_store_action_def[simplified atomize_eq]] (splits: mem_store_action.split)
lemma do_store_action_prj_simps[simp]:
"fM (do_store_action w s) = fl ⟷ (fM s = fl ∧ w ≠ mw_fM (¬fM s)) ∨ w = mw_fM fl"
"fl = fM (do_store_action w s) ⟷ (fl = fM s ∧ w ≠ mw_fM (¬fM s)) ∨ w = mw_fM fl"
"fA (do_store_action w s) = fl ⟷ (fA s = fl ∧ w ≠ mw_fA (¬fA s)) ∨ w = mw_fA fl"
"fl = fA (do_store_action w s) ⟷ (fl = fA s ∧ w ≠ mw_fA (¬fA s)) ∨ w = mw_fA fl"
"ghost_hs_in_sync (do_store_action w s) = ghost_hs_in_sync s"
"ghost_hs_phase (do_store_action w s) = ghost_hs_phase s"
"ghost_honorary_grey (do_store_action w s) = ghost_honorary_grey s"
"hs_pending (do_store_action w s) = hs_pending s"
"hs_type (do_store_action w s) = hs_type s"
"heap (do_store_action w s) r = None ⟷ heap s r = None"
"mem_lock (do_store_action w s) = mem_lock s"
"phase (do_store_action w s) = ph ⟷ (phase s = ph ∧ (∀ph'. w ≠ mw_Phase ph') ∨ w = mw_Phase ph)"
"ph = phase (do_store_action w s) ⟷ (ph = phase s ∧ (∀ph'. w ≠ mw_Phase ph') ∨ w = mw_Phase ph)"
"W (do_store_action w s) = W s"
by (auto simp: do_store_action_def fun_upd_apply split: mem_store_action.splits obj_at_splits)
text‹ reaches ›
lemma reaches_refl[iff]:
"(r reaches r) s"
unfolding reaches_def by blast
lemma reaches_step[intro]:
"⟦(x reaches y) s; (y points_to z) s⟧ ⟹ (x reaches z) s"
"⟦(y reaches z) s; (x points_to y) s⟧ ⟹ (x reaches z) s"
unfolding reaches_def
apply (simp add: rtranclp.rtrancl_into_rtrancl)
apply (simp add: converse_rtranclp_into_rtranclp)
done
lemma reaches_induct[consumes 1, case_names refl step, induct set: reaches]:
assumes "(x reaches y) s"
assumes "⋀x. P x x"
assumes "⋀x y z. ⟦(x reaches y) s; P x y; (y points_to z) s⟧ ⟹ P x z"
shows "P x y"
using assms unfolding reaches_def by (rule rtranclp.induct)
lemma converse_reachesE[consumes 1, case_names base step]:
assumes "(x reaches z) s"
assumes "x = z ⟹ P"
assumes "⋀y. ⟦(x points_to y) s; (y reaches z) s⟧ ⟹ P"
shows P
using assms unfolding reaches_def by (blast elim: converse_rtranclpE)
lemma reaches_fields:
assumes "(x reaches y) s'"
assumes "∀r'. ⋃(ran ` obj_fields ` set_option (sys_heap s' r')) = ⋃(ran ` obj_fields ` set_option (sys_heap s r'))"
shows "(x reaches y) s"
using assms
proof induct
case (step x y z)
then have "(y points_to z) s"
by (cases "sys_heap s y")
(auto 10 10 simp: ran_def obj_at_def split: option.splits dest!: spec[where x=y])
with step show ?case by blast
qed simp
lemma reaches_eq_imp:
"eq_imp (λr' s. ⋃(ran ` obj_fields ` set_option (sys_heap s r')))
(x reaches y)"
unfolding eq_imp_def by (metis reaches_fields)
lemmas reaches_fun_upd[simp] = eq_imp_fun_upd[OF reaches_eq_imp, simplified eq_imp_simps, rule_format]
text‹
Location-specific facts.
›
lemma obj_at_mark_dequeue[simp]:
"obj_at P r (s(sys := s sys⦇ heap := (sys_heap s)(r' := map_option (obj_mark_update (λ_. fl)) (sys_heap s r')), mem_store_buffers := wb' ⦈))
⟷ obj_at (λobj. (P (if r = r' then obj⦇ obj_mark := fl ⦈ else obj))) r s"
by (clarsimp simp: fun_upd_apply split: obj_at_splits)
lemma obj_at_field_on_heap_mw_simps[simp]:
"obj_at_field_on_heap P r0 f0
(s(sys := (s sys)⦇ heap := (sys_heap s)(r := map_option (λobj :: ('field, 'payload, 'ref) object. obj⦇obj_fields := (obj_fields obj)(f := opt_r')⦈) (sys_heap s r)),
mem_store_buffers := (mem_store_buffers (s Sys))(p := ws) ⦈))
⟷ ( (r ≠ r0 ∨ f ≠ f0) ∧ obj_at_field_on_heap P r0 f0 s )
∨ (r = r0 ∧ f = f0 ∧ valid_ref r s ∧ (case opt_r' of Some r'' ⇒ P r'' | _ ⇒ True))"
"obj_at_field_on_heap P r f (s(sys := s sys⦇heap := (sys_heap s)(r' := map_option (obj_mark_update (λ_. fl)) (sys_heap s r')), mem_store_buffers := sb'⦈))
⟷ obj_at_field_on_heap P r f s"
by (auto simp: obj_at_field_on_heap_def fun_upd_apply split: option.splits obj_at_splits)
lemma obj_at_field_on_heap_no_pending_stores:
"⟦ sys_load (mutator m) (mr_Ref r f) (s sys) = mv_Ref opt_r'; ∀opt_r'. mw_Mutate r f opt_r' ∉ set (sys_mem_store_buffers (mutator m) s); valid_ref r s ⟧
⟹ obj_at_field_on_heap (λr. opt_r' = Some r) r f s"
unfolding sys_load_def fold_stores_def
apply clarsimp
apply (rule fold_invariant[where P="λfr. obj_at_field_on_heap (λr'. Option.bind (heap (fr (s sys)) r) (λobj. obj_fields obj f) = Some r') r f s"
and Q="λw. w ∈ set (sys_mem_store_buffers (mutator m) s)"])
apply fastforce
apply (fastforce simp: obj_at_field_on_heap_def split: option.splits obj_at_splits)
apply (auto simp: do_store_action_def map_option_case fun_upd_apply
split: obj_at_field_on_heap_splits option.splits obj_at_splits mem_store_action.splits)
done
end