1 files changed, 64 insertions, 0 deletions
diff --git a/content/zettel/3c3c3.md b/content/zettel/3c3c3.md
new file mode 100644
index 0000000..ba62c7c
--- /dev/null
+++ b/content/zettel/3c3c3.md
@@ -0,0 +1,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