From 47a9db6d6dc421f0e587332a452326071b34f513 Mon Sep 17 00:00:00 2001 From: Alban Gruin <alban.gruin@irit.fr> Date: Wed, 27 Jul 2022 23:32:38 +0200 Subject: [PATCH] =?UTF-8?q?correct=5Fstore=5Fbuffer:=20the=20behaviour=20i?= =?UTF-8?q?s=20monotonic=20if=20e=20=E2=8A=8F=20e'?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This proves that if e <> e', and if state_leb e e' = true, then the behaviour of the store buffer is monotonic. Signed-off-by: Alban Gruin <alban.gruin@irit.fr> --- src/correct_store_buffer.v | 58 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 58 insertions(+) diff --git a/src/correct_store_buffer.v b/src/correct_store_buffer.v index 46b97db..35430b2 100644 --- a/src/correct_store_buffer.v +++ b/src/correct_store_buffer.v @@ -307,4 +307,62 @@ Section monotonicity. (* st = Su, st' = Sn *) - now destruct (ready _ _ _ && free _ _ _ _), opc. Qed. + + Hypothesis HvalidStLat : forall (e : instr_kind) st n, e = (Store, (st, n)) -> n = 0. + Hypothesis HvalidLdLat : forall (e : instr_kind) st n dlat, e = (Load dlat, (st, n)) -> 0 <> n -> st = Lu /\ n <= dlat. + + Lemma moved_lat_is_lower : + forall n n', e = (opc, (st, n)) -> e' = (opc, (st', n')) -> e <> e' -> + state_leb (st, n) (st', n') = true -> + compare_two (List.nth_error tc i) (List.nth_error tc' i) = true. + Proof. + intros n n' He He' Hed Hsl. + pose proof (HvalidStLat e' st' n') as HvalidStLat'. + specialize (HvalidStLat e st n). + pose proof (HvalidLdLat e' st' n') as HvalidLdLat'. + specialize (HvalidLdLat e st n). + + destruct n, n'; [ + (* n and n' are = 0. We have a lemma for that. *) + now apply moved_no_lat_is_lower | + (* Other cases: rewrite the goal to make cycle appear. *) + rewrite Htc, Htc', Ht, Ht'; + unfold cycle; + rewrite (map_in_the_middle _ _ e d _ _ tpre tpost _ (eq_refl _) Hi), + (map_in_the_middle _ _ e' d _ _ tpre' tpost' _ (eq_refl _) Hi'); + unfold cycle_elt; + rewrite <- Ht, <- Ht'; + subst e; + subst e'; + (* Since n or n' is not equal to 0, opc is a load. Remove other cases. *) + destruct opc; + [| discriminate (HvalidStLat (eq_refl _)) + || discriminate (HvalidStLat' (eq_refl _))] .. + ]. + + (* From there, opc = Load. *) + (* n = 0 and n' <> 0. *) + - (* st' = Lu. *) + destruct (HvalidLdLat' n (eq_refl _) (O_S n')) as [Hst' Hlat']. + rewrite Hst' in Hsl, Hed |- *. + destruct st; + try discriminate. + + now destruct (_ && _). + + destruct (_ && _). + * simpl. + rewrite Nat.leb_le. + lia. + * reflexivity. + + (* n <> 0 and n' = 0. *) + - (* st = Lu. *) + destruct (HvalidLdLat n0 (eq_refl _) (O_S n)) as [Hst Hlat]. + rewrite Hst in Hsl, Hed |- *. + now destruct st'. + + (* n and n' <> 0. *) + - destruct (HvalidLdLat n0 (eq_refl _) (O_S n)) as [Hst Hlat]. + rewrite Hst in Hsl, Hed |- *. + now destruct (HvalidLdLat' n0 (eq_refl _) (O_S n')). + Qed. End monotonicity. -- GitLab