Proving Failure-Free Properties of Concurrent Systems Using Temporal Logic

Abstract

In a failure-free concurrent system, no process is delayed forever by any of the system synchronization primitives.Previously, it was difficult to prove even the simplest concurrent system failure free, let alone attempt such a proof for a "real" operating system.First for semaphores and then for monitors, necessary and sufficient conditions for failure-free systems are derived.In both cases, the important properties of the system are stated using temporal logic, a concise formalism that allows reasoning about the future progress of program computations.Temporal logic permits a precise and explicit statement of exactly those properties necessary to establish that a concurrent system is truly failure free.In conclusion, a short example is given and then the applicability of these results to several existing systems and languages (UNIX o, MODULA and MESA) is examined.