diff options
Diffstat (limited to 'content/zettel/3a8g5i.md')
| -rw-r--r-- | content/zettel/3a8g5i.md | 32 |
1 files changed, 32 insertions, 0 deletions
diff --git a/content/zettel/3a8g5i.md b/content/zettel/3a8g5i.md new file mode 100644 index 0000000..8e99f27 --- /dev/null +++ b/content/zettel/3a8g5i.md @@ -0,0 +1,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. |