| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/ConcurrentGC/ (Archive of formal Proofs Version 2026-5©) Datei vom 29.4.2026 mit Größe 47 kB |
|
Quelle Model.thy Sprache: Isabelle |
|||||||||||||||||||||||||
|
(*<*) (* * Copyright 2015, NICTA * * This software may be distributed and modified according to the terms of * the BSD 2-Clause license. Note that NO WARRANTY is provided. * See "LICENSE_BSD2.txt" for details. * * @TAG(NICTA_BSD) *) theory Model imports ConcurrentIMP.CIMP "HOL-Library.Sublist" begin (* From 40e16c534243 by Makarius. Doesn't seem to have a huge impact on run time now (2021-01-07 declare subst_all [simp del] [[simproc del: defined_all]] (*>*) section‹A model of a Schism garbage collector \label{sec:gc-model}› text ‹ following formalises Figures~2.8 (‹mark_object_fn›), .9 (load and store but not alloc), and 2.15 (garbage collector) of 🚫‹"Pizlo201xPhd"›; see also 🚫‹"Pizlo+2010PLDI"›. additionally need to model TSO memory, the handshakes and -and-swap (\texttt{CAS}). We closely model things where is possible and abstract everything else. {bold ‹@{emph ‹NOTE›}: this model is for TSO emph{only}. We elide any details irrelevant for that memory .›} begin by defining the types of the various parts. Our program are labelled with strings for readability. We enumerate the of the processes in our system. The safety proof treats an (unbounded) number of mutators. › type_synonym location = string datatype 'mut process_name = mutator 'mut | gc | sys text ‹ garbage collection process can be in one of the following phases. › datatype gc_phase = ph_Idle | ph_Init | ph_Mark | ph_Sweep text ‹ garbage collector instructs mutators to perform certain actions, blocks until the mutators signal these actions are done. The always respond with their work list (a set of ). The handshake can be of one of the specified types. › datatype hs_type = ht_NOOP | ht_GetRoots | ht_GetWork text‹ track how many \texttt{noop} and \texttt{get\_roots} handshakes process has participated in as ghost state. See S\ref{sec:gc_handshakes}. › datatype hs_phase = hp_Idle ― ‹done 1 noop› | hp_IdleInit | hp_InitMark | hp_Mark ― ‹done 4 noops› | hp_IdleMarkSweep ― ‹done get roots› definition hs_step :: "hs_phase → hs_phase" where "hs_step ph = (case ph of hp_Idle → hp_IdleInit | hp_IdleInit → hp_InitMark | hp_InitMark → hp_Mark | hp_Mark → hp_IdleMarkSweep | hp_IdleMarkSweep → hp_Idle)" text ‹ object consists of a garbage collection mark and two partial . Firstly the types: ▪ @{typ "'field"} is the abstract type of fields. ▪ @{typ "'ref"} is the abstract type of object references. ▪ @{typ "'mut"} is the abstract type of the mutators' names. maps: ▪ ‹obj_fields› maps @{typ "'field"}s to object references (or @{const "None"} signifying \texttt{NULL} or type error). ▪ ‹obj_payload› maps a @{typ "'field"} to non-reference data. For convenience we similarly allow that to be \texttt{NULL}. › type_synonym gc_mark = bool record ('field, 'payload, 'ref) object = obj_mark :: "gc_mark" obj_fields :: "'field ⇀ 'ref" obj_payload :: "'field ⇀ 'payload" text‹ TSO store buffers track store actions, represented by ‹('field, 'ref) mem_store › datatype ('field, 'payload, 'ref) mem_store_action = mw_Mark 'ref gc_mark | mw_Mutate 'ref 'field "'ref option" | mw_Mutate_Payload 'ref 'field "'payload option" | mw_fA gc_mark | mw_fM gc_mark | mw_Phase gc_phase text‹ action is a request by a mutator or the garbage collector to the . › datatype ('field, 'ref) mem_load_action = mr_Ref 'ref 'field | mr_Payload 'ref 'field | mr_Mark 'ref | mr_Phase | mr_fM | mr_fA datatype ('field, 'mut, 'payload, 'ref) request_op = ro_MFENCE | ro_Load "('field, 'ref) mem_load_action" | ro_Store "('field, 'payload, 'ref) mem_store_action" | ro_Lock | ro_Unlock | ro_Alloc | ro_Free 'ref | ro_hs_gc_load_pending 'mut | ro_hs_gc_store_type hs_type | ro_hs_gc_store_pending 'mut | ro_hs_gc_load_W | ro_hs_mut_load_pending | ro_hs_mut_load_type | ro_hs_mut_done "'ref set" abbreviation "LoadfM ≡ ro_Load mr_fM" abbreviation "LoadMark r ≡ ro_Load (mr_Mark r)" abbreviation "LoadPayload r f ≡ ro_Load (mr_Payload r f)" abbreviation "LoadPhase ≡ ro_Load mr_Phase" abbreviation "LoadRef r f ≡ ro_Load (mr_Ref r f)" abbreviation "StorefA m ≡ ro_Store (mw_fA m)" abbreviation "StorefM m ≡ ro_Store (mw_fM m)" abbreviation "StoreMark r m ≡ ro_Store (mw_Mark r m)" abbreviation "StorePayload r f pl ≡ ro_Store (mw_Mutate_Payload r f pl)" abbreviation "StorePhase ph ≡ ro_Store (mw_Phase ph)" abbreviation "StoreRef r f r' ≡ ro_Store (mw_Mutate r f r')" type_synonym ('field, 'mut, 'payload, 'ref) request = "'mut process_name × ('field, 'mut, 'payload, 'ref) request_op" datatype ('field, 'payload, 'ref) response = mv_Bool "bool" | mv_Mark "gc_mark option" | mv_Payload "'payload option" ―‹ the requested reference might be invalid › | mv_Phase "gc_phase" | mv_Ref "'ref option" | mv_Refs "'ref set" | mv_Void | mv_hs_type hs_type text‹ following record is the type of all processes's local states. For mutators and the garbage collector, consider these to be local or registers. system's ‹fA›, ‹fM›, ‹phase› and ‹heap› variables are subject to the TSO memory . record ('field, 'mut, 'payload, 'ref) local_state = ― ‹System-specific fields› heap :: "'ref ⇀ ('field, 'payload, 'ref) object" ― ‹TSO memory state› mem_store_buffers :: "'mut process_name → ('field, 'payload, 'ref) mem_store_action mem_lock :: "'mut process_name option" ― ‹Handshake state› hs_pending :: "'mut → bool" ― ‹Ghost state› ghost_hs_in_sync :: "'mut → bool" ghost_hs_phase :: "hs_phase" ― ‹Mutator-specific temporaries› new_ref :: "'ref option" roots :: "'ref set" ghost_honorary_root :: "'ref set" payload_value :: "'payload option" mutator_data :: "'field ⇀ 'payload" mutator_hs_pending :: "bool" ― ‹Garbage collector-specific temporaries› field_set :: "'field set" mut :: "'mut" muts :: "'mut set" ― ‹Local variables used by multiple processes› fA :: "gc_mark" fM :: "gc_mark" cas_mark :: "gc_mark option" field :: "'field" mark :: "gc_mark option" phase :: "gc_phase" tmp_ref :: "'ref" ref :: "'ref option" refs :: "'ref set" W :: "'ref set" ― ‹Handshake state› hs_type :: "hs_type" ― ‹Ghost state› ghost_honorary_grey :: "'ref set" text‹We instantiate CIMP's types as follows:› type_synonym ('field, 'mut, 'payload, 'ref) gc_com = "(('field, 'payload, 'ref) response, location, ('field, 'mut, 'payload, 'ref) r type_synonym ('field, 'mut, 'payload, 'ref) gc_loc_comp = "(('field, 'payload, 'ref) response, location, ('field, 'mut, 'payload, 'ref) r type_synonym ('field, 'mut, 'payload, 'ref) gc_pred = "(('field, 'payload, 'ref) response, location, 'mut process_name, ('field, 'mut type_synonym ('field, 'mut, 'payload, 'ref) gc_system = "(('field, 'payload, 'ref) response, location, 'mut process_name, ('field, 'mut type_synonym ('field, 'mut, 'payload, 'ref) gc_event = "('field, 'mut, 'payload, 'ref) request × ('field, 'payload, 'ref) response" type_synonym ('field, 'mut, 'payload, 'ref) gc_history = "('field, 'mut, 'payload, 'ref) gc_event list" type_synonym ('field, 'mut, 'payload, 'ref) lst_pred = "('field, 'mut, 'payload, 'ref) local_state → bool" type_synonym ('field, 'mut, 'payload, 'ref) lsts = "'mut process_name → ('field, 'mut, 'payload, 'ref) local_state" type_synonym ('field, 'mut, 'payload, 'ref) lsts_pred = "('field, 'mut, 'payload, 'ref) lsts → bool" text‹ use one locale per process to define a namespace for definitions to these processes. Mutator definitions are parametrised by the 's identifier ‹m›. We never interpret these locales; we use their contents by prefixing identifiers with the locale . This might be considered an abuse. The attributes depend on scoping somewhat, which is a mixed blessing. we have more than one mutator then we need to show that mutators do mutually interfere. To that end we define an extra locale that these proofs. › locale mut_m = fixes m :: "'mut" locale mut_m' = mut_m + fixes m' :: "'mut" assumes mm'[iff]: "m ≠ m'" locale gc locale sys subsection‹Object marking \label{sec:gc-marking}› text‹ the mutators and the garbage collector mark references, which that a reference is live in the current round of . This operation is defined in 🚫‹‹Figure~2.8› in "Pizlo201xPhd"›. These definit by the name of the process. context fixes p :: "'mut process_name" begin abbreviation lock_syn :: "location → ('field, 'mut, 'payload, 'ref) gc_com" where "lock_syn l ≡ {l} Request (λs. (p, ro_Lock)) (λ_ s. {s})" notation lock_syn (‹{_} lock›) abbreviation unlock_syn :: "location → ('field, 'mut, 'payload, 'ref) gc_com" where "unlock_syn l ≡ {l} Request (λs. (p, ro_Unlock)) (λ_ s. {s})" notation unlock_syn (‹{_} unlock›) abbreviation load_mark_syn :: "location → (('field, 'mut, 'payload, 'ref) local_state → 'ref) → ((gc_mark option → gc_mark option) → ('field, 'mut, 'payload, 'ref) local_state → ('field, 'mut, 'payload, 'ref) local_state) → ('field, 'mut, 'payload, 'ref) gc_ where "load_mark_syn l r upd ≡ {l} Request (λs. (p, LoadMark (r s))) (λmv s. { upd ⟨m⟩ s | notation load_mark_syn (‹{_} load'_mark›) abbreviation load_fM_syn :: "location → ('field, 'mut, 'payload, 'ref) gc_com" where "load_fM_syn l ≡ {l} Request (λs. (p, ro_Load mr_fM)) (λmv s. { s(fM := m) |m. mv = notation load_fM_syn (‹{_} load'_fM›) abbreviation load_phase :: "location → ('field, 'mut, 'payload, 'ref) gc_com" where "load_phase l ≡ {l} Request (λs. (p, LoadPhase)) (λmv s. { s(phase := ph) |ph. mv = notation load_phase (‹{_} load'_phase›) abbreviation store_mark_syn :: "location → (('field, 'mut, 'payload, 'ref) local_state → 'ref) → ( where "store_mark_syn l r fl ≡ {l} Request (λs. (p, StoreMark (r s) (fl s))) (λ_ s. { s( notation store_mark_syn (‹{_} store'_mark›) abbreviation add_to_W_syn :: "location → (('field, 'mut, 'payload, 'ref) local_state → 'ref) → ('f where "add_to_W_syn l r ≡ {l} ⌊λs. s( W := W s ∪ {r s}, ghost_honorary_grey := {} )⌋" notation add_to_W_syn (‹{_} add'_to'_W›) text‹ reference we're marking is given in @{const "ref"}. If the current wins the \texttt{CAS} race then the reference is marked and to the local work list @{const "W"}. means we cannot avoid having the mark store pending in a store ; in other words, we cannot have objects atomically transition white to grey. The following scheme blackens a white object, and reverts it to grey. The @{const "ghost_honorary_grey"} variable used to track objects undergoing this transition. CIMP provides no support for function calls, we prefix each 's label with a string from its callsite. › definition mark_object_fn :: "location → ('field, 'mut, 'payload, 'ref) gc_com" where "mark_object_fn l = {l @ ''_mo_null''} IF \<not> (NULL ref) THEN {l @ ''_mo_mark''} load_mark (the ∘ ref) mark_update ;; {l @ ''_mo_fM''} load_fM ;; {l @ ''_mo_mtest''} IF mark \<noteq> Some ∘ fM THEN {l @ ''_mo_phase''} load_phase ;; {l @ ''_mo_ptest''} IF phase \<noteq> ⟨ph_Idle⟩ THEN ― ‹CAS: claim object› {l @ ''_mo_co_lock''} lock ;; {l @ ''_mo_co_cmark''} load_mark (the ∘ ref) cas_mark_update ;; {l @ ''_mo_co_ctest''} IF cas_mark = mark THEN {l @ ''_mo_co_mark''} store_mark (the ∘ ref) fM FI ;; {l @ ''_mo_co_unlock''} unlock ;; {l @ ''_mo_co_won''} IF cas_mark = mark THEN {l @ ''_mo_co_W''} add_to_W (the ∘ ref) FI FI FI FI" end text‹ worklists (field @{term "W"}) are not subject to TSO. As we later (\S\ref{def:valid_W_inv}), these are disjoint and hence on these are private to each process, with the sole of when the GC requests them from the mutators. We describe mechanism next. › subsection‹Handshakes \label{sec:gc_handshakes}› text‹ garbage collector needs to synchronise with the mutators. we do so by having the GC busy-wait: it sets a ‹pending› flag for each mutator then waits for each to respond. system side of the interface collects the responses from the into a single worklist, which acts as a proxy for the garbage 's local worklist during ‹get_roots› and ‹get_work› handshakes. carefully model the effect these handshakes have on the processes' TSO buffers. system and mutators track handshake phases using ghost state; see S\ref{sec:phase-invariants}. handshake type and handshake pending bit are not subject to TSO as we expect realistic implementation of handshakes would involve synchronisation. › abbreviation hp_step :: "hs_type → hs_phase → hs_phase" where "hp_step ht ≡ case ht of ht_NOOP → hs_step | ht_GetRoots → hs_step | ht_GetWork → id" context sys begin definition handshake :: "('field, 'mut, 'payload, 'ref) gc_com" where "handshake = {''sys_hs_gc_set_type''} Response (λreq s. { (s( hs_type := ht, ghost_hs_in_sync := ⟨False⟩, ghost_hs_phase := hp_step ht (ghost_hs_phase s) ), mv_Void) |ht. req = (gc, ro_hs_gc_store_type ht) }) ⊕ {''sys_hs_gc_mut_reqs''} Response (λreq s. { (s( hs_pending := (hs_pending s)(m := True) ), mv_Void) |m. req = (gc, ro_hs_gc_store_pending m) }) ⊕ {''sys_hs_gc_done''} Response (λreq s. { (s, mv_Bool (¬hs_pending s m)) |m. req = (gc, ro_hs_gc_load_pending m) }) ⊕ {''sys_hs_gc_load_W''} Response (λreq s. { (s( W := {} ), mv_Refs (W s)) |_::unit. req = (gc, ro_hs_gc_load_W) }) ⊕ {''sys_hs_mut_pending''} Response (λreq s. { (s, mv_Bool (hs_pending s m)) |m. req = (mutator m, ro_hs_mut_load_pending) }) ⊕ {''sys_hs_mut''} Response (λreq s. { (s, mv_hs_type (hs_type s)) |m. req = (mutator m, ro_hs_mut_load_type) }) ⊕ {''sys_hs_mut_done''} Response (λreq s. { (s( hs_pending := (hs_pending s)(m := False), W := W s ∪ W', ghost_hs_in_sync := (ghost_hs_in_sync s)(m := True) ), mv_Void) |m W'. req = (mutator m, ro_hs_mut_done W') })" end text‹ mutators' side of the interface. Also updates the ghost state the handshake state for @{const "ht_NOOP"} and @{const ht_GetRoots"} but not @{const "ht_GetWork"}. we could make these subject to TSO, but that would be over specification. › context mut_m begin abbreviation mark_object_syn :: "location → ('field, 'mut, 'payload, 'ref) gc_com" (‹ "{l} mark_object ≡ mark_object_fn (mutator m) l" abbreviation mfence_syn :: "location → ('field, 'mut, 'payload, 'ref) gc_com" (‹{_} M "{l} MFENCE ≡ {l} Request (λs. (mutator m, ro_MFENCE)) (λ_ s. {s})" abbreviation hs_load_pending_syn :: "location → ('field, 'mut, 'payload, 'ref) gc_co "{l} hs_load_pending_ ≡ {l} Request (λs. (mutator m, ro_hs_mut_load_pending)) (λmv abbreviation hs_load_type_syn :: "location → ('field, 'mut, 'payload, 'ref) gc_com" ( "{l} hs_load_type ≡ {l} Request (λs. (mutator m, ro_hs_mut_load_type)) (λmv s. { s( abbreviation hs_noop_done_syn :: "location → ('field, 'mut, 'payload, 'ref) gc_com" ( "{l} hs_noop_done_ ≡ {l} Request (λs. (mutator m, ro_hs_mut_done {})) (λ_ s. {s( ghost_hs_phase := hs_step (ghost_hs_phase s) )})" abbreviation hs_get_roots_done_syn :: "location → (('field, 'mut, 'payload, 'ref) lo "{l} hs_get_roots_done_ wl ≡ {l} Request (λs. (mutator m, ro_hs_mut_done (wl s))) (λ_ s. {s( W := {}, ghost_hs_phase := hs_step (ghost_hs_phase s) )})" abbreviation hs_get_work_done_syn :: "location → (('field, 'mut, 'payload, 'ref) loc "{l} hs_get_work_done wl ≡ {l} Request (λs. (mutator m, ro_hs_mut_done (wl s))) (λ_ s. {s( W := {} )})" definition handshake :: "('field, 'mut, 'payload, 'ref) gc_com" where "handshake = {''hs_load_pending''} hs_load_pending_ ;; {''hs_pending''} IF mutator_hs_pending THEN {''hs_mfence''} MFENCE ;; {''hs_load_ht''} hs_load_type ;; {''hs_noop''} IF hs_type = ⟨ht_NOOP⟩ THEN {''hs_noop_done''} hs_noop_done_ ELSE {''hs_get_roots''} IF hs_type = ⟨ht_GetRoots⟩ THEN {''hs_get_roots_refs''} 🚫refs := 🚫roots ;; {''hs_get_roots_loop''} WHILE \<not>EMPTY refs DO {''hs_get_roots_loop_choose_ref''} 🚫ref :∈ Some ` 🚫refs ;; {''hs_get_roots_loop''} mark_object ;; {''hs_get_roots_loop_done''} 🚫refs := (🚫refs - {the 🚫ref}) OD ;; {''hs_get_roots_done''} hs_get_roots_done_ W ELSE {''hs_get_work''} IF hs_type = ⟨ht_GetWork⟩ THEN {''hs_get_work_done''} hs_get_work_done W FI FI FI FI" end text‹ garbage collector's side of the interface. › context gc begin abbreviation set_hs_type :: "location → hs_type → ('field, 'mut, 'payload, 'ref) gc_c "{l} set_hs_type ht ≡ {l} Request (λs. (gc, ro_hs_gc_store_type ht)) (λ_ s. {s})" abbreviation set_hs_pending :: "location → (('field, 'mut, 'payload, 'ref) local_sta "{l} set_hs_pending m ≡ {l} Request (λs. (gc, ro_hs_gc_store_pending (m s))) (λ_ s abbreviation load_W :: "location → ('field, 'mut, 'payload, 'ref) gc_com" (‹{_} load' "{l} load_W ≡ {l @ ''_load_W''} Request (λs. (gc, ro_hs_gc_load_W)) (λresp s. {s(W := W') |W'. resp = mv_Refs W'})" abbreviation mfence :: "location → ('field, 'mut, 'payload, 'ref) gc_com" (‹{_} MFENC "{l} MFENCE ≡ {l} Request (λs. (gc, ro_MFENCE)) (λ_ s. {s})" definition handshake_init :: "location → hs_type → ('field, 'mut, 'payload, 'ref) gc_com" (‹{_} where "{l} handshake_init req = {l @ ''_init_type''} set_hs_type req ;; {l @ ''_init_muts''} 🚫muts := UNIV ;; {l @ ''_init_loop''} WHILE \<not> (EMPTY muts) DO {l @ ''_init_loop_choose_mut''} 🚫mut :∈ 🚫muts ;; {l @ ''_init_loop_set_pending''} set_hs_pending mut ;; {l @ ''_init_loop_done''} 🚫muts := (🚫muts - {🚫mut}) OD" definition handshake_done :: "location → ('field, 'mut, 'payload, 'ref) gc_com" (‹{_} handshake where "{l} handshake_done = {l @ ''_done_muts''} 🚫muts := UNIV ;; \<lbrace>l @ ''_done_loop''\<rbrace> WHILE \<^bold>\<not>EMPTY muts DO \<lbrace>l @ ''_done_loop_choose_mut''\<rbrace> \<acute>mut :\<in> \<acute>muts ;; \<lbrace>l @ ''_done_loop_rendezvous''\<rbrace> Request (\<lambda>s. (gc, ro_hs_gc_load_pending (mut s))) (\<lambda>mv s. { s\<lparr> muts := muts s - { mut s |done. mv = mv_Bool done \<and> done } \<rparr>}) OD" definition handshake_noop :: "location \<Rightarrow> ('field, 'mut, 'payload, 'ref) gc_com" (\<open>\<lbr where "\<lbrace>l\<rbrace> handshake_noop = \<lbrace>l @ ''_mfence''\<rbrace> MFENCE ;; \<lbrace>l\<rbrace> handshake_init ht_NOOP ;; \<lbrace>l\<rbrace> handshake_done" definition handshake_get_roots :: "location \<Rightarrow> ('field, 'mut, 'payload, 'ref) gc_com" (\<ope where "\<lbrace>l\<rbrace> handshake_get_roots = \<lbrace>l\<rbrace> handshake_init ht_GetRoots ;; \<lbrace>l\<rbrace> handshake_done ;; \<lbrace>l\<rbrace> load_W" definition handshake_get_work :: "location \<Rightarrow> ('field, 'mut, 'payload, 'ref) gc_com" (\<open> where "\<lbrace>l\<rbrace> handshake_get_work = \<lbrace>l\<rbrace> handshake_init ht_GetWork ;; \<lbrace>l\<rbrace> handshake_done ;; \<lbrace>l\<rbrace> load_W" end subsection\<open>The system process\<close> text \<open> The system process models the environment in which the garbage collector and mutators execute. We translate the x86-TSO memory model due to \<^citet>\<open>"DBLP:journals/cacm/SewellSONM10"\<close> into a CIMP process. It is a reactive system: it receives requests and returns values, but initiates no communication itself. It can, however, autonomously commit a store pending in a TSO store buffer. The memory bus can be locked by atomic compare-and-swap (\texttt{CAS}) instructions (and others in general). A processor is not blocked (i.e., it can read from memory) when it holds the lock, or no-one does. \<close> definition not_blocked :: "('field, 'mut, 'payload, 'ref) local_state \<Rightarrow> 'mut process_name \< where "not_blocked s p = (case mem_lock s of None \<Rightarrow> True | Some p' \<Rightarrow> p = p')" text\<open> We compute the view a processor has of memory by applying all its pending stores. \<close> definition do_store_action :: "('field, 'payload, 'ref) mem_store_action \<Rightarrow> ('field, 'mut, where "do_store_action wact = (\<lambda>s. case wact of mw_Mark r gc_mark \<Rightarrow> s\<lparr>heap := (heap s)(r := map_option (\<lambda>obj. obj\<lpar | mw_Mutate r f new_r \<Rightarrow> s\<lparr>heap := (heap s)(r := map_option (\<lambda>obj. obj\<lp | mw_Mutate_Payload r f pl \<Rightarrow> s\<lparr>heap := (heap s)(r := map_option (\<lambda>obj. o | mw_fM gc_mark \<Rightarrow> s\<lparr>fM := gc_mark\<rparr> | mw_fA gc_mark \<Rightarrow> s\<lparr>fA := gc_mark\<rparr> | mw_Phase gc_phase \<Rightarrow> s\<lparr>phase := gc_phase\<rparr>)" definition fold_stores :: "('field, 'payload, 'ref) mem_store_action list \<Rightarrow> ('field, 'mut, where "fold_stores ws = fold (\<lambda>w. (\<circ>) (do_store_action w)) ws id" abbreviation processors_view_of_memory :: "'mut process_name \<Rightarrow> ('field, 'mut, 'payload, 're where "processors_view_of_memory p s \<equiv> fold_stores (mem_store_buffers s p) s" definition do_load_action :: "('field, 'ref) mem_load_action \<Rightarrow> ('field, 'mut, 'payload, 'ref) local_state \<Rightarrow> ('field, 'payload, 'ref) response" where "do_load_action ract = (\<lambda>s. case ract of mr_Ref r f \<Rightarrow> mv_Ref (Option.bind (heap s r) (\<lambda>obj. obj_fields obj f)) | mr_Payload r f \<Rightarrow> mv_Payload (Option.bind (heap s r) (\<lambda>obj. obj_payload obj | mr_Mark r \<Rightarrow> mv_Mark (map_option obj_mark (heap s r)) | mr_Phase \<Rightarrow> mv_Phase (phase s) | mr_fM \<Rightarrow> mv_Mark (Some (fM s)) | mr_fA \<Rightarrow> mv_Mark (Some (fA s)))" definition sys_load :: "'mut process_name \<Rightarrow> ('field, 'ref) mem_load_action \<Rightarrow> ('field, 'mut, 'payload, 'ref) local_state \<Rightarrow> ('field, 'payload, 'ref) response" where "sys_load p ract = do_load_action ract \<circ> processors_view_of_memory p" context sys begin text\<open> The semantics of TSO memory following \<^citet>\<open>\<open>\S3\<close> in "DBLP:journals/cacm/ from the earlier \<^citet>\<open>"DBLP:conf/tphol/OwensSS09"\<close> by allowing the TSO lock t process with a non-empty store buffer. We omit their treatment of registers; these are handled by the local states of the other processes. The system can autonomously take the oldest store in the store buffer for processor \<open>p\<close> and commit it to memory, provided \<open>p\<close> either holds the lock or no processor does. \<close> definition mem_TSO :: "('field, 'mut, 'payload, 'ref) gc_com" where "mem_TSO = \<lbrace>''tso_load''\<rbrace> Response (\<lambda>req s. { (s, sys_load p mr s) |p mr. req = (p, ro_Load mr) \<and> not_blocked s p }) \<oplus> \<lbrace>''tso_store''\<rbrace> Response (\<lambda>req s. { (s\<lparr> mem_store_buffers |p w. req = (p, ro_Store w) }) \<oplus> \<lbrace>''tso_mfence''\<rbrace> Response (\<lambda>req s. { (s, mv_Void) |p. req = (p, ro_MFENCE) \<and> mem_store_buffers s p = [] }) \<oplus> \<lbrace>''tso_lock''\<rbrace> Response (\<lambda>req s. { (s\<lparr> mem_lock := Some p \<rp |p. req = (p, ro_Lock) \<and> mem_lock s = None }) \<oplus> \<lbrace>''tso_unlock''\<rbrace> Response (\<lambda>req s. { (s\<lparr> mem_lock := None \<r |p. req = (p, ro_Unlock) \<and> mem_lock s = Some p \<and> mem_store_buffers s p = [] }) \<oplus> \<lbrace>''tso_dequeue_store_buffer''\<rbrace> LocalOp (\<lambda>s. { (do_store_acti | p w ws. mem_store_buffers s p = w # ws \<and> not_blocked s p \<and> p \<noteq> sys })" text\<open> We track which references are allocated using the domain of @{const "heap"}. \label{sec:sys_alloc} For now we assume that the system process magically allocates and deallocates references. We also arrange for the object to be marked atomically (see \S\ref{sec:mut_alloc}) which morally should be done by the mutator. In practice allocation pools enable this kind of atomicity (wrt the sweep loop in the GC described in \S\ref{sec:gc-model-gc}). Note that the \texttt{abort} in \<^citet>\<open>\<open>Figure~2.9: Alloc\<close> in "Pizlo201xPh fails and the mutator can revert to activity outside of \texttt{Alloc}, avoiding deadlock. We instead signal the exhaustion of the heap explicitly, i.e., the @{const "ro_Alloc"} action cannot fail. \<close> definition alloc :: "('field, 'mut, 'payload, 'ref) gc_com" where "alloc = \<lbrace>''alloc''\<rbrace> Response (\<lambda>req s. if dom (heap s) = UNIV then {(s, mv_Ref None) |_::unit. snd req = ro_Alloc } else { ( s\<lparr> heap := (heap s)(r := Some \<lparr> obj_mark = fA s, obj_fields = Map.empty, obj_pa |r. r \<notin> dom (heap s) \<and> snd req = ro_Alloc })" text\<open> References are freed by removing them from @{const "heap"}. \<close> definition free :: "('field, 'mut, 'payload, 'ref) gc_com" where "free = \<lbrace>''sys_free''\<rbrace> Response (\<lambda>req s. { (s\<lparr>heap := (heap s)(r := None)\<rparr>, mv_Void) |r. snd req = ro_Free r })" text\<open> The top-level system process. \<close> definition com :: "('field, 'mut, 'payload, 'ref) gc_com" where "com = LOOP DO mem_TSO \<oplus> alloc \<oplus> free \<oplus> handshake OD" end subsection\<open>Mutators\<close> text\<open> The mutators need to cooperate with the garbage collector. In particular, when the garbage collector is not idle the mutators use a \emph{write barrier} (see \S\ref{sec:gc-marking}). The local state for each mutator tracks a working set of references, which abstracts from how the process's registers and stack are traversed to discover roots. \<close> context mut_m begin text\<open> \label{sec:mut_alloc} Allocation is defined in \<^citet>\<open>\<open>Figure~2.9\<close> in "Pizlo201xPhd"\<close>. See for how we abstract it. \<close> abbreviation alloc :: "('field, 'mut, 'payload, 'ref) gc_com" where "alloc \<equiv> \<lbrace>''alloc''\<rbrace> Request (\<lambda>s. (mutator m, ro_Alloc)) (\<lambda>mv s. { s\<lparr> roots := roots s \<union> set_option opt_r \<rparr> |opt_r. mv = mv_Ref opt_ text\<open> The mutator can always discard any references it holds. \<close> abbreviation discard :: "('field, 'mut, 'payload, 'ref) gc_com" where "discard \<equiv> \<lbrace>''discard_refs''\<rbrace> LocalOp (\<lambda>s. { s\<lparr> roots := roots' \<rparr> |roots text\<open> Load and store are defined in \<^citet>\<open>\<open>Figure~2.9\<close> in "Pizlo201xPhd"\<close>. Dereferencing a reference can increase the set of mutator roots. \<close> abbreviation load :: "('field, 'mut, 'payload, 'ref) gc_com" where "load \<equiv> \<lbrace>''mut_load_choose''\<rbrace> LocalOp (\<lambda>s. { s\<lparr> tmp_ref := r, field := f \<rp \<lbrace>''mut_load''\<rbrace> Request (\<lambda>s. (mutator m, LoadRef (tmp_ref s) (field s))) (\<lambda>mv s. { s\<lparr> roots := roots s \<union> set_option r \<rparr> |r. mv = mv_Ref r })" text\<open> \label{sec:write-barriers} Storing a reference involves marking both the old and new references, i.e., both \emph{insertion} and \emph{deletion} barriers are installed. The deletion barrier preserves the \emph{weak tricolour invariant}, and the insertion barrier preserves the \emph{strong tricolour invariant}; see \S\ref{sec:strong-tricolour-invariant} for further discussion. Note that the the mutator reads the overwritten reference but does not store it in its roots. \<close> abbreviation mut_deref :: "location \<Rightarrow> (('field, 'mut, 'payload, 'ref) local_state \<Rightarrow> 'ref) \<Rightarrow> (('field, 'mut, 'payload, 'ref) local_state \<Rightarrow> 'field) \<Rightarrow> (('ref option \<Rightarrow> 'ref option) \<Rightarrow> ('field, 'mut, 'payload, 'r where "\<lbrace>l\<rbrace> deref r f upd \<equiv> \<lbrace>l\<rbrace> Request (\<lambda>s. (mutator m, LoadRe (\<lambda>mv s. { upd \<langle>opt_r'\<rangle> (s\<lparr>ghost_honorary_root := set_option opt_r (* Does not work in local theory mode: syntax "_mut_fassign" :: "location \<Rightarrow> idt \<Rightarrow> 'ref \<Rightarrow> 'field \<Rightarr translations "\<lbrace>l\<rbrace> \<acute>q := \<acute>r\<rightarrow>f" => "CONST mut_deref l r \<guillemotleft>f\<g \<acute>ref := \<acute>tmp_ref\<rightarrow>\<acute>field ;; *) abbreviation store_ref :: "location \<Rightarrow> (('field, 'mut, 'payload, 'ref) local_state \<Rightarrow> 'ref) \<Rightarrow> (('field, 'mut, 'payload, 'ref) local_state \<Rightarrow> 'field) \<Rightarrow> (('field, 'mut, 'payload, 'ref) local_state \<Rightarrow> 'ref option) \<Rightarrow> ('field, 'mut, 'payload, 'ref) gc_com" (\<open>\<lbrace>_\<rbrace> store'_ref\<clo where "\<lbrace>l\<rbrace> store_ref r f r' \<equiv> \<lbrace>l\<rbrace> Request (\<lambda>s. (mutator m, Sto definition store :: "('field, 'mut, 'payload, 'ref) gc_com" where "store = \<comment> \<open>Choose vars for \<open>ref\<rightarrow>field := new_ref\<close>\<close> \<lbrace>''store_choose''\<rbrace> LocalOp (\<lambda>s. { s\<lparr> tmp_ref := r, field := f, new_r |r f r'. r \<in> roots s \<and> r' \<in> Some ` roots s \<union> {None} }) ;; \<comment> \<open>Mark the reference we're about to overwrite. Does not update roots.\<close> \<lbrace>''deref_del''\<rbrace> deref tmp_ref field ref_update ;; \<lbrace>''store_del''\<rbrace> mark_object ;; \<comment> \<open>Mark the reference we're about to insert.\<close> \<lbrace>''lop_store_ins''\<rbrace> \<acute>ref := \<acute>new_ref ;; \<lbrace>''store_ins''\<rbrace> mark_object ;; \<lbrace>''store_ins''\<rbrace> store_ref tmp_ref field new_ref" text\<open> Load and store payload data. \<close> abbreviation load_payload :: "('field, 'mut, 'payload, 'ref) gc_com" where "load_payload \<equiv> \<lbrace>''mut_load_payload_choose''\<rbrace> LocalOp (\<lambda>s. { s\<lparr> tmp_ref := r, fie \<lbrace>''mut_load_payload''\<rbrace> Request (\<lambda>s. (mutator m, LoadPayload (tmp_ref (\<lambda>mv s. { s\<lparr> mutator_data := (mutator_data s)(var := pl) \<rparr> |var pl. mv = mv_Payload pl })" abbreviation store_payload :: "('field, 'mut, 'payload, 'ref) gc_com" where "store_payload \<equiv> \<lbrace>''mut_store_payload_choose''\<rbrace> LocalOp (\<lambda>s. { s\<lparr> tmp_ref := r, fi \<lbrace>''mut_store_payload''\<rbrace> Request (\<lambda>s. (mutator m, StorePayload (tmp_r (\<lambda>mv s. { s\<lparr> mutator_data := (mutator_data s)(f := pl) \<rparr> |f pl. mv = mv_Payload pl })" text\<open> A mutator makes a non-deterministic choice amongst its possible actions. For completeness we allow mutators to issue \texttt{MFENCE} instructions. We leave \texttt{CAS} (etc) to future work. Neither has a significant impact on the rest of the development. \<close> (* FIXME add SKIP before alloc, mfence. handshake needs work too: want to commit to checking for handshakes in a strongly fair way. A SKIP at the top level of \<open>handshake\<close> + a noop transition + appropriate fairness constrain FIXME is mut local computation strong enough? only works on mutator data; not roots. *) definition com :: "('field, 'mut, 'payload, 'ref) gc_com" where "com = LOOP DO \<lbrace>''mut_local_computation''\<rbrace> LocalOp (\<lambda>s. {s\<lparr>mutator_data := f ( \<oplus> alloc \<oplus> discard \<oplus> load \<oplus> store \<oplus> load_payload \<oplus> store_payload \<oplus> \<lbrace>''mut_mfence''\<rbrace> MFENCE \<oplus> handshake OD" end subsection \<open>Garbage collector \label{sec:gc-model-gc}\<close> text\<open> We abstract the primitive actions of the garbage collector thread. \<close> abbreviation gc_deref :: "location \<Rightarrow> (('field, 'mut, 'payload, 'ref) local_state \<Rightarrow> 'ref) \<Rightarrow> (('field, 'mut, 'payload, 'ref) local_state \<Rightarrow> 'field) \<Rightarrow> (('ref option \<Rightarrow> 'ref option) \<Rightarrow> ('field, 'mut, 'payload, 'r where "gc_deref l r f upd \<equiv> \<lbrace>l\<rbrace> Request (\<lambda>s. (gc, LoadRef (r s) (f s))) (\<lambda>mv s. { upd \<langle>r'\<rangle> s |r'. mv = mv_Ref r' })" abbreviation gc_load_mark :: "location \<Rightarrow> (('field, 'mut, 'payload, 'ref) local_state \<Rightarrow> 'ref) \<Rightarrow> ((gc_mark option \<Rightarrow> gc_mark option) \<Rightarrow> ('field, 'mut, 'payl \<Rightarrow> ('field, 'mut, 'payload, 'ref) gc_com" where "gc_load_mark l r upd \<equiv> \<lbrace>l\<rbrace> Request (\<lambda>s. (gc, LoadMark (r s))) (\<lamb syntax "_gc_fassign" :: "location \<Rightarrow> idt \<Rightarrow> 'ref \<Rightarrow> 'field \<Rightarro "_gc_massign" :: "location \<Rightarrow> idt \<Rightarrow> 'ref \<Rightarrow> ('field, 'mut, 'pa syntax_consts "_gc_fassign" \<rightleftharpoons> gc_deref and "_gc_massign" \<rightleftharpoons> gc_load_mark translations "\<lbrace>l\<rbrace> \<acute>q := \<acute>r\<rightarrow>f" => "CONST gc_deref l r \<guillemotleft>f\<gu "\<lbrace>l\<rbrace> \<acute>m := \<acute>r\<rightarrow>flag" => "CONST gc_load_mark l r (_update_na context gc begin abbreviation store_fA_syn :: "location \<Rightarrow> (('field, 'mut, 'payload, 'ref) local_ "\<lbrace>l\<rbrace> store_fA f \<equiv> \<lbrace>l\<rbrace> Request (\<lambda>s. (gc, StorefA (f s))) abbreviation load_fM_syn :: "location \<Rightarrow> ('field, 'mut, 'payload, 'ref) gc_com" ( "\<lbrace>l\<rbrace> load_fM \<equiv> \<lbrace>l\<rbrace> Request (\<lambda>s. (gc, LoadfM)) (\<lambd abbreviation store_fM_syn :: "location \<Rightarrow> ('field, 'mut, 'payload, 'ref) gc_com" "\<lbrace>l\<rbrace> store_fM \<equiv> \<lbrace>l\<rbrace> Request (\<lambda>s. (gc, StorefM (fM s))) abbreviation store_phase_syn :: "location \<Rightarrow> gc_phase \<Rightarrow> ('field, 'mut "\<lbrace>l\<rbrace> store_phase ph \<equiv> \<lbrace>l\<rbrace> Request (\<lambda>s. (gc, StorePhas abbreviation mark_object_syn :: "location \<Rightarrow> ('field, 'mut, 'payload, 'ref) gc_c "\<lbrace>l\<rbrace> mark_object \<equiv> mark_object_fn gc l" abbreviation free_syn :: "location \<Rightarrow> (('field, 'mut, 'payload, 'ref) local_stat "\<lbrace>l\<rbrace> free r \<equiv> \<lbrace>l\<rbrace> Request (\<lambda>s. (gc, ro_Free (r s))) (\<la text\<open> The following CIMP program encodes the garbage collector algorithm proposed in Figure~2.15 of \<^citet>\<open>"Pizlo201xPhd"\<close>. \<close> definition (in gc) com :: "('field, 'mut, 'payload, 'ref) gc_com" where "com = LOOP DO \<lbrace>''idle_noop''\<rbrace> handshake_noop ;; \<comment> \<open>\<open>hp_Idle\<close>\<close> \<lbrace>''idle_load_fM''\<rbrace> load_fM ;; \<lbrace>''idle_invert_fM''\<rbrace> \<acute>fM := (\<not> \<acute>fM) ;; \<lbrace>''idle_store_fM''\<rbrace> store_fM ;; \<lbrace>''idle_flip_noop''\<rbrace> handshake_noop ;; \<comment> \<open>\<open>hp_IdleInit\<cl \<lbrace>''idle_phase_init''\<rbrace> store_phase ph_Init ;; \<lbrace>''init_noop''\<rbrace> handshake_noop ;; \<comment> \<open>\<open>hp_InitMark\<close>\<c \<lbrace>''init_phase_mark''\<rbrace> store_phase ph_Mark ;; \<lbrace>''mark_load_fM''\<rbrace> load_fM ;; \<lbrace>''mark_store_fA''\<rbrace> store_fA fM ;; \<lbrace>''mark_noop''\<rbrace> handshake_noop ;; \<comment> \<open>\<open>hp_Mark\<close>\<close> \<lbrace>''mark_loop_get_roots''\<rbrace> handshake_get_roots ;; \<comment> \<open>\<open>hp_I \<lbrace>''mark_loop''\<rbrace> WHILE \<^bold>\<not>EMPTY W DO \<lbrace>''mark_loop_inner''\<rbrace> WHILE \<^bold>\<not>EMPTY W DO \<lbrace>''mark_loop_choose_ref''\<rbrace> \<acute>tmp_ref :\<in> \<acute>W ;; \<lbrace>''mark_loop_fields''\<rbrace> \<acute>field_set := UNIV ;; \<lbrace>''mark_loop_mark_object_loop''\<rbrace> WHILE \<^bold>\<not>EMPTY field_set DO \<lbrace>''mark_loop_mark_choose_field''\<rbrace> \<acute>field :\<in> \<acute>field_set ;; \<lbrace>''mark_loop_mark_deref''\<rbrace> \<acute>ref := \<acute>tmp_ref\<rightarrow>\<acute>f \<lbrace>''mark_loop''\<rbrace> mark_object ;; \<lbrace>''mark_loop_mark_field_done''\<rbrace> \<acute>field_set := (\<acute>field_set - {\<a OD ;; \<lbrace>''mark_loop_blacken''\<rbrace> \<acute>W := (\<acute>W - {\<acute>tmp_ref}) OD ;; \<lbrace>''mark_loop_get_work''\<rbrace> handshake_get_work OD ;; \<comment> \<open>sweep\<close> \<lbrace>''mark_end''\<rbrace> store_phase ph_Sweep ;; \<lbrace>''sweep_load_fM''\<rbrace> load_fM ;; \<lbrace>''sweep_refs''\<rbrace> \<acute>refs := UNIV ;; \<lbrace>''sweep_loop''\<rbrace> WHILE \<^bold>\<not>EMPTY refs DO \<lbrace>''sweep_loop_choose_ref''\<rbrace> \<acute>tmp_ref :\<in> \<acute>refs ;; \<lbrace>''sweep_loop_load_mark''\<rbrace> \<acute>mark := \<acute>tmp_ref\<rightarrow>flag ;; \<lbrace>''sweep_loop_check''\<rbrace> IF \<^bold>\<not>NULL mark \<^bold>\<and> the \<circ> mark \<^bo \<lbrace>''sweep_loop_free''\<rbrace> free tmp_ref FI ;; \<lbrace>''sweep_loop_ref_done''\<rbrace> \<acute>refs := (\<acute>refs - {\<acute>tmp_ref}) OD ;; \<lbrace>''sweep_idle''\<rbrace> store_phase ph_Idle OD" end primrec gc_coms :: "'mut process_name \<Rightarrow> ('field, 'mut, 'payload, 'ref) gc_com" where "gc_coms (mutator m) = mut_m.com m" | "gc_coms gc = gc.com" | "gc_coms sys = sys.com" (*<*) end (*>*)
¤ Dauer der Verarbeitung: 0.86 Sekunden ¤*© Formatika GbR, Deutschland |
|
||||||||||||||||||||||||
2026-11-01