{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T22:34:30Z","timestamp":1725834870847},"publisher-location":"Cham","reference-count":19,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319252575"},{"type":"electronic","value":"9783319252582"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-25258-2_28","type":"book-chapter","created":{"date-parts":[[2015,10,19]],"date-time":"2015-10-19T03:10:18Z","timestamp":1445224218000},"page":"399-413","source":"Crossref","is-referenced-by-count":2,"title":["Under the Hood of the Bakery Algorithm: Mutual Exclusion as a Matter of Priority"],"prefix":"10.1007","author":[{"given":"Yoram","family":"Moses","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Katia","family":"Patkin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,11,20]]},"reference":[{"issue":"25","key":"28_CR1","doi-asserted-by":"publisher","first-page":"2724","DOI":"10.1016\/j.tcs.2011.01.030","volume":"412","author":"U. Abraham","year":"2011","unstructured":"Abraham, U.: Logical classification of distributed algorithms (Bakery Algorithms as an example). Theor. Comput. Sci.\u00a0412(25), 2724\u20132745 (2011)","journal-title":"Theor. Comput. Sci."},{"key":"28_CR2","doi-asserted-by":"crossref","unstructured":"Anderson, J.H.: Lamport on mutual exclusion: 27 years of planting seeds. In: Proceedings of the 20th ACM PODC Conference, pp. 3\u201312 (2001)","DOI":"10.1145\/383962.383967"},{"key":"28_CR3","doi-asserted-by":"crossref","unstructured":"Attiya, H., Welch, J.: Distributed computing: fundamentals, simulations, and advanced topics, vol.\u00a019 (2004)","DOI":"10.1002\/0471478210"},{"key":"28_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/978-3-642-14203-1_12","volume-title":"Automated Reasoning","author":"K. Chaudhuri","year":"2010","unstructured":"Chaudhuri, K., Doligez, D., Lamport, L., Merz, S.: Verifying safety properties with the TLA+ proof system. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS, vol.\u00a06173, pp. 142\u2013148. Springer, Heidelberg (2010)"},{"issue":"9","key":"28_CR5","doi-asserted-by":"publisher","first-page":"569","DOI":"10.1145\/365559.365617","volume":"8","author":"E.W. Dijkstra","year":"1965","unstructured":"Dijkstra, E.W.: Solution of a problem in concurrent programming control. Commun. ACM\u00a08(9), 569 (1965)","journal-title":"Commun. ACM"},{"key":"28_CR6","doi-asserted-by":"crossref","unstructured":"Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning about Knowledge (2003)","DOI":"10.7551\/mitpress\/5803.001.0001"},{"issue":"3","key":"28_CR7","doi-asserted-by":"publisher","first-page":"549","DOI":"10.1145\/79147.79161","volume":"37","author":"J.Y. Halpern","year":"1990","unstructured":"Halpern, J.Y., Moses, Y.: Knowledge and common knowledge in a distributed environment. Journal of the ACM\u00a037(3), 549\u2013587 (1990)","journal-title":"Journal of the ACM"},{"issue":"9","key":"28_CR8","doi-asserted-by":"publisher","first-page":"1622","DOI":"10.1016\/j.scico.2013.03.003","volume":"78","author":"W.H. Hesselink","year":"2013","unstructured":"Hesselink, W.H.: Mechanical verification of Lamport\u2019s Bakery Algorithm. Science of Computer Programming\u00a078(9), 1622 (2013)","journal-title":"Science of Computer Programming"},{"issue":"8","key":"28_CR9","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/361082.361093","volume":"17","author":"L. Lamport","year":"1974","unstructured":"Lamport, L.: A new solution of Dijkstra\u2019s concurrent programming problem. Commun. ACM\u00a017(8), 453\u2013455 (1974)","journal-title":"Commun. ACM"},{"issue":"1","key":"28_CR10","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1145\/357062.357068","volume":"1","author":"L. Lamport","year":"1979","unstructured":"Lamport, L.: A new approach to proving the correctness of multiprocess programs. ACM Trans. Program. Lang. Syst.\u00a01(1), 84\u201397 (1979)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"28_CR11","doi-asserted-by":"crossref","unstructured":"Lamport, L.: What it means for a concurrent program to satisfy a specification: Why no one has specified priority. In: Proceedings of the 12th ACM POPL, pp. 78\u201383 (1985)","DOI":"10.1145\/318593.318616"},{"issue":"2","key":"28_CR12","first-page":"77","volume":"1","author":"L. Lamport","year":"1986","unstructured":"Lamport, L.: On Interprocess Communication. Part I: Basic Formalism. Distributed Computing\u00a01(2), 77\u201385 (1986)","journal-title":"Part I: Basic Formalism. Distributed Computing"},{"issue":"1","key":"28_CR13","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/7351.7352","volume":"5","author":"L. Lamport","year":"1987","unstructured":"Lamport, L.: A fast mutual exclusion algorithm. ACM Trans. Comput. Syst.\u00a05(1), 1\u201311 (1987)","journal-title":"ACM Trans. Comput. Syst."},{"key":"28_CR14","unstructured":"Lamport, L.: A TLA+ mechanical proof of the Boulangerie Algorithm (2015). \n                    \n                      http:\/\/research.microsoft.com\/en-us\/um\/people\/lamport\/tla\/boulangerie.html"},{"key":"28_CR15","unstructured":"Lamport, L.: The TLA+ Hyperbook (2015). \n                    \n                      http:\/\/research.microsoft.com\/en-us\/um\/people\/lamport\/tla\/hyperbook.html"},{"key":"28_CR16","unstructured":"Lynch, N.A.: Distributed Algorithms (1996)"},{"key":"28_CR17","unstructured":"Raynal, M., Beeson, D.: Algorithms for Mutual Exclusion (1986)"},{"key":"28_CR18","unstructured":"Rosenzweig, D., B\u00f6rger, E., Gurevich, Y.: The bakery algorithm: yet another specification and verification. In: B\u00f6rger, E. (ed.) Specification and Validation Methods, pp. 231\u2013243 (1995)"},{"key":"28_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/3-540-44450-5_26","volume-title":"FST TCS 2000: Foundations of Software Technology and Theoretical Science","author":"E. Sedletsky","year":"2000","unstructured":"Sedletsky, E., Pnueli, A., Ben-Ari, M.: Formal verification of the ricart-agrawala algorithm. In: Kapoor, S., Prasad, S. (eds.) FST TCS 2000. LNCS, vol.\u00a01974, pp. 325\u2013335. Springer, Heidelberg (2000)"}],"container-title":["Lecture Notes in Computer Science","Structural Information and Communication Complexity"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-25258-2_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T03:43:56Z","timestamp":1559274236000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-25258-2_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319252575","9783319252582"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-25258-2_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}