Advertisement

Partially Ordered Runs: A Case Study

  • Yuri Gurevich
  • Dean Rosenzweig
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1912)

Abstract

We look at some sources of insecurity and dificulty in reasoning about partially ordered runs of distributed ASMs, and propose some techniques to facilitate such reasoning. As a case study, we prove in detail correctness and deadlock-freedom for general partially ordered runs of distributed ASM models of Lamport’s Bakery Algorithm.

Keywords

Partial Order Initial Segment Critical Section Finale Move Coherence Condition 
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.
    Uri Abraham. Bakery algorithms. Unpublished manuscript, pp. 35, 1993.Google Scholar
  2. 2.
    Egon Börger, Yuri Gurevich, and Dean Rosenzweig. The bakery algorithm: Yet another specification and verification. In E. Börger, editor, Specification and Validation Methods, pages 231–243. Oxford University Press, 1995.Google Scholar
  3. 3.
    Paola Glavan and Dean Rosenzweig. Communicating evolving algebras. In E. Börger, H. Kleine Büning, G. Jäger, S. Martini, and M. M. Richter, editors, Computer Science Logic, number 702 in Lecture Notes in Computer Science, pages 182–215. Springer, 1993.CrossRefGoogle Scholar
  4. 4.
    Yuri Gurevich. Evolving algebra 1993: Lipari guide. In E. Börger, editor, Specification and Validation Methods, pages 9–36. Oxford University Press, 1995.Google Scholar
  5. 5.
    Yuri Gurevich and Larry Moss. Algebraic operational semantics and Occam. In E. Börger, H. Kleine Büning, and M. M. Richter, editors, CSL’89, 3rd Workshop on Computer Science Logic, number 440 in Lecture Notes in Computer Science, pages 176–192. Springer, 1990.Google Scholar
  6. 6.
    Leslie Lamport. A new solution of Dijkstra concurrent programming problem. Communications of the ACM, 17(8):453–455, 1974.MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2000

Authors and Affiliations

  • Yuri Gurevich
    • 1
  • Dean Rosenzweig
    • 1
  1. 1.Microsoft ResearchUniversity of ZagrebCroatia

Personalised recommendations