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
|
+++
title = "Hash-consing for proof of scheduling"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3c3c2", "2e1c7", "2e1c6b"]
forwardlinks = []
zettelid = "3c3c3"
+++
Hash-consing is used by Six et al. \[1\] to prove scheduling
efficiently, as that was proposed by Tristan et al. \[2\] as one way to
improve the scheduling algorithm. However, I don't think that this is a
necessary improvement for the kinds of scheduling that was done in that
paper, as in Tristan et al., the note about hash-consing was mostly
meant about their trace-scheduling equivalence checker, as that does
equivalence checking of a tree without any redundancy help.
However, the work on superblock scheduling \[3\] might actually benefit
from that, as it also does equivalence checking of trees in some way, I
think.
<div id="refs" class="references csl-bib-body" markdown="1">
<div id="ref-six20_certif_effic_instr_sched" class="csl-entry"
markdown="1">
<span class="csl-left-margin">\[1\]
</span><span class="csl-right-inline">C. Six, S. Boulmé, and D.
Monniaux, “Certified and efficient instruction scheduling: Application
to interlocked VLIW processors,” *Proc. ACM Program. Lang.*, vol. 4, no.
OOPSLA, Nov. 2020, doi: [10.1145/3428197].</span>
</div>
<div id="ref-tristan08_formal_verif_trans_valid" class="csl-entry"
markdown="1">
<span class="csl-left-margin">\[2\]
</span><span class="csl-right-inline">J.-B. Tristan and X. Leroy,
“Formal verification of translation validators: A case study on
instruction scheduling optimizations,” in *Proceedings of the 35th
annual ACM SIGPLAN-SIGACT symposium on principles of programming
languages*, in POPL ’08. San Francisco, California, USA: Association for
Computing Machinery, 2008, pp. 17–27. doi:
[10.1145/1328438.1328444].</span>
</div>
<div id="ref-six21_verif_super_sched_relat_optim" class="csl-entry"
markdown="1">
<span class="csl-left-margin">\[3\]
</span><span class="csl-right-inline">C. Six, L. Gourdin, S. Boulmé, and
D. Monniaux, “<span class="nocase">Verified Superblock Scheduling with
Related Optimizations</span>,” Apr. 2021. Available:
<https://hal.archives-ouvertes.fr/hal-03200774></span>
</div>
</div>
[10.1145/3428197]: https://doi.org/10.1145/3428197
[10.1145/1328438.1328444]: https://doi.org/10.1145/1328438.1328444
|
