{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T01:29:16Z","timestamp":1760059756230,"version":"build-2065373602"},"reference-count":18,"publisher":"MDPI AG","issue":"3","license":[{"start":{"date-parts":[[2025,7,7]],"date-time":"2025-07-07T00:00:00Z","timestamp":1751846400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Software"],"abstract":"<jats:p>In this paper we examine the OpenJDK library implementation of the ConcurrentLinkedQueue. We use model checking to verify that it behaves according to the algorithm it is based on: Michael and Scott\u2019s fast and practical non-blocking concurrent queue algorithm. In addition, we develop a simple concurrent queue specification in CSP and verify that Michael and Scott\u2019s algorithm satisfies it. We conclude that both the algorithm and the implementation are correct and both conform to our simpler concurrent queue specification, which we can use in place of either implementation in future verification tasks. The complete code is available on GitHub.<\/jats:p>","DOI":"10.3390\/software4030015","type":"journal-article","created":{"date-parts":[[2025,7,8]],"date-time":"2025-07-08T02:25:53Z","timestamp":1751941553000},"page":"15","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Analysing Concurrent Queues Using CSP: Examining Java\u2019s ConcurrentLinkedQueue"],"prefix":"10.3390","volume":"4","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, 6 Penrose Way, London SE10 0EW, UK"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2800-5095","authenticated-orcid":false,"given":"Jan B\u00e6kgaard","family":"Pedersen","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Nevada Las Vegas, 4505 S. Maryland Parkway, Las Vegas, NV 89154, USA"}]}],"member":"1968","published-online":{"date-parts":[[2025,7,7]]},"reference":[{"key":"ref_1","doi-asserted-by":"crossref","unstructured":"Michael, M.M., and Scott, M.L. (1996, January 23\u201326). Simple, fast, and practical non-blocking and blocking concurrent queue algorithms. Proceedings of the Fifteenth Annual ACM Symposium on Principles of Distributed Computing (PODC \u201996), New York, NY, USA.","DOI":"10.1145\/248052.248106"},{"key":"ref_2","doi-asserted-by":"crossref","unstructured":"Gibson-Robinson, T., Hopcroft, P., and Lazi\u0107, R. (2017). Analysing Lock-Free Linearizable Datatypes Using CSP. Concurrency, Security and Puzzles: Essays Dedicated to Andrew William Roscoe on the Occasion of His 60th Birthday, Springer. LNCS.","DOI":"10.1007\/978-3-319-51046-0"},{"key":"ref_3","doi-asserted-by":"crossref","first-page":"666","DOI":"10.1145\/359576.359585","article-title":"Communicating Sequential Processes","volume":"21","author":"Hoare","year":"1978","journal-title":"Commun. ACM"},{"key":"ref_4","doi-asserted-by":"crossref","unstructured":"Hoare, C.A.R. (1985). Communicating Sequential Processes, Prentice-Hall.","DOI":"10.1007\/978-3-642-82921-5_4"},{"key":"ref_5","doi-asserted-by":"crossref","unstructured":"Roscoe, A. (2010). CSP is expressive enough for \u03c0. Reflections on the Work of CAR Hoare, Springer.","DOI":"10.1007\/978-1-84882-912-1"},{"key":"ref_6","unstructured":"Roscoe, A.W. (1998). The Theory and Practice of Concurrency, Prentice Hall. Available online: http:\/\/www.comlab.ox.ac.uk\/publications\/books\/concurrency\/."},{"key":"ref_7","unstructured":"(2025, April 29). FDR 4.2 Documentation. Available online: https:\/\/cocotec.io\/fdr\/manual\/."},{"key":"ref_8","unstructured":"Liu, Y., Chen, W., Liu, Y.A., and Sun, J. (2009, January 2\u20136). Model checking linearizability via refinement. Proceedings of the FM 2009: Formal Methods: Second World Congress, Eindhoven, The Netherlands. Proceedings 2."},{"key":"ref_9","doi-asserted-by":"crossref","first-page":"463","DOI":"10.1145\/78969.78972","article-title":"Linearizability: A correctness condition for concurrent objects","volume":"12","author":"Herlihy","year":"1990","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"ref_10","doi-asserted-by":"crossref","unstructured":"Roscoe, A.W. (2010). Understanding Concurrent Systems, Springer.","DOI":"10.1007\/978-1-84882-258-0"},{"key":"ref_11","first-page":"187","article-title":"FDR3\u2014A Modern Refinement Checker for CSP","volume":"Volume 8413","author":"Havelund","year":"2014","journal-title":"Tools and Algorithms for the Construction and Analysis of Systems"},{"key":"ref_12","unstructured":"Herlihy, M., Shavit, N., Luchangco, V., and Spear, M. (2020). The Art of Multiprocessor Programming, Morgan Kaufmann."},{"key":"ref_13","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P.W., Rinetzky, N., Vechev, M.T., Yahav, E., and Yorsh, G. (2010, January 25\u201328). Verifying linearizability with hindsight. Proceedings of the 29th ACM SIGACT-SIGOPS Symposium on Principles of Distributed Computing, Zurich, Switzerland.","DOI":"10.1145\/1835698.1835722"},{"key":"ref_14","doi-asserted-by":"crossref","first-page":"547","DOI":"10.1007\/s00165-021-00541-8","article-title":"Verifying correctness of persistent concurrent data structures: A sound and complete method","volume":"33","author":"Derrick","year":"2021","journal-title":"Form. Asp. Comput."},{"key":"ref_15","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2796550","article-title":"Verifying linearisability: A comparative survey","volume":"48","author":"Dongol","year":"2015","journal-title":"ACM Comput. Surv. (CSUR)"},{"key":"ref_16","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3605942","article-title":"Toward verifying cooperatively scheduled runtimes using CSP","volume":"35","author":"Pedersen","year":"2023","journal-title":"Form. Asp. Comput."},{"key":"ref_17","doi-asserted-by":"crossref","unstructured":"Mahmoud, A.T., Mohammed, A.A., Ayman, M., Medhat, W., Selim, S., Zayed, H., Yousef, A.H., and Elaraby, N. (2024). Formal Verification of Code Conversion: A Comprehensive Survey. Technologies, 12.","DOI":"10.3390\/technologies12120244"},{"key":"ref_18","unstructured":"OpenJDK (2025, April 29). LinkedBlockingQueue.java. Available online: https:\/\/docs.oracle.com\/javase\/8\/docs\/api\/java\/util\/concurrent\/LinkedBlockingQueue.html."}],"container-title":["Software"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/2674-113X\/4\/3\/15\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T18:06:09Z","timestamp":1760033169000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/2674-113X\/4\/3\/15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,7,7]]},"references-count":18,"journal-issue":{"issue":"3","published-online":{"date-parts":[[2025,9]]}},"alternative-id":["software4030015"],"URL":"https:\/\/doi.org\/10.3390\/software4030015","relation":{},"ISSN":["2674-113X"],"issn-type":[{"type":"electronic","value":"2674-113X"}],"subject":[],"published":{"date-parts":[[2025,7,7]]}}}