summaryrefslogtreecommitdiffstats
path: root/content/zettel/3c3j.md
blob: 1bbe9a9fb7728d49e070fbde06c6839f907be74f (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
+++
title = "Design Trade-offs for the Scheduling Proof"
date = "2022-11-16"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3c3i"]
forwardlinks = ["3c3k"]
zettelid = "3c3j"
+++

There are a few trade-offs that were made during the scheduling proof,
such as:

-   deciding to use flat predicates instead of a tree-like structure
-   if-conversion, which is a more self-contained way to prove the
    translation without having to worry about the performance of the
    code
-   The representation of the predicates is also an interesting
    trade-off, because there are various ways to do this.
-   Using if-statements or constraints to prove the backwards simulation
    in the abstract interpretation.

**\*\***