{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,12]],"date-time":"2026-03-12T01:06:35Z","timestamp":1773277595464,"version":"3.50.1"},"publisher-location":"Singapore","reference-count":28,"publisher":"Springer Nature Singapore","isbn-type":[{"value":"9789819789429","type":"print"},{"value":"9789819789436","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,10,28]],"date-time":"2024-10-28T00:00:00Z","timestamp":1730073600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,10,28]],"date-time":"2024-10-28T00:00:00Z","timestamp":1730073600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Stateless model checking (SMC) is crucial for productivity in verified concurrent programming, and its recent developments for C\/C++ and weak memory models are remarkable. The state-of-the-art SMC for C, GenMC, efficiently verifies C programs based on C11 atomics and pthreads. However, it does not support mixed-size accesses, accesses to the same memory region with different-sized types, even though they are ubiquitous in C\/C++, particularly the code for memory management. As a result, GenMC does not work for C\/C++ programs containing memory management. To resolve this problem, we develop a method of adapting GenMC to mixed-size accesses preserving its optimality. We experimentally evaluate the efficiency of our extended implementation of GenMC and its efficacy for memory management programs.<\/jats:p>","DOI":"10.1007\/978-981-97-8943-6_17","type":"book-chapter","created":{"date-parts":[[2024,10,28]],"date-time":"2024-10-28T08:45:29Z","timestamp":1730105129000},"page":"346-364","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Efficiently Adapting Stateless Model Checking for C11\/C++11 to Mixed-Size Accesses"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1496-1422","authenticated-orcid":false,"given":"Shigeyuki","family":"Sato","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0005-4870-9574","authenticated-orcid":false,"given":"Taiyo","family":"Mizuhashi","sequence":"additional","affiliation":[]},{"given":"Genki","family":"Kimura","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5224-382X","authenticated-orcid":false,"given":"Kenjiro","family":"Taura","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,10,28]]},"reference":[{"key":"17_CR1","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Aronis, S., Atig, M.F., Jonsson, B., Leonardsson, C., Sagonas, K.: Stateless model checking for TSO and PSO. In: Tools and Algorithms for the Construction and Analysis of Systems: 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11\u201318, 2015, Proceedings. Lecture Notes in Computer Science, vol.\u00a09035, pp. 353\u2013367. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_28","DOI":"10.1007\/978-3-662-46681-0_28"},{"key":"17_CR2","doi-asserted-by":"publisher","first-page":"789","DOI":"10.1007\/s00236-016-0275-0","volume":"54","author":"PA Abdulla","year":"2017","unstructured":"Abdulla, P.A., Aronis, S., Atig, M.F., Jonsson, B., Leonardsson, C., Sagonas, K.: Stateless model checking for TSO and PSO. Acta Informatica 54, 789\u2013818 (2017). https:\/\/doi.org\/10.1007\/s00236-016-0275-0","journal-title":"Acta Informatica"},{"key":"17_CR3","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Aronis, S., Jonsson, B., Sagonas, K.: Optimal dynamic partial order reduction. In: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 373\u2013384. POPL \u201914, ACM (2014). https:\/\/doi.org\/10.1145\/2535838.2535845","DOI":"10.1145\/2535838.2535845"},{"key":"17_CR4","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Aronis, S., Jonsson, B., Sagonas, K.: Source sets: a foundation for optimal dynamic partial order reduction. J. ACM 64(4), 25:1\u201325:49 (2017). https:\/\/doi.org\/10.1145\/3073408","DOI":"10.1145\/3073408"},{"key":"17_CR5","doi-asserted-by":"publisher","unstructured":"Alglave, J., Deacon, W., Grisenthwaite, R., Hacquard, A., Maranget, L.: Armed cats: Formal concurrency modelling at Arm. ACM Trans. Program. Lang. Syst. 43(2), 8:1\u20138:54 (2021). https:\/\/doi.org\/10.1145\/3458926","DOI":"10.1145\/3458926"},{"key":"17_CR6","doi-asserted-by":"publisher","unstructured":"Alglave, J., Maranget, L., Tautschnig, M.: Herding cats: Modelling, simulation, testing, and data mining for weak memory. ACM Trans. Program. Lang. Syst. 36(2), 7:1\u20137:74 (2014). https:\/\/doi.org\/10.1145\/2627752","DOI":"10.1145\/2627752"},{"key":"17_CR7","doi-asserted-by":"publisher","unstructured":"Appel, A.W., Naumann, D.A.: Verified sequential malloc\/free. In: Proceedings of the 2020 ACM SIGPLAN International Symposium on Memory Management, pp. 48\u201359. ISMM \u201920, ACM (2020). https:\/\/doi.org\/10.1145\/3381898.3397211","DOI":"10.1145\/3381898.3397211"},{"key":"17_CR8","doi-asserted-by":"publisher","unstructured":"Batty, M., Owens, S., Sarkar, S., Sewell, P., Weber, T.: Mathematizing C++ concurrency. In: Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 55\u201366. POPL \u201911, ACM (2011). https:\/\/doi.org\/10.1145\/1925844.1926394","DOI":"10.1145\/1925844.1926394"},{"key":"17_CR9","doi-asserted-by":"publisher","unstructured":"Boehm, H.J., Adve, S.V.: Foundations of the C++ concurrency memory model. In: Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 68\u201378. PLDI \u201908, ACM (2008). https:\/\/doi.org\/10.1145\/1375581.1375591","DOI":"10.1145\/1375581.1375591"},{"key":"17_CR10","doi-asserted-by":"publisher","unstructured":"Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 110\u2013121. POPL \u201905, ACM (2005). https:\/\/doi.org\/10.1145\/1040305.1040315","DOI":"10.1145\/1040305.1040315"},{"key":"17_CR11","doi-asserted-by":"publisher","unstructured":"Flur, S., Sarkar, S., Pulte, C., Nienhuis, K., Maranget, L., Gray, K.E., Sezgin, A., Batty, M., Sewell, P.: Mixed-size concurrency: ARM, POWER, C\/C++11, and SC. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, pp. 429\u2013442. POPL \u201917, ACM (2017). https:\/\/doi.org\/10.1145\/3009837.3009839","DOI":"10.1145\/3009837.3009839"},{"key":"17_CR12","doi-asserted-by":"publisher","unstructured":"Godefroid, P.: Model checking for programming languages using VeriSoft. In: Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 174\u2013186. POPL \u201997, ACM (1997). https:\/\/doi.org\/10.1145\/263699.263717","DOI":"10.1145\/263699.263717"},{"key":"17_CR13","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/s10703-005-1489-x","volume":"26","author":"P Godefroid","year":"2005","unstructured":"Godefroid, P.: Software model checking: the VeriSoft approach. Form. Method Syst. Des. 26, 77\u2013101 (2005). https:\/\/doi.org\/10.1007\/s10703-005-1489-x","journal-title":"Form. Method Syst. Des."},{"key":"17_CR14","doi-asserted-by":"publisher","unstructured":"Gorjiara, H., Xu, G.H., Demsky, B.: Jaaru: efficiently model checking persistent memory programs. In: Proceedings of the 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, pp. 415\u2013428. ASPLOS \u201921, ACM (2021). https:\/\/doi.org\/10.1145\/3445814.3446735","DOI":"10.1145\/3445814.3446735"},{"key":"17_CR15","doi-asserted-by":"publisher","unstructured":"Kokologiannakis, M., Kaysin, I., Raad, A., Vafeiadis, V.: PerSeVerE: persistency semantics for verification under ext4. Proc. ACM Program. Lang. 5(POPL), 43:1\u201343:29 (2021). https:\/\/doi.org\/10.1145\/3434324","DOI":"10.1145\/3434324"},{"key":"17_CR16","doi-asserted-by":"publisher","unstructured":"Kokologiannakis, M., Lahav, O., Sagonas, K., Vafeiadis, V.: Effective stateless model checking for C\/C++ concurrency. Proc. ACM Program. Lang. 2(POPL), 17:1\u201317:32 (2018). https:\/\/doi.org\/10.1145\/3158105","DOI":"10.1145\/3158105"},{"key":"17_CR17","doi-asserted-by":"publisher","unstructured":"Kokologiannakis, M., Raad, A., Vafeiadis, V.: Model checking for weakly consistent libraries. In: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 96\u2013110. PLDI \u201919, ACM (2019). https:\/\/doi.org\/10.1145\/3314221.3314609, full paper with the technical appendix: https:\/\/plv.mpi-sws.org\/genmc\/full-paper.pdf","DOI":"10.1145\/3314221.3314609"},{"key":"17_CR18","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1007\/s10009-019-00514-6","volume":"21","author":"M Kokologiannakis","year":"2019","unstructured":"Kokologiannakis, M., Sagonas, K.: Stateless model checking of the linux kernel\u2019s read-copy update (RCU). Int. J. Softw. Tools Technol. Transfer 21, 283\u2013306 (2019). https:\/\/doi.org\/10.1007\/s10009-019-00514-6","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"17_CR19","doi-asserted-by":"publisher","unstructured":"Kokologiannakis, M., Vafeiadis, V.: GenMC: a model checker for weak memory models. In: Computer Aided Verification: 33rd International Conference, CAV 2021, Virtual Event, July 20\u201323, 2021, Proceedings, Part I. LNCS, vol. 12759, pp. 427\u2013440. Springer, Heidelberg (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_20","DOI":"10.1007\/978-3-030-81685-8_20"},{"key":"17_CR20","doi-asserted-by":"publisher","unstructured":"Lahav, O., Vafeiadis, V., Kang, J., Hur, C.K., Dreyer, D.: Repairing sequential consistency in C\/C++11. In: Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 618\u2013632. PLDI \u201917, ACM (2017). https:\/\/doi.org\/10.1145\/3062341.3062352","DOI":"10.1145\/3062341.3062352"},{"key":"17_CR21","doi-asserted-by":"publisher","unstructured":"L\u00e5ng, M., Sagonas, K.: Parallel graph-based stateless model checking. In: ATVA 2020: Automated Technology for Verification and Analysis. Lecture Notes in Computer Science, vol. 12302, pp. 377\u2013393. Springer, Heidelberg (2020). https:\/\/doi.org\/10.1007\/978-3-030-59152-6_21","DOI":"10.1007\/978-3-030-59152-6_21"},{"key":"17_CR22","doi-asserted-by":"publisher","unstructured":"Musuvathi, M., Qadeer, S.: Iterative context bounding for systematic testing of multithreaded programs. In: Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and Implementation. pp. 446\u2013455. PLDI \u201907, ACM (2007). https:\/\/doi.org\/10.1145\/1250734.1250785","DOI":"10.1145\/1250734.1250785"},{"key":"17_CR23","doi-asserted-by":"publisher","unstructured":"Norris, B., Demsky, B.: CDSCheker: checking concurrent data structures written with C\/C++ atomics. In: Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications, pp. 131\u2013150. OOPSLA \u201913, ACM (2013). https:\/\/doi.org\/10.1145\/2509136.2509514","DOI":"10.1145\/2509136.2509514"},{"key":"17_CR24","doi-asserted-by":"publisher","unstructured":"Norris, B., Demsky, B.: A practical approach for model checking C\/C++11 code. ACM Trans. Program. Lang. Syst. 58(3), 10:1\u201310:51 (2016). https:\/\/doi.org\/10.1145\/2806886","DOI":"10.1145\/2806886"},{"key":"17_CR25","doi-asserted-by":"publisher","unstructured":"Pulte, C., Pichon-Pharabod, J., Kang, J., Lee, S.H., Hur, C.K.: Promising-ARM\/RISC-V: a simpler and faster operational concurrency model. In: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 1\u201315. PLDI \u201919, ACM (2019). https:\/\/doi.org\/10.1145\/3314221.3314624","DOI":"10.1145\/3314221.3314624"},{"key":"17_CR26","doi-asserted-by":"publisher","unstructured":"Sato, S., Mizuhashi, T., Kimura, G., Taura, K.: Efficiently Adapting Stateless Model Checking for C11\/C++11 to Mixed-Size Accesses (Supplemental Material) (2024). https:\/\/doi.org\/10.5281\/zenodo.13624833","DOI":"10.5281\/zenodo.13624833"},{"key":"17_CR27","doi-asserted-by":"publisher","unstructured":"Ugawa, T., Abe, T., Maeda, T.: Model checking copy phases of concurrent copying garbage collection with various memory models. Proc. ACM Program. Lang. 1(OOPSLA), 53:1\u201353:26 (2017). https:\/\/doi.org\/10.1145\/3133877","DOI":"10.1145\/3133877"},{"key":"17_CR28","doi-asserted-by":"publisher","unstructured":"Yodaiken, V.: How ISO C became unusable for operating systems development. In: Proceedings of the 11th Workshop on Programming Languages and Operating Systems, pp. 84\u201390. PLOS \u201921, ACM (2021). https:\/\/doi.org\/10.1145\/3477113.3487274","DOI":"10.1145\/3477113.3487274"}],"updated-by":[{"DOI":"10.1007\/978-981-97-8943-6_19","type":"correction","label":"Correction","source":"publisher","updated":{"date-parts":[[2025,5,28]],"date-time":"2025-05-28T00:00:00Z","timestamp":1748390400000}}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-981-97-8943-6_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,27]],"date-time":"2025-05-27T16:52:41Z","timestamp":1748364761000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-981-97-8943-6_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,28]]},"ISBN":["9789819789429","9789819789436"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-981-97-8943-6_17","relation":{"correction":[{"id-type":"doi","id":"10.1007\/978-981-97-8943-6_19","asserted-by":"object"}]},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,10,28]]},"assertion":[{"value":"28 October 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"28 May 2025","order":2,"name":"change_date","label":"Change Date","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"Correction","order":3,"name":"change_type","label":"Change Type","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"A correction has been published.","order":4,"name":"change_details","label":"Change Details","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"APLAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Asian Symposium on Programming Languages and Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Kyoto","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":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 October 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 October 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"aplas2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/aplas-2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}