diff options
Diffstat (limited to 'content/zettel/3a7d.md')
| -rw-r--r-- | content/zettel/3a7d.md | 50 |
1 files changed, 50 insertions, 0 deletions
diff --git a/content/zettel/3a7d.md b/content/zettel/3a7d.md new file mode 100644 index 0000000..0ca7da1 --- /dev/null +++ b/content/zettel/3a7d.md @@ -0,0 +1,50 @@ ++++ +title = "Adding predicates to symbolic execution" +author = "Yann Herklotz" +tags = [] +categories = [] +backlinks = ["3a7c"] +forwardlinks = ["1b8", "3c3f", "2e1b", "3a7e"] +zettelid = "3a7d" ++++ + +Adding predicates to the symbolic execution and abstract interpretation +lets us compare the executions of hyperblocks ([\#1b8]), and is linked +to the formal verification of HLS ([\#3c3f]). However, this seems to add +a lot of complexity, because predicates take exponential time to check. +My main argument is though that often you will not have that many +predicates that are active within a block, and that it should therefore +not take that long to check. + +In general, the idea is that each instruction can be conditionally +executed, meaning the results of the registers should also contain +conditionals. When checking the equivalences, it is therefore necessary +to evaluate the predicates somehow, to be able to then evaluate the +equivalence of the expressions, I believe that one first has to reduce +the expressions to a form which does not include the predicates. Then +one can compare bare expressions again. + +This is similar to how the comparison of predicates in gated-SSA +([\#2e1b]) is performed \[1\], where extra functions are added to SSA +which contain the predicate that the choice functions act upon. + +<div id="refs" class="references csl-bib-body" markdown="1"> + +<div id="ref-tu95_gated_ssa_based_deman_driven" class="csl-entry" +markdown="1"> + +<span class="csl-left-margin">\[1\] +</span><span class="csl-right-inline">P. Tu and D. Padua, “Gated +SSA-based demand-driven symbolic analysis for parallelizing compilers,” +in *Proceedings of the 9th international conference on supercomputing*, +in ICS ’95. Barcelona, Spain: Association for Computing Machinery, 1995, +pp. 414–423. doi: [10.1145/224538.224648].</span> + +</div> + +</div> + + [\#1b8]: /zettel/1b8 + [\#3c3f]: /zettel/3c3f + [\#2e1b]: /zettel/2e1b + [10.1145/224538.224648]: https://doi.org/10.1145/224538.224648 |