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
|
+++
title = "How to make optimisations more predictable"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["1f4b", "1f4"]
forwardlinks = ["3a7", "1f4b"]
zettelid = "1f4a"
+++
The way to address this issue is to make optimisations more predictable.
This is quite tough though, because it's hard to even imagine what this
means. One way this could be approached is by formalising the
optimisations, so that properties can be proven about them. For example,
one could formalise loop pipelining in polyhedral analysis \[1\], \[2\]
to understand more about the algorithm. However, this would probably be
done using translation validation ([\#3a7]), therefore not being that
perfect for understanding the algorithm.
However, in addition to that, it might be possible to define a theorem
that proves predictability of the algorithms. For example, one might
imagine a situation where adding no-ops to the input of an algorithm
drastically changes the output. One might therefore want to define a
theorem that states that adding a no-op will either not change the
hardware in any way, or weaken it by saying that the adding a no-op
should always increase the size of the hardware if there are any changes
to it.
<div id="refs" class="references csl-bib-body" markdown="1">
<div id="ref-liu18_polyh_based_dynam_loop_pipel" class="csl-entry"
markdown="1">
<span class="csl-left-margin">\[1\]
</span><span class="csl-right-inline">J. Liu, J. Wickerson, S. Bayliss,
and G. A. Constantinides, “Polyhedral-based dynamic loop pipelining for
high-level synthesis,” *IEEE Transactions on Computer-Aided Design of
Integrated Circuits and Systems*, vol. 37, no. 9, pp. 1802–1815, Sep.
2018, doi: [10.1109/TCAD.2017.2783363].</span>
</div>
<div id="ref-courant21_verif_code_gener_polyh_model" class="csl-entry"
markdown="1">
<span class="csl-left-margin">\[2\]
</span><span class="csl-right-inline">N. Courant and X. Leroy, “Verified
code generation for the polyhedral model,” *Proc. ACM Program. Lang.*,
vol. 5, no. POPL, Jan. 2021, doi: [10.1145/3434321].</span>
</div>
</div>
[\#3a7]: /zettel/3a7
[10.1109/TCAD.2017.2783363]: https://doi.org/10.1109/TCAD.2017.2783363
[10.1145/3434321]: https://doi.org/10.1145/3434321
|
