Correctness and performance of a multicomputer operating system

Our discussion assumes parallel or distributed computer systems that allow dynamic migration of processes between processors. Because the overall performance of these systems is strongly dependent on the overheads of migration, it is vital that migration be implemented as efficiently as possible. However, efficient implementations are often complex implementations and thus we have a conflict between performance and correctness. We cannot make the conflict go away, but we should be able to find ways of describing migration designs such that it is easy for system developers to make changes (for performance reasons) and see straight away what the implications for correctness are. We suggest that the formal specification language Z provides just such a way of describing migration designs. To support this suggestion we present an extended example based on the specification of a migration-proof communication protocol. This example is particularly appropriate because the possibility that a communicating process may migrate several times between communications greatly complicates the implementation. Yet we still require that communication should be efficient and correct, i.e. that messages should not be lost or duplicated. We make three contributions. First, we suggest a two-level plan for specification which separates issues of what operations do from when they do it. Second, we outline a rigorous proof style which combines formal statements of assumptions and proof steps with informal reasoning. Third, we show that we can link performance measurements with the specification but that we need to do this via finite state machines