Add content

1 files changed, 25 insertions, 0 deletions

diff --git a/content/zettel/3c3h4.md b/content/zettel/3c3h4.md
new file mode 100644
index 0000000..dbbbd43
--- /dev/null
+++ b/content/zettel/3c3h4.md
@@ -0,0 +1,25 @@
++++
+title = "Adding to the BTL language"
+author = "Yann Herklotz"
+tags = []
+categories = []
+backlinks = ["3c3h3"]
+forwardlinks = []
+zettelid = "3c3h4"
++++
+
+Implementing scheduling seems to be more difficult than initially
+thought. Proving the translation to basic blocks is not simple, however,
+CompCert-kvx seems to have a working solution.
+
+However, their BTL language is quite special, it uses recursive blocks,
+which I had thought of initially, instead of list of instructions.
+However, this makes scheduling harder (and reasoning about scheduling
+harder I think). But it seems like CompCert KVX have already implemented
+all of this. If I reuse their work, then I would at least have the
+proofs available for most of the scheduling, but it also means I have to
+understand it again and also reimplement the scheduling algorithm.
+
+The other option is just to reimplement their proofs and use it as
+inspiration. The differences in the scheduling and the proofs at a high
+level are still quite substantial.