A Type-Theoretic Approach to Deadlock-Freedom of Asynchronous Systems

We present a type-based technique for the veri cation of deadlock-freedom in asynchronous concurrent systems. Our general approach is to start with a simple interaction category, in which objects are types containing safety speci cations and morphisms are processes. We then use a speci cation structure to add information to the types so that they specify stronger properties. In this paper the starting point is the category ASProc and the extra type information concerns deadlockfreedom. In the resulting category ASProcD, combining well-typed processes preserves deadlock-freedom. It is also possible to accommodate non-compositional methods within the same framework. The systems we consider are asynchronous, hence issues of divergence become signi cant; our approach incorporates an elegant treatment of both divergence and successful termination. As an example, we use our methods to verify the deadlock-freedom of an implementation of the alternating-bit protocol.

• Type: Conference
• Year: 1997
• Where: TACS
• Authors: Samson Abramsky, Simon J. Gay, Rajagopal Nagarajan
• Keywords: Asynchronous Concurrent Systems, Cation, Software Engineering, Speci Cation, TACS 1997