{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,21]],"date-time":"2026-05-21T09:07:31Z","timestamp":1779354451389,"version":"3.51.4"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032267511","type":"print"},{"value":"9783032267528","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-26752-8_11","type":"book-chapter","created":{"date-parts":[[2026,5,21]],"date-time":"2026-05-21T08:12:58Z","timestamp":1779351178000},"page":"180-190","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Identifying Design Flaws in\u00a0a\u00a0Lock-Free Task Pool with\u00a0TLA+"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0001-7429-1475","authenticated-orcid":false,"given":"Vasil","family":"Dyadov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4873-8306","authenticated-orcid":false,"given":"Alexander","family":"Kogtenkov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-5630-1896","authenticated-orcid":false,"given":"Ilya","family":"Shchepetkov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2026,5,22]]},"reference":[{"key":"11_CR1","doi-asserted-by":"publisher","unstructured":"Abrial, J.R.: Modeling in Event-B: system and software engineering. Cambridge Univ. Press (2010). https:\/\/doi.org\/10.1017\/CBO9781139195881","DOI":"10.1017\/CBO9781139195881"},{"key":"11_CR2","unstructured":"Abrial, J.R., Hallerstede, S.: Refinement, decomposition, and instantiation of discrete models: application to Event-B. Fund. Inform. 77(1\u20132), 1\u201328 (Jan2007)"},{"key":"11_CR3","doi-asserted-by":"publisher","unstructured":"Alistarh, D., Censor-Hillel, K., Shavit, N.: Are lock-free concurrent algorithms practically wait-free? J. ACM (JACM) 63(4) (2016). https:\/\/doi.org\/10.1145\/2903136","DOI":"10.1145\/2903136"},{"key":"11_CR4","doi-asserted-by":"publisher","unstructured":"Ben-David, N., Blelloch, G.E., Wei, Y.: Lock-free locks revisited. In: Proceedings of the 27th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, pp. 278\u2013293. PPoPP \u201922, Association for Computing Machinery, New York (2022). https:\/\/doi.org\/10.1145\/3503221.3508433","DOI":"10.1145\/3503221.3508433"},{"key":"11_CR5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5","author":"Y Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive theorem proving and program development. Springer (2004). https:\/\/doi.org\/10.1007\/978-3-662-07964-5","journal-title":"Springer"},{"issue":"6","key":"11_CR6","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1145\/3729175","volume":"68","author":"M Brooker","year":"2025","unstructured":"Brooker, M., Desai, A.: Systems correctness practices at Amazon Web Services. Commun. ACM 68(6), 38\u201342 (2025). https:\/\/doi.org\/10.1145\/3729175","journal-title":"Commun. ACM"},{"key":"11_CR7","doi-asserted-by":"publisher","unstructured":"Carbonneaux, Q., Zilberstein, N., Klee, C., O\u2019Hearn, P.W., Zappa Nardelli, F.: Applying formal verification to microkernel IPC at meta. In: Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 116\u2013129. ACM, Philadelphia (2022). https:\/\/doi.org\/10.1145\/3497775.3503681","DOI":"10.1145\/3497775.3503681"},{"key":"11_CR8","doi-asserted-by":"publisher","unstructured":"Cong, G., Bader, D.: Lock-free parallel algorithms: an experimental study. In: Boug\u00e9, L., Prasanna, V.K. (eds.) High Performance Computing - HiPC 2004, pp. 516\u2013527. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-30474-6_54","DOI":"10.1007\/978-3-540-30474-6_54"},{"key":"11_CR9","doi-asserted-by":"publisher","unstructured":"Cousineau, D., Doligez, D., Lamport, L., Merz, S., Ricketts, D., Vanzetto, H.: TLA+ Proofs. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) FM 2012: Formal Methods, pp. 147\u2013154. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-32759-9_14","DOI":"10.1007\/978-3-642-32759-9_14"},{"key":"11_CR10","doi-asserted-by":"publisher","unstructured":"Doherty, S., Groves, L., Luchangco, V., Moir, M.: Formal verification of a practical lock-free queue algorithm. In: Formal Techniques for Networked and Distributed Systems - FORTE 2004, pp. 97\u2013114. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30232-2_7","DOI":"10.1007\/978-3-540-30232-2_7"},{"key":"11_CR11","unstructured":"Fraser, K.: Practical Lock-Freedom. Tech. rep., University of Cambridge, Computer Laboratory (2004). https:\/\/doi.org\/10.48456\/tr-579"},{"key":"11_CR12","doi-asserted-by":"publisher","unstructured":"Gidron, E., Keidar, I., Perelman, D., Perez, Y.: SALSA: scalable and low synchronization NUMA-aware algorithm for producer-consumer pools. In: Proceedings of the 24th ACM symposium on Parallelism in algorithms and architectures - SPAA \u201912, p. 151. ACM Press, Pittsburgh (2012). https:\/\/doi.org\/10.1145\/2312005.2312035","DOI":"10.1145\/2312005.2312035"},{"key":"11_CR13","doi-asserted-by":"crossref","unstructured":"Gidron, E., Keidar, I., Perelman, D., Perez, Y.: SALSA: scalable and low synchronization NUMA-aware algorithm for producer-consumer pools. Tech. rep., Technion (2012). https:\/\/ece.technion.ac.il\/wp-content\/uploads\/2021\/01\/publication_807-1.pdf","DOI":"10.1145\/2312005.2312035"},{"key":"11_CR14","unstructured":"Hackett, F., Wrench, E., Macko, P., Davis, A.J.J., Wei, Y., Beschastnikh, I.: Trace Validation of Unmodified Concurrent Systems with OmniLink (2026). https:\/\/arxiv.org\/abs\/2601.11836"},{"issue":"3","key":"11_CR15","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1145\/78969.78972","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"11_CR16","doi-asserted-by":"publisher","unstructured":"Hurault, A., Qu\u00e9innec, P.: Proving a non-blocking algorithm for process renaming with TLA. In: Tests and Proofs, pp. 147\u2013166. Springer International Publishing (2019). https:\/\/doi.org\/10.1007\/978-3-030-31157-5_10","DOI":"10.1007\/978-3-030-31157-5_10"},{"issue":"2","key":"11_CR17","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1145\/505145.505149","volume":"11","author":"D Jackson","year":"2002","unstructured":"Jackson, D.: Alloy: a lightweight object modelling notation. ACM Trans. Softw. Eng. Methodol. 11(2), 256\u2013290 (2002). https:\/\/doi.org\/10.1145\/505145.505149","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"11_CR18","doi-asserted-by":"publisher","unstructured":"Jung, R., Krebbers, R., Jourdan, J.H., Bizjak, A., Birkedal, L., Dreyer, D.: Iris from the ground up: a modular foundation for higher-order concurrent separation logic. J. Funct. Programm. 28 (2018). https:\/\/doi.org\/10.1017\/S0956796818000151","DOI":"10.1017\/S0956796818000151"},{"key":"11_CR19","doi-asserted-by":"publisher","unstructured":"Konnov, I., Kukovec, J., Tran, T.H.: TLA+ Model checking made symbolic. Proc. ACM Program. Lang. 3(OOPSLA) (2019). https:\/\/doi.org\/10.1145\/3360549","DOI":"10.1145\/3360549"},{"issue":"3","key":"11_CR20","doi-asserted-by":"publisher","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L Lamport","year":"1994","unstructured":"Lamport, L.: The temporal logic of actions. ACM Trans. Program. Lang. Syst. 16(3), 872\u2013923 (1994). https:\/\/doi.org\/10.1145\/177492.177726","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"11_CR21","unstructured":"Lamport, L.: Specifying concurrent systems with TLA+. Calculational System Design, pp. 183\u2013247 (1999). https:\/\/www.microsoft.com\/en-us\/research\/publication\/specifying-concurrent-systems-tla\/"},{"key":"11_CR22","doi-asserted-by":"publisher","unstructured":"Lamport, L.: The PlusCal algorithm language. In: Theoretical Aspects of Computing - ICTAC 2009, pp. 36\u201360. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03466-4_2","DOI":"10.1007\/978-3-642-03466-4_2"},{"issue":"4","key":"11_CR23","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1145\/2699417","volume":"58","author":"C Newcombe","year":"2015","unstructured":"Newcombe, C., Rath, T., Zhang, F., Munteanu, B., Brooker, M., Deardeuff, M.: How amazon web services uses formal methods. Commun. ACM 58(4), 66\u201373 (2015). https:\/\/doi.org\/10.1145\/2699417","journal-title":"Commun. ACM"},{"key":"11_CR24","doi-asserted-by":"publisher","unstructured":"Nipkow, T., Klein, G.: Concrete Semantics. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-10542-0","DOI":"10.1007\/978-3-319-10542-0"},{"key":"11_CR25","doi-asserted-by":"publisher","unstructured":"Reif, W., Schellhorn, G., Stenzel, K., Balser, M.: Structured Specifications and Interactive Proofs with KIV, pp. 13\u201339. Springer (1998). https:\/\/doi.org\/10.1007\/978-94-017-0435-9_1","DOI":"10.1007\/978-94-017-0435-9_1"},{"key":"11_CR26","doi-asserted-by":"publisher","unstructured":"Tofan, B., Schellhorn, G., Reif, W.: Formal verification of a lock-free stack with hazard pointers. In: Cerone, A., Pihlajasaari, P. (eds.) ICTAC 2011. LNCS, vol. 6916, pp. 239\u2013255. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-23283-1_16","DOI":"10.1007\/978-3-642-23283-1_16"},{"key":"11_CR27","doi-asserted-by":"publisher","unstructured":"Vindum, S.F., Frumin, D., Birkedal, L.: Mechanized verification of a fine-grained concurrent queue from meta\u2019s folly library. In: Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, New York, NY, USA, pp. 100\u2013115 (2022). https:\/\/doi.org\/10.1145\/3497775.3503689","DOI":"10.1145\/3497775.3503689"},{"key":"11_CR28","doi-asserted-by":"publisher","unstructured":"Xiao, L., Hou, Z., Zhu, H., He, M., Qin, S.: Specifying and verifying programs over the MCA ARMv8 architecture with TLA. J. Circ. Syst. Comput. 35(01) (2026). DOI: https:\/\/doi.org\/10.1142\/S0218126625300089","DOI":"10.1142\/S0218126625300089"},{"key":"11_CR29","doi-asserted-by":"publisher","unstructured":"Yu, Y., Manolios, P., Lamport, L.: Model checking TLA+ specifications. In: Correct Hardware Design and Verification Methods, pp. 54\u201366. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48153-2_6","DOI":"10.1007\/3-540-48153-2_6"}],"container-title":["Lecture Notes in Computer Science","Rigorous State-Based Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-26752-8_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,21]],"date-time":"2026-05-21T08:13:01Z","timestamp":1779351181000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-26752-8_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032267511","9783032267528"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-26752-8_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"22 May 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ABZ","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Rigorous State-Based Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Tokyo","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Japan","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 May 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 May 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"abz2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/abz-conf.org\/site\/2026\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}