{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T10:56:02Z","timestamp":1761648962770},"reference-count":36,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2021,11,30]],"date-time":"2021-11-30T00:00:00Z","timestamp":1638230400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,11,30]],"date-time":"2021-11-30T00:00:00Z","timestamp":1638230400000},"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":["J. Comput. Sci. Technol."],"published-print":{"date-parts":[[2021,12]]},"DOI":"10.1007\/s11390-021-1616-1","type":"journal-article","created":{"date-parts":[[2021,12,15]],"date-time":"2021-12-15T03:03:42Z","timestamp":1639537422000},"page":"1269-1290","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Trace Semantics and Algebraic Laws for Total Store Order Memory Model"],"prefix":"10.1007","volume":"36","author":[{"given":"Li-Li","family":"Xiao","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hui-Biao","family":"Zhu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Qi-Wen","family":"Xu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,11,30]]},"reference":[{"key":"1616_CR1","doi-asserted-by":"publisher","unstructured":"Passos L B C, Pfitscher G H, Filho R T M. Performance evaluation of two parallel programming paradigms applied to the symplectic integrator running on COTS PC cluster. In Proc. the 21st Int. Symp. Parallel and Distributed Processing, Mar. 2007, pp.1-8. https:\/\/doi.org\/10.1109\/IPDPS.2007.370563.","DOI":"10.1109\/IPDPS.2007.370563"},{"issue":"12","key":"1616_CR2","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1109\/2.546611","volume":"29","author":"SV Adve","year":"1996","unstructured":"Adve S V, Gharachorloo K. Shared memory consistency models: A tutorial. Computer, 1996, 29(12): 66-76. https:\/\/doi.org\/10.1109\/2.546611.","journal-title":"Computer"},{"key":"1616_CR3","doi-asserted-by":"publisher","unstructured":"Lamport L. How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Computers, 1979, C-28(9): 690-691. https:\/\/doi.org\/10.1109\/TC.1979.1675439.","DOI":"10.1109\/TC.1979.1675439"},{"key":"1616_CR4","doi-asserted-by":"crossref","unstructured":"Sorin D J, Hill M D, Wood D A. A Primer on Memory Consistency and Cache Coherence. Morgan & Claypool Publishers, 2011. https:\/\/doi.org\/10.2200\/S00346ED1V01Y201104CAC016.","DOI":"10.2200\/S00346ED1V01Y201104CAC016"},{"key":"1616_CR5","doi-asserted-by":"publisher","unstructured":"Owens S, Sarkar S, Sewell P. A better x86 memory model: x86-TSO. In Proc. the 22nd Int. Conf. Theorem Proving in Higher Order Logics, Aug. 2009, pp.391-407. https:\/\/doi.org\/10.1007\/978-3-642-03359-9_27.","DOI":"10.1007\/978-3-642-03359-9_27"},{"key":"1616_CR6","doi-asserted-by":"publisher","unstructured":"Dongol B, Derrick J, Smith G. Reasoning algebraically about refinement on TSO architectures. In Proc. the 11th Int. Colloquium on Theoretical Aspects of Computing, Sept. 2014, pp.151-168. https:\/\/doi.org\/10.1007\/978-3-319-10882-7_10.","DOI":"10.1007\/978-3-319-10882-7_10"},{"key":"1616_CR7","doi-asserted-by":"publisher","unstructured":"Kang J, Hur C K, Lahav O, Vafeiadis V, Dreyer D. A promising semantics for relaxed-memory concurrency. In Proc. the 44th Symp. Principles of Programming Languages, Jan. 2017, pp.175-189. https:\/\/doi.org\/10.1145\/3009837.3009850.","DOI":"10.1145\/3009837.3009850"},{"issue":"7","key":"1616_CR8","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 F Z, Myreen M O. x86-TSO: A rigorous and usable programmer\u2019s model for x86 multiprocessors. Communications of the ACM, 2010, 53(7): 89-97. https:\/\/doi.org\/10.1145\/1785414.1785443.","journal-title":"Communications of the ACM"},{"key":"1616_CR9","doi-asserted-by":"crossref","unstructured":"Hoare C A R, He J. Unifying Theories of Programming. Prentice Hall, 1998.","DOI":"10.1007\/BFb0002714"},{"key":"1616_CR10","unstructured":"Plotkin G D. A structural approach to operational semantics. Technical Report, Aarhus University, 1981. http:\/\/citeseerx.ist.psu.edu\/viewdoc\/download;jsessionid=5155CF1E81938DF7CA5AEE78AA3CCD0D?doi=10.1.1.4.8186-&rep=rep1&type=pdf, Sept. 2021."},{"key":"1616_CR11","unstructured":"Stoy J E. Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory. MIT Press, 1981."},{"issue":"8","key":"1616_CR12","doi-asserted-by":"publisher","first-page":"672","DOI":"10.1145\/27651.27653","volume":"30","author":"CAR Hoare","year":"1987","unstructured":"Hoare C A R, Hayes I J, He J, Morgan C C, Roscoe A W, Sanders J W, Sorensen I H, Spivey J M, Sufrin B A. Laws of programming. Communications of the ACM, 1987, 30(8): 672-686. https:\/\/doi.org\/10.1145\/27651.27653.","journal-title":"Communications of the ACM"},{"issue":"8","key":"1616_CR13","doi-asserted-by":"publisher","first-page":"701","DOI":"10.1007\/BF01191809","volume":"30","author":"CAR Hoare","year":"1993","unstructured":"Hoare C A R, He J, Sampaio A. Normal form approach to compiler design. Acta Informatica, 1993, 30(8): 701-739. https:\/\/doi.org\/10.1007\/BF01191809.","journal-title":"Acta Informatica"},{"key":"1616_CR14","doi-asserted-by":"publisher","unstructured":"Sampaio A. An Algebraic Approach to Compiler Design. World Scientific, 1997. https:\/\/doi.org\/10.1142\/2870.","DOI":"10.1142\/2870"},{"key":"1616_CR15","doi-asserted-by":"publisher","unstructured":"Kavanagh R, Brookes S. A denotational semantics for SPARC TSO. In Proc. the 33rd Conf. Mathematical Foundations of Programming Semantics, Jun. 2017, pp.223-239. https:\/\/doi.org\/10.1016\/j.entcs.2018.03.025.","DOI":"10.1016\/j.entcs.2018.03.025"},{"key":"1616_CR16","doi-asserted-by":"publisher","unstructured":"Travkin O, Wehrheim H. Handling TSO in mechanized linearizability proofs. In Proc. the 10th Int. Haifa Verification Conference, Nov. 2014, pp.132-147. https:\/\/doi.org\/10.1007\/978-3-319-13338-6_11.","DOI":"10.1007\/978-3-319-13338-6_11"},{"key":"1616_CR17","doi-asserted-by":"publisher","unstructured":"Winter K, Smith G, Derrick J. Observational models for linearizability checking on weak memory models. In Proc. the 12th Int. Symp. Theoretical Aspects of Software Engineering, Aug. 2018, pp.100-107. https:\/\/doi.org\/10.1109\/TASE.2018.00021.","DOI":"10.1109\/TASE.2018.00021"},{"issue":"2","key":"1616_CR18","doi-asserted-by":"publisher","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","volume":"5","author":"A Tarski","year":"1955","unstructured":"Tarski A. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 1955, 5(2): 285-309. https:\/\/doi.org\/10.2140\/pjm.1955.5.285.","journal-title":"Pacific Journal of Mathematics"},{"issue":"2","key":"1616_CR19","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1006\/inco.1996.0056","volume":"127","author":"SD Brookes","year":"1996","unstructured":"Brookes S D. Full abstraction for a shared-variable parallel language. Information and Computation, 1996, 127(2): 145-163. https:\/\/doi.org\/10.1006\/inco.1996.0056.","journal-title":"Information and Computation"},{"key":"1616_CR20","doi-asserted-by":"crossref","unstructured":"Hoare C A R. Communicating Sequential Processes. Prentice-Hall, 1985.","DOI":"10.1007\/978-3-642-82921-5_4"},{"issue":"8","key":"1616_CR21","doi-asserted-by":"publisher","first-page":"789","DOI":"10.1007\/s00236-016-0275-0","volume":"54","author":"PA Abdulla","year":"2017","unstructured":"Abdulla P A, Aronis S, Atig M F, Jonsson B, Leonardsson C, Sagonas K. Stateless model checking for TSO and PSO. Acta Informatica, 2017, 54(8): 789-818. https:\/\/doi.org\/10.1007\/s00236-016-0275-0.","journal-title":"Acta Informatica"},{"issue":"4","key":"1616_CR22","doi-asserted-by":"publisher","first-page":"569","DOI":"10.1007\/s10817-020-09579-4","volume":"65","author":"Z H\u00f3u","year":"2021","unstructured":"H\u00f3u Z, San\u00e1n D, Tiu A, Liu Y, Hoa K C, Dong J S. An Isabelle\/HOL formalisation of the SPARC instruction set architecture and the TSO memory model. Journal of Automated Reasoning, 2021, 65(4): 569-598. https:\/\/doi.org\/10.1007\/s10817-020-09579-4.","journal-title":"Journal of Automated Reasoning"},{"key":"1616_CR23","unstructured":"Khyzha A, Gotsman A. Compositional reasoning about concurrent libraries on the axiomatic TSO memory model. Technical Report, IMDEA Software Institute, 2012. https:\/\/pageperso.lis-lab.fr\/~pierrealain.reynier\/publis\/movep12.pdf#page=116, Mar. 2021."},{"key":"1616_CR24","unstructured":"Batty M J. The C11 and C++ 11 concurrency model [Ph.D. Thesis]. Wolfson College, University of Cambridge, Cambridge, 2015."},{"key":"1616_CR25","doi-asserted-by":"crossref","unstructured":"Ridge T. A Rely-Guarantee proof system for x86-TSO. In Proc. the 3rd Int. Conf. Verified Software: Theories, Tools, and Experiments, Aug. 2010, pp.55-70. 10.1007\/978-3-642-15057-9 4.","DOI":"10.1007\/978-3-642-15057-9_4"},{"key":"1616_CR26","unstructured":"Kavanagh R, Brookes S. A denotational account of C11-style memory. arXiv:1804.04214, 2018. https:\/\/arxiv.org\/abs\/1804.04214, Mar. 2021."},{"issue":"2","key":"1616_CR27","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1016\/0020-0190(93)90219-Y","volume":"45","author":"J He","year":"1993","unstructured":"He J, Hoare C A R. From algebra to operational semantics. Information Processing Letters, 1993, 45(2): 75-80. https:\/\/doi.org\/10.1016\/0020-0190(93)90219-Y.","journal-title":"Information Processing Letters"},{"key":"1616_CR28","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1016\/j.scico.2013.08.012","volume":"85","author":"CAR Hoare","year":"2014","unstructured":"Hoare C A R, Van Staden S. The laws of programming unify process calculi. Science of Computer Programming, 2014, 85: 102-114. https:\/\/doi.org\/10.1016\/j.scico.2013.08.012.","journal-title":"Science of Computer Programming"},{"key":"1616_CR29","doi-asserted-by":"publisher","unstructured":"Hoare C A R. Laws of programming: The algebraic unification of theories of concurrency. In Proc. the 25th Int. Conf. Concurrency Theory, Sept. 2014, pp.1-6. https:\/\/doi.org\/10.1007\/978-3-662-44584-6_1.","DOI":"10.1007\/978-3-662-44584-6_1"},{"issue":"2","key":"1616_CR30","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/s00165-020-00513-4","volume":"32","author":"F Sheng","year":"2020","unstructured":"Sheng F, Zhu H, He J, Yang Z, Bowen J P. Theoretical and practical approaches to the denotational semantics for MDESL based on UTP. Formal Aspects of Computing, 2020, 32(2): 275-314. https:\/\/doi.org\/10.1007\/s00165-020-00513-4.","journal-title":"Formal Aspects of Computing"},{"key":"1616_CR31","doi-asserted-by":"publisher","unstructured":"Sheng F, Zhu H, He J, Yang Z, Bowen J P. Theoretical and practical aspects of linking operational and algebraic semantics for MDESL. ACM Transactions on Software Engineering and Methodology, 2019, 28(3): Article No. 14. https:\/\/doi.org\/10.1145\/3295699.","DOI":"10.1145\/3295699"},{"issue":"1","key":"1616_CR32","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1016\/j.jlap.2011.06.003","volume":"81","author":"H Zhu","year":"2012","unstructured":"Zhu H, Yang F, He J, Bowen J P, Sanders J W, Qin S. Linking operational semantics and algebraic semantics for a probabilistic timed shared-variable language. The Journal of Logic and Algebraic Methods Program, 2012, 81(1): 2-25. https:\/\/doi.org\/10.1016\/j.jlap.2011.06.003.","journal-title":"The Journal of Logic and Algebraic Methods Program"},{"key":"1616_CR33","unstructured":"Zhu H. Linking the semantics of a multithreaded discrete event simulation language [Ph.D. Thesis]. Institute for Computing Research, London South Bank University, 2005."},{"issue":"2","key":"1616_CR34","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/s001650200031","volume":"14","author":"Y Chen","year":"2002","unstructured":"Chen Y. Generic composition. Formal Aspects of Computing, 2002, 14(2): 108-122. https:\/\/doi.org\/10.1007\/s001650200031.","journal-title":"Formal Aspects of Computing"},{"key":"1616_CR35","unstructured":"Huet G, Kahn G, Paulin-Mohring C. The Coq proof assistant\u2014A tutorial (Version v8.1). Technical Report, INRIA, 2005. https:\/\/coq.inria.fr\/distrib\/current\/refman\/, Mar. 2021."},{"key":"1616_CR36","doi-asserted-by":"publisher","unstructured":"Owre S, Rushby J M, Shankar N. PVS: A prototype verification system. In Proc. the 11th Int. Conf. Automated Deduction, Jun. 1992, pp.748-752. https:\/\/doi.org\/10.1007\/3-540-55602-8_217.","DOI":"10.1007\/3-540-55602-8_217"}],"container-title":["Journal of Computer Science and Technology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11390-021-1616-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11390-021-1616-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11390-021-1616-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,14]],"date-time":"2024-09-14T12:47:45Z","timestamp":1726318065000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11390-021-1616-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,11,30]]},"references-count":36,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2021,12]]}},"alternative-id":["1616"],"URL":"https:\/\/doi.org\/10.1007\/s11390-021-1616-1","relation":{},"ISSN":["1000-9000","1860-4749"],"issn-type":[{"type":"print","value":"1000-9000"},{"type":"electronic","value":"1860-4749"}],"subject":[],"published":{"date-parts":[[2021,11,30]]},"assertion":[{"value":"27 May 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"7 November 2021","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"30 November 2021","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}