{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,2]],"date-time":"2026-07-02T00:50:13Z","timestamp":1782953413543,"version":"3.54.5"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319712369","type":"print"},{"value":"9783319712376","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-71237-6_14","type":"book-chapter","created":{"date-parts":[[2017,11,17]],"date-time":"2017-11-17T20:13:02Z","timestamp":1510949582000},"page":"273-297","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":18,"title":["Safety and Liveness of MCS Lock\u2014Layer by Layer"],"prefix":"10.1007","author":[{"given":"Jieung","family":"Kim","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Vilhelm","family":"Sj\u00f6berg","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ronghui","family":"Gu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zhong","family":"Shao","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2017,11,19]]},"reference":[{"key":"14_CR1","unstructured":"Boyd-wickizer, S., Kaashoek, M.F., Morris, R., Zeldovich, N.: Non-scalable locks are dangerous. In: Proceedings of the Ottawa Linux Symposium (OLS 2012) (2012)"},{"key":"14_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-03359-9_2","volume-title":"Theorem Proving in Higher Order Logics","author":"E Cohen","year":"2009","unstructured":"Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: a practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 23\u201342. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03359-9_2"},{"key":"14_CR3","unstructured":"Corbet, J.: Ticket spinlocks, February 2008. https:\/\/lwn.net\/Articles\/267968\/"},{"issue":"1","key":"14_CR4","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1889997.1890001","volume":"33","author":"J Derrick","year":"2011","unstructured":"Derrick, J., Schellhorn, G., Wehrheim, H.: Mechanically verified proof obligations for linearizability. ACM Trans. Program. Lang. Syst. 33(1), 1\u201343 (2011)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"14_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"504","DOI":"10.1007\/978-3-642-14107-2_24","volume-title":"ECOOP 2010 \u2013 Object-Oriented Programming","author":"T Dinsdale-Young","year":"2010","unstructured":"Dinsdale-Young, T., Dodds, M., Gardner, P., Parkinson, M.J., Vafeiadis, V.: Concurrent abstract predicates. In: D\u2019Hondt, T. (ed.) ECOOP 2010. LNCS, vol. 6183, pp. 504\u2013528. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14107-2_24"},{"key":"14_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/978-3-540-30232-2_7","volume-title":"Formal Techniques for Networked and Distributed Systems \u2013 FORTE 2004","author":"S Doherty","year":"2004","unstructured":"Doherty, S., Groves, L., Luchangco, V., Moir, M.: Formal verification of a practical lock-free queue algorithm. In: de Frutos-Escrig, D., N\u00fa\u00f1ez, M. (eds.) FORTE 2004. LNCS, vol. 3235, pp. 97\u2013114. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30232-2_7"},{"key":"14_CR7","doi-asserted-by":"crossref","unstructured":"Gu, R., Koenig, J., Ramananandro, T., Shao, Z., Wu, X., Weng, S.-C., Zhang, H., Guo, Y.: Deep specifications and certified abstraction layers. In: Proceedings of the 42nd ACM Symposium on Principles of Programming Languages, pp. 595\u2013608 (2015)","DOI":"10.1145\/2676726.2676975"},{"key":"14_CR8","unstructured":"Gu, R., Shao, Z., Chen, H., Wu, X., Kim, J., Sjoberg, V., Costanzo, D.: Certikos: an extensible architecture for building certified concurrent OS kernels. In: 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI 2016). USENIX Association (2016)"},{"key":"14_CR9","unstructured":"Gu, R., Shao, Z., Wu, X., Kim, J., Koenig, J., Ramananandro, T., Sjoberg, V., Chen, H., Costanzo, D.: Language and compiler support for building certified concurrent abstraction layers. Technical report YALEU\/DCS\/TR-1530, Department of Computer Science, Yale University, New Haven, CT, October 2016"},{"key":"14_CR10","unstructured":"Hawblitzel, C., Howell, J., Lorch, J.R., Narayan, A., Parno, B., Zhang, D., Zill, B.: Ironclad apps: end-to-end security via automated full-system verification. In: Proceedings of the 11th USENIX Conference on Operating Systems Design and Implementation, (OSDI 2014) USENIX Association (2014)"},{"issue":"1","key":"14_CR11","doi-asserted-by":"crossref","first-page":"124","DOI":"10.1145\/114005.102808","volume":"13","author":"M Herlihy","year":"1991","unstructured":"Herlihy, M.: Wait-free synchronization. ACM Trans. Program. Lang. Syst. 13(1), 124\u2013149 (1991)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"14_CR12","volume-title":"The Art of Multiprocessor Programming","author":"M Herlihy","year":"2008","unstructured":"Herlihy, M., Shavit, N.: The Art of Multiprocessor Programming. Morgan Kaufmann, Burlington (2008)"},{"issue":"3","key":"14_CR13","doi-asserted-by":"crossref","first-page":"463","DOI":"10.1145\/78969.78972","volume":"12","author":"MP Herlihy","year":"1990","unstructured":"Herlihy, M.P., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst. 12(3), 463\u2013492 (1990)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"14_CR14","doi-asserted-by":"crossref","unstructured":"Jung, R., Swasey, D., Sieczkowski, F., Svendsen, K., Turon, A., Birkedal, L., Dreyer, D.: Iris: monoids and invariants as an orthogonal basis for concurrent reasoning. In: Proceedings 42nd ACM Symposium on Principles of Programming Languages, pp. 637\u2013650 (2015)","DOI":"10.1145\/2676726.2676980"},{"key":"14_CR15","doi-asserted-by":"crossref","unstructured":"Kim, J., Sj\u00f6berg, V., Gu, R., Shao, Z.: Safety and liveness of MCS lock\u2013layer by layer (long version). Technical report YALEU\/DCS\/TR-1535, Department of Computer Science, Yale University, New Haven, CT, September 2017","DOI":"10.1007\/978-3-319-71237-6_14"},{"key":"14_CR16","doi-asserted-by":"crossref","unstructured":"Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., et al.: seL4: formal verification of an OS kernel. In: SOSP 2009: the 22nd ACM SIGOPS Symposium on Operating Systems Principles, pp. 207\u2013220 (2009)","DOI":"10.1145\/1629575.1629596"},{"issue":"7","key":"14_CR17","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009)","journal-title":"Commun. ACM"},{"issue":"4","key":"14_CR18","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1007\/s10817-009-9155-4","volume":"43","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: A formally verified compiler back-end. J. Autom. Reason. 43(4), 363\u2013446 (2009)","journal-title":"J. Autom. Reason."},{"key":"14_CR19","doi-asserted-by":"crossref","unstructured":"Liang, H., Feng, X.: A program logic for concurrent objects under fair scheduling. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, pp. 385\u2013399. ACM, New York (2016)","DOI":"10.1145\/2837614.2837635"},{"key":"14_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1007\/978-3-642-40184-8_17","volume-title":"CONCUR 2013 \u2013 Concurrency Theory","author":"H Liang","year":"2013","unstructured":"Liang, H., Hoffmann, J., Feng, X., Shao, Z.: Characterizing progress properties of concurrent objects via contextual refinements. In: D\u2019Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013. LNCS, vol. 8052, pp. 227\u2013241. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40184-8_17"},{"issue":"1","key":"14_CR21","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1145\/103727.103729","volume":"9","author":"JM Mellor-Crummey","year":"1991","unstructured":"Mellor-Crummey, J.M., Scott, M.L.: Algorithms for scalable synchronization on shared-memory multiprocessors. ACM Trans. Comput. Syst. 9(1), 21\u201365 (1991)","journal-title":"ACM Trans. Comput. Syst."},{"key":"14_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/3-540-46674-6_24","volume-title":"Advances in Computing Science \u2014 ASIAN\u201999","author":"K Ogata","year":"1999","unstructured":"Ogata, K., Futatsugi, K.: Formal verification of the MCS list-based queuing lock. In: Thiagarajan, P.S., Yap, R. (eds.) ASIAN 1999. LNCS, vol. 1742, pp. 281\u2013293. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-46674-6_24"},{"key":"14_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/978-3-662-44202-9_9","volume-title":"ECOOP 2014 \u2013 Object-Oriented Programming","author":"P Rocha Pinto da","year":"2014","unstructured":"da Rocha Pinto, P., Dinsdale-Young, T., Gardner, P.: TaDA: a logic for time and data abstraction. In: Jones, R. (ed.) ECOOP 2014. LNCS, vol. 8586, pp. 207\u2013231. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-662-44202-9_9"},{"key":"14_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/978-3-662-49498-1_8","volume-title":"Programming Languages and Systems","author":"P Rocha Pinto da","year":"2016","unstructured":"da Rocha Pinto, P., Dinsdale-Young, T., Gardner, P., Sutherland, J.: Modular termination verification for non-blocking concurrency. In: Thiemann, P. (ed.) ESOP 2016. LNCS, vol. 9632, pp. 176\u2013201. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49498-1_8"},{"key":"14_CR25","doi-asserted-by":"crossref","unstructured":"Sergey, I., Nanevski, A., Banerjee, A.: Mechanized verification of fine-grained concurrent programs. In: PLDI 2015, pp. 77\u201387 (2015)","DOI":"10.1145\/2737924.2737964"},{"key":"14_CR26","doi-asserted-by":"crossref","unstructured":"Turon, A., Thamsborg, J., Ahmed, A., Birkedal, L., Dreyer, D.: Logical relations for fine-grained concurrency. In: POPL, pp. 343\u2013356 (2013)","DOI":"10.1145\/2429069.2429111"},{"key":"14_CR27","doi-asserted-by":"crossref","unstructured":"Yang , J., Hawblitzel, C.: Safe to the last instruction: automated verification of a type-safe operating system. In: Proceedings of the 2010 ACM Conference on Programming Language Design and Implementation, pp. 99\u2013110 (2010)","DOI":"10.1145\/1806596.1806610"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-71237-6_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,6]],"date-time":"2019-10-06T05:17:11Z","timestamp":1570339031000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-71237-6_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319712369","9783319712376"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-71237-6_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}