Theory Local_Invariants
theory Local_Invariants
imports
Proofs_Basis
begin
section‹ Local invariants \label{sec:local-invariants}›
subsection‹TSO invariants›
context gc
begin
text ‹
The GC holds the TSO lock only during the \texttt{CAS} in ‹mark_object›.
›
locset_definition tso_lock_locs :: "location set" where
"tso_lock_locs = (⋃l∈{ ''mo_co_cmark'', ''mo_co_ctest'', ''mo_co_mark'', ''mo_co_unlock'' }. suffixed l)"
definition tso_lock_invL :: "('field, 'mut, 'payload, 'ref) gc_pred" where
[inv]: "tso_lock_invL =
(atS_gc tso_lock_locs (tso_locked_by gc)
❙∧ atS_gc (- tso_lock_locs) (❙¬ tso_locked_by gc))"
end
context mut_m
begin
text ‹
A mutator holds the TSO lock only during the \texttt{CAS}s in ‹mark_object›.
›
locset_definition "tso_lock_locs =
(⋃l∈{ ''mo_co_cmark'', ''mo_co_ctest'', ''mo_co_mark'', ''mo_co_unlock'' }. suffixed l)"
definition tso_lock_invL :: "('field, 'mut, 'payload, 'ref) gc_pred" where
[inv]: "tso_lock_invL =
(atS_mut tso_lock_locs (tso_locked_by (mutator m))
❙∧ atS_mut (-tso_lock_locs) (❙¬tso_locked_by (mutator m)))"
end
subsection‹Handshake phases \label{sec:local-handshake-phases}›
text‹
Connect @{const "sys_ghost_hs_phase"} with locations in the GC.
›
context gc
begin
locset_definition "idle_locs = prefixed ''idle''"
locset_definition "init_locs = prefixed ''init''"
locset_definition "mark_locs = prefixed ''mark''"
locset_definition "sweep_locs = prefixed ''sweep''"
locset_definition "mark_loop_locs = prefixed ''mark_loop''"
locset_definition "hp_Idle_locs =
(prefixed ''idle_noop'' - { idle_noop_mfence, idle_noop_init_type })
∪ { idle_load_fM, idle_invert_fM, idle_store_fM, idle_flip_noop_mfence, idle_flip_noop_init_type }"
locset_definition "hp_IdleInit_locs =
(prefixed ''idle_flip_noop'' - { idle_flip_noop_mfence, idle_flip_noop_init_type })
∪ { idle_phase_init, init_noop_mfence, init_noop_init_type }"
locset_definition "hp_InitMark_locs =
(prefixed ''init_noop'' - { init_noop_mfence, init_noop_init_type })
∪ { init_phase_mark, mark_load_fM, mark_store_fA, mark_noop_mfence, mark_noop_init_type }"
locset_definition "hp_IdleMarkSweep_locs =
{ idle_noop_mfence, idle_noop_init_type, mark_end }
∪ sweep_locs
∪ (mark_loop_locs - { mark_loop_get_roots_init_type })"
locset_definition "hp_Mark_locs =
(prefixed ''mark_noop'' - { mark_noop_mfence, mark_noop_init_type })
∪ { mark_loop_get_roots_init_type }"
abbreviation
"hs_noop_prefixes ≡ {''idle_noop'', ''idle_flip_noop'', ''init_noop'', ''mark_noop'' }"
locset_definition "hs_noop_locs =
(⋃l ∈ hs_noop_prefixes. prefixed l - (suffixed ''_noop_mfence'' ∪ suffixed ''_noop_init_type''))"
locset_definition "hs_get_roots_locs =
prefixed ''mark_loop_get_roots'' - {mark_loop_get_roots_init_type}"
locset_definition "hs_get_work_locs =
prefixed ''mark_loop_get_work'' - {mark_loop_get_work_init_type}"
abbreviation "hs_prefixes ≡
hs_noop_prefixes ∪ { ''mark_loop_get_roots'', ''mark_loop_get_work'' }"
locset_definition "hs_init_loop_locs = (⋃l ∈ hs_prefixes. prefixed (l @ ''_init_loop''))"
locset_definition "hs_done_loop_locs = (⋃l ∈ hs_prefixes. prefixed (l @ ''_done_loop''))"
locset_definition "hs_done_locs = (⋃l ∈ hs_prefixes. prefixed (l @ ''_done''))"
locset_definition "hs_none_pending_locs = - (hs_init_loop_locs ∪ hs_done_locs)"
locset_definition "hs_in_sync_locs =
(- ( (⋃l ∈ hs_prefixes. prefixed (l @ ''_init'')) ∪ hs_done_locs ))
∪ (⋃l ∈ hs_prefixes. {l @ ''_init_type''})"
locset_definition "hs_out_of_sync_locs =
(⋃l ∈ hs_prefixes. {l @ ''_init_muts''})"
locset_definition "hs_mut_in_muts_locs =
(⋃l ∈ hs_prefixes. {l @ ''_init_loop_set_pending'', l @ ''_init_loop_done''})"
locset_definition "hs_init_loop_done_locs =
(⋃l ∈ hs_prefixes. {l @ ''_init_loop_done''})"
locset_definition "hs_init_loop_not_done_locs =
(hs_init_loop_locs - (⋃l ∈ hs_prefixes. {l @ ''_init_loop_done''}))"
definition handshake_invL :: "('field, 'mut, 'payload, 'ref) gc_pred" where
[inv]: "handshake_invL =
(atS_gc hs_noop_locs (sys_hs_type ❙= ⟨ht_NOOP⟩)
❙∧ atS_gc hs_get_roots_locs (sys_hs_type ❙= ⟨ht_GetRoots⟩)
❙∧ atS_gc hs_get_work_locs (sys_hs_type ❙= ⟨ht_GetWork⟩)
❙∧ atS_gc hs_mut_in_muts_locs (gc_mut ❙∈ gc_muts)
❙∧ atS_gc hs_init_loop_locs (❙∀m. ❙¬⟨m⟩ ❙∈ gc_muts ❙⟶ sys_hs_pending m
❙∨ sys_ghost_hs_in_sync m)
❙∧ atS_gc hs_init_loop_not_done_locs (❙∀m. ⟨m⟩ ❙∈ gc_muts ❙⟶ ❙¬sys_hs_pending m
❙∧ ❙¬sys_ghost_hs_in_sync m)
❙∧ atS_gc hs_init_loop_done_locs ( (sys_hs_pending ❙$ gc_mut
❙∨ sys_ghost_hs_in_sync ❙$ gc_mut)
❙∧ (❙∀m. ⟨m⟩ ❙∈ gc_muts ❙∧ ⟨m⟩ ❙≠ gc_mut
❙⟶ ❙¬sys_hs_pending m
❙∧ ❙¬sys_ghost_hs_in_sync m) )
❙∧ atS_gc hs_done_locs (❙∀m. sys_hs_pending m ❙∨ sys_ghost_hs_in_sync m)
❙∧ atS_gc hs_done_loop_locs (❙∀m. ❙¬⟨m⟩ ❙∈ gc_muts ❙⟶ ❙¬sys_hs_pending m)
❙∧ atS_gc hs_none_pending_locs (❙∀m. ❙¬sys_hs_pending m)
❙∧ atS_gc hs_in_sync_locs (❙∀m. sys_ghost_hs_in_sync m)
❙∧ atS_gc hs_out_of_sync_locs (❙∀m. ❙¬sys_hs_pending m
❙∧ ❙¬sys_ghost_hs_in_sync m)
❙∧ atS_gc hp_Idle_locs (sys_ghost_hs_phase ❙= ⟨hp_Idle⟩)
❙∧ atS_gc hp_IdleInit_locs (sys_ghost_hs_phase ❙= ⟨hp_IdleInit⟩)
❙∧ atS_gc hp_InitMark_locs (sys_ghost_hs_phase ❙= ⟨hp_InitMark⟩)
❙∧ atS_gc hp_IdleMarkSweep_locs (sys_ghost_hs_phase ❙= ⟨hp_IdleMarkSweep⟩)
❙∧ atS_gc hp_Mark_locs (sys_ghost_hs_phase ❙= ⟨hp_Mark⟩))"
text‹
Tie the garbage collector's control location to the value of @{const
"gc_phase"}.
›
locset_definition no_pending_phase_locs :: "location set" where
"no_pending_phase_locs =
(idle_locs - { idle_noop_mfence })
∪ (init_locs - { init_noop_mfence })
∪ (mark_locs - { mark_load_fM, mark_store_fA, mark_noop_mfence })"
definition phase_invL :: "('field, 'mut, 'payload, 'ref) gc_pred" where
[inv]: "phase_invL =
(atS_gc idle_locs (gc_phase ❙= ⟨ph_Idle⟩)
❙∧ atS_gc init_locs (gc_phase ❙= ⟨ph_Init⟩)
❙∧ atS_gc mark_locs (gc_phase ❙= ⟨ph_Mark⟩)
❙∧ atS_gc sweep_locs (gc_phase ❙= ⟨ph_Sweep⟩)
❙∧ atS_gc no_pending_phase_locs (LIST_NULL (tso_pending_phase gc)))"
end
text‹
Local handshake phase invariant for the mutators.
›
context mut_m
begin
locset_definition "hs_noop_locs = prefixed ''hs_noop_''"
locset_definition "hs_get_roots_locs = prefixed ''hs_get_roots_''"
locset_definition "hs_get_work_locs = prefixed ''hs_get_work_''"
locset_definition "no_pending_mutations_locs =
{ hs_load_ht }
∪ (prefixed ''hs_noop'')
∪ (prefixed ''hs_get_roots'')
∪ (prefixed ''hs_get_work'')"
locset_definition "hs_pending_loaded_locs = (prefixed ''hs_'' - { hs_load_pending })"
locset_definition "hs_pending_locs = (prefixed ''hs_'' - { hs_load_pending, hs_pending })"
locset_definition "ht_loaded_locs = (prefixed ''hs_'' - { hs_load_pending, hs_pending, hs_mfence, hs_load_ht })"
definition handshake_invL :: "('field, 'mut, 'payload, 'ref) gc_pred" where
[inv]: "handshake_invL =
(atS_mut hs_noop_locs (sys_hs_type ❙= ⟨ht_NOOP⟩)
❙∧ atS_mut hs_get_roots_locs (sys_hs_type ❙= ⟨ht_GetRoots⟩)
❙∧ atS_mut hs_get_work_locs (sys_hs_type ❙= ⟨ht_GetWork⟩)
❙∧ atS_mut ht_loaded_locs (mut_hs_pending ❙⟶ mut_hs_type ❙= sys_hs_type)
❙∧ atS_mut hs_pending_loaded_locs (mut_hs_pending ❙⟶ sys_hs_pending m)
❙∧ atS_mut hs_pending_locs (mut_hs_pending)
❙∧ atS_mut no_pending_mutations_locs (LIST_NULL (tso_pending_mutate (mutator m))))"
end
text‹
Validity of @{const "sys_fM"} wrt @{const "gc_fM"} and the handshake
phase. Effectively we use @{const "gc_fM"} as ghost state. We also
include the TSO lock to rule out the GC having any pending marks
during the @{const "hp_Idle"} handshake phase.
›
context gc
begin
locset_definition "fM_eq_locs = (- { idle_store_fM, idle_flip_noop_mfence })"
locset_definition "fM_tso_empty_locs = (- { idle_flip_noop_mfence })"
locset_definition "fA_tso_empty_locs = (- { mark_noop_mfence })"
locset_definition
"fA_eq_locs = { idle_load_fM, idle_invert_fM }
∪ prefixed ''idle_noop''
∪ (mark_locs - { mark_load_fM, mark_store_fA, mark_noop_mfence })
∪ sweep_locs"
locset_definition
"fA_neq_locs = { idle_phase_init, idle_store_fM, mark_load_fM, mark_store_fA }
∪ prefixed ''idle_flip_noop''
∪ init_locs"
definition fM_fA_invL :: "('field, 'mut, 'payload, 'ref) gc_pred" where
[inv]: "fM_fA_invL =
(atS_gc fM_eq_locs (gc_fM ❙= sys_fM)
❙∧ at_gc idle_store_fM (gc_fM ❙≠ sys_fM)
❙∧ at_gc idle_flip_noop_mfence (sys_fM ❙≠ gc_fM ❙⟶ ❙¬LIST_NULL (tso_pending_fM gc))
❙∧ atS_gc fM_tso_empty_locs (LIST_NULL (tso_pending_fM gc))
❙∧ atS_gc fA_eq_locs (gc_fM ❙= sys_fA)
❙∧ atS_gc fA_neq_locs (gc_fM ❙≠ sys_fA)
❙∧ at_gc mark_noop_mfence (gc_fM ❙≠ sys_fA ❙⟶ ❙¬LIST_NULL (tso_pending_fA gc))
❙∧ atS_gc fA_tso_empty_locs (LIST_NULL (tso_pending_fA gc)))"
end
subsection‹Mark Object›
text‹
Local invariants for @{const "mark_object_fn"}. Invoking this code in
phases where @{const "sys_fM"} is constant marks the reference in
@{const "ref"}. When @{const "sys_fM"} could vary this code is not
called. The two cases are distinguished by @{term "p_ph_enabled"}.
Each use needs to provide extra facts to justify validity of
references, etc. We do not include a post-condition for @{const
"mark_object_fn"} here as it is different at each call site.
›
locale mark_object =
fixes p :: "'mut process_name"
fixes l :: "location"
fixes p_ph_enabled :: "('field, 'mut, 'payload, 'ref) lsts_pred"
assumes p_ph_enabled_eq_imp: "eq_imp (λ(_::unit) s. s p) p_ph_enabled"
begin
abbreviation (input) "p_cas_mark s ≡ cas_mark (s p)"
abbreviation (input) "p_mark s ≡ mark (s p)"
abbreviation (input) "p_fM s ≡ fM (s p)"
abbreviation (input) "p_ghost_hs_phase s ≡ ghost_hs_phase (s p)"
abbreviation (input) "p_ghost_honorary_grey s ≡ ghost_honorary_grey (s p)"
abbreviation (input) "p_ghost_hs_in_sync s ≡ ghost_hs_in_sync (s p)"
abbreviation (input) "p_phase s ≡ phase (s p)"
abbreviation (input) "p_ref s ≡ ref (s p)"
abbreviation (input) "p_the_ref ≡ the ∘ p_ref"
abbreviation (input) "p_W s ≡ W (s p)"
abbreviation at_p :: "location ⇒ ('field, 'mut, 'payload, 'ref) lsts_pred ⇒ ('field, 'mut, 'payload, 'ref) gc_pred" where
"at_p l' P ≡ at p (l @ l') ❙⟶ LSTP P"
abbreviation (input) "p_en_cond P ≡ p_ph_enabled ❙⟶ P"
abbreviation (input) "p_valid_ref ≡ ❙¬NULL p_ref ❙∧ valid_ref ❙$ p_the_ref"
abbreviation (input) "p_tso_no_pending_mark ≡ LIST_NULL (tso_pending_mark p)"
abbreviation (input) "p_tso_no_pending_mutate ≡ LIST_NULL (tso_pending_mutate p)"
abbreviation (input)
"p_valid_W_inv ≡ ((p_cas_mark ❙≠ p_mark ❙∨ p_tso_no_pending_mark) ❙⟶ marked ❙$ p_the_ref)
❙∧ (tso_pending_mark p ❙∈ (λs. {[], [mw_Mark (p_the_ref s) (p_fM s)]}) )"
abbreviation (input)
"p_mark_inv ≡ ❙¬NULL p_mark
❙∧ ((λs. obj_at (λobj. Some (obj_mark obj) = p_mark s) (p_the_ref s) s)
❙∨ marked ❙$ p_the_ref)"
abbreviation (input)
"p_cas_mark_inv ≡ (λs. obj_at (λobj. Some (obj_mark obj) = p_cas_mark s) (p_the_ref s) s)"
abbreviation (input) "p_valid_fM ≡ p_fM ❙= sys_fM"
abbreviation (input)
"p_ghg_eq_ref ≡ p_ghost_honorary_grey ❙= pred_singleton (the ∘ p_ref)"
abbreviation (input)
"p_ghg_inv ≡ If p_cas_mark ❙= p_mark Then p_ghg_eq_ref Else EMPTY p_ghost_honorary_grey"
definition mark_object_invL :: "('field, 'mut, 'payload, 'ref) gc_pred" where
"mark_object_invL =
(at_p ''_mo_null'' ⟨True⟩
❙∧ at_p ''_mo_mark'' (p_valid_ref)
❙∧ at_p ''_mo_fM'' (p_valid_ref ❙∧ p_en_cond (p_mark_inv))
❙∧ at_p ''_mo_mtest'' (p_valid_ref ❙∧ p_en_cond (p_mark_inv ❙∧ p_valid_fM))
❙∧ at_p ''_mo_phase'' (p_valid_ref ❙∧ p_mark ❙≠ Some ∘ p_fM ❙∧ p_en_cond (p_mark_inv ❙∧ p_valid_fM))
❙∧ at_p ''_mo_ptest'' (p_valid_ref ❙∧ p_mark ❙≠ Some ∘ p_fM ❙∧ p_en_cond (p_mark_inv ❙∧ p_valid_fM))
❙∧ at_p ''_mo_co_lock'' (p_valid_ref ❙∧ p_mark_inv ❙∧ p_valid_fM ❙∧ p_mark ❙≠ Some ∘ p_fM ❙∧ p_tso_no_pending_mark)
❙∧ at_p ''_mo_co_cmark'' (p_valid_ref ❙∧ p_mark_inv ❙∧ p_valid_fM ❙∧ p_mark ❙≠ Some ∘ p_fM ❙∧ p_tso_no_pending_mark)
❙∧ at_p ''_mo_co_ctest'' (p_valid_ref ❙∧ p_mark_inv ❙∧ p_valid_fM ❙∧ p_mark ❙≠ Some ∘ p_fM ❙∧ p_cas_mark_inv ❙∧ p_tso_no_pending_mark)
❙∧ at_p ''_mo_co_mark'' (p_cas_mark ❙= p_mark ❙∧ p_valid_ref ❙∧ p_valid_fM ❙∧ white ❙$ p_the_ref ❙∧ p_tso_no_pending_mark)
❙∧ at_p ''_mo_co_unlock'' (p_ghg_inv ❙∧ p_valid_ref ❙∧ p_valid_fM ❙∧ p_valid_W_inv)
❙∧ at_p ''_mo_co_won'' (p_ghg_inv ❙∧ p_valid_ref ❙∧ p_valid_fM ❙∧ marked ❙$ p_the_ref ❙∧ p_tso_no_pending_mutate)
❙∧ at_p ''_mo_co_W'' (p_ghg_eq_ref ❙∧ p_valid_ref ❙∧ p_valid_fM ❙∧ marked ❙$ p_the_ref ❙∧ p_tso_no_pending_mutate))"
end
text‹
The uses of @{const "mark_object_fn"} in the GC and during the root
marking are straightforward.
›
interpretation gc_mark: mark_object "gc" "gc.mark_loop" "⟨True⟩"
by standard (simp add: eq_imp_def)
lemmas (in gc) gc_mark_mark_object_invL_def2[inv] = gc_mark.mark_object_invL_def[unfolded loc_defs, simplified, folded loc_defs]
interpretation mut_get_roots: mark_object "mutator m" "mut_m.hs_get_roots_loop" "⟨True⟩" for m
by standard (simp add: eq_imp_def)
lemmas (in mut_m) mut_get_roots_mark_object_invL_def2[inv] = mut_get_roots.mark_object_invL_def[unfolded loc_defs, simplified, folded loc_defs]
text‹
The most interesting cases are the two asynchronous uses of @{const
"mark_object_fn"} in the mutators: we need something that holds even
before we read the phase. In particular we need to avoid interference
by an @{const "fM"} flip.
›
interpretation mut_store_del: mark_object "mutator m" "''store_del''" "mut_m.mut_ghost_hs_phase m ❙≠ ⟨hp_Idle⟩" for m
by standard (simp add: eq_imp_def)
lemmas (in mut_m) mut_store_del_mark_object_invL_def2[inv] = mut_store_del.mark_object_invL_def[simplified, folded loc_defs]
interpretation mut_store_ins: mark_object "mutator m" "mut_m.store_ins" "mut_m.mut_ghost_hs_phase m ❙≠ ⟨hp_Idle⟩" for m
by standard (simp add: eq_imp_def)
lemmas (in mut_m) mut_store_ins_mark_object_invL_def2[inv] = mut_store_ins.mark_object_invL_def[unfolded loc_defs, simplified, folded loc_defs]
text‹
Local invariant for the mutator's uses of ‹mark_object›.
›
context mut_m
begin
locset_definition "hs_get_roots_loop_locs = prefixed ''hs_get_roots_loop''"
locset_definition "hs_get_roots_loop_mo_locs =
prefixed ''hs_get_roots_loop_mo'' ∪ {hs_get_roots_loop_done}"
abbreviation "mut_async_mark_object_prefixes ≡ { ''store_del'', ''store_ins'' }"
locset_definition "hs_not_hp_Idle_locs =
(⋃pref∈mut_async_mark_object_prefixes.
⋃l∈{''mo_co_lock'', ''mo_co_cmark'', ''mo_co_ctest'', ''mo_co_mark'', ''mo_co_unlock'', ''mo_co_won'', ''mo_co_W''}. {pref @ ''_'' @ l})"
locset_definition "async_mo_ptest_locs =
(⋃pref∈mut_async_mark_object_prefixes. {pref @ ''_mo_ptest''})"
locset_definition "mo_ptest_locs =
(⋃pref∈mut_async_mark_object_prefixes. {pref @ ''_mo_ptest''})"
locset_definition "mo_valid_ref_locs =
(prefixed ''store_del'' ∪ prefixed ''store_ins'' ∪ {deref_del, lop_store_ins})"
text‹
This local invariant for the mutators illustrates the handshake
structure: we can rely on the insertion barrier earlier than on the
deletion barrier. Both need to be installed before ‹get_roots›
to ensure we preserve the strong tricolour invariant. All black
objects at that point are allocated: we need to know that the
insertion barrier is installed to preserve it. This limits when ‹fA› can be set.
It is interesting to contrast the two barriers. Intuitively a mutator
can locally guarantee that it, in the relevant phases, will insert
only marked references. Less often can it be sure that the reference
it is overwriting is marked. We also need to consider stores pending
in TSO buffers: it is key that after the ‹''init_noop''›
handshake there are no pending white insertions
(mutations that insert unmarked references). This ensures the deletion barrier
does its job.
›
locset_definition
"ghost_honorary_grey_empty_locs =
(- (⋃pref∈{ ''hs_get_roots_loop'', ''store_del'', ''store_ins'' }.
⋃l∈{ ''mo_co_unlock'', ''mo_co_won'', ''mo_co_W'' }. {pref @ ''_'' @ l}))"
locset_definition
"ghost_honorary_root_empty_locs =
(- (prefixed ''store_del'' ∪ {lop_store_ins} ∪ prefixed ''store_ins''))"
locset_definition "ghost_honorary_root_nonempty_locs = prefixed ''store_del'' - {store_del_mo_null}"
locset_definition "not_idle_locs = suffixed ''_mo_ptest''"
locset_definition "ins_barrier_locs = prefixed ''store_ins''"
locset_definition "del_barrier1_locs = prefixed ''store_del_mo'' ∪ {lop_store_ins}"
definition mark_object_invL :: "('field, 'mut, 'payload, 'ref) gc_pred" where
[inv]: "mark_object_invL =
(atS_mut hs_get_roots_loop_locs (mut_refs ❙⊆ mut_roots ❙∧ (❙∀r. ⟨r⟩ ❙∈ mut_roots ❙- mut_refs ❙⟶ marked r))
❙∧ atS_mut hs_get_roots_loop_mo_locs (❙¬NULL mut_ref ❙∧ mut_the_ref ❙∈ mut_roots)
❙∧ at_mut hs_get_roots_loop_done (marked ❙$ mut_the_ref)
❙∧ at_mut hs_get_roots_loop_mo_ptest (mut_phase ❙≠ ⟨ph_Idle⟩)
❙∧ at_mut hs_get_roots_done (❙∀r. ⟨r⟩ ❙∈ mut_roots ❙⟶ marked r)
❙∧ atS_mut mo_valid_ref_locs ( (❙¬NULL mut_new_ref ❙⟶ mut_the_new_ref ❙∈ mut_roots)
❙∧ (mut_tmp_ref ❙∈ mut_roots) )
❙∧ at_mut store_del_mo_null (❙¬NULL mut_ref ❙⟶ mut_the_ref ❙∈ mut_ghost_honorary_root)
❙∧ atS_mut ghost_honorary_root_nonempty_locs (mut_the_ref ❙∈ mut_ghost_honorary_root)
❙∧ atS_mut not_idle_locs (mut_phase ❙≠ ⟨ph_Idle⟩ ❙⟶ mut_ghost_hs_phase ❙≠ ⟨hp_Idle⟩)
❙∧ atS_mut hs_not_hp_Idle_locs (mut_ghost_hs_phase ❙≠ ⟨hp_Idle⟩)
❙∧ atS_mut mo_ptest_locs (mut_phase ❙= ⟨ph_Idle⟩ ❙⟶ (mut_ghost_hs_phase ❙∈ ⟨{hp_Idle, hp_IdleInit}⟩
❙∨ (mut_ghost_hs_phase ❙= ⟨hp_IdleMarkSweep⟩
❙∧ sys_phase ❙= ⟨ph_Idle⟩)))
❙∧ atS_mut ghost_honorary_grey_empty_locs (EMPTY mut_ghost_honorary_grey)
❙∧ at_mut store_ins ( (mut_ghost_hs_phase ❙∈ ⟨{hp_InitMark, hp_Mark}⟩
❙∨ (mut_ghost_hs_phase ❙= ⟨hp_IdleMarkSweep⟩ ❙∧ sys_phase ❙≠ ⟨ph_Idle⟩))
❙∧ ❙¬NULL mut_new_ref
❙⟶ marked ❙$ mut_the_new_ref )
❙∧ atS_mut ins_barrier_locs ( ( (mut_ghost_hs_phase ❙= ⟨hp_Mark⟩
❙∨ (mut_ghost_hs_phase ❙= ⟨hp_IdleMarkSweep⟩ ❙∧ sys_phase ❙≠ ⟨ph_Idle⟩))
❙∧ (λs. ∀opt_r'. ¬tso_pending_store (mutator m) (mw_Mutate (mut_tmp_ref s) (mut_field s) opt_r') s)
❙⟶ (λs. obj_at_field_on_heap (λr'. marked r' s) (mut_tmp_ref s) (mut_field s) s) )
❙∧ (mut_ref ❙= mut_new_ref) )
❙∧ atS_mut del_barrier1_locs ( (mut_ghost_hs_phase ❙= ⟨hp_Mark⟩
❙∨ (mut_ghost_hs_phase ❙= ⟨hp_IdleMarkSweep⟩ ❙∧ sys_phase ❙≠ ⟨ph_Idle⟩))
❙∧ (λs. ∀opt_r'. ¬tso_pending_store (mutator m) (mw_Mutate (mut_tmp_ref s) (mut_field s) opt_r') s)
❙⟶ (λs. obj_at_field_on_heap (λr. mut_ref s = Some r ∨ marked r s) (mut_tmp_ref s) (mut_field s) s))
❙∧ at_mut lop_store_ins ( (mut_ghost_hs_phase ❙= ⟨hp_Mark⟩
❙∨ (mut_ghost_hs_phase ❙= ⟨hp_IdleMarkSweep⟩ ❙∧ sys_phase ❙≠ ⟨ph_Idle⟩))
❙∧ ❙¬NULL mut_ref
❙⟶ marked ❙$ mut_the_ref )
❙∧ at_mut mut_load (mut_tmp_ref ❙∈ mut_roots)
❙∧ atS_mut ghost_honorary_root_empty_locs (EMPTY mut_ghost_honorary_root) )"
end
subsection‹The infamous termination argument›
text‹
We need to know that if the GC does not receive any further work to do
at ‹get_roots› and ‹get_work›, then there are no grey
objects left. Essentially this encodes the stability property that
grey objects must exist for mutators to create grey objects.
Note that this is not invariant across the scan: it is possible for
the GC to hold all the grey references. The two handshakes transform
the GC's local knowledge that it has no more work to do into a global
property, or gives it more work.
›
definition (in mut_m) gc_W_empty_mut_inv :: "('field, 'mut, 'payload, 'ref) lsts_pred" where
"gc_W_empty_mut_inv =
((EMPTY sys_W ❙∧ sys_ghost_hs_in_sync m ❙∧ ❙¬EMPTY (WL (mutator m)))
❙⟶ (❙∃m'. ❙¬sys_ghost_hs_in_sync m' ❙∧ ❙¬EMPTY (WL (mutator m'))))"
context gc
begin
locset_definition gc_W_empty_locs :: "location set" where
"gc_W_empty_locs =
idle_locs ∪ init_locs ∪ sweep_locs ∪ {mark_load_fM, mark_store_fA, mark_end}
∪ prefixed ''mark_noop''
∪ prefixed ''mark_loop_get_roots''
∪ prefixed ''mark_loop_get_work''"
locset_definition "get_roots_UN_get_work_locs = hs_get_roots_locs ∪ hs_get_work_locs"
locset_definition "black_heap_locs = {sweep_idle, idle_noop_mfence, idle_noop_init_type}"
locset_definition "no_grey_refs_locs = black_heap_locs ∪ sweep_locs ∪ {mark_end}"
definition gc_W_empty_invL :: "('field, 'mut, 'payload, 'ref) gc_pred" where
[inv]: "gc_W_empty_invL =
(atS_gc get_roots_UN_get_work_locs (❙∀m. mut_m.gc_W_empty_mut_inv m)
❙∧ at_gc mark_loop_get_roots_load_W (EMPTY sys_W ❙⟶ no_grey_refs)
❙∧ at_gc mark_loop_get_work_load_W (EMPTY sys_W ❙⟶ no_grey_refs)
❙∧ at_gc mark_loop (EMPTY gc_W ❙⟶ no_grey_refs)
❙∧ atS_gc no_grey_refs_locs no_grey_refs
❙∧ atS_gc gc_W_empty_locs (EMPTY gc_W))"
end
subsection‹Sweep loop invariants›
context gc
begin
locset_definition "sweep_loop_locs = prefixed ''sweep_loop''"
locset_definition "sweep_loop_not_choose_ref_locs = (prefixed ''sweep_loop_'' - {sweep_loop_choose_ref})"
definition sweep_loop_invL :: "('field, 'mut, 'payload, 'ref) gc_pred" where
[inv]: "sweep_loop_invL =
(at_gc sweep_loop_check ( (❙¬NULL gc_mark ❙⟶ (λs. obj_at (λobj. Some (obj_mark obj) = gc_mark s) (gc_tmp_ref s) s))
❙∧ ( NULL gc_mark ❙∧ valid_ref ❙$ gc_tmp_ref ❙⟶ marked ❙$ gc_tmp_ref ) )
❙∧ at_gc sweep_loop_free ( ❙¬NULL gc_mark ❙∧ the ∘ gc_mark ❙≠ gc_fM ❙∧ (λs. obj_at (λobj. Some (obj_mark obj) = gc_mark s) (gc_tmp_ref s) s) )
❙∧ at_gc sweep_loop_ref_done (valid_ref ❙$ gc_tmp_ref ❙⟶ marked ❙$ gc_tmp_ref)
❙∧ atS_gc sweep_loop_locs (❙∀r. ❙¬⟨r⟩ ❙∈ gc_refs ❙∧ valid_ref r ❙⟶ marked r)
❙∧ atS_gc black_heap_locs (❙∀r. valid_ref r ❙⟶ marked r)
❙∧ atS_gc sweep_loop_not_choose_ref_locs (gc_tmp_ref ❙∈ gc_refs))"
text‹
For showing that the GC's use of @{const "mark_object_fn"} is correct.
When we take grey @{const "tmp_ref"} to black, all of the objects it
points to are marked, ergo the new black does not point to white, and
so we preserve the strong tricolour invariant.
›
definition obj_fields_marked :: "('field, 'mut, 'payload, 'ref) lsts_pred" where
"obj_fields_marked =
(❙∀f. ⟨f⟩ ❙∈ (- gc_field_set) ❙⟶ (λs. obj_at_field_on_heap (λr. marked r s) (gc_tmp_ref s) f s))"
locset_definition "mark_loop_mo_locs = prefixed ''mark_loop_mo''"
locset_definition "obj_fields_marked_good_ref_locs = mark_loop_mo_locs ∪ {mark_loop_mark_field_done}"
locset_definition
"ghost_honorary_grey_empty_locs =
(- { mark_loop_mo_co_unlock, mark_loop_mo_co_won, mark_loop_mo_co_W })"
locset_definition
"obj_fields_marked_locs =
{mark_loop_mark_object_loop, mark_loop_mark_choose_field, mark_loop_mark_deref, mark_loop_mark_field_done, mark_loop_blacken}
∪ mark_loop_mo_locs"
definition obj_fields_marked_invL :: "('field, 'mut, 'payload, 'ref) gc_pred" where
[inv]: "obj_fields_marked_invL =
(atS_gc obj_fields_marked_locs (obj_fields_marked ❙∧ gc_tmp_ref ❙∈ gc_W)
❙∧ atS_gc obj_fields_marked_good_ref_locs (λs. obj_at_field_on_heap (λr. gc_ref s = Some r ∨ marked r s) (gc_tmp_ref s) (gc_field s) s)
❙∧ atS_gc mark_loop_mo_locs (❙∀y. ❙¬NULL gc_ref ❙∧ (λs. ((gc_the_ref s) reaches y) s) ❙⟶ valid_ref y)
❙∧ at_gc mark_loop_fields (gc_tmp_ref ❙∈ gc_W)
❙∧ at_gc mark_loop_mark_field_done (❙¬NULL gc_ref ❙⟶ marked ❙$ gc_the_ref)
❙∧ at_gc mark_loop_blacken (EMPTY gc_field_set)
❙∧ atS_gc ghost_honorary_grey_empty_locs (EMPTY gc_ghost_honorary_grey))"
end
subsection‹ The local innvariants collected ›
definition (in gc) invsL :: "('field, 'mut, 'payload, 'ref) gc_pred" where
"invsL =
(fM_fA_invL
❙∧ gc_mark.mark_object_invL
❙∧ gc_W_empty_invL
❙∧ handshake_invL
❙∧ obj_fields_marked_invL
❙∧ phase_invL
❙∧ sweep_loop_invL
❙∧ tso_lock_invL)"
definition (in mut_m) invsL :: "('field, 'mut, 'payload, 'ref) gc_pred" where
"invsL =
(mark_object_invL
❙∧ mut_get_roots.mark_object_invL m
❙∧ mut_store_ins.mark_object_invL m
❙∧ mut_store_del.mark_object_invL m
❙∧ handshake_invL
❙∧ tso_lock_invL)"
definition invsL :: "('field, 'mut, 'payload, 'ref) gc_pred" where
"invsL = (gc.invsL ❙∧ (❙∀m. mut_m.invsL m))"
end