Invariance and non-determinacy

Since the earliest days of proving the correctness of programs, predicates on the program’s state space have played a central role. This role became essential when non-deterministic systems were considered. The first (and still best known) source of non-determinacy was provided by operating systems, which had to regulate the cooperation between components that had speed ratios that were beyond our control. Distributed systems have revived our interest in such configurations. I know of only one satisfactory way of reasoning about such systems: to prove that none of the atomic actions falsifies a special predicate, the so-called ‘global invariant’. Once initialized, the global invariant will then be maintained by any interleaving of the atomic actions. That solves the problem in principle; in each particular case, however, we have to choose how to write down the global invariant. The choice of notation influences the ease with which we can show that, indeed, none of the atomic actions falsifies the global invariant. An example will be given and discussed.