Understanding and using asynchronous message passing (Preliminary Version)
Richard D. Schlichting, Fred B. Schneider · 1982
Message passing provides a way for concurrently executing processes to communicate and synchronize. In this paper, we develop proof rules for asynchronous message-passing primitives (i.e. “send no-wait”). Two benefits accrue from this. The obvious one is that partial correctness proofs can be written for concurrent programs that use such primitives. This allows programs to be understood as predicate transformers, instead of by contemplating all possible execution interleavings. The second benefit is that the proof rules and their derivation shed light on how interference arises when message-passing operations are used and on how this interference can be controlled. This provides insight into programming techniques to eliminate interference in programs that involve asynchronous activity. Three safe uses of asynchronous message passing are described here: the transfer of values, the transfer of monotonic predicates, and the use of acknowledgments.