On the diversity of asynchronous communication. (September 2016)

• Record Type: Journal Article
• Authors: Chevrou, Florent; Hurault, Aurélie; Quéinnec, Philippe
• Is Part Of: Formal aspects of computing. Volume 28:Number 5(2016)
• Page Start: 847
• Page End: 879
• Publication Date: 2016-09
• Subjects: Asynchronous communication -- Formal verification -- Compatibility checking -- TLA+; Computer science -- Periodicals; 004.05
• DOI: 10.1007/s00165-016-0379-x
• Languages: English
• ISSNs: 0934-5043

Abstract

Abstract Asynchronous communication is often viewed as a single entity, the counterpart of synchronous communication. Although the basic concept of asynchronous communication is the decoupling of send and receive events, there is actually room for a variety of additional specification of the communication, for instance in terms of ordering. Yet, these different asynchronous communications are used interchangeably and seldom distinguished. This paper is a contribution to the study of these models, their differences, and how they are related. In this paper, the variety of point-to-point asynchronous communication paradigms is considered with two approaches. In the first and theoretical one, communication models are specified as properties on the ordering of events in distributed executions. In the second and more practical approach that involves composition of peers, they are modeled with transition systems and message histories as part of a framework. The described framework enables to model peer composition and compatibility properties. Besides, an implemented tool chain based on the TLA+ formalism and model checking is also proposed and illustrated. The conformance of the two approaches is highlighted. A hierarchy is established between the studied communication models. From the execution viewpoint, it completes existing work in the area by introducing more asynchronous communication models and showing their differences. The framework is shown to offer abstract implementations of the communication models. Both the correctness and the completeness of the descriptions in the framework are studied. This reveals necessary restrictions on the behavior of the peers so that the communication models are actually implementable.