Correctness analysis for class of asynchronous communication mechanisms

Real-time system design options increase significantly if the individual concurrent processes are able to communicate with no mutual timing interference. This requirement can be met by a particular class of asynchronous communication mechanisms for the transfer of reference data between a single writer and a single reader, which is characterised by the use of multiple shared memory locations (slots), and where access to these slots is co-ordinated by small shared control variables. Such mechanisms guarantee that the data obtained by the reader is always the most recent (freshest) to have been supplied by the writer, and that the data is valid (coherent) within some timing constraints expressed in terms of the relative rates and phases of the two processes. The data coherence and freshness properties of one, two, three and four slot mechanisms are examined by analysing the dynamically changing roles of the slots during asynchronous operation. This novel approach rigorously proves the predicted properties, and it provides a useful insight to the nature of shared memory communication under asynchronous operating conditions.