{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T04:33:48Z","timestamp":1768278828661,"version":"3.49.0"},"publisher-location":"Cham","reference-count":17,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031321566","type":"print"},{"value":"9783031321573","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"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":[[2023]]},"DOI":"10.1007\/978-3-031-32157-3_3","type":"book-chapter","created":{"date-parts":[[2023,5,1]],"date-time":"2023-05-01T15:11:26Z","timestamp":1682953886000},"page":"41-58","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Model Checking Futexes"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0001-7956-0371","authenticated-orcid":false,"given":"Hugues","family":"Evrard","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7448-7961","authenticated-orcid":false,"given":"Alastair F.","family":"Donaldson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,5,2]]},"reference":[{"key":"3_CR1","unstructured":"Android: Bionic C library, pthread_cond implementation (2023). https:\/\/android.googlesource.com\/platform\/bionic\/+\/refs\/tags\/android-13.0.0_r24\/libc\/bionic\/pthread_cond.cpp. Accessed 10 Jan 2023"},{"key":"3_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"136","DOI":"10.1007\/978-3-540-39989-6_10","volume-title":"Distributed Computing","author":"Y Bar-David","year":"2003","unstructured":"Bar-David, Y., Taubenfeld, G.: Automatic discovery of mutual exclusion algorithms. In: Fich, F.E. (ed.) DISC 2003. LNCS, vol. 2848, pp. 136\u2013150. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-39989-6_10"},{"key":"3_CR3","unstructured":"Benderski, E.: Basics of futexes (2018). https:\/\/eli.thegreenplace.net\/2018\/basics-of-futexes\/. Accessed 10 Jan 2023"},{"key":"3_CR4","doi-asserted-by":"crossref","unstructured":"Bogunovic, N., Pek, E.: Verification of mutual exclusion algorithms with SMV system. In: The IEEE Region 8 EUROCON 2003. Computer as a Tool. vol. 2, pp. 21\u201325. IEEE (2003)","DOI":"10.1109\/EURCON.2003.1248127"},{"key":"3_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Clarke","year":"2004","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168\u2013176. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24730-2_15"},{"key":"3_CR6","unstructured":"Denis-Courmont, R.: Condition variable with futex (2020). https:\/\/www.remlab.net\/op\/futex-condvar.shtml. Accessed 10 Jan 2023"},{"key":"3_CR7","unstructured":"Drepper, U.: Futexes are tricky (2011). https:\/\/www.akkadia.org\/drepper\/futex.pdf. Accessed 10 Jan 2023"},{"key":"3_CR8","unstructured":"Evrard, H., Donaldson, A.: Model checking futexes: code examples (2022). https:\/\/github.com\/mc-imperial\/modelcheckingfutexes. Accessed 16 Jan 2022"},{"key":"3_CR9","unstructured":"Franke, H., Russell, R., Kirkwood, M.: Fuss, futexes and furwocks: fast userlevel locking in Linux. In: Ottawa Linux Symposium 2002, pp. 479\u2013495 (2002). https:\/\/www.kernel.org\/doc\/ols\/2002\/ols2002-pages-479-495.pdf. Accessed 10 Jan 2022"},{"key":"3_CR10","unstructured":"Futex manual page section 2 (system calls) (2023). https:\/\/man7.org\/linux\/man-pages\/man2\/futex.2.html. Accessed 16 Jan 2023"},{"key":"3_CR11","unstructured":"Futex manual page section 7 (miscellaneous) (2023). https:\/\/man7.org\/linux\/man-pages\/man7\/futex.7.html. Accessed 16 Jan 2023"},{"issue":"6","key":"3_CR12","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1145\/1453775.1453793","volume":"42","author":"R Hamberg","year":"2008","unstructured":"Hamberg, R., Vaandrager, F.: Using model checkers in an introductory course on operating systems. ACM SIGOPS Operat. Syst. Rev. 42(6), 101\u2013111 (2008)","journal-title":"ACM SIGOPS Operat. Syst. Rev."},{"key":"3_CR13","unstructured":"Holzmann, G.: The SPIN model checker: primer and reference manual. Addison-Wesley Professional, 1st edn. (2011)"},{"key":"3_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/978-3-030-91014-3_16","volume-title":"Networked Systems","author":"M Kokologiannakis","year":"2021","unstructured":"Kokologiannakis, M., Vafeiadis, V.: BAM: efficient model checking for barriers. In: Echihabi, K., Meyer, R. (eds.) NETYS 2021. LNCS, vol. 12754, pp. 223\u2013239. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-91014-3_16"},{"key":"3_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"180","DOI":"10.1007\/978-3-642-15898-8_12","volume-title":"Formal Methods for Industrial Critical Systems","author":"R Mateescu","year":"2010","unstructured":"Mateescu, R., Serwe, W.: A study of shared-memory mutual exclusion protocols using CADP. In: Kowalewski, S., Roveri, M. (eds.) FMICS 2010. LNCS, vol. 6371, pp. 180\u2013197. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15898-8_12"},{"key":"3_CR16","doi-asserted-by":"crossref","unstructured":"Mateescu, R., Serwe, W.: Model checking and performance evaluation with CADP illustrated on shared-memory mutual exclusion protocols. Sci. Comput. Program. 78(7), 843\u2013861 (2013)","DOI":"10.1016\/j.scico.2012.01.003"},{"key":"3_CR17","unstructured":"Mechanical sympathy email group, discussion titled linux futex_wait() bug (2015). https:\/\/groups.google.com\/g\/mechanical-sympathy\/c\/QbmpZxp6C64. Accessed 16 Jan 2023"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-32157-3_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,19]],"date-time":"2024-10-19T14:52:32Z","timestamp":1729349552000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-32157-3_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031321566","9783031321573"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-32157-3_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"2 May 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SPIN","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Model Checking Software","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 April 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 April 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"spin2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/spin-web.github.io\/SPIN2023\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Easy Chair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"21","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"9","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"2","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"43% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.2","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"2.3","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}