1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
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
|
