This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Proof Rules for Flush Channels
April 1993 (vol. 19 no. 4)
pp. 366-378

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.

[1] M. Ahuja, "Flushprimitives for asynchronous distributed systems,"Inform. Processing Lett., vol. 34, no. 2, pp. 5-12, Feb. 1990.
[2] K. M. Chandy and L. Lamport, "Distributed snapshots: Determining global states of distributed systems,"ACM Trans. Comput. Syst., vol. 3, no. 1, pp. 63-75, Feb. 1985.
[3] M. Ahuja, K. Varadhan, and A. B. Sinha, "Flush message passing in communicating sequential processes," inParallel Architectures, N. Rishe, S. Navathe, and D. Tal, Eds. Washington, DC: IEEE Computer Society Press, 1991.
[4] M. Ahuja, "An implementation ofF-Channels, A preferable alternative to FIFO channels," inProc. Eleventh Int. Conf. Distributed Comput. Syst., IEEE, 1991, pp. 180-189.
[5] P. Kearns, T. Camp, and M. Ahuja, "Implementation ofFlushchannels based on a verification methodology," inProc. Twelfth Int. Conf. Distributed Comput. Syst., IEEE, 1992, pp. 336-343.
[6] P. Kearns and T. Camp, "An implementation of flush channels based on a verification methodology," College William and Mary, Tech. Rep. 91-6, 1991.
[7] S. Agrawal and R. Ramaswamy, "Analysis of the resequencing delay forM/M/msystems," inProc. 1987 SIGMETRlCS Conf. Measurement and Modeling of Computer Systems, 1987, pp. 27-35.
[8] S. Chowdhury, "The mean resequencing delay forM/Hk/∞systems,"IEEE Trans. Software Eng., vol. 15, no. 12, pp. 1633-1638, 1989.
[9] T.-S. Yum and T.-Y. Ngai, "Resequencing of messages in communication networks,"IEEE Trans. Commun., vol. COM-34, no. 2, pp. 143-149, 1986.
[10] L. Lamport, "Control predicates are better than dummy variables for reasoning about program control,"ACM Trans. Program. Lang. Syst., vol. 10, no. 2, pp. 267-281, 1988.
[11] R. D. Schlichting and F. B. Schneider, "Using message passing for distributed programming: Proof rules and disciplines,"ACM Trans. Program. Lang. Syst., vol. 6, no. 3, pp. 402-431, 1984.
[12] G. M. Levin and D. Gries, "A proof technique for communicating sequential processes,"Acta Inform., vol. 15, pp. 281-302, 1981.
[13] S. Owicki and D. Gries, "An axiomatic proof technique for parallel programs,"Acta Inform., vol. 6, pp. 319-340, 1976.
[14] C. A. R. Hoare, "An axiomatic basis for computer programming,"Commun. ACM, vol. 12, no. 10, pp. 576-583, 1969.
[15] E. W. Dijkstra,A Discipline of Programming. Englewood Cliffs, NJ: Prentice-Hall, 1976.
[16] T. Camp and P. Kearns, "Proof rules for flush channels: An axiomatic approach," College William and Mary, Tech. Rep. 91-2, 1991.

Index Terms:
flush channels; asynchronous communication constructs; virtual circuits; datagrams; receipt-order restrictions; message-by-message basis; concurrency; distributed program; Hoare-style partial correctness verification methodology; distributed processing; program verification
Citation:
T. Camp, P. Kearns, M. Ahuja, "Proof Rules for Flush Channels," IEEE Transactions on Software Engineering, vol. 19, no. 4, pp. 366-378, April 1993, doi:10.1109/32.223804
Usage of this product signifies your acceptance of the Terms of Use.