Data transfer analysis for a pair of asynchronous communication algorithms

A common form of asynchronous communication mechanism (ACM) provides a one-way data transfer connection between two concurrent processes in which the writer uses a control algorithm to release data within the mechanism and the reader uses a control algorithm to acquire data within the mechanism, without recourse to arbitration or exclusion which could impede the progress of either the writer or the reader. When execution of the control algorithms is distinct, the reader acquires the latest data item released by the writer. When execution of the control algorithms overlaps, the reader acquires either a data item which is being or has been released during the overlapped acquisition, or the data item which is the latest released prior to the start of acquisition. The particular data item acquired is determined by the interleaving of critical events in each algorithm. The paper formally analyses a pair of algorithms to determine the way in which the data item acquired depends on the precise ordering of interleaved algorithm events. New insights into the notion of data freshness in ACMs are gained, and the essential similarity between several well known pairs of control algorithms is exposed. The formal analysis of ACM algorithms complements the previously derived formal specifications for such ACMs.