An implementation of flush channels based on a verification methodology

Flush channels generalize more conventional asynchronous message passing protocols. A distributed system that uses flush channels allows a programmer the flexibility of specifying the delivery order of each message in relation to other messages transmitted on the channel. An implementation technique that follows directly from a verification methodology for flush channels is presented. A relatively formal argument in support of the technique is included