Abstract:
We propose a type system to ensure the property of noninterference in a system of concurrent programs, described in a standard imperative language extended with parallelism. Our proposal is in the line of some recent work by Irvine, Volpano and Smith. Our type system, as well as our semantics for concurrent programs, seem more natural and less restrictive than those originally presented by these authors. Moreover, we show how to extend the language in order to formalise scheduling policies. The type system is extended to the new constructs, and we show that noninterference still holds, while remaining in a nonprobabilistic setting.

[PostScript, .ps.gz]