Library ArchSemRiscV.GenAxiomaticRiscV

From ASCommon Require Import Options.
From ASCommon Require Import Common GRel FMon.

Require Import RiscVInst.

Definition of barriers categories and barrier sets

This section defines the event sets of RISC-V barrier and the corresponding classification.

This development assumes that all hardware threads are in the same inner shareability domain, therefore we identify barriers that are:

Full system
Outer shareable
Inner shareable

This might need to change when considering device interaction later

Section Barriers.
  Import Candidate.
  Context {et : exec_type} {nmth : nat}.
  Implicit Type cd : (pre et nmth).
  Implicit Type b : barrier.
  #[local] Hint Extern 10 (Decision (?x _)) ⇒ unfold x : typeclass_instances.
  #[local] Hint Extern 10 (Decision (?x _ _)) ⇒ unfold x : typeclass_instances.
  #[local] Hint Extern 10 (Decision (?x _ _ _)) ⇒ unfold x : typeclass_instances.

  Inductive fenced_accesses := FA_read | FA_write | FA_readwrite.
  #[export] Instance fenced_accesses_eq_dec : EqDecision fenced_accesses.
  Proof. solve_decision. Defined.
  #[export, refine] Instance fenced_accesses_fin : Finite fenced_accesses := { enum := _}.
  Proof.
    all:clear et.
    - exact [FA_read ; FA_write ; FA_readwrite].
    - sauto q:on.
    - sauto lq:on.
  Qed.

  Definition fence_from (input output : fenced_accesses) : barrier_kind :=
    match input, output with
    | FA_read, FA_read ⇒ Barrier_RISCV_r_r
    | FA_read, FA_write ⇒ Barrier_RISCV_r_w
    | FA_read, FA_readwrite ⇒ Barrier_RISCV_r_rw
    | FA_write, FA_read ⇒ Barrier_RISCV_w_r
    | FA_write, FA_write ⇒ Barrier_RISCV_w_w
    | FA_write, FA_readwrite ⇒ Barrier_RISCV_w_rw
    | FA_readwrite, FA_read ⇒ Barrier_RISCV_rw_r
    | FA_readwrite, FA_write ⇒ Barrier_RISCV_rw_w
    | FA_readwrite, FA_readwrite ⇒ Barrier_RISCV_rw_rw
    end.

  Definition fences (input output : fenced_accesses) cd :=
    collect_all (λ _, is_barrierP (.= fence_from input output )) cd.

  Definition fences_tso cd :=
    collect_all (λ _, is_barrierP (.= Barrier_RISCV_tso)) cd.

  Definition fences_i cd :=
    collect_all (λ _, is_barrierP (.= Barrier_RISCV_i)) cd.

End Barriers.

Standard names and definitions for RISC-V axiomatic models

Module AxRiscVNames.
  Import Candidate.
  Section RiscVNames.

  Context {et : exec_type} {nmth : nat}.
  Context `(cd : t et nmth).

Thread relations

  Notation pe := (pre_exec cd).
  Notation int := (same_thread pe).
  Notation si := (same_instruction_instance cd).
  Notation sca := (same_access cd).
  Notation po := (instruction_order pe).
  Notation full_instruction_order := (full_instruction_order pe).
  Notation iio := (iio pe).

Registers

  Notation RR := (reg_reads pe).
  Notation RW := (reg_writes pe).
  Definition RE := RR ∪ RW.
  Notation rrf := (reg_reads_from cd).
  Notation rfr := (reg_from_reads cd).

Memory

  Notation W := (explicit_writes pe).
  Notation R := (explicit_reads pe).
  Notation M := (mem_explicit pe).
  Notation Wx := (exclusive_writes pe).
  Notation Rx := (exclusive_writes pe).
  Notation X := (mem_exclusive pe).
  Definition RL := (rel_acq_rcpc_writes pe ) ∪ (rel_acq_rcsc_writes pe ).
  Definition AQ := (rel_acq_rcpc_reads pe ) ∪ (rel_acq_rcsc_reads pe ).
  Notation RCsc := (mem_rel_acq_rcsc pe).
  Notation IF := (ifetch_reads pe).
  Notation IR := (init_mem_reads cd).

  Notation lxsx := (lxsx cd).
  Notation amo := (atomic_update cd).
  Definition rmw := lxsx ∪ amo.

  Definition co := ⦗W ⦘⨾coherence cd ⨾⦗W ⦘ ∩ overlapping cd.
  Definition coi := co ∩ int.
  Definition coe := co ∖ coi.

  Definition rf := reads_from cd ⨾⦗R ⦘.
  Definition rfi := rf ∩ int.
  Definition rfe := rf ∖ rfi.
  Definition fr := ⦗R ⦘⨾from_reads cd.
  Definition fri := fr ∩ int.
  Definition fre := fr ∖ fri.

Reading same write

  Definition rsw := (rf ⁻¹ ⨾rf).

  Definition irf := reads_from cd ⨾⦗IF ⦘.
  Definition irfi := irf ∩ int.
  Definition irfe := irf ∖ irfi.
  Definition ifr := ⦗IF ⦘⨾from_reads cd.
  Definition ifri := ifr ∩ int.
  Definition ifre := ifr ∖ ifri.

Internal coherence

  Record reg_coherence := {
      rrf_internal : rrf ⊆ full_instruction_order;
      rfr_internal : rfr ⊆ not_after cd
    }.
  #[export] Instance reg_coherence_dec : Decision reg_coherence := ltac:(decide_record).
  End RiscVNames.
End AxRiscVNames.