diff options
Diffstat (limited to 'content/zettel/3a8.md')
| -rw-r--r-- | content/zettel/3a8.md | 37 |
1 files changed, 37 insertions, 0 deletions
diff --git a/content/zettel/3a8.md b/content/zettel/3a8.md new file mode 100644 index 0000000..09ece36 --- /dev/null +++ b/content/zettel/3a8.md @@ -0,0 +1,37 @@ ++++ +title = "CompcertSSA " +author = "Yann Herklotz" +tags = [] +categories = [] +backlinks = ["3a9", "3a8g", "3a7", "2e1b1b"] +forwardlinks = ["3c", "1c6", "3a9", "3a8a"] +zettelid = "3a8" ++++ + +CompcertSSA[^1] \[1\] is a version of CompCert that integrates a static +single assignment (SSA) form as a middle-end optimisation platform in +CompCert. The main workflow is to go from RTL to SSA and then back to +RTL, which means that it could be easily added onto Vericert ([\#3c]). +This would allow for more optimisations that may benefit from a static +single assignment, such as modulo scheduling even ([\#1c6]). + +<div id="refs" class="references csl-bib-body" markdown="1"> + +<div id="ref-barthe14_formal_verif_ssa_based_middl_end_compc" +class="csl-entry" markdown="1"> + +<span class="csl-left-margin">\[1\] +</span><span class="csl-right-inline">G. Barthe, D. Demange, and D. +Pichardie, “Formal verification of an SSA-based middle-end for +CompCert,” *ACM Trans. Program. Lang. Syst.*, vol. 36, no. 1, Mar. 2014, +doi: [10.1145/2579080].</span> + +</div> + +</div> + +[^1]: //gitlab.inria.fr/compcertssa/compcertssa + + [\#3c]: /zettel/3c + [\#1c6]: /zettel/1c6 + [10.1145/2579080]: https://doi.org/10.1145/2579080 |