Causing communication closure: safe program composition with reliable non-FIFO channels
Abstract
A rigorous framework for analyzing safe composition of distributed programs is presented. It facilitates specifying notions of safe sequential execution of distributed programs in various models of communication. A notion of sealing is defined, where if a program P is immediately followed by a program Q that seals P then P will be —it will execute as if it runs in isolation. None of its send or receive actions will match or interact with actions outside P. The applicability of sealing is illustrated by a study of program composition when communication is reliable but not necessarily FIFO. In this model, special care must be taken to ensure that messages do not accidentally overtake one another in the composed program. In this model no program that sends or receives messages can be composed automatically with arbitrary programs without jeopardizing their intended behavior. Safety of composition becomes context-sensitive and new tools are needed for ensuring it. The investigation of sealing in this model reveals a novel connection between Lamport causality and safe composition. A characterization of sealable programs is given, as well as efficient algorithms for testing if Q seals P and for constructing a seal for a class of straight-line programs. It is shown that every sealable program can be sealed using O(n) messages. In fact, 3n ? 4 messages are necessary and sufficient in the worst case, despite the fact that a sealable program may be open to interference on Ω(n2) channels.
References
[1]
Afek Y., Attiya H., Fekete A., Fischer M., Lynch N.A., Mansour Y., Wang D.-W., Zuck L.: Reliable communication over unreliable channels. J. ACM 41(6), 1267---1297 (1994)
[2]
Awerbuch B.: Complexity of network synchronization. J. ACM 32(4), 804---823 (1985)
[3]
Ben-Ari M.: Principles of Concurrent and Distributed Programming, 2nd edn. Addison-Wesley, Boston (2006)
[4]
Coffman E.G. Jr, Elphick M.J., Shoshani A.: System deadlocks. ACM Comput. Surv. 3(2), 67---78 (1971)
[5]
Elrad T., Francez N.: Decomposition of distributed programs into communication-closed layers. Sci. Comput. Program. 2(3), 155---173 (1982)
[6]
Engelhardt, K., Moses, Y.: Causing communication closure: Safe program composition with non-FIFO channels. In: Fraigniaud, P. (ed.) DISC 2005 19th International Symposium on Distributed Computing, volume 3724 of LNCS, pp. 229---243. Springer, 26---29 September (2005)
[7]
Engelhardt, K., Moses, Y.: Safe composition of distributed programs communicating over order-preserving imperfect channels. In: Pal, A., Kshemkalyani, A., Kumar, R., Gupta, A. (eds.) 7th International Workshop on Distributed Computing IWDC 2005, volume 3741 of LNCS, pp. 32---44. Springer, 27---30 December (2005)
[8]
Fokkinga, M., Poel, M., Zwiers, J.: Modular completeness for communication closed layers. In: Best, E. (ed.) CONCUR '93: 4th International Conference on Concurrency Theory, volume 715 of LNCS, pp. 50---65. Springer, Germany, Hildesheim, 23---26 August (1993)
[9]
Gerth, R., Shrira, L.: On proving communication closedness of distributed layers. In: Nori, K.V. (ed.) Foundations of Software Technology and Theoretical Computer Science, Sixth Conference, volume 241 of LNCS, pp. 330---343, Springer, New Delhi, India, 18---20 December (1986)
[10]
Janssen, W.: Layers as knowledge transitions in the design of distributed systems. In: Engberg, U.H., Larsen, K.G., Skou, A. (eds.) Proceedings of the Workshop on Tools and Algorithms for the Construction and Analysis of Systems, TACAS (Aarhus, Denmark, 19---20 May, 1995), number NS-95-2 in Notes Series, pp. 304---318, Department of Computer Science, University of Aarhus, May 1995. BRICS
[11]
Janssen, W., Poel, M., Zwiers, J.: Action systems and action refinement in the development of parallel systems. In: Baeten J.C.M., Groote, J.F. (eds.) Proceedings of CONCUR '91, 2nd International Conference on Concurrency Theory, volume 527 of LNCS, pp. 298---316, Amsterdam, The Netherlands (1991)
[12]
Janssen, W., Zwiers, J.: From sequential layers to distributed processes, deriving a minimum weight spanning tree algorithm, (extended abstract). In: Proceedings 11th ACM Symposium on Principles of Distributed Computing, pp. 215---227. ACM (1992)
[13]
Janssen, W., Zwiers, J.: Protocol design by layered decomposition: A compositional approach. In: Vytopil, J. (ed.) Formal Techniques in Real-Time and Fault-Tolerant Systems, volume 571 of LNCS, pp. 307---326. Springer (1992)
[14]
Janssen, W., Zwiers, J.: Specifiying and proving communication closedness in protocols. In: Danthine, A.A.S., Leduc, G., Wolper, P. (eds.) PSTV, volume C-16 of IFIP Transactions, pp. 323---339. North-Holland (1993)
[15]
Lamport L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM 7, 558---565 (1978)
[16]
Lynch N.A.: Distributed Algorithms. Morgan Kaufmann, San Mateo (1996)
[17]
Poel, M., Zwiers, J.: Layering techniques for development of parallel systems. In: von Bochmann, G., Probst, D.K. (eds.) Computer Aided Verification, Fourth International Workshop, CAV '92, volume 663 of LNCS, pp. 16---29. Springer, Montreal, Canada, 29 June---1 July (1992)
[18]
Stomp, F., de Roever, W.-P.: A correctness proof of a minimum-weight spanning tree algorithm (extended abstract). In: Popescu-Zeletin, R., Le Lann, G., Kim, K. (eds.) Proceedings of the 7th International Conference on Distributed Computing Systems, pp. 440---447. Computer Society Press of the IEEE (1987)
[19]
Stomp, F.A., de Roever, W.P.: Designing distributed algorithms by means of formal sequentially phased reasoning (extended abstract). In: Bermond J.-C., Raynal, M. (eds.) Distributed Algorithms, 3rd International Workshop, Nice, France, 26---28 September 1989, Proceedings, volume 392 of LNCS, pp. 242---253. Springer (1989)
[20]
Stomp F.A., de Roever W.-P.: A principle for sequential reasoning about distributed algorithms. Formal Asp. Comput. 6(6), 716---737 (1994)
[21]
Wang, D.-W., Zuck, L.D.: Tight bounds for the sequence transmission problem. In: PODC '89: Proceedings of the eighth annual ACM Symposium on Principles of Distributed Computing, pp. 73---83. ACM Press (1989)
[22]
Zwiers, J.: Layering and action refinement for timed systems. In: de Bakker, J.W., Huizing, C., de Roever, W.P., Rozenberg, G. (eds.) Real-Time: Theory in Practice, REX Workshop, volume 600 of LNCS, pp. 687---723. Springer (1991)
Recommendations
Causing communication closure: safe program composition with Non-FIFO channels
DISC'05: Proceedings of the 19th international conference on Distributed ComputingA semantic framework for analyzing safe composition of distributed programs is presented. Its applicability is illustrated by a study of program composition when communication is reliable but not necessarily FIFO . In this model, special care must be ...
Requirements Analysis for Vehicle-to-Vehicle Safety Communication
ICICEE '12: Proceedings of the 2012 International Conference on Industrial Control and Electronics EngineeringVehicle-to-vehicle safety communication has become an important means for improving driving safety. Vehicle-to vehicle safety communication requirements are studied systematically in this paper. The major safety applications are analyzed. Safety message ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Copyright © Copyright © 2009 Springer-Verlag.
Publisher
Springer-Verlag
Berlin, Heidelberg
Publication History
Published: 01 October 2009
Qualifiers
- Article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 16 Feb 2025