blob: a07a46961761fb3fc8c075629aef372f677f65d8 (
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 = "Backward Simulation"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3a5a"]
forwardlinks = ["3a5c"]
zettelid = "3a5b"
+++
A more relaxed version to prove semantic preservation of the compiler is
to use backward simulation.
$\forall B,\ C \Downarrow B \implies S \Downarrow B$
However, this is also too strict, as some important optimisations
violate this property. One example is dead code elimination, meaning if
*S* contains dead code that also contains undefined behaviour, then C
will not contain that undefined behaviour anymore and will therefore
behave in a different way. To restrict that, we can therefore first
assume that if the behaviour of the program is safe, then the backward
simulation will hold.
Therefore, assuming that the behaviour of the source is safe, we can
then prove the same backward simulation.
|
