A Proof System for Asynchronously Communicating Deterministic Processes

We introduce in this paper new communication and synchronization constructs which allow deterministic processes, communicating asynchronously via unbounded FIFO bu ers, to cope with an indeterminate environment. We develop for the resulting parallel programming language, which subsumes deterministic data ow, a simple compositional proof system. Reasoning about communication and synchronization is formalized in terms of input output variables which record for each bu er the sequence of values sent and received. These input output variovide an abstraction of the usual notion of history variables which denote sequences of communication events. History variables are in general necessary for compositional reasoning about the correctness of distributed systems composed of non-deterministic processes.

• Type: Conference
• Year: 1994
• Where: MFCS
• Authors: Frank S. de Boer, M. van Hulst
• Keywords: Bu Er, History Variables, Input Output, MFCS 1994, Theoretical Computer Science