diff --git a/README.md b/README.md index 7808139..bc7c0f2 100644 --- a/README.md +++ b/README.md @@ -1,10 +1,5 @@ -This repository contains the artifact of POPL 2024 paper -"An axiomatic basis for computer programming on the relaxed Arm-A architecture: the AxSL Logic". - -## About the Artifact - -This artifact is a mechanised proof development that contains formalised definitions and proofs that -can be checked by the Coq proof assistant. It contains all the results presented in the paper. +This repository contains the Coq mechanisation of the Arm-A instance of AxSL, +an Iris-based program logic for Arm-A relaxed concurrency. ## Building the Project @@ -66,49 +61,3 @@ memory models, including: - `Common`: This directory contains standard-library-like features, support type definitions, and automation helpers. - `Common/GRel.v` contains an implementation of relations and operations for relation algebra. - - -## 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 the 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 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 more 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` are assumed again. | -| | `(15)` | | `eid ↦ₐ R addr val eid_w` | | -| | Fig. 13, 14 | `examples/lb/data_data2.v` | `instrs`, `userprot_val`, `write_val_thread_1`, `write_val_thread_2` | `instrs` is the LB program, `userprot_val` is `Φ`, and the remaining two are the specs and their proofs. | -| | Oneshot | `one_shot` | 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 instructions, not microinstructions, but the definition 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 importantly: `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` | `={⊤,∅}=∗ ▷ \|={∅,⊤}=>` 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` contain 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. |