SE547: Sequential noninterference [8/23]

Write μ ~ ρ whenever μ and ρ agree on L variables:

1. { x_H = 37, y_L = 5 } ~ { x_H = 0, y_L = 5 }?
2. { x_H = 37, y_L = 5 } ~ { x_H = 37, y_L = 0 }?

A command c satisfies sequential noninterference when:

If μ₁ ~ ρ₁ and (c, μ₁) ^* μ₂ and (c, ρ₁) ^* ρ₂ then μ₂ ~ ρ₂.

Which of these satisfy sequential noninterference?

1. x_H=y_L;
2. y_L=x_H;
3. x_H=0; if(even(y_L)) { x_H=1; }
4. y_L=0; if(even(x_H)) { y_L=1; }