README.md

This is the directory for the Coq development of AxSL, a program logic building atop of Arm's axiomatic relaxed memory model, formalised with Iris.

Structure of the development

The theories directory contains the Coq development of the work. In particular,

• lang contains definitions of instructions, the Arm memory model, and our opax semantics.
  • lang/instrs.v defines the semantics of instruction using the outcome interface.
  • lang/mm.v defines the (user) Arm memory model.
  • lang/opsem.v defines the opax semantics.
• algebra contains most of the ghost state constructions for the logical assertions of AxSL.
• low contains the definition of weakest preconditions, the soundness proof of low-level proof rules, and the adequacy theorem.
  • low/weakestpre.v defines the base weakest precondition that is parametrised by the implementation of state interpretaions.
  • low/instantiation.v contains the instantiation of the base weakest precondition, with a specific state interpretation implementaion.
  • low/rules/*.v contain base proof rules and their soundness proofs.
  • low/lifting.v and low/adequacy.v contain the adequacy proof with respect to the base weakest precondition.
  • low/lib/annotations.v contains the definitions of protocols and flow implications.
• middle contains the proof rules for all microinstructions and abstraction layers.
  • middle/weakestpre.v defines an abstraction layer based on low-level weakest preconditions.
  • middle/rules.v contains proof rules for some instructions and their soundness proofs (using the results of low/rules/*.v).
  • middle/excl.v contains our solution for supporting exclusives.
  • middle/specialised_rules.v contains proof rules for specific instructions used in verified examples, and their soundness proofs.
• examples contains the examples.
  • examples/lb.v contains two variants of load-buffering, and their proofs.
  • example/mp.v contains two variants of message-passing, and their proofs.

Reference for the results of the paper

§	Result(s) in paper	Location in code	Object(s) in code	Remarks/Diffs
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

Build the project

See INSTALL.md