1 files changed, 71 insertions, 0 deletions
diff --git a/content/zettel/3c7a.md b/content/zettel/3c7a.md
new file mode 100644
index 0000000..bcd0923
--- /dev/null
+++ b/content/zettel/3c7a.md
@@ -0,0 +1,71 @@
++++
+title = "Notes to Tristan and Leroy's paper"
+date = "2022-05-01"
+author = "Yann Herklotz"
+tags = []
+categories = []
+backlinks = ["3c7"]
+forwardlinks = []
+zettelid = "3c7a"
++++
+
+These are notes to the following paper \[1\].
+
+The proof mainly relies on creating the pipelined version of the loop,
+using $\mathcal{P}$, $\mathcal{S}$ and the epilogue $\mathcal{E}$, which
+is then followed by final iterations of the loop $\mathcal{B}$ to prove
+the correctness.
+
+Then, the proof shows the equivalence of all the variables, up to the
+equivalence of temporary variables introduced in the pipelined loop to
+add the pipeline stages.
+
+The actual reasoning of the proof is the following, where the idea is
+that it changes the undecidable property of:
+
+$$ \forall N, \alpha(X_N) = \alpha(Y_N) $$
+
+for two pieces of code $X_N$ and $Y_N$.
+
+The first insight is that the following property holds:
+
+$$ \alpha(\mathcal{E}; \mathcal{B}^{\delta}) = \alpha(\mathcal{S}; \mathcal{E})$$
+
+This property says that one always has the choice of doing two things.
+
+-   Either one leaves the steady state immediately by executing the
+    epilogue $\mathcal{E}$, and then executing $\delta$ iterations of
+    the initial loop $\mathcal{B}$,
+-   or one executes one more iteration of the steady state followed by
+    the epilogue.
+
+Secondly, the following property is also true:
+
+$$ \alpha(\mathcal{B}^{\mu}) = \alpha(\mathcal{P}; \mathcal{E}) $$
+
+This says that if the original code performs exactly $\mu$ iterations,
+then the initial loop performed $\mathcal{B}^{\mu}$ whereas the
+transformed and pipelined loop performed exactly
+$\mathcal{P}; \mathcal{E}$.
+
+These two properties are now checkable statically, because $\delta$ and
+$\mu$ are already known.
+
+<div id="refs" class="references csl-bib-body" markdown="1">
+
+<div id="ref-tristan10_simpl_verif_valid_softw_pipel" class="csl-entry"
+markdown="1">
+
+<span class="csl-left-margin">\[1\]
+</span><span class="csl-right-inline">J.-B. Tristan and X. Leroy, “A
+simple, verified validator for software pipelining,” in *Proceedings of
+the 37th annual ACM SIGPLAN-SIGACT symposium on principles of
+programming languages*, in POPL ’10. Madrid, Spain: Association for
+Computing Machinery, 2010, pp. 83–92. doi:
+[10.1145/1706299.1706311].</span>
+
+</div>
+
+</div>
+
+  [10.1145/1706299.1706311]: https://doi.org/10.1145/1706299.1706311