From ef62c3b7e50705893f32d2a73531d4f7493cf806 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9ophile=20Bastian?= Date: Thu, 20 Jun 2024 17:56:52 +0200 Subject: [PATCH] Small backports from paper --- manuscrit/60_staticdeps/35_rob_proof.tex | 2 +- manuscrit/60_staticdeps/50_eval.tex | 36 +++++++++++------------- 2 files changed, 17 insertions(+), 21 deletions(-) diff --git a/manuscrit/60_staticdeps/35_rob_proof.tex b/manuscrit/60_staticdeps/35_rob_proof.tex index 62687ee..569a8b2 100644 --- a/manuscrit/60_staticdeps/35_rob_proof.tex +++ b/manuscrit/60_staticdeps/35_rob_proof.tex @@ -59,7 +59,7 @@ $(i_q)_{q\in Q_p}$ are the \uops{} obtained from the decoding of $I_p$. \begin{lemma}[Distance of in-flight \uops{}] For any pair of instructions $(I_p,I_{p'})$, and two corresponding \uops{}, - $(i_q,i_{q'})$ such that q \in Q_p, q' \in Q_{p'}$, + $(i_q,i_{q'})$ such that $q \in Q_p, q' \in Q_{p'}$, \[ \operatorname{inflight}(i_q) \wedge \operatorname{inflight}(i_{q'}) \Rightarrow \distance{I_p}{I_{p'}}