Freshness specification for a class of asynchronous communication mechanisms

The paper is concerned with a common form of asynchronous communication mechanism (ACM) which can be used to connect a single writer to a single reader, so that the intermediate data in the ACM can be updated at any time by the writer and can be inspected at any time by the reader, without recourse to arbitration or exclusion which would impede either writer or reader. A class of such ACMs is considered in which data is inserted into the ACM and then released by the writer, and data is acquired within the ACM and then extracted by the reader. The temporal relationship between output and input data is analysed in terms of the control sequences which release and acquire the data. Freshness of data is an essential property, and a formal real-time logic specification is derived giving the relationship between written and read values using the events delineating the starts and ends of the control sequences. A formal specification for the independent property of data sequencing is also given. The paper derives a more precise and relevant freshness specification for these ACMs than can be achieved using the alternative atomic register concept.