Verification of multiprocess probabilistic protocols

ABSTRACT

A new probabilistic symmetric solution to the n processes mutual exclusion problem is presented. The algorithm is verified formally using the extreme fairness approach to probabilistic verification.

REFERENCES

• 1: Burns, J.E., M.J. Fischer, P. Jackson, N.A. Lynch and G.L. Peterson, Shared Data Requirements for Imolementatin of Mutual Exclusion Using a Test-and-Set Primitive, in Proc. Intr. Conf. on Parallel Processing, 1978, 79-87.
• 2: Cohen, S.D. Lehmann and A. Pnueli, Symmetric and Economical Solution to the Mutual Exclusion Problem in Distributed Systems, The Hebrew University, Jerusalem, Aug. 1882.
• 3: Feller, W., An Introduction to Probability Theory and its application, Wiley International edition, 3rd edition, Vol. 1 Ch. XIII Section 7 pp. 322-324.
• 4: Sergiu Hart , Micha Sharir , Amir Pnueli, Termination of probabilistic concurrent programs: (extended abstract), Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-6, January 25-27, 1982, Albuquerque, Mexico [doi>10.1145/582153.582154]
• 5: Itai, A. and M. Rodeh, The Lord of the Ring, or Probabilistic Methods for Breaking Symmetry in Distributive Networks, RJ 3110, IBM, San Jose, 1981.
• 6: Daniel Lehmann , Michael O. Rabin, On the advantages of free choice: a symmetric and fully distributed solution to the dining philosophers problem, Proceedings of the 8th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.133-138, January 26-28, 1981, Williamsburg, Virginia [doi>10.1145/567532.567547]
• 7: Lehmann, D. and S. Shelah, Reasoning with Time and Chance, Institute of Mathematics, The Hebrew University, Jerusalem, Oct. 1982.
• 8: Zohar Manna , Amir Pnueli, Verification of Concurrent Programs: Temporal Proof Principles, Logic of Programs, Workshop, p.200-252, May 01, 1981
• 9: Manna, Z. and A. Pnueli, Verification of Concurrent Programs: A Temporal Proof System, in Prof. 4th School on Advanced Programming, Amsterdam, June 1982.
• 10: Zohar Manna , Amir Pnueli, How to cook a temporal proof system for your pet language, Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.141-154, January 24-26, 1983, Austin, Texas [doi>10.1145/567067.567082]
• 11: Susan Owicki , Leslie Lamport, Proving Liveness Properties of Concurrent Programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.4 n.3, p.455-495, July 1982 [doi>10.1145/357172.357178]
• 12: Amir Pnueli, On the extremely fair treatment of probabilistic algorithms, Proceedings of the fifteenth annual ACM symposium on Theory of computing, p.278-290, December 1983 [doi>10.1145/800061.808757]
• 13: Rabin, M.O., Probabilistic Algorithms, in Algorithms and Complexity, New Directions and Recent Results, Academic Press, NY, 1976.
• 14: Rabin, M.O., N-process Synchronization by 4log N-valued Shared Variables, in Tech Report Forschungs-institute fur Mathmatik, ETH, Zurich, Mar. 1980.
• 15: Rabin, M.O., The Choice Coordination Problem, Acta Informatica 17, (1982), 121-134.
• 16: Sharir, M. and S. Hart, Probabilistic Temporal Logics for Finite and Bounded Models, Tel-Aviv University, Tel-Aviv, Feb. 1983.
• 17: Zuck, L. and A. Pnueli, Verification of Concurrent Probabilistic Protocols, in Tech. Report, Dept. of Appl Math., Weizmann Institute of Science, Rehovot, Israel, 1983.

INDEX TERMS

Primary Classification:
  G. Mathematics of Computing
  G.3 PROBABILITY AND STATISTICS
      Subjects: Probabilistic algorithms (including Monte Carlo)

Additional Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.3 Concurrent Programming
  D.4 OPERATING SYSTEMS
      D.4.1 Process Management
          Subjects: Mutual exclusion

General Terms:
Algorithms, Design, Languages, Management