blob: dbbbd43146bb8702394b328a5a190e72610f0ea4 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
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.
|
