Partially Ordered Runs: A Case Study
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.
KeywordsPartial Order Initial Segment Critical Section Finale Move Coherence Condition
Unable to display preview. Download preview PDF.
- 1.Uri Abraham. Bakery algorithms. Unpublished manuscript, pp. 35, 1993.Google Scholar
- 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
- 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.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