Advertisement

Multiway synchronization verified with coupled simulation

  • Joachim Parrow
  • Peter Sjödin
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 630)

Abstract

We consider the problem of implementing multiway synchronization in a distributed environment providing only binary asynchronous communication. Our implementation strategy is formulated as a transformation on transition systems and we give a distributed algorithm for multiway synchronization. Correctness assertions and proofs are based on a new method: coupled simulations. The coupled simulation equivalence is weaker than observation equivalence and stronger than testing equivalence and combines some of their advantages. Like observation equivalence (and unlike testing) it is established through case analysis over single transitions. Like testing equivalence (and unlike observation) it allows an internal choice to be distributed onto several internal choices. The latter is particularly important when relating our distributed implementations to their specifications.

Keywords

Transition System External Action Parallel Composition Couple Simulation Correctness Property 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    R. J. R. Back and R. Kurki-Suonio. Distributed cooperation with action systems. ACM Transactions on Programming Languages and Systems, 10(4):513–554, 1988.zbMATHCrossRefGoogle Scholar
  2. 2.
    R. Bagrodia. Process synchronization: Design and performance evaluation of distributed algorithms. IEEE Transactions on Software Engineering, 15(9):1053–1065, September 1989.CrossRefGoogle Scholar
  3. 3.
    T. Bolognesi and E. Brinksma. Introduction to the ISO specification language LOTOS. In P. H. J. van Eijk, C. A. Vissers, and M. Diaz, editors, The Formal Description Technique LOTOS, pages 23–73. North-Holland, 1989.Google Scholar
  4. 4.
    A. Charlesworth. The multiway rendezvous. ACM Transactions on Programming Languages and Systems, 9(2):350–366, July 1987.zbMATHCrossRefGoogle Scholar
  5. 5.
    R. De Nicola and M. C. B. Hennessy. Testing equivalences for processes. Theoretical Computer Science, 34(1,2):83–133, 1984.zbMATHMathSciNetCrossRefGoogle Scholar
  6. 6.
    P. Eklund. Synchronizing multiple processes in common handshakes. Reports on Computer Science and Mathematics 39, Åbo Akademi, Finland, 1984.Google Scholar
  7. 7.
    M. Evangelist, N. Francez, and S. Katz. Multiparty interactions for interprocess communication and synchronization. IEEE Transactions on Software Engineering, 15(11):1417–1426, November 1989.CrossRefGoogle Scholar
  8. 8.
    N. Francez and I. R. Forman. Superimposition for interacting processes. In J. C. M. Baeten and J. W. Klop, editors, Proceedings of CONCUR '90, volume 458 of Lecture Notes in Computer Science, pages 230–245. Springer-Verlag, 1990.Google Scholar
  9. 9.
    N. Francez, B. Hailpern, and G. Taubenfeld. Script: A communication abstraction mechanism. Science of Computer Programming, 6(1):35–88, January 1986.zbMATHCrossRefGoogle Scholar
  10. 10.
    Y.-J. Joung and S. A. Smolka. Coordinating first-order multiparty interactions. In Proc. 17th Annual ACM Symposium on Principles of Programming Languages, pages 209–220, Orlando, Florida, January 1991.Google Scholar
  11. 11.
    D. Kumar. An implementation of N-party synchronization using tokens. In Proc. 10th International Conference on Distributed Computing Systems, pages 320–327. IEEE, 1990.Google Scholar
  12. 12.
    R. Milner. Communication and Concurrency. Prentice Hall, 1989.Google Scholar
  13. 13.
    K. Mitchell. Implementations of Process Synchronization and their Analysis. PhD thesis, Department of Computer Science, University of Edinburgh, July 1986.Google Scholar
  14. 14.
    M. H. Park and M. Kim. A distributed synchronization scheme for fair multi-process handshakes. Information Processing Letters, 34(3):131–138, April 1990.zbMATHMathSciNetCrossRefGoogle Scholar
  15. 15.
    S. Ramesh. A new and efficient implementation of multiprocess synchronization. In Parallel Architectures and Languages Europe, volume 259 of Lecture Notes in Computer Science, pages 387–401. Springer-Verlag, 1987.Google Scholar
  16. 16.
    S. Ramesh and S. L. Mehndiratta. A methodology for developing distributed programs. IEEE Transactions on Software Engineering, SE-13(8):967–976, August 1987.Google Scholar
  17. 17.
    P. Sjödin. From LOTOS Specifications to Distributed Implementations. PhD thesis, Department of Computer Systems, Uppsala University, Uppsala, Sweden, 1991.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1992

Authors and Affiliations

  • Joachim Parrow
    • 1
    • 2
  • Peter Sjödin
    • 1
    • 2
  1. 1.Swedish Institute of Computer ScienceKistaSweden
  2. 2.Department of Computer SystemsUppsala UniversitySweden

Personalised recommendations