+++
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.
\[1\]
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].
\[2\]
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].
\[3\]
C. Six, L. Gourdin, S. Boulmé, and
D. Monniaux, “Verified Superblock Scheduling with
Related Optimizations,” Apr. 2021. Available:
[10.1145/3428197]: https://doi.org/10.1145/3428197
[10.1145/1328438.1328444]: https://doi.org/10.1145/1328438.1328444