§ SSA as linear typed language
- Control flow is linear in a basic block: ie, we can have a sea of nodes representation, where each terminator instruction produces linear control flow tokens:
br: token[-1] --> token.
brcond: token[-1] -> -> (token, token),
return: token[-1] -> (). This ensures that each branching only happens once, thereby "sealing their fate. On the other hand, reguar instructions also take a "control token", but don't consume it . so for example,
add: token -> (name, name) -> name.
- Next question: is dominance also somehow 'linear'?
- Answer: yes. We need quantitative types. When we branch from basic block
B, C, attach
1/2A to the control tokens from
(%tokb, %tokc) = br cond %cond0 B, C. Now, if someone builds a token that's at a basic block
D that is merged into by both
B, C, they will receive a "full"
A that they can use. Pictorially: