Advertisement

Categorial Semantics of a Solution to Distributed Dining Philosophers Problem

  • Zhen You
  • Jinyun Xue
  • Shi Ying
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6213)

Abstract

Distributed dining philosophers is regarded as one of the most representative resource allocation problems. Many strategies are employed for avoiding deadlock and starvation, the two well-known problems in Distributed Dining Philosophers Problem(DDPP). In this paper, the formal semantics of DDPP are originally proposed by using category theory based on the Chandy-Mirsa’s acyclic directed graph strategy. The goal is to demonstrate how category theory is used in precisely defining categorical semantics and diagrammatically describing philosophers’ priority, states-transition, and composition of processes, rather than to design a new algorithm to solve the DDPP. Compared with other formal techniques, category theory not only provides a good mathematical structure for formalizing different relationships and interactions at different abstract levels, but also its diagrammatical representation strengthens the traceability and understandability of philosophers’ priority and states-transformation; additionally, its universal constructions (like colimit) offer the ability to manipulate and reason about system configuration.

Keywords

Categorial Semantics Distributed Dining Philosophers Problem Category Theory Universal Constructions 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Dijkstra, E.W.: Hierarchical Ordering of Sequenial Processes. In: Operating Systems Techniques. Academic Press, London (1971)Google Scholar
  2. 2.
    Dijkstra, E.W.: Two Starvation-free Solutions of a General Exclusion Problem. EWD 625, Platanstraat 5, AI Nuenen, The Netherlands (1978)Google Scholar
  3. 3.
    Awerbuch, B., Saks, M.: A dining philosophers Algorithm With Polynomial Response Time. In: Proceedings of the 31st Annual IEEE Symposium on Foundations of Computer Science, pp. 65–74 (1990)Google Scholar
  4. 4.
    Page, I.A., Jacob, R.T., Chern, S.E.: Optimal Algorithms for Distributed Resource Allocation. IEEE Distributed Computing (1991)Google Scholar
  5. 5.
    Lehmann, D., Rabin, M.O.: On The Advantages of Free Choice: a Symetric and Fully Distributed Solution for The Dining Philosophers Problem. In: Roscoe, A.W. (ed.) A classical mind: essays in honour of C.A.R. Hoare, ch. 20, pp. 333–352. Prentice Hall, Englewood Cliffs (1994)Google Scholar
  6. 6.
    Duflot, M., Fribourg, L., Picaronny, C.: Randomized Dining Philosophers Without Fairness Assumption. Distrib. Comput. 17(1), 65–76 (2004)CrossRefGoogle Scholar
  7. 7.
    Garg, V.K.: Analysis of Distributed Systems With Many Identical Processes. Distributed Computing Systems, 358–365 (1988)Google Scholar
  8. 8.
    Aggarwal, S., Barbara, D., Meth, K.Z.: A Software Environment for The Specification And Analysis of Problems of Coordination And Concurrency. IEEE Transactions on Software Engineering 14(3), 280–290 (1988)CrossRefGoogle Scholar
  9. 9.
    Parashkevov, A.N., Yantchev, J.: ARC-a Tool for Efficient Refinement And Equivalence Checking for CSP. In: ICAPP 1996, pp. 68–75 (1996)Google Scholar
  10. 10.
    Furia, C.A., Rossi, M., Dino, M., Morzenti, A.: Automated Compositional Proofs for Real-time Systems. Theoretical Computer Science (2007)Google Scholar
  11. 11.
    Chandy, K.M., Misra, J.: The Drinking Philosophers Problem. Prog. Lang. Syst. 6(4), 632–646 (1984)CrossRefGoogle Scholar
  12. 12.
    Rine, D.C.: A Category Theory For Programming Languages. Mathematical System Theory 7(4), 304–317 (1973)MathSciNetCrossRefzbMATHGoogle Scholar
  13. 13.
    Reynolds, J.C.: Using Category Theory to Design Programming Languages. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 62–63. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  14. 14.
    Fiadeiro, J.L., Maibaum, T.: Categorical Semantics of Parallel Program Design. Science of Computer Programming 28(2-3), 111–138 (1997)CrossRefzbMATHGoogle Scholar
  15. 15.
    Minamizono, K., Katai, O., Shiose, T., Kawakami, H.: Analyses of Design Processes Based on Category Theory and Channel Theory. In: SICE Annual Conference in Fukui (2003)Google Scholar
  16. 16.
    Buisse, A., Dybjer, P.: The Interpretation of Intuitionistic Type Theory in Lacolly Cartesian Closed Categories an Intuitionistic Perspective. Electronic Notes in Theoretical Computer Science 218, 21–23 (2008)CrossRefzbMATHGoogle Scholar
  17. 17.
    Buisse, A., Dybjeri, P.: Towards Formallizing Categorical Models of Type Theory in Type Theory. Electronic Notes in Theoretical Computer Science 196, 137–151 (2008)CrossRefzbMATHGoogle Scholar
  18. 18.
    Ehrig, H., Grobe-Rhode, M., Wolter, U.: Applications of Category Theory to the Area of Algebraic Specification in Computer Science. Applied Categorical Structures 6, 1–35 (1998)MathSciNetCrossRefzbMATHGoogle Scholar
  19. 19.
    Altuncher, J.A., Panangaden, P.: A Mechanically Assisted Constructive Proof in Category Theory. In: Stickel, M.E. (ed.) CADE 1990. LNCS, vol. 449, pp. 673–674. Springer, Heidelberg (1990)CrossRefGoogle Scholar
  20. 20.
    Kozen, D., Kreitz, C., Richter, E.: Automating Proofs in Category Theory. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 392–407. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  21. 21.
    Fiadeiro, J.L., Maibaum, T.: A Mathematical Toolbox for Software Architect. In: Proc. 8th Int. Workshop on Software Sepcification and Design, pp. 44–55. IEEE Computer Science Press, Silver Springer, MD (1996)Google Scholar
  22. 22.
    Yang, X., Hou, J., Wan, J.: Formal Semantic Meanings of Architecture-Centric Model Mapping. In: Xu, M., Zhan, Y.-W., Cao, J., Liu, Y. (eds.) APPT 2007. LNCS, vol. 4847, pp. 640–649. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  23. 23.
    Crole, R.L.: Basic Category Theory for Models of Syntax. In: course notes for Summer School on Generic Programming, SSGP’s (2002)Google Scholar
  24. 24.
    Lenisa, M., Power, J., Watanabe, H.: Category Theory for Operational Semantics. Theoretical Computer Science 327, 135–154 (2004)MathSciNetCrossRefzbMATHGoogle Scholar
  25. 25.
    van Oosten, J.: Basic Category Theory (2002)Google Scholar
  26. 26.
    Fiadeiro, J.L.: Categories for Software Engnieering. Springer, Heidelberg (2005)zbMATHGoogle Scholar
  27. 27.
    Chandy, K.M., Misra, J.: Parallel Program Design: A Foundation. Addison-Wesley, Reading (1988)zbMATHGoogle Scholar
  28. 28.
    Milner, R.: Communiciation and Concurrency. Prentice Hall, Englewood Cliffs (1989)Google Scholar
  29. 29.
    Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall, Englewood Cliffs (1985)zbMATHGoogle Scholar
  30. 30.
    Moszkowshi, B.: Executing Temporal Logic Porgrams. Cambridge University Press, Cambridge (1986)Google Scholar
  31. 31.
    Duan, Z., Tian, C., Zhang, L.: A decision procedure for propositional projection temporal logic with infinite models. Acta Informatica 45(1) (2008)Google Scholar
  32. 32.
    Dijkstra, E.W.: Cooperating Sequential Proccess. In: Genuys, F. (ed.) Programming Langugages. Academic Press, London (1968)Google Scholar
  33. 33.
    Weidman, E.B., Page, I.P., Pervin, W.J.: Explicit Dynamic Exclusion Algorithm. In: Proceedings of the Third IEEE Symposium on Parallel and Distributed Processing, pp. 7142–7149. IEEE, Los Alamitos (1991)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2010

Authors and Affiliations

  • Zhen You
    • 1
    • 2
  • Jinyun Xue
    • 1
    • 2
  • Shi Ying
    • 1
  1. 1.State Key Lab of Software EngineeringWuhan UniversityWuhanP.R. China
  2. 2.Provincial Key Laboratory for High-Performance Computing TechnologyJiangxi Normal UniversityNanchangP.R. China

Personalised recommendations