blob: e983ff4c1d9086afc1ed540d1a35786601a70903 (
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 = "Proving correctness of renaming"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3a8g5e"]
forwardlinks = ["3a8g5g"]
zettelid = "3a8g5f"
+++
To prove the correctness in general, one has to prove that the result of
the register in `rs'` is equivalent to the register in `rs`, where `rs'`
is the register state in GSA and `rs` is the register state in SSA.
However, the problem is how to map the registers in GSA to the registers
in SSA, because they may have been renamed.
The first thing to note is that renaming is only performed for η
functions, and the special feature of η functions is that the argument
can only be the assignment of a μ function. Therefore, the argument to
the η function has to be a value that is less than the max register in
the SSA function. It also means that the renaming succeeded, and
therefore indexing the map with the SSA register gave the GSA register.
This cannot continue recursively, therefor the map will always go from
SSA registers which are less than the max register, and return a
register that is greater than the max register.
The agree function should therefore have the following form:
$$ (\forall r,\ r \leq m \Rightarrow r_s \mathbin{\#} r = r_s' \mathbin{\#} r)\lor (\forall r \ r',\ r > m \Rightarrow t_r\ !\ r' = \texttt{Some } r\Rightarrow rs' \mathbin{\#} r = rs' \mathbin{\#} r' \land r' \leq m) $$
|
