{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,2]],"date-time":"2026-07-02T00:49:38Z","timestamp":1782953378763,"version":"3.54.5"},"publisher-location":"Cham","reference-count":47,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031666759","type":"print"},{"value":"9783031666766","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"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":[[2024]]},"DOI":"10.1007\/978-3-031-66676-6_4","type":"book-chapter","created":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T12:04:18Z","timestamp":1725451458000},"page":"65-87","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Practical Rely\/Guarantee Verification of\u00a0an\u00a0Efficient Lock for\u00a0seL4 on\u00a0Multicore Architectures"],"prefix":"10.1007","author":[{"given":"Robert J.","family":"Colvin","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ian J.","family":"Hayes","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Scott","family":"Heiner","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Peter","family":"H\u00f6fner","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Larissa","family":"Meinicke","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Roger C.","family":"Su","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2024,9,4]]},"reference":[{"key":"4_CR1","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"},{"issue":"4","key":"4_CR2","doi-asserted-by":"publisher","first-page":"807","DOI":"10.1093\/logcom\/exm030","volume":"17","author":"JW Coleman","year":"2007","unstructured":"Coleman, J.W., Jones, C.B.: A structural proof of the soundness of rely\/guarantee rules. J. Log. Comput. 17(4), 807\u2013841 (2007). https:\/\/doi.org\/10.1093\/logcom\/exm030","journal-title":"J. Log. Comput."},{"key":"4_CR3","doi-asserted-by":"publisher","unstructured":"Colvin, R.J.: Parallelized sequential composition and hardware weak memory models. In: SEFM, pp. 201\u2013221 (2021). https:\/\/doi.org\/10.1007\/978-3-030-92124-8_12","DOI":"10.1007\/978-3-030-92124-8_12"},{"key":"4_CR4","doi-asserted-by":"publisher","unstructured":"Colvin, R.J.: Separation of concerning things: a simpler basis for defining and programming with the C\/C++ memory model. In: ICFEM, pp. 71\u201389 (2022). https:\/\/doi.org\/10.1007\/978-3-031-17244-1_5","DOI":"10.1007\/978-3-031-17244-1_5"},{"key":"4_CR5","doi-asserted-by":"publisher","unstructured":"Colvin, R.J.: A fine-grained semantics for arrays and pointers under weak memory models. In: FM, pp. 301\u2013320 (2023). https:\/\/doi.org\/10.1007\/978-3-031-27481-7_18","DOI":"10.1007\/978-3-031-27481-7_18"},{"issue":"5","key":"4_CR6","doi-asserted-by":"publisher","first-page":"853","DOI":"10.1007\/s00165-017-0416-4","volume":"29","author":"RJ Colvin","year":"2017","unstructured":"Colvin, R.J., Hayes, I.J., Meinicke, L.A.: Designing a semantic model for a wide-spectrum language with concurrency. Form. Asp. Comput. 29(5), 853\u2013875 (2017). https:\/\/doi.org\/10.1007\/s00165-017-0416-4","journal-title":"Form. Asp. Comput."},{"key":"4_CR7","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2022.102779","volume":"217","author":"N Coughlin","year":"2022","unstructured":"Coughlin, N., Smith, G.: Compositional noninterference on hardware weak memory models. Sci. Comput. Program. 217, 102779 (2022). https:\/\/doi.org\/10.1016\/j.scico.2022.102779","journal-title":"Sci. Comput. Program."},{"key":"4_CR8","doi-asserted-by":"publisher","unstructured":"Coughlin, N., Winter, K., Smith, G.: Compositional reasoning for non-multicopy atomic architectures. Form. Asp. Comput. 35(2) (2023). https:\/\/doi.org\/10.1145\/3574137","DOI":"10.1145\/3574137"},{"key":"4_CR9","unstructured":"Craig, T.S.: Building FIFO and priority-queuing spin locks from atomic swap. Tech. Rep. 93-02-02, University of Washington (1993)"},{"key":"4_CR10","doi-asserted-by":"publisher","unstructured":"Dinsdale-Young, T., Birkedal, L., Gardner, P., Parkinson, M., Yang, H.: Views: compositional reasoning for concurrent programs. In: POPL, pp. 287-300 (2013). https:\/\/doi.org\/10.1145\/2429069.2429104","DOI":"10.1145\/2429069.2429104"},{"key":"4_CR11","doi-asserted-by":"publisher","unstructured":"Doherty, S., Dalvandi, S., Dongol, B., Wehrheim, H.: Unifying operational weak memory verification: An axiomatic approach. ACM Trans. Comput. Log. 23(4) (2022). https:\/\/doi.org\/10.1145\/3545117","DOI":"10.1145\/3545117"},{"key":"4_CR12","doi-asserted-by":"publisher","unstructured":"D\u2019Osualdo, E., Sutherland, J., Farzan, A., Gardner, P.: TaDA Live: compositional reasoning for termination of fine-grained concurrent programs. ACM Trans. Program. Lang. Syst. 43(4) (2021). https:\/\/doi.org\/10.1145\/3477082","DOI":"10.1145\/3477082"},{"key":"4_CR13","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1090\/psapm\/019\/0235771","volume":"19","author":"RW Floyd","year":"1967","unstructured":"Floyd, R.W.: Assigning meanings to programs. Math. Asp. Comput. Sci. 19, 19\u201332 (1967)","journal-title":"Math. Asp. Comput. Sci."},{"key":"4_CR14","doi-asserted-by":"publisher","unstructured":"Gharachorloo, K., Lenoski, D., Laudon, J., Gibbons, P., Gupta, A., Hennessy, J.: Memory consistency and event ordering in scalable shared-memory multiprocessors. In: ISCA, pp. 15\u201326 (1990). https:\/\/doi.org\/10.1145\/325164.325102","DOI":"10.1145\/325164.325102"},{"key":"4_CR15","doi-asserted-by":"publisher","unstructured":"Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.W.: FDR3 \u2014 a modern refinement checker for CSP. In: TACAS, pp. 187\u2013201 (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_13","DOI":"10.1007\/978-3-642-54862-8_13"},{"key":"4_CR16","doi-asserted-by":"publisher","unstructured":"Hayes, I.J., Colvin, R.J., Meinicke, L.A., Winter, K., Velykis, A.: An algebra of synchronous atomic steps. In: FM, pp. 352\u2013369 (2016). https:\/\/doi.org\/10.1007\/978-3-319-48989-6_22","DOI":"10.1007\/978-3-319-48989-6_22"},{"key":"4_CR17","doi-asserted-by":"publisher","unstructured":"He, J., Hoare, C., Sanders, J.: Data refinement refined (resume). In: ESOP, pp. 187\u2013196 (1986). https:\/\/doi.org\/10.1007\/3-540-16442-1_14","DOI":"10.1007\/3-540-16442-1_14"},{"issue":"4","key":"4_CR18","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1145\/3378426","volume":"63","author":"G Heiser","year":"2020","unstructured":"Heiser, G., Klein, G., Andronick, J.: seL4 in Australia: from research to real-world trustworthy systems. Commun. ACM 63(4), 72\u201375 (2020). https:\/\/doi.org\/10.1145\/3378426","journal-title":"Commun. ACM"},{"issue":"9","key":"4_CR19","doi-asserted-by":"publisher","first-page":"1622","DOI":"10.1016\/j.scico.2013.03.003","volume":"78","author":"WH Hesselink","year":"2013","unstructured":"Hesselink, W.H.: Mechanical verification of Lamport\u2019s Bakery algorithm. Sci. Comput. Program. 78(9), 1622\u20131638 (2013). https:\/\/doi.org\/10.1016\/j.scico.2013.03.003","journal-title":"Sci. Comput. Program."},{"issue":"10","key":"4_CR20","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969). https:\/\/doi.org\/10.1145\/363235.363259","journal-title":"Commun. ACM"},{"issue":"5","key":"4_CR21","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"GJ Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker SPIN. IEEE Trans. Softw. Eng. 23(5), 279\u2013295 (1997). https:\/\/doi.org\/10.1109\/32.588521","journal-title":"IEEE Trans. Softw. Eng."},{"key":"4_CR22","unstructured":"Jones, C.B.: Development Methods for Computer Programs including a Notion of Interference. Ph.D. thesis, Oxford University (1981)"},{"key":"4_CR23","unstructured":"Jones, C.B.: Specification and design of (parallel) programs. In: IFIP Congress, pp. 321\u2013332 (1983)"},{"issue":"4","key":"4_CR24","doi-asserted-by":"publisher","first-page":"596","DOI":"10.1145\/69575.69577","volume":"5","author":"CB Jones","year":"1983","unstructured":"Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst. 5(4), 596\u2013619 (1983). https:\/\/doi.org\/10.1145\/69575.69577","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"4_CR25","doi-asserted-by":"publisher","unstructured":"Kang, J., Hur, C.K., Lahav, O., Vafeiadis, V., Dreyer, D.: A promising semantics for relaxed-memory concurrency. In: POPL, pp. 175\u2013189 (2017). https:\/\/doi.org\/10.1145\/3009837.3009850","DOI":"10.1145\/3009837.3009850"},{"key":"4_CR26","doi-asserted-by":"publisher","unstructured":"Kim, J., Sj\u00f6berg, V., Gu, R., Shao, Z.: Safety and liveness of MCS lock\u2014layer by layer. In: APLAS, pp. 273\u2013297 (2017). https:\/\/doi.org\/10.1007\/978-3-319-71237-6_14","DOI":"10.1007\/978-3-319-71237-6_14"},{"key":"4_CR27","doi-asserted-by":"publisher","unstructured":"Klein, G., Andronick, J., Elphinstone, K., Murray, T., Sewell, T., Kolanski, R., Heiser, G.: Comprehensive formal verification of an OS microkernel. ACM Trans. Comput. Syst. 32(1) (2014). https:\/\/doi.org\/10.1145\/2560537","DOI":"10.1145\/2560537"},{"key":"4_CR28","doi-asserted-by":"publisher","unstructured":"Klein, G., et al.: seL4: formal verification of an OS kernel. In: SOSP, pp. 207\u2013220 (2009). https:\/\/doi.org\/10.1145\/1629575.1629596","DOI":"10.1145\/1629575.1629596"},{"key":"4_CR29","doi-asserted-by":"publisher","unstructured":"Liang, H., Feng, X.: A program logic for concurrent objects under fair scheduling. In: POPL, pp. 385\u2013399 (2016). https:\/\/doi.org\/10.1145\/2837614.2837635","DOI":"10.1145\/2837614.2837635"},{"key":"4_CR30","unstructured":"Magnusson, P., Landin, A., Hagersten, E.: Efficient software synchronization on large cache coherent multiprocessors. Tech. Rep. T94-07, Swedish Inst. C. S. (1994)"},{"key":"4_CR31","doi-asserted-by":"publisher","unstructured":"Magnusson, P., Landin, A., Hagersten, E.: Queue locks on cache coherent multiprocessors. In: IPPS, pp. 165\u2013171 (1994). https:\/\/doi.org\/10.1109\/IPPS.1994.288305","DOI":"10.1109\/IPPS.1994.288305"},{"key":"4_CR32","doi-asserted-by":"publisher","unstructured":"Morgan, C., Gardiner, P.: Data refinement by calculation. Acta Inform. 27, 481\u2013503 (1990). https:\/\/doi.org\/10.1007\/BF00277386","DOI":"10.1007\/BF00277386"},{"key":"4_CR33","unstructured":"Morgan, C.: Programming from Specifications. Prentice Hall, second edn. (1994)"},{"key":"4_CR34","doi-asserted-by":"publisher","unstructured":"Murray, T., et al.: seL4: from general purpose to a proof of information flow enforcement. In: SP, pp. 415\u2013429 (2013). https:\/\/doi.org\/10.1109\/SP.2013.35","DOI":"10.1109\/SP.2013.35"},{"key":"4_CR35","doi-asserted-by":"publisher","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol.\u00a02283. Springer (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9","DOI":"10.1007\/3-540-45949-9"},{"key":"4_CR36","doi-asserted-by":"publisher","unstructured":"Nipkow, T., Prensa\u00a0Nieto, L.: Owicki\/Gries in Isabelle\/HOL. In: FASE, pp. 188\u2013203 (1999). https:\/\/doi.org\/10.1007\/978-3-540-49020-3_13","DOI":"10.1007\/978-3-540-49020-3_13"},{"issue":"4","key":"4_CR37","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/BF00268134","volume":"6","author":"S Owicki","year":"1976","unstructured":"Owicki, S., Gries, D.: An axiomatic proof technique for parallel programs I. Acta Inform. 6(4), 319\u2013340 (1976). https:\/\/doi.org\/10.1007\/BF00268134","journal-title":"Acta Inform."},{"key":"4_CR38","doi-asserted-by":"crossref","unstructured":"Paulson, L.C.: Isabelle: a generic theorem prover. Springer (1994)","DOI":"10.1007\/BFb0030541"},{"key":"4_CR39","doi-asserted-by":"publisher","unstructured":"Prensa\u00a0Nieto, L.: The rely-guarantee method in Isabelle\/HOL. In: ESOP, pp. 348\u2013362 (2003). https:\/\/doi.org\/10.1007\/3-540-36575-3_24","DOI":"10.1007\/3-540-36575-3_24"},{"key":"4_CR40","doi-asserted-by":"publisher","unstructured":"Reinhard, T., Jacobs, B.: Ghost signals: Verifying termination with busy waiting. In: CAV, pp. 27\u201350 (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_2","DOI":"10.1007\/978-3-030-81688-9_2"},{"key":"4_CR41","unstructured":"de\u00a0Roever, W.P., Engelhardt, K.: Data Refinement: Model-Oriented Proof Methods and their Comparison. Cambridge University Press (2001)"},{"key":"4_CR42","doi-asserted-by":"publisher","unstructured":"Schellhorn, G., Travkin, O., Wehrheim, H.: Towards a thread-local proof technique for starvation freedom. In: IFM, pp. 193\u2013209 (2016). https:\/\/doi.org\/10.1007\/978-3-319-33693-0_13","DOI":"10.1007\/978-3-319-33693-0_13"},{"key":"4_CR43","doi-asserted-by":"publisher","unstructured":"Scott, M.L.: Shared-Memory Synchronization. Synthesis Lectures on Computer Architecture, Morgan and Claypool (2013). https:\/\/doi.org\/10.1007\/978-3-031-01740-7","DOI":"10.1007\/978-3-031-01740-7"},{"key":"4_CR44","unstructured":"The seL4 Foundation: CLH lock in seL4 (2020). https:\/\/github.com\/seL4\/seL4\/blob\/master\/include\/smp\/lock.h"},{"key":"4_CR45","doi-asserted-by":"publisher","unstructured":"Thornton, J.E.: Parallel operation in the Control Data 6600. In: Proceedings of the October 27-29, 1964, Fall Joint Computer Conference, Part II: Very High Speed Computer Systems, AFIPS 1964, pp. 33-40. (1964). https:\/\/doi.org\/10.1145\/1464039.1464045","DOI":"10.1145\/1464039.1464045"},{"issue":"1","key":"4_CR46","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1147\/rd.111.0025","volume":"11","author":"RM Tomasulo","year":"1967","unstructured":"Tomasulo, R.M.: An efficient algorithm for exploiting multiple arithmetic units. IBM J. Res. Dev. 11(1), 25\u201333 (1967)","journal-title":"IBM J. Res. Dev."},{"key":"4_CR47","doi-asserted-by":"publisher","unstructured":"Windsor, M., Dodds, M., Simner, B., Parkinson, M.J.: Starling: Lightweight concurrency verification with views. In: CAV, pp. 544\u2013569 (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_27","DOI":"10.1007\/978-3-319-63387-9_27"}],"container-title":["Lecture Notes in Computer Science","The Practice of Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-66676-6_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T12:04:53Z","timestamp":1725451493000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-66676-6_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031666759","9783031666766"],"references-count":47,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-66676-6_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"4 September 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}