Sciweavers

MFCS
1994
Springer

A Proof System for Asynchronously Communicating Deterministic Processes

13 years 7 months ago
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.
Frank S. de Boer, M. van Hulst
Added 10 Aug 2010
Updated 10 Aug 2010
Type Conference
Year 1994
Where MFCS
Authors Frank S. de Boer, M. van Hulst
Comments (0)