Aliasing problem with indices

[MattWindsor91]

In the microcode translations of individual commands, the semantics of the resulting list of microcode instructions is that they are under disjoint parallel composition. This means that each assignment in that single command assigns the same MarkedVar level to the same MarkedVar level. For example,

[ Assign x 3; Assign y z ]

would translate into

(x!after == 3 && y!after == z!before && frame)

This is perfectly sound for variables, as disjointness is guaranteed lexically. However, translating

[ Assign a[x] 3; Assign a[y] z ]

to

(a!after = (a!before with [x] == 3) && a!after == (a!before with [y] == z) && frame)

is wrong, and

(a!after = ((a!before with [x] == 3) with [y] == z)) && frame)

has unsound, or at least unclear, semantics when x == y.

I think what I'll need to do is change the semantics here to sequential composition, so each separate microcode operation generates a new intermediate stage. This, however, is fairly nontrivial when it comes to branches.

Failing this, we could disallow use of the same array multiple times in a command. In fact, I think this is technically done right now, since our current command set doesn't allow multiple assignments to the same environment in one command.

[bensimner]

Why not the obviously-correct semantics of

[ Assign a[x] i; Assign a[y] j ] -> (a!after[x] == i) && (a!after[y] == j) && (k not i or j => a!after[k] = a!before[k]) && frame

[MattWindsor91]

@bensimner inefficiency, I think