Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Automated implementation of complex distributed algorithms specified in the IOA language

  • Regular Contribution
  • Published:
International Journal on Software Tools for Technology Transfer Aims and scope Submit manuscript

Abstract

IOA is a formal language for describing Input/Output automata that serves both as a formal specification language and as a programming language (Garland et al. in http://theory.lcs.mit.edu/tds/ioa/manual.ps, 2004). The IOA compiler automatically translates IOA specifications into Java code that runs on a set of workstations communicating via the Message Passing Interface. This paper describes the process of compiling IOA specifications and our experiences running several distributed algorithms, ranging from simple ones such as the Le Lann, Chang and Roberts (LCR) leader election in a ring algorithm to that of Gallager, Humblet and Spira (GHS) for minimum-weight spanning tree formation in an arbitrary graph (Humblet et al. in ACM Trans Program Lang Syst 5(1):66–77, 1983). Our IOA code for all the algorithms is derived from their Input/Output automaton descriptions that have already been formally proved correct. The successful implementation of these algorithms is significant for two reasons: (a) it is an indication of the capabilities of the IOA compiler and of its advanced state of development, and (b) to the best of our knowledge, these are the first complex, distributed algorithms implemented in an automated way that have been formally and rigorously proved correct. Thus, this work shows that it is possible to formally specify, prove correct, and implement complex distributed algorithms using a common formal methodology.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Georgiou, C., Lynch, N., Mavrommatis, P., Tauber, J.A.: Automated implementation of complex distributed algorithms specified in the IOA language. In: Proceedings of 18th International Conference on Parallel and Distributed Computing Systems (PDCS 2005), pp. 128–134 (2005)

  2. Garland, S., Lynch, N., Tauber, J., Vaziri, M.: IOA user guide and reference manual. Technical Report MIT/LCS/TR-961, Laboratory for Computer Science, Massachusetts Institute of Technology, Cambridge, MA, July 2004. http://theory.lcs.mit.edu/tds/ioa/manual.ps.

  3. Lynch, N.A., Tuttle, M.R.: Hierarchical correctness proofs for distributed algorithms. In: Proceedings of the Sixth Annual ACM Symposium on Principles of Distributed Computing, pp. 137–151, Vancouver, British Columbia, Canada (1987)

  4. Lynch N.A., Tuttle, M.R.: An introduction to input/output automata. CWI-Quarterly. 2 (3), 219–246, September 1989. Centrum voor Wiskunde en Informatica, Amsterdam, The Netherlands. Technical Memo MIT/LCS/TM-373, Laboratory for Computer Science, Massachusetts Institute of Technology, Cambridge, MA, November 1988

  5. Chefter, A.E.: A simulator for the IOA language. Master’s thesis, Department of Electrical Engineering and Computer Science, Massachusetts Institute of Technology, Cambridge, MA (1998)

  6. Dean, L.G.: Improved simulation of Input/Output automata. Master’s thesis, Department of Electrical Engineering and Computer Science, Massachusetts Institute of Technology, Cambridge, MA (2001)

  7. Kırlı Kaynar, D., Chefter, A., Dean, L., Garland, S., Lynch, N., Ne Win, T., Ramırez-Robredo, A.: The IOA simulator. Technical Report MIT-LCS-TR-843, MIT Laboratory for Computer Science, Cambridge, MA, July 2002

  8. Antonio Ramırez-Robredo, J.: Paired simulation of I/O automata. Master’s thesis, Department of Electrical Engineering and Computer Science, Massachusetts Institute of Technology, Cambridge, MA (2000)

  9. Solovey, E.: Simulation of composite I/O automata. Master’s thesis, Department of Electrical Engineering and Computer Science, Massachusetts Institute of Technology, Cambridge, MA (2003)

  10. Tsai, M.J.: Code generation for the IOA language. Master’s thesis, Department of Electrical Engineering and Computer Science, Massachusetts Institute of Technology, Cambridge, MA (2002)

  11. Ne Win, T.: Theorem-proving distributed algorithms with dynamic analysis. Master’s thesis, Department of Electrical Engineering and Computer Science, Massachusetts Institute of Technology, Cambridge, MA (2003)

  12. Bogdanov, A.: Formal verification of simulations between I/O automata. Master’s thesis, Department of Electrical Engineering and Computer Science, Massachusetts Institute of Technology, Cambridge, MA (2001)

  13. Garland, S.J., Lynch, N.A.: The IOA language and toolset: support for designing, analyzing, and building distributed systems. Technical Report MIT/LCS/TR-762, Laboratory for Computer Science, Massachusetts Institute of Technology, Cambridge, MA, August 1998. http://theory.lcs.mit.edu/tds/papers/Lynch/IOA-TR-762.ps

  14. Tauber, J.A.: Verifiable Compilation of I/O Automata without Global Synchronization. PhD thesis, Department of Electrical Engineering and Computer Science, Massachusetts Institute of Technology, Cambridge, MA (2004)

  15. Tauber, J.A., Lynch, N.A., Tsai, M.J.: Compiling IOA without global synchronization. In: Proceedings of the 3rd IEEE International Symposium on Network Computing and Applications (IEEE NCA04), pp. 121–130. Cambridge, MA (2004)

  16. Chang E., Roberts R.: An improved algorithm for decentralized extrema-finding in circular configurations of processes. Commun. ACM 22(5), 281–283 (1979)

    Article  MATH  Google Scholar 

  17. Chang E.J.H.: Echo algorithms: depth parallel operations on general graphs. IEEE Trans. Softw. Eng. SE-8(4), 391–401 (1982)

    Article  Google Scholar 

  18. Le Lann, G.: Distributed systems—towards a formal approach. In: Gilchrist, B. (ed.) Information Processing 77 (Toronto, August 1977). Proceedings of IFIP Congress, vol. 7, pp. 155–160. North-Holland Publishing Co., Amsterdam (1977)

  19. Segall, A.: Distributed network protocols. IEEE Trans. Inf. Theory IT-29(1), 23–35 (1983)

    Google Scholar 

  20. Lynch N.: Distributed Algorithms. Morgan Kaufmann Publishers Inc., San Mateo, CA (1996)

    MATH  Google Scholar 

  21. Humblet, P.A., Gallager, R.G., Spira, P.M.: A distributed algorithm for minimum-weight spanning trees. In: ACM Transactions on Programming Languages and Systems, vol. 5(1), pp. 66–77 (1983)

  22. Lampoft, L., Welch, J., Lynch, N.: A lattice-structured proof of a minimum spanning tree algorithm. In: Proceedings of 7th ACM Symposium on Principles of Distributed Computing, pp. 28–43 (1988)

  23. Message Passing Interface Forum. MPI: A message-passing interface standard. Int. J. Supercomput. Appl. 8(3–4), 1994

  24. Goldman K.J.: Highly concurrent logically synchronous multicast. Distrib. Comput. 6(4), 189–207 (1991)

    Article  Google Scholar 

  25. Goldman K.J., Swaminathan B., Paul McCartney T., Anderson M.D., Sethuraman R.: The Programmers’ Playground: I/O abstraction for user-configurable distributed applications. IEEE Trans. Softw. Eng. 21(9), 735–746 (1995)

    Article  Google Scholar 

  26. Cheiner, O., Shvartsman, A.: Implementing an eventually-serializable data service as a distributed system building block. In: Mavronicolas, M., Merritt, M., Shavit, N. (eds.) Networks in Distributed Computing. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 45, pp. 43–72. American Mathematical Society, Providence, RI (1999)

  27. Fekete, A., Gupta, D., Luchangco, V., Lynch, N., Shvartsman, A.: Eventually-serializable data services. In: Proceedings of the Fifteenth Annual ACM Symposium on Principles of Distributed Computing, pp. 300–309, Philadelphia, PA (1996)

  28. Hoare C.A.R.: Communicating Sequential Processes. Prentice-Hall International, UK (1985)

    MATH  Google Scholar 

  29. INMOS Ltd: occam Programming Manual (1984)

  30. Milner R.: Communication and Concurrency. Prentice-Hall International, UK (1989)

    MATH  Google Scholar 

  31. Vaandrager, F.W.: On the relationship between process algebra and input/output automata. In: Proceedings of the 6th Annual Symposium on Logic in Computer Science (LICS 1991), pp. 387–398 (1991)

  32. Gelastou, M., Georgiou, C., Philippou, A.: On the application of formal methods for specifying and verifying distributed protocols. In: Proceedings of the 7th IEEE International Symposium on Network Computing and Applications (NCA 2008), pp. 195–204 (2008)

  33. Cleaveland, R., Parrow, J., Steffen ,B.U.: The concurrency workbench: a semantics-based tool for the verification of concurrent systems. ACM TOPLAS 15(1), 1993 (1993)

  34. Cleaveland, R., Gada, J.N., Lewis, P.M., Smolka, S.A., Sokolsky, O., Zhang, S.: The Concurrency Factory—practical tools for specification, simulation, verification and implementation of concurrent systems. In: Specification of Parallel Algorithms. DIMACS Workshop, pp. 75–89. American Mathematical Society, Providence, RI (1994)

  35. Baker, M., Carpenter, B., Ko, S.H., Li, X.: mpiJava: A Java interface to MPI. First UK Workshop on Java for High Performance Network Computing, Europar (1998, presented)

  36. Tauber, J.A., Garland, S.J.: Definition and expansion of composite automata in IOA. Technical Report MIT/LCS/TR-959, Laboratory for Computer Science, Massachusetts Institute of Technology, Cambridge, MA, July 2004. http://theory.lcs.mit.edu/tds/papers/Tauber/MIT-LCS-TR-959.pdf

  37. Georgiou, C., Musial, P.M., Shvartsman, A.A., Sonderegger, E.L.: An abstract channel specification and an algorithm implementing it using java sockets. In: Proceedings of the 7th IEEE International Symposium on Network Computing and Applications (NCA 2008), pp. 211–219 (2008)

  38. Kaynar D.K., Lynch N., Segala R., Vaandrager F.: The Theory of Timed I/O Automata. Morgan & Claypool Publishers, San Francisco (2006)

    Google Scholar 

  39. Lynch, N., Michel, L., Shvartsman, A.: Tempo: A toolkit for the timed input/output automata formalism. In: Proceedings of the 1st International Conference on Simulation Tools and Techniques for Communications, Networks, and Systems (SIMUTools 2008)—Industrial Track: Simulation Works (2008)

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Cyprus, Nicosia, Cyprus

    Chryssis Georgiou

  2. MIT CSAIL, Cambridge, MA, USA

    Nancy Lynch & Joshua A. Tauber

  3. Google Inc., Mountain View, CA, USA

    Panayiotis Mavrommatis

Authors
  1. Chryssis Georgiou
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Nancy Lynch
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Panayiotis Mavrommatis
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Joshua A. Tauber
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Chryssis Georgiou.

Additional information

This work was supported in part by the USAF, AFRL award #FA9550-04-1-0121 and MURI AFOSR award #SA2796PO 1-0000243658. A preliminary version of this paper has appeared in [1].

The work of the author C. Georgiou is supported in part by research funds at the University of Cyprus.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Georgiou, C., Lynch, N., Mavrommatis, P. et al. Automated implementation of complex distributed algorithms specified in the IOA language. Int J Softw Tools Technol Transfer 11, 153–171 (2009). https://doi.org/10.1007/s10009-008-0097-7

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10009-008-0097-7

Keywords

Search

Navigation