Proof rules for flush channels
Tracy K. Camp, Phil Kearns, Mohan L. Ahuja · IEEE Transactions on Software Engineering · 1993
Flush channels generalize conventional asynchronous communication constructs such as virtual circuits and datagrams. They permit the programmer to specify receipt-order restrictions on a message-by-message basis, providing an opportunity for more concurrency in a distributed program. A Hoare-style partial correctness verification methodology for distributed systems which use flush channel communication is developed, and it is shown that it it possible to reason about such systems in a relatively natural way.>