{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,14]],"date-time":"2026-03-14T11:01:18Z","timestamp":1773486078044,"version":"3.50.1"},"reference-count":40,"publisher":"Association for Computing Machinery (ACM)","issue":"1","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2026,3,31]]},"abstract":"<jats:p>\n                    We carry out an analysis of message-passing concurrency primitives, namely a synchronous channel and an alt (alternation) construct, implemented in Scala. We model these primitives using the process algebra CSP, and analyse them using the model checker FDR. We consider the correctness properties of\n                    <jats:italic toggle=\"yes\">synchronisation linearisation<\/jats:italic>\n                    (informally, that each completed operation execution corresponds to a correct synchronisation) and\n                    <jats:italic toggle=\"yes\">progressibility<\/jats:italic>\n                    (informally, that executions don\u2019t get stuck if they could synchronise): we show how these properties can be captured in CSP. Our initial analysis discovered an error in a previous implementation; our subsequent analysis helped us to produce a correct implementation. It turns out that a direct analysis of the composition of an alt and corresponding channels scales quite poorly. To overcome this, we perform a compositional analysis: we show that a channel and an alt each satisfies a more abstract description; and show that the composition of these abstract descriptions satisfies synchronisation linearisation and progressibility.\n                  <\/jats:p>","DOI":"10.1145\/3779649","type":"journal-article","created":{"date-parts":[[2026,1,31]],"date-time":"2026-01-31T20:36:44Z","timestamp":1769891804000},"page":"1-42","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Analysing a Library of Concurrency Primitives using CSP"],"prefix":"10.1145","volume":"38","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6453-5675","authenticated-orcid":false,"given":"Gavin","family":"Lowe","sequence":"first","affiliation":[{"name":"St Catherine's College, Oxford University","place":["Oxford, United Kingdom"]}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2026,3,14]]},"reference":[{"key":"e_1_3_4_2_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-015-0406-x"},{"key":"e_1_3_4_3_2","volume-title":"Concurrent Programming: Principles and Practice","author":"Andrews Gregory","year":"1991","unstructured":"Gregory Andrews. 1991. Concurrent Programming: Principles and Practice. Benjamin\/Cummings."},{"key":"e_1_3_4_4_2","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(86)90071-2"},{"key":"e_1_3_4_5_2","first-page":"294","volume-title":"Proceedings of the 6th Annual Association for Computing Machinery Symposium on Principles of Distributed Computing","author":"Clarke E. M.","year":"1987","unstructured":"E. M. Clarke and O. Grumberg. 1987. Avoiding the state explosion problem in temporal logic model checking. In Proceedings of the 6th Annual Association for Computing Machinery Symposium on Principles of Distributed Computing. 294\u2013303."},{"key":"e_1_3_4_6_2","series-title":"LNCS","first-page":"222","volume-title":"Proceedings of SEFM 2021","volume":"13085","author":"Dongol Brijesh","year":"2021","unstructured":"Brijesh Dongol and Jay Le-Papin. 2021. Checking opacity and durable opacity with FDR. In Proceedings of SEFM 2021(LNCS, Vol. 13085). Springer, 222\u2013242."},{"key":"e_1_3_4_7_2","volume-title":"Proceedings of the Symposium on Principles of Programming Languages (POPL \u201995)","author":"Emerson E. Allen","year":"1995","unstructured":"E. Allen Emerson and Kedar S. Namjoshi. 1995. Reasoning about rings. In Proceedings of the Symposium on Principles of Programming Languages (POPL \u201995)."},{"key":"e_1_3_4_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/146637.146681"},{"key":"e_1_3_4_9_2","volume-title":"The Art of Multiprocessor Programming","author":"Herlihy Maurice","year":"2012","unstructured":"Maurice Herlihy and Nir Shavit. 2012. The Art of Multiprocessor Programming. Morgan Kaufmann."},{"key":"e_1_3_4_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972"},{"key":"e_1_3_4_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/69575.69577"},{"key":"e_1_3_4_12_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1007\/11423348_9","volume-title":"Communicating Sequential Processes: The First 25 Years","author":"Lawrence Jonathan","year":"2005","unstructured":"Jonathan Lawrence. 2005. Practical applications of CSP and FDR to software design. In Communicating Sequential Processes: The First 25 Years, Ali E. Abdallah, Cliff B. Jones, and Jeff W. Sanders (Eds.). Lecture Notes in Computer Science, Vol. 3525, Springer, 151\u2013174."},{"key":"e_1_3_4_13_2","unstructured":"Jonathan Lawrence and Gavin Lowe. 2025. Synchronisation: Specification and Testing. (2025). Submitted for publication."},{"key":"e_1_3_4_14_2","volume-title":"A Semanti Study of Data Independence with Applications to Model Checking","author":"Lazi\u0107 Ranko","year":"1999","unstructured":"Ranko Lazi\u0107. 1999. A Semanti Study of Data Independence with Applications to Model Checking. DPhil thesis. University of Oxford."},{"key":"e_1_3_4_15_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/3-540-61042-1_43","volume-title":"Proceedings of TACAS","volume":"1055","author":"Lowe Gavin","year":"1996","unstructured":"Gavin Lowe. 1996. Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In Proceedings of TACAS(Lecture Notes in Computer Science, Vol. 1055). Springer Verlag, 147\u2013166. Also in Software\u2014Concepts and Tools, 17:93\u2013102, 1996."},{"key":"e_1_3_4_16_2","first-page":"1","volume-title":"Communicating Process Architectures","author":"Lowe Gavin","year":"2011","unstructured":"Gavin Lowe. 2011. Implementing generalised Alt \u2014 A case study in validated design using CSP. In Communicating Process Architectures, J. F. Broenink, J. Kerridge, P. H. Welch, F. R. M. Barnes, A. T. Sampson, and J. B. Pedersen (Eds.). 1\u201334."},{"key":"e_1_3_4_17_2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"162","DOI":"10.1007\/978-3-319-51046-0_9","volume-title":"Concurrency, Security, and Puzzles.","author":"Lowe Gavin","year":"2017","unstructured":"Gavin Lowe. 2017. Analysing lock-free linearizable datatypes using CSP. In Concurrency, Security, and Puzzles.Thomas Gibson-Robinson, Philippa Hopcroft, and Ranko Lazi\u0107 (Eds.), LNCS, Vol. 10160, Springer, 162\u2013184."},{"key":"e_1_3_4_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-019-00487-y"},{"issue":"2","key":"e_1_3_4_19_2","article-title":"Parameterized verification of systems with component identities, using view abstraction","volume":"24","author":"Lowe Gavin","year":"2022","unstructured":"Gavin Lowe. 2022. Parameterized verification of systems with component identities, using view abstraction. Software Tools for Technology Transfer 24, 2 (2022), 287\u2013324.","journal-title":"Software Tools for Technology Transfer"},{"key":"e_1_3_4_20_2","volume-title":"On Data Independence","author":"Lowe Gavin","year":"2024","unstructured":"Gavin Lowe. 2024. On Data Independence. Technical Report. University of Oxford. Retrieved from https:\/\/www.cs.ox.ac.uk\/people\/gavin.lowe\/Papers\/dataindependence.pdf"},{"key":"e_1_3_4_21_2","volume-title":"Analysing a Library of Concurrency Primitives using CSP","author":"Lowe Gavin","year":"2025","unstructured":"Gavin Lowe. 2025. Analysing a Library of Concurrency Primitives using CSP. Technical Report. University of Oxford. Retrieved from https:\/\/www.cs.ox.ac.uk\/people\/gavin.lowe\/SCL-CSP\/"},{"key":"e_1_3_4_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00289237"},{"key":"e_1_3_4_23_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2013.03.018"},{"key":"e_1_3_4_24_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1981.230844"},{"key":"e_1_3_4_25_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(00)00023-X"},{"key":"e_1_3_4_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF02311231"},{"key":"e_1_3_4_27_2","volume-title":"Automated Modelling of an Imperative Language using CSP","author":"Pay Alex","year":"2023","unstructured":"Alex Pay. 2023. Automated Modelling of an Imperative Language using CSP. Master of Computer Science, final-year project. University of Oxford."},{"key":"e_1_3_4_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/3605942"},{"key":"e_1_3_4_29_2","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1007\/3-540-45657-0_9","volume-title":"CAV\u201902: Proceedings of the 14th International Conference on Computer Aided Verification","author":"Pnueli A.","year":"2002","unstructured":"A. Pnueli, J. Xu, and L. D. Zuck. 2002. Liveness with (0, 1, \\(\\infty\\) )-counter abstraction. In CAV\u201902: Proceedings of the 14th International Conference on Computer Aided Verification. 107\u2013122."},{"key":"e_1_3_4_30_2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"150","DOI":"10.1007\/978-3-031-57267-8_6","volume-title":"Programming Languages and Systems (ESOP 2024)","author":"Raad Azalea","year":"2024","unstructured":"Azalea Raad, Ori Lahav, John Wickerson, Piotr Balcer, and Brijesh Dongol. 2024. Intel PMDK Transations: Specification, validation and concurrency. In Programming Languages and Systems (ESOP 2024)(LNCS, Vol. 14577). 150\u2013179."},{"key":"e_1_3_4_31_2","volume-title":"The Theory and Practice of Concurrency","author":"Roscoe A. W.","year":"1998","unstructured":"A. W. Roscoe. 1998. The Theory and Practice of Concurrency. Prentice Hall."},{"key":"e_1_3_4_32_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-84882-258-0"},{"key":"e_1_3_4_33_2","first-page":"177","volume-title":"Proceedings of AVoCS 2007","author":"Roscoe A. W.","year":"2007","unstructured":"A. W. Roscoe and David Hopkins. 2007. SVA, a tool for analysing shared-variable programs. In Proceedings of AVoCS 2007. 177\u2013183."},{"key":"e_1_3_4_34_2","volume-title":"Communicating Process Architectures","author":"Sputh Bernhard H. C.","year":"2005","unstructured":"Bernhard H. C. Sputh and Alastair R. Allen. 2005. JCSP-Poison: Safe termination of CSP process networks. In Communicating Process Architectures, Jan F. Broenink, Herman W. Roebbers, Johan P. E. Sunter, Peter H. Welch, and David C. Wood (Eds.)."},{"key":"e_1_3_4_35_2","volume-title":"Proceedings of Concurrent Process Architectures","author":"Sufrin Bernard","year":"2008","unstructured":"Bernard Sufrin. 2008. Communicating scala objects. In Proceedings of Concurrent Process Architectures."},{"key":"e_1_3_4_36_2","unstructured":"P.H. Welch and P.D. Austin. 2014. JCSP home page. Retrieved February 12 2026 from http:\/\/www.cs.ukc.ac.uk\/projects\/ofa\/jcsp\/"},{"key":"e_1_3_4_37_2","doi-asserted-by":"crossref","first-page":"114","DOI":"10.1109\/PDSE.2000.847856","volume-title":"Proceedings of the International Symposium on Software Engineering for Parallel and Distributed Systems","author":"Welch Peter","year":"2000","unstructured":"Peter Welch and Jeremy Martin. 2000. A CSP model for Java multithreading. In Proceedings of the International Symposium on Software Engineering for Parallel and Distributed Systems. IEEE, 114\u2013122."},{"key":"e_1_3_4_38_2","volume-title":"Proceedings of Communicating Process Architecture","author":"Welch Peter","year":"2000","unstructured":"Peter Welch and Jeremy Martin. 2000. Formal analysis of concurrent Java systems. In Proceedings of Communicating Process Architecture."},{"key":"e_1_3_4_39_2","first-page":"184","volume-title":"Proceedings of the 13th Annual ACM Symposium on Principles of Programming Languages","author":"Wolper Pierre","year":"1986","unstructured":"Pierre Wolper. 1986. Expressing interesting properties of programs in propositional temporal logic. In Proceedings of the 13th Annual ACM Symposium on Principles of Programming Languages. 184\u2013193."},{"key":"e_1_3_4_40_2","doi-asserted-by":"publisher","DOI":"10.5555\/646691.703266"},{"key":"e_1_3_4_41_2","volume-title":"Model Checking Concurrent Objects","author":"Zhao Zeyang","year":"2022","unstructured":"Zeyang Zhao. 2022. Model Checking Concurrent Objects. Master\u2019s thesis. Oxford University."}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3779649","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,14]],"date-time":"2026-03-14T10:34:25Z","timestamp":1773484465000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3779649"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,3,14]]},"references-count":40,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2026,3,31]]}},"alternative-id":["10.1145\/3779649"],"URL":"https:\/\/doi.org\/10.1145\/3779649","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,3,14]]},"assertion":[{"value":"2024-06-18","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-12-04","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-03-14","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}