From c9648f2dc56a0c970a90e1539925ae78b0610fbc Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 5 May 2022 17:08:12 +0100 Subject: First realistic draft --- chapters/pipelining.tex | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'chapters/pipelining.tex') diff --git a/chapters/pipelining.tex b/chapters/pipelining.tex index 09fae11..b0bdb20 100644 --- a/chapters/pipelining.tex +++ b/chapters/pipelining.tex @@ -168,9 +168,10 @@ all, the proof from the paper was actually never fully completed: location=middle, width=\dimexpr \textwidth - 1cm \relax, ] - {\noindent\it [Semantic preservation going from unrolled loops in a basic-block representation to - the actual loops in a CFG] is intuitively obvious but surprisingly tedious to formalize in full - details: indeed, this is the only result in this paper that we have not yet mechanized in Coq.} + {\noindent\it [Semantic preservation going from unrolled loops in a basic block representation to + the actual loops in a CFG] is intuitively obvious but surprisingly tedious to formalize in + full details: indeed, this is the only result in this paper that we have not yet mechanized in + Coq.} \startalignment[flushright] --- \cite[alternative=authoryears,right={, Section -- cgit