Partially Ordered Runs: A Case Study

Abstract. We look at some sources of insecurity and difficulty 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.

• Type: Conference
• Year: 2000
• Where: ASM
• Authors: Yuri Gurevich, Dean Rosenzweig
• Keywords: ASM 2000, Case Study, Computational Biology, Lamport’s Bakery Algorithm, Partially Ordered