State-of-the-art: ban high-security while loops. Not very practical!
Also relies on a nondeterministic scheduler, otherwise timing channels are possible.