summaryrefslogtreecommitdiffstats
path: root/content/zettel/3a8g5i.md
blob: 8e99f272a4d39b5527b127d5121f37fda4f8a138 (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
31
32
+++
title = "Problem with renaming in GSA"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3a8g5h", "3a8g1b"]
forwardlinks = []
zettelid = "3a8g5i"
+++

There is an additional problem that had to be fixed with respect to the
renaming of registers. Initially, this was just a map from registers to
a rename of that register. However, the problem is that this actually
only allows for a single rename, whereas actually each eta variable can
be renamed to multiple other eta variables, as we are instantiating a
new variable for each η, and one may have multiple η for each μ.
Therefore, we actually need to keep track of multiple possible renames,
by having a list of tuples, containing the new name and the initial node
where the register is initially assigned. Then, during the rename, every
possible node in the rename list is checked for on if the assigning node
dominates the current point, and if it does, we can rename the current
register.

One extra thing to take care of is that a property that should be true
in general is that in a list of possible renames for a register, there
will only ever be one whose definition point dominates the current
point, because otherwise the insertion of the etas did not complete
correctly. This is something that doesn't really affect the correctness
of the generation, because if this situation ever occurs, then it should
be safe to take either rename. However, when one needs properties about
the GSA language, then it might be necessary to prove those things about
it.