Typing Confluence

by Uwe Nestmann and Martin Steffen

March 14, 1997

Abstract

We investigate confluence properties for concurrent systems of message-passing processes, because such properties have proved to be useful for a variety of applications, ranging from reasoning about concurrent objects to mobile and high-speed telecommunication protocols. Roughly, confluence means that for every two computations starting from a common system state, it is possible to continue the computations, so to reach a common state again. In order to prove confluence for a given system, we are required to demonstrate that for all states reachable by computation from the starting state, the 'owing together' of possible computations is possible. In this paper, we aim at proving confluence properties for concurrent systems without having to generate all reachable states. Instead, we use a type system that supports a static analysis of possible sources of non-confluence. In message-passing systems, confluence is invalidated whenever two processes compete for communication with another process. We may statically check the occurrence of such situations by reducing them to the concurrent access on a shared communication port. For the technical development, we focus on the setting of a polarized pi-calculus, where we formalize the notion of port-uniqueness by means of overlapping-free context-redex decompositions. We then present a type system for port-uniqueness that, taking advantage of a subject reduction property, yields a sucient criterion for guaranteeing confluence.

Interested?

gziped PostScript file (use the "load to disc" option)
PDF file (For PDF files, a free viewer (Acrobat Reader) is available from Adobe Systems.

return to the research reports content list