{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,12]],"date-time":"2026-02-12T00:04:02Z","timestamp":1770854642478,"version":"3.50.1"},"reference-count":27,"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>This article presents the modelling of the ProcessJ cooperative runtime environment for the implementation of a CSP-inspired communication channel. We used the CSP tool FDR to verify the correctness of the ProcessJ runtime and primitives, demonstrating how we have overcome a limitation in the existing ProcessJ runtime to improve behaviour. However, our work has demonstrated a limitation when trying to claim a cooperatively-scheduled channel implementation meets the abstract specification of a CSP channel. Our conclusion is that without sufficient hardware to execute all processes at once, a channel implementation cannot fully meet its specification when considering the execution environment in which the channel must operate. We are assured that the ProcessJ channel works correctly, such as other implementations including JCSP and CSO, but we are not assured that modelling can use a pure CSP channel in place of a ProcesssJ channel or other implementation when undertaking modelling due to unintended prioritisation occurring when not enough resources are available for full concurrency. Our work has demonstrated the need to consider the execution environment as it may cause behavioural issues not detected when only modelling a system in the abstract.<\/jats:p>","DOI":"10.1145\/3771735","type":"journal-article","created":{"date-parts":[[2025,10,16]],"date-time":"2025-10-16T11:06:52Z","timestamp":1760612812000},"page":"1-45","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Communicating Cooperatively Scheduled Processes: On the Unlikelihood of Implementing a Pure CSP Channel"],"prefix":"10.1145","volume":"38","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3409-432X","authenticated-orcid":false,"given":"Kevin","family":"Chalmers","sequence":"first","affiliation":[{"name":"School of Computing, Architecture, and Emerging Technologies, Ravensbourne University London","place":["London, United Kingdom of Great Britain and Northern Ireland"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2800-5095","authenticated-orcid":false,"given":"Jan B\u00e6kgaard","family":"Pedersen","sequence":"additional","affiliation":[{"name":"Computer Science, University of Nevada Las Vegas","place":["Las Vegas, United States"]}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2026,2,11]]},"reference":[{"key":"e_1_3_3_2_2","unstructured":"FDR 4.2.7 Documentation. Retrieved from https:\/\/cocotec.io\/fdr\/manual. (n.d.). Accessed: 2023-08-23."},{"key":"e_1_3_3_3_2","volume-title":"Erlang Programming: A Concurrent Approach to Software Development","author":"Cesarini Francesco","year":"2009","unstructured":"Francesco Cesarini and Simon Thompson. 2009. Erlang Programming: A Concurrent Approach to Software Development. O\u2019Reilly Media, Inc."},{"key":"e_1_3_3_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523720"},{"key":"e_1_3_3_5_2","volume-title":"Investigating Communicating Sequential Processes for Java to Support Ubiquitous Computing","author":"Chalmers Kevin","year":"2009","unstructured":"Kevin Chalmers. 2009. Investigating Communicating Sequential Processes for Java to Support Ubiquitous Computing. Ph.D. Dissertation. Edinburgh Napier University."},{"key":"e_1_3_3_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/3547276.3548519"},{"key":"e_1_3_3_7_2","volume-title":"ProcessJ: The JVMCSP Code Generator","author":"Cisneros Benjamin","year":"2018","unstructured":"Benjamin Cisneros. 2018. ProcessJ: The JVMCSP Code Generator. Master\u2019s thesis. University of Nevada Las Vegas."},{"key":"e_1_3_3_8_2","first-page":"187","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems (Lecture Notes in Computer Science)","author":"Gibson-Robinson Thomas","year":"2014","unstructured":"Thomas Gibson-Robinson, Philip Armstrong, Alexandre Boulgakov, and A. W. Roscoe. 2014. FDR3 \u2014 a modern refinement checker for CSP. In Tools and Algorithms for the Construction and Analysis of Systems (Lecture Notes in Computer Science). Erika \u00c1brah\u00e1m and Klaus Havelund (Eds.), Vol. 8413. 187\u2013201."},{"key":"e_1_3_3_9_2","volume-title":"FDR: From Theory to Industrial Application","author":"Gibson-Robinson Thomas","year":"2017","unstructured":"Thomas Gibson-Robinson, Guy Broadfoot, Gustavo Carvalho, Philippa Hopcroft, Gavin Lowe, Sidney Nogueira, Colin O\u2019Halloran, and Augusto Sampaio. 2017. FDR: From Theory to Industrial Application. Springer International Publishing. 65\u201387 pages."},{"key":"e_1_3_3_10_2","doi-asserted-by":"crossref","unstructured":"C. A. R. Hoare. 1978. Communicating sequential processes. CACM 21 8 (August1978) 666\u2013677.","DOI":"10.1145\/359576.359585"},{"key":"e_1_3_3_11_2","doi-asserted-by":"publisher","DOI":"10.5555\/3921"},{"key":"e_1_3_3_12_2","doi-asserted-by":"publisher","unstructured":"Leslie Lamport. 1987. A fast mutual exclusion algorithm. ACM Transactions on Computer Systems 5 1 (Jan.1987) 1\u201311. DOI:10.1145\/7351.7352","DOI":"10.1145\/7351.7352"},{"key":"e_1_3_3_13_2","doi-asserted-by":"publisher","unstructured":"Gavin Lowe. 2019. Discovering and correcting a deadlock in a channel implementation. Formal Aspects of Computing 31 4 (01 August2019) 411\u2013419. DOI:10.1007\/s00165-019-00487-y","DOI":"10.1007\/s00165-019-00487-y"},{"key":"e_1_3_3_14_2","doi-asserted-by":"publisher","DOI":"10.5555\/898201"},{"key":"e_1_3_3_15_2","doi-asserted-by":"publisher","unstructured":"Ana L\u00facia De Moura and Roberto Ierusalimschy. 2009. Revisiting coroutines. ACM Trans. Program. Lang. Syst. 31 2 Article 6 (February2009) 31 pages. DOI:10.1145\/1462166.1462167","DOI":"10.1145\/1462166.1462167"},{"key":"e_1_3_3_16_2","unstructured":"Oracle. Oracle Help Center. Retrieved from https:\/\/docs.oracle.com\/javase\/10\/docs\/api\/java\/util\/concurrent\/locks\/Condition.html. (n.d.). Accessed: 2022-12-09."},{"key":"e_1_3_3_17_2","first-page":"65","volume-title":"Proceedings of the 7th International Workshop on Formal Methods in Software Engineering (FormaliSE \u201919)","author":"Pedersen Jan B.","year":"2019","unstructured":"Jan B. Pedersen and Kevin Chalmers. 2019. Verifying channel communication correctness for a multi-core cooperatively scheduled runtime using CSP. In Proceedings of the 7th International Workshop on Formal Methods in Software Engineering (FormaliSE \u201919). IEEE Press, Piscataway, NJ, USA, 65\u201374. DOI:10.1109\/FormaliSE.2019.00016"},{"key":"e_1_3_3_18_2","doi-asserted-by":"publisher","unstructured":"Jan B. Pedersen and Kevin Chalmers. 2023. Towards verifying cooperatively-scheduled runtimes using CSP. Formal Aspects of Computing 1 1 (January2023). DOI:10.1145\/3605942","DOI":"10.1145\/3605942"},{"key":"e_1_3_3_19_2","doi-asserted-by":"publisher","unstructured":"Jan B. Pedersen and Peter H. Welch. 2018. The symbiosis of concurrency and verification: Teaching and case studies. Formal Aspects of Computing 30 2 (March2018) 239\u2013277. DOI:10.1007\/s00165-017-0447-x","DOI":"10.1007\/s00165-017-0447-x"},{"key":"e_1_3_3_20_2","doi-asserted-by":"publisher","DOI":"10.1109\/REAL.2002.1181585"},{"key":"e_1_3_3_21_2","doi-asserted-by":"crossref","first-page":"163","DOI":"10.1007\/978-3-642-02053-7_9","volume-title":"Coordination Models and Languages","author":"Ritson Carl G.","year":"2009","unstructured":"Carl G. Ritson, Adam T. Sampson, and Frederick R. M. Barnes. 2009. Multicore scheduling for lightweight communicating processes. In Coordination Models and Languages. John Field and Vasco T. Vasconcelos (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 163\u2013183."},{"key":"e_1_3_3_22_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. Retrieved from http:\/\/www.cs.ox.ac.uk\/people\/bill.roscoe\/publications\/68b.pdf. The text book teaching material can be found athttp:\/\/www.comlab.ox.ac.uk\/publications\/books\/concurrency\/"},{"key":"e_1_3_3_23_2","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-84882-258-0","volume-title":"Understanding Concurrent Systems","author":"Roscoe A. W.","year":"2010","unstructured":"A. W. Roscoe. 2010. Understanding Concurrent Systems. Springer. Retrieved from http:\/\/www.comlab.ox.ac.uk\/ucs"},{"key":"e_1_3_3_24_2","volume-title":"Proceedings of Communicating Process Architecture 2016","author":"Shrestha Cable","year":"2016","unstructured":"Cable Shrestha and Jan B. Pedersen. 2016. JVMCSP\u2014approaching billions of processes on a single-core JVM. In Proceedings of Communicating Process Architecture 2016. Kevin Chalmers, Jan B. Pedersen, Jan F. Broenink, Brian Vinter, and Peter H. Welch (Eds.). IOS Press, Amsterdam, The Netherlands."},{"key":"e_1_3_3_25_2","first-page":"35","volume-title":"CPA","author":"Sufrin Bernard","year":"2008","unstructured":"Bernard Sufrin. 2008. Communicating scala objects.. In CPA, Vol. 66. 35\u201354."},{"key":"e_1_3_3_26_2","volume-title":"Proceedings of the 8th International Python Conference","volume":"1","author":"Tismer Christian","year":"2000","unstructured":"Christian Tismer. 2000. Continuations and stackless python. In Proceedings of the 8th International Python Conference, Vol. 1."},{"key":"e_1_3_3_27_2","doi-asserted-by":"publisher","unstructured":"Peter Welch Neil Brown James Moores Kevin Chalmers and Bernhard Sputh. 2010. Alting barriers: Synchronisation with choice in java using JCSP. Concurrency and Computation: Practice and Experience 22 8 (2010) 1049\u20131062. DOI:10.1002\/cpe.1471. arXiv:https:\/\/onlinelibrary.wiley.com\/doi\/pdf\/10.1002\/cpe.1471","DOI":"10.1002\/cpe.1471"},{"key":"e_1_3_3_28_2","first-page":"275","volume-title":"Communicating Process Architectures 2000","author":"Welch Peter H.","year":"2000","unstructured":"Peter H. Welch and Jeremy M. R. Martin. 2000. Formal analysis of concurrent java systems. In Communicating Process Architectures 2000. Peter H. Welch and Andr\u00e9 W. P. Bakkers (Eds.), Vol. 66, WoTUG-31. IOS Press, Amsterdam, The Netherlands, 275\u2013301. ISBN: 978-1-58603-907-3."}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3771735","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,11]],"date-time":"2026-02-11T23:20:11Z","timestamp":1770852011000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3771735"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,2,11]]},"references-count":27,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2026,3,31]]}},"alternative-id":["10.1145\/3771735"],"URL":"https:\/\/doi.org\/10.1145\/3771735","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,2,11]]},"assertion":[{"value":"2023-11-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-10-09","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-02-11","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}