{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,12]],"date-time":"2026-05-12T09:17:21Z","timestamp":1778577441462,"version":"3.51.4"},"reference-count":25,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2022,5,23]],"date-time":"2022-05-23T00:00:00Z","timestamp":1653264000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,5,23]],"date-time":"2022-05-23T00:00:00Z","timestamp":1653264000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Mobile Netw Appl"],"published-print":{"date-parts":[[2022,10]]},"DOI":"10.1007\/s11036-022-01989-5","type":"journal-article","created":{"date-parts":[[2022,5,23]],"date-time":"2022-05-23T09:04:58Z","timestamp":1653296698000},"page":"2068-2083","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Modeling and Verifying PSO Memory Model Using CSP"],"prefix":"10.1007","volume":"27","author":[{"given":"Lili","family":"Xiao","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Huibiao","family":"Zhu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Qiwen","family":"Xu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Phan Cong","family":"Vinh","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,5,23]]},"reference":[{"issue":"7","key":"1989_CR1","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1145\/1785414.1785443","volume":"53","author":"P Sewell","year":"2010","unstructured":"Sewell P, Sarkar S, Owens S, Nardelli FZ, Myreen MO (2010) x86-tso: a rigorous and usable programmer\u2019s model for x86 multiprocessors. Commun ACM 53(7):89\u201397. https:\/\/doi.org\/10.1145\/1785414.1785443","journal-title":"Commun ACM"},{"key":"1989_CR2","doi-asserted-by":"crossref","unstructured":"Colvin RJ, Smith G (2018) A wide-spectrum language for verification of programs on weak memory models. In: Havelund K, Peleska J, Roscoe B, de Vink EP (eds) Formal Methods - 22nd International Symposium, FM 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 15-17, 2018, Proceedings, Lecture Notes in Computer Science, vol 10951. Springer, pp 240\u2013257","DOI":"10.1007\/978-3-319-95582-7_14"},{"key":"1989_CR3","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.jlamp.2018.10.004","volume":"103","author":"DS Fava","year":"2019","unstructured":"Fava DS, Steffen M, Stolz V (2019) Operational semantics of a weak memory model with channel synchronization. J Log Algebraic Methods Program 103:1\u201330. https:\/\/doi.org\/10.1016\/j.jlamp.2018.10.004","journal-title":"J Log Algebraic Methods Program"},{"key":"1989_CR4","doi-asserted-by":"publisher","unstructured":"Sorin DJ, Hill MD, Wood DA (2011) A primer on memory consistency and cache coherence. Synthesis Lectures on Computer Architecture, Morgan & Claypool Publishers. https:\/\/doi.org\/10.2200\/S00346ED1V01Y201104CAC016","DOI":"10.2200\/S00346ED1V01Y201104CAC016"},{"key":"1989_CR5","unstructured":"(1992) SPARC architecture manual - version 8. Prentice Hall. Accessed 1 Mar 2020"},{"key":"1989_CR6","doi-asserted-by":"crossref","unstructured":"Kang J, Hur C, Lahav O, Vafeiadis V, Dreyer D (2017) A promising semantics for relaxed-memory concurrency. In: Castagna G, Gordon AD (eds) Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017. http:\/\/dl.acm.org\/citation.cfm?id=3009850. ACM, pp 175\u2013189","DOI":"10.1145\/3093333.3009850"},{"issue":"8","key":"1989_CR7","doi-asserted-by":"publisher","first-page":"666","DOI":"10.1145\/359576.359585","volume":"21","author":"CAR Hoare","year":"1978","unstructured":"Hoare CAR (1978) Communicating sequential processes. Commun ACM 21(8):666\u2013677. https:\/\/doi.org\/10.1145\/359576.359585","journal-title":"Commun ACM"},{"key":"1989_CR8","doi-asserted-by":"publisher","unstructured":"Sun J, Liu Y, Dong JS, Pang J (2009) PAT: towards flexible verification under fairness. In: Bouajjani A, Maler O (eds) Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings, Lecture Notes in Computer Science. https:\/\/doi.org\/10.1007\/978-3-642-02658-4_59, vol 5643. Springer, pp 709\u2013714","DOI":"10.1007\/978-3-642-02658-4_59"},{"key":"1989_CR9","doi-asserted-by":"publisher","unstructured":"Huang S, Huang J (2016) Maximal causality reduction for TSO and PSO. In: Visser E, Smaragdakis Y (eds) Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2016, part of SPLASH 2016, Amsterdam, The Netherlands, October 30 - November 4, 2016. https:\/\/doi.org\/10.1145\/2983990.2984025. ACM, pp 447\u2013461","DOI":"10.1145\/2983990.2984025"},{"key":"1989_CR10","doi-asserted-by":"publisher","unstructured":"Kavanagh R, Brookes S (2018) A denotational semantics for SPARC TSO. In: Staton S (ed) Proceedings of the Thirty-Fourth Conference on the Mathematical Foundations of Programming Semantics, MFPS 2018, Dalhousie University, Halifax, Canada, June 6-9, 2018, Electronic Notes in Theoretical Computer Science. https:\/\/doi.org\/10.1016\/j.entcs.2018.03.025, vol 341. Elsevier, pp 223\u2013239","DOI":"10.1016\/j.entcs.2018.03.025"},{"key":"1989_CR11","doi-asserted-by":"publisher","first-page":"102,343","DOI":"10.1016\/j.scico.2019.102343","volume":"187","author":"S Xiang","year":"2020","unstructured":"Xiang S, Zhu H, Wu X, Xiao L, Bonsangue MM, Xie W, Zhang L (2020) Modeling and verifying the topology discovery mechanism of openflow controllers in software-defined networks using process algebra. Sci Comput Program 187:102,343. https:\/\/doi.org\/10.1016\/j.scico.2019.102343","journal-title":"Sci Comput Program"},{"key":"1989_CR12","doi-asserted-by":"publisher","unstructured":"Buth B, Kouvaras M, Peleska J, Shi H (1997) Deadlock analysis for a fault-tolerant system. In: Johnson M (ed) Algebraic Methodology and Software Technology, 6th International Conference, AMAST \u201997, Sydney, Australia, December 13-17, 1997, Proceedings, Lecture Notes in Computer Science. https:\/\/doi.org\/10.1007\/BFb0000463, vol 1349. Springer, pp 60\u201374","DOI":"10.1007\/BFb0000463"},{"issue":"10","key":"1989_CR13","doi-asserted-by":"publisher","first-page":"659","DOI":"10.1109\/32.637148","volume":"23","author":"G Lowe","year":"1997","unstructured":"Lowe G, Roscoe AW (1997) Using CSP to detect errors in the TMN protocol. IEEE Trans Software Eng 23(10):659\u2013669. https:\/\/doi.org\/10.1109\/32.637148","journal-title":"IEEE Trans Software Eng"},{"key":"1989_CR14","doi-asserted-by":"publisher","unstructured":"Liu Y, Sun J, Dong JS (2010) Analyzing hierarchical complex real-time systems. In: Roman G, van der Hoek A (eds) Proceedings of the 18th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2010, Santa Fe, NM, USA, November 7-11, 2010. https:\/\/doi.org\/10.1145\/1882291.1882350. ACM, pp 365\u2013366","DOI":"10.1145\/1882291.1882350"},{"issue":"1","key":"1989_CR15","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s11704-013-3091-5","volume":"8","author":"Y Si","year":"2014","unstructured":"Si Y, Sun J, Liu Y, Dong JS, Pang J, Zhang SJ, Yang X (2014) Model checking with fairness assumptions using PAT. Frontiers Comput Sci 8(1):1\u201316. https:\/\/doi.org\/10.1007\/s11704-013-3091-5","journal-title":"Frontiers Comput Sci"},{"issue":"POPL","key":"1989_CR16","doi-asserted-by":"publisher","first-page":"19:1","DOI":"10.1145\/3158107","volume":"2","author":"C Pulte","year":"2018","unstructured":"Pulte C, Flur S, Deacon W, French J, Sarkar S, Sewell P (2018) Simplifying ARM concurrency: multicopy-atomic axiomatic and operational models for armv8. Proc ACM Program Lang 2(POPL):19:1\u201319:29. https:\/\/doi.org\/10.1145\/3158107","journal-title":"Proc ACM Program Lang"},{"key":"1989_CR17","doi-asserted-by":"publisher","unstructured":"Lahav O, Vafeiadis V (2016) Explaining relaxed memory models with program transformations. In: Fitzgerald JS, Heitmeyer CL, Gnesi S, Philippou A (eds) FM 2016: Formal Methods - 21st International Symposium, Limassol, Cyprus, November 9-11, 2016, Proceedings, Lecture Notes in Computer Science. https:\/\/doi.org\/10.1007\/978-3-319-48989-6_29, vol 9995, pp 479\u2013495","DOI":"10.1007\/978-3-319-48989-6_29"},{"key":"1989_CR18","doi-asserted-by":"publisher","unstructured":"Owens S, Sarkar S, Sewell P (2009) A better x86 memory model: x86-tso. In: Berghofer S, Nipkow T, Urban C, Wenzel M (eds) Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, Lecture Notes in Computer Science. https:\/\/doi.org\/10.1007\/978-3-642-03359-9_27, vol 5674. Springer, pp 391\u2013407","DOI":"10.1007\/978-3-642-03359-9_27"},{"issue":"4","key":"1989_CR19","doi-asserted-by":"publisher","first-page":"569","DOI":"10.1007\/s10817-020-09579-4","volume":"65","author":"Z Ho\u0307u","year":"2021","unstructured":"Ho\u0307u Z, Sana\u0307n D, Tiu A, Liu Y, Hoa KC, Dong JS (2021) An isabelle\/hol formalisation of the SPARC instruction set architecture and the TSO memory model. J Autom Reason 65(4):569\u2013598. https:\/\/doi.org\/10.1007\/s10817-020-09579-4","journal-title":"J Autom Reason"},{"key":"1989_CR20","doi-asserted-by":"publisher","unstructured":"Dodds M, Batty M (2018) Compositional verification of compiler optimisations on relaxed memory. In: Ahmed A (ed) Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Lecture Notes in Computer Science. https:\/\/doi.org\/10.1007\/978-3-319-89884-1_36, vol 10801. Springer, pp 1027\u20131055","DOI":"10.1007\/978-3-319-89884-1_36"},{"key":"1989_CR21","doi-asserted-by":"publisher","unstructured":"Alglave J, Kroening D, Tautschnig M (2013) Partial orders for efficient bounded model checking of concurrent software. In: Sharygina N, Veith H (eds) Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings, Lecture Notes in Computer Science. https:\/\/doi.org\/10.1007\/978-3-642-39799-8_9, vol 8044. Springer, pp 141\u2013157","DOI":"10.1007\/978-3-642-39799-8_9"},{"issue":"8","key":"1989_CR22","doi-asserted-by":"publisher","first-page":"789","DOI":"10.1007\/s00236-016-0275-0","volume":"54","author":"PA Abdulla","year":"2017","unstructured":"Abdulla PA, Aronis S, Atig MF, Jonsson B, Leonardsson C, Sagonas K (2017) Stateless model checking for TSO and PSO. Acta Informatica 54(8):789\u2013818. https:\/\/doi.org\/10.1007\/s00236-016-0275-0","journal-title":"Acta Informatica"},{"issue":"POPL","key":"1989_CR23","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3434285","volume":"5","author":"R Margalit","year":"2021","unstructured":"Margalit R, Lahav O (2021) Verifying observational robustness against a c11-style memory model. Proc ACM Program Lang 5(POPL):1\u201333. https:\/\/doi.org\/10.1145\/3434285","journal-title":"Proc ACM Program Lang"},{"key":"1989_CR24","doi-asserted-by":"publisher","unstructured":"Flur S, Gray KE, Pulte C, Sarkar S, Sezgin A, Maranget L, Deacon W, Sewell P (2016) Modelling the armv8 architecture, operationally: concurrency and ISA. In: Bod\u00edk R, Majumdar R (eds) Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016. https:\/\/doi.org\/10.1145\/2837614.2837615. ACM, pp 608\u2013621","DOI":"10.1145\/2837614.2837615"},{"key":"1989_CR25","doi-asserted-by":"publisher","unstructured":"Sarkar S, Sewell P, Alglave J, Maranget L, Williams D (2011) Understanding POWER multiprocessors. In: Hall MW, Padua DA (eds) Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, San Jose, CA, USA, June 4-8, 2011. https:\/\/doi.org\/10.1145\/1993498.1993520. ACM, pp 175\u2013186","DOI":"10.1145\/1993498.1993520"}],"container-title":["Mobile Networks and Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11036-022-01989-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11036-022-01989-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11036-022-01989-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,10,24]],"date-time":"2022-10-24T09:22:19Z","timestamp":1666603339000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11036-022-01989-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,5,23]]},"references-count":25,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2022,10]]}},"alternative-id":["1989"],"URL":"https:\/\/doi.org\/10.1007\/s11036-022-01989-5","relation":{},"ISSN":["1383-469X","1572-8153"],"issn-type":[{"value":"1383-469X","type":"print"},{"value":"1572-8153","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,5,23]]},"assertion":[{"value":"9 February 2022","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"23 May 2022","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"We have no competing interests to declare that are relevant to the content of this article. This article does not involve ethics issues.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"<!--Emphasis Type='Bold' removed-->Competing interests"}}]}}