2 Fig. 3 lang/mm.v Module AAConsistent consistency axioms are in record t 3 The splitting rule used in Fig. 7 low/rules/prelude.v annot_split_iupd ↦ₐ is the notation for tied assertions 4 Fig. 8 lang/instrs.v Section instructions os and vr are defined in system-semantics-coq Fig. 9 Section interpretation The outcome interface is from system-semantics-coq. ;; corresponds to >>= Whole-system-execution low/adequacy.v tpsteps, tpstate_done, tp_state_init There is no a formal definition of the rule, we instead only defined the premises Fig. 10 lang/opsem.v Module LThreadStep t of the module defines the reduction relation, see below for more Graph X and Instruction memory I Module GlobalState H-mem-read TStepReadMem We use ⊆ instead of = for addr and ctrl; po1 is handled differently in our formalisation H-reg-write TStepRegWrite po1 is handled differently in our formalisation H-reload TStepReload ts_is_done_instr is omitted in the rule H-term TStepTerm ts_is_done_thd implements the last premise T of Ctd T and R of Done R Module ThreadState Field ts.reqs of record t corresponds to program T.p. R is the rest of the fields, except for that we have an extra ts_rmw_pred to handle exclusive; iis_iid and iis_cntr together correspond to e; next-e is inline; e_{po} is defined separately as lls_pop of LogicalLocalState. Ctd T and Done R Module LThreadState Both take ThreadState.t in the code. 5 Protocol Φ low/instantiation.v Typeclass UserProt The type prot_t is defined in low/lib/annotations.v Fig. 11 middle/specialised_rules.v mem_read_external Hoare triples are implemented in a continuation-passing style using WP: the preconditions are premises; the post conditions are in the continuation. The Coq definition is slightly general: it does not have constraint (2). Detailed correspondence can be found below. (1) & (10) NoLocalWrites last_local_write (3) & (11) PoPred o_po_src -{LPo}> (4) & (12) CtrlPreds ctrl_srcs -{Ctrl}> (5) & (13) ([∗ map] dr ↦ dv ∈ dep_regs, dr ↦ᵣ dv) dep_regs is regs (6) ([∗ map] node ↦ annot ∈ lob_annot, node ↦ₐ annot) lob_annot is m (7) & (14) GraphFacts R_graph_facts of mem_read_external (8) Lob Lines between comments Lob edge formers and FE (9) FlowIn Lines between comment FE and continuation ={⊤}[∅]▷=∗ is the view shift that also supports invariants; prot (field of UserProt) is the protocol Φ The persistent R_graph_facts is assumed again. (15) eid ↦ₐ R addr val eid_w Fig. 13 examples/lb_datas/proof.v instrs_val, write_val_thread_1, write_val_thread_2 instrs_val is the LB program, the definitions are the specs Fig. 14 userprot_val, write_val_thread_1, write_val_thread_2 userprot_val is Φ, the rest two is the proof Oneshot Section one_shot Instruction Hoare triple SSWPi Defined using single-step instruction weakest precondition SSWPi Fig. 15 wpi_pln_read, wpi_pln_write_data Fig. 16 examples/mp.v send_instrs, dep_receive_instrs Φ(flag,v,e) flag_prot The invariant for exclusives middle/excl.v excl_inv Proof rules for exclusives middle/rules.v mem_write_xcl_Some_inv, mem_write_xcl_None Again in the continuation-passing style. For successful and unsuccessful exclusive stores; Exclusive loads are handled in mem_read_external with extra machinery. 6 The microinstruction Hoare triple middle/weakestpre.v wpi_def Defined using weakest preconditions, so P is not mentioned. The Coq definition (WPi) is actually a weakest precondition for instuctions, not microinstructions, but the definiton follows the same spirit as the presented microinstruction one. SI-reg-agree and SI-reg-update reg_interp_agree, reg_interp_update Definition of weakest precondition low/weakestpre.v wp_pre The formalisation in Coq is quite different -- the paper only demonstrates the key ideas. Most important correspondence: annot_interp is SI_{T}; gconst_interp is SI_{G}; flow_eq is FlowImp; post_lifting is PullOutTied FlowImp low/lib/annotations.v flow_eq_ea, na_splitting_wf flow_eq_ea is the view shift; na_splitting_wf is Detach; the map extension is inlined in wp_pre Supporting framing low/instantiation.v annot_split Supporting invariants low/lib/annotations.v With ={⊤,∅}=∗ ▷ |={∅,⊤}=> of flow_eq_ea Same as ={⊤}[∅]▷=∗ Theorem 6.1 middle/rules.v, middle/specialised_rules.v, low/rules/*.v middle/rules.v and middle/specialised_rules.v contains the soundness proof of all microinstruction proof rules (in continuation style, proved using results in low/rules/*.v) Theorem 6.2 low/adequacy.v adequacy_pure With insignificant details omitted