An Intuitionistic Epistemic Logic for Sequential Consistency on Shared Memory

  • Yoichi Hirai
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6355)


In the celebrated Gödel Prize winning papers, Herlihy, Shavit, Saks and Zaharoglou gave topological characterization of waitfree computation. In this paper, we characterize waitfree communication logically. First, we give an intuitionistic epistemic logic k∨ for asynchronous communication. The semantics for the logic k∨ is an abstraction of Herlihy and Shavit’s topological model. In the same way Kripke model for intuitionistic logic informally describes an agent increasing its knowledge over time, the semantics of k∨ describes multiple agents passing proofs around and developing their knowledge together. On top of the logic k∨, we give an axiom type that characterizes sequential consistency on shared memory. The advantage of intuitionistic logic over classical logic then becomes apparent as the axioms for sequential consistency are meaningless for classical logic because they are classical tautologies. The axioms are similar to the axiom type for prelinearity (ϕ ⊃ ψ) ∨ (ψ ⊃ ϕ). This similarity reflects the analogy between sequential consistency for shared memory scheduling and linearity for Kripke frames: both require total order on schedules or models. Finally, under sequential consistency, we give soundness and completeness between a set of logical formulas called waitfree assertions and a set of models called waitfree schedule models.


Modal Logic Shared Memory Simplicial Complex Intuitionistic Logic Kripke Model 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Alechina, N., Mendler, M., de Paiva, V., Hitter, E.: Categorical and Kripke Semantics for Constructive S4 Modal Logic. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol. 2142, pp. 292–307. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  2. 2.
    Attiya, H., Welch, J.L.: Sequential consistency versus linearizability. ACM Transactions on Computer Systems 12(2), 122 (1994)CrossRefGoogle Scholar
  3. 3.
    Balbiani, P., et al.: ‘Knowable’ as ‘known after an announcement’. The Review of Symbolic Logic 1(03), 305–334 (2008)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Baltag, A., Coecke, B., Sadrzadeh, M.: Epistemic actions as resources. Journal of Logic and Computation 17(3), 555 (2007)MathSciNetCrossRefzbMATHGoogle Scholar
  5. 5.
    Bieber, P., Onera-Cert, T.: A logic of communication in hostile environment. In: Proceedings of Computer Security Foundations Workshop III, 1990, pp. 14–22 (1990)Google Scholar
  6. 6.
    Costa, V., Benevides, M.: Formalizing concurrent common knowledge as product of modal logics. Logic Journal of IGPL 13(6), 665 (2005)MathSciNetCrossRefzbMATHGoogle Scholar
  7. 7.
    Ewald, W.B.: Intuitionistic tense and modal logic. The Journal of Symbolic Logic 51(1), 166–179 (1986)MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    Gafni, E., Koutsoupias, E.: Three-processor tasks are undecidable. SIAM Journal on Computing 28(3), 970–983 (1999)MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    Halpern, J.Y., Moses, Y.: Knowledge and common knowledge in a distributed environment. Journal of the ACM (JACM) 37(3), 549–587 (1990)MathSciNetCrossRefzbMATHGoogle Scholar
  10. 10.
    Herlihy, M.: Wait-free synchronization. ACM Transactions on Programming Languages and Systems 13(1), 124–149 (1991)CrossRefGoogle Scholar
  11. 11.
    Herlihy, M., Shavit, N.: The topological structure of asynchronous computability. Journal of the ACM 46(6), 858–923 (1999)MathSciNetCrossRefzbMATHGoogle Scholar
  12. 12.
    Herlihy, M., Wing, J.M.: Linearizability: A correctness condition for concurrent objects. ACM Transactions on Programming Languages and Systems (TOPLAS) 12(3), 463–492 (1990)CrossRefGoogle Scholar
  13. 13.
    Hintikka, J.: Knowledge and belief: an introduction to the logic of the two notions. Cornell University Press, Ithica (1962)Google Scholar
  14. 14.
    Jia, L., Walker, D.: Modal Proofs as Distributed Programs (Extended Abstract). In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, p. 219. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  15. 15.
    Kobayashi, N., Yonezawa, A.: Asynchronous communication model based on linear logic. Formal Aspects of Computing 7(2), 113–149 (1995)CrossRefzbMATHGoogle Scholar
  16. 16.
    Kojima, K., Igarashi, A.: On constructive linear-time temporal logic. In: Proc. of IMLA, p. 8 (2008)Google Scholar
  17. 17.
    Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess program. IEEE Transactions on Computers 100(28), 690–691 (1979)CrossRefzbMATHGoogle Scholar
  18. 18.
    Liau, C.J.: Belief, information acquisition, and trust in multi-agent systemsA modal logic formulation. Artificial Intelligence 149(1), 31–60 (2003)MathSciNetCrossRefzbMATHGoogle Scholar
  19. 19.
    Majer, O., Peliš, M.: Epistemic logic with relevant agents. In: The Logica Yearbook 2008, pp. 123–135. Kings College Publications (2009)Google Scholar
  20. 20.
    Ono, H.: On some intuitionistic modal logics. Publ. Res. Inst. Math. Sci. 13(3), 687–722 (1977)MathSciNetCrossRefzbMATHGoogle Scholar
  21. 21.
    Peleg, D.: Communication in concurrent dynamic logic. J. Comp. Syst. Sci. 35(1), 23–58 (1987)MathSciNetCrossRefzbMATHGoogle Scholar
  22. 22.
    Plaza, J.: Logics of public communications. Synthese 158(2), 165–179 (2007)MathSciNetCrossRefzbMATHGoogle Scholar
  23. 23.
    Plotkin, G., Stirling, C.: A framework for intuitionistic modal logics: extended abstract. In: TARK 1986: Proceedings of the 1986 Conference on Theoretical Aspects of Reasoning About Knowledge, pp. 399–406. Morgan Kaufmann Publishers Inc., San Francisco (1986)Google Scholar
  24. 24.
    Saks, M., Zaharoglou, F.: Wait-free k-set agreement is impossible: The topology of public knowledge. SIAM Journal on Computing 29(5), 1449–1483 (2000)MathSciNetCrossRefzbMATHGoogle Scholar
  25. 25.
    Steinke, R.C., Nutt, G.J.: A unified theory of shared memory consistency. Journal of the ACM 51(5), 800–849 (2004)MathSciNetCrossRefzbMATHGoogle Scholar
  26. 26.
    Suzuki, N.Y.: Kripke bundles for intermediate predicate logics and Kripke frames for intuitionistic modal logics. Studia Logica 49(3), 289–306 (1990)MathSciNetCrossRefzbMATHGoogle Scholar
  27. 27.
    Troelstra, A.S., van Dalen, D.: Constructivism in Mathematics: An Introduction, vol. 1. North-Holland, Amsterdam (1988)zbMATHGoogle Scholar
  28. 28.
    van Benthem, J.: The information in intuitionistic logic. Synthese 167(2), 251–270 (2009)MathSciNetCrossRefzbMATHGoogle Scholar
  29. 29.
    Woo, T.Y.C., Lam, S.S.: A lesson on authentication protocol design. SIGOPS Oper. Syst. Rev. 28(3), 24–37 (1994)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2010

Authors and Affiliations

  • Yoichi Hirai
    • 1
  1. 1.Dept. of Computer ScienceUniversity of TokyoTokyoJapan

Personalised recommendations