From 4b36b928ba2fc5bfe6cf929faeb090db35c22c29 Mon Sep 17 00:00:00 2001
From: Alban Gruin <alban.gruin@irit.fr>
Date: Mon, 4 Jul 2022 16:34:03 +0200
Subject: [PATCH] correct_store_buffer: new store buffer definition

This adds a new store buffer definiton, with more locking than before.
Provided are the ready and free functions, as well as a proof of
no-regression.

Signed-off-by: Alban Gruin <alban.gruin@irit.fr>
---
 _CoqProject                |  1 +
 src/correct_store_buffer.v | 98 ++++++++++++++++++++++++++++++++++++++
 2 files changed, 99 insertions(+)
 create mode 100644 src/correct_store_buffer.v

diff --git a/_CoqProject b/_CoqProject
index 9679100..cd6ca14 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -2,3 +2,4 @@
 src/definitions.v
 src/utils.v
 src/store_buffer.v
+src/correct_store_buffer.v
diff --git a/src/correct_store_buffer.v b/src/correct_store_buffer.v
new file mode 100644
index 0000000..8ffa7ce
--- /dev/null
+++ b/src/correct_store_buffer.v
@@ -0,0 +1,98 @@
+Require Import Bool Lia List Nat PeanoNat.
+From StoreBuffer Require Import definitions utils.
+Import ListNotations.
+
+Variant sbStateT :=
+  | Empty
+  | NotEmpty
+  | Full.
+
+Scheme Equality for sbStateT.
+
+(* free and cycle functions. *)
+Definition busFree isSuUsed sbState :=
+  (sbStateT_beq sbState Empty) && (negb isSuUsed).
+
+Definition ready isSuUsed sbState (elt : instr_kind) :=
+  match elt with
+  | (Load, (Lsu, 0)) => busFree isSuUsed sbState
+  | (_, (Su, 0)) => negb (sbStateT_beq sbState Full)
+  | (_, (_, 0)) => true
+  | _ => false
+  end.
+
+Definition luFree isSuUsed sbState trace :=
+  let instr := get_instr_in_stage trace Lu in
+  match instr with
+  | Some elt => ready isSuUsed sbState elt
+  | None => true
+  end.
+
+Definition suFree isSuUsed sbState trace :=
+  let instr := get_instr_in_stage trace Su in
+  match instr with
+  | Some elt => ready isSuUsed sbState elt
+  | None => true
+  end.
+
+Definition lsuFree isSuUsed sbState trace :=
+  let instr := get_instr_in_stage trace Lsu in
+  match instr with
+  | Some elt => ready isSuUsed sbState elt
+  | None => true
+  end.
+
+Definition free isSuUsed sbState trace (elt : instr_kind) :=
+  let (opc, state) := elt in
+  let (st, _) := state in
+  match nstg st opc with
+  | Lu => luFree isSuUsed sbState trace
+  | Su => suFree isSuUsed sbState trace
+  | Lsu => lsuFree isSuUsed sbState trace
+  | _ => true
+  end.
+
+Definition cycle_elt isSuUsed sbState trace elt :=
+  match elt with
+  | (opc, (st, S n)) => (opc, (st, n))
+  | (opc, (st, 0)) =>
+      if ready isSuUsed sbState elt && free isSuUsed sbState trace elt then
+        (opc, (nstg st opc, 0))
+      else
+        elt
+  end.
+
+Definition cycle sbState trace :=
+  let isSuUsed := List.existsb is_in_su trace in
+  List.map (cycle_elt isSuUsed sbState trace) trace.
+
+Section can_advance.
+  Variable isSuUsed : bool.
+  Variable sbState : sbStateT.
+  Variable n : nat.
+  Variable t : trace_kind.
+
+  Theorem instruction_never_regresses :
+    forall t' e1, t' = cycle sbState t ->
+             List.nth_error t n = Some e1 ->
+             compare_two (List.nth_error t n) (List.nth_error t' n) = true.
+  Proof.
+    intros t' e1 Ht' He1.
+
+    rewrite Ht', He1.
+    unfold cycle.
+    rewrite (map_nth_error _ _ _ He1).
+
+    unfold compare_two.
+    destruct e1.
+    unfold cycle_elt.
+    destruct s, n0.
+    - destruct (ready _ _ _ && free _ _ _ _);
+        destruct s, o;
+        reflexivity.
+    - destruct s;
+        simpl;
+        rewrite Nat.leb_le;
+        lia.
+  Qed.
+End can_advance.
-- 
GitLab