Semantics of nondeterministic asynchronous broadcast networks

Abstract

We present a compositional denotational semantics for a spectrum of nondeterministic broadcast networks of processes. It is based on the real-time semantics of variants of CSP proposed in Koymans et al. (1988, Inform, and Comput.78, 210-256). We consider two classes of broadcast communications, namely, unbuffered broadcast and buffered broadcast. Unbuffered broadcast allows us to model broadcast communication structures similar to the schemes available in Ethenet. Buffered broadcast models varieties of multiprocessor architectures based on broadcast protocols. Based on the availability of buffers, immediate/delayed initiation of broadcast, we classify the buffered broadcast into (i) unbounded buffer broadcast; (ii) bounded buffer broadcast where the message is sent on only those channels that have at least one empty buffer, ignoring the rest of the channels that are full; (iii) bounded buffer broadcast where the message is sent on channels that have at least one empty buffer at that point of time and that have not yet received the message until the message is sent over all the channels; and (iv) atomic broadcast, where the broadcast is delayed until it is possible to send the message over all the channels at the same time. We show that such a classification is meaningful only for real-time models and that a maximal parallelism model provides a realistic execution model for defining the denotational semantics of broadcast networks. Basically, we use the semantic domain of prefix-closed sets of state-history pairs; it is only the structure of the communication assumptions in the histories that varies from category to category. In the semantics, properties such as reliable (or lossy) transmission and order preserving asynchronous communication medium are captured through the prefix property (or the subsequence property) of the projections of the histories of the underlying processes. The semantics provides a realistic model of the various broadcast categories and throws light on the suitability of broadcast networks for real-time programming. Further, our semantics, naturally, leads to a compositional specification-oriented proof system for broadcast networks.