Noninterfering schedulers: when possibilistic noninterference implies probabilistic noninterference
Andrei Popescu, Johannes Hölzl, Tobias Nipkow · Middlesex University Research Repository (Middlesex University Of London) · 2013
Abstract. We develop a framework for expressing and analyzing the behavior of probabilistic schedulers. There, we define noninterfering schedulers by a proba-bilistic interpretation of Goguen and Meseguer’s seminal notion of noninterfer-ence. Noninterfering schedulers are proved to be safe in the following sense: if a multi-threaded program is possibilistically noninterfering, then it is also proba-bilistically noninterfering when run under this scheduler. 1