blob: 7b68517eaf28b47284ab986cb518ac9c983b2656 (
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
26
27
28
29
30
|
+++
title = "General overview"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3c3a", "2e1c6a"]
forwardlinks = ["1b8", "3c3c", "3c3b1"]
zettelid = "3c3b"
+++
The following two intermediate languages were created for scheduling:
- **RTLPar**: A basic block version of RTL with parallel blocks inside
a basic block.
- **RTLBlock**: A standard basic block.
It should be possible to extend these with conditional execution to
support hyperblocks ([\#1b8]), however the translation validation might
have to change for that.
- **RTL** is translated to **RTLBlock** using translation validation
to prove the correctness of the generation of basic blocks.
- **RTLBlock** is translated to **RTLPar** by scheduling, which is
also proven using translation validation.
- **RTLPar** is finally translated to **HTL** in a verified manner, as
no optimisations need to be performed.
This should replace the verified **RTL** to **HTL** translation.
[\#1b8]: /zettel/1b8
|
