{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,4]],"date-time":"2025-05-04T16:10:06Z","timestamp":1746375006983,"version":"3.40.4"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319108810"},{"type":"electronic","value":"9783319108827"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-10882-7_10","type":"book-chapter","created":{"date-parts":[[2014,9,11]],"date-time":"2014-09-11T06:54:19Z","timestamp":1410418459000},"page":"151-168","source":"Crossref","is-referenced-by-count":2,"title":["Reasoning Algebraically About Refinement on TSO Architectures"],"prefix":"10.1007","author":[{"given":"Brijesh","family":"Dongol","sequence":"first","affiliation":[]},{"given":"John","family":"Derrick","sequence":"additional","affiliation":[]},{"given":"Graeme","family":"Smith","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"12","key":"10_CR1","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1109\/2.546611","volume":"29","author":"S.V. Adve","year":"1996","unstructured":"Adve, S.V., Gharachorloo, K.: Shared memory consistency models: A tutorial. IEEE Computer\u00a029(12), 66\u201376 (1996)","journal-title":"IEEE Computer"},{"issue":"2","key":"10_CR2","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/s10703-012-0161-5","volume":"41","author":"J. Alglave","year":"2012","unstructured":"Alglave, J.: A formal hierarchy of weak memory models. Formal Methods in System Design\u00a041(2), 178\u2013210 (2012)","journal-title":"Formal Methods in System Design"},{"issue":"4","key":"10_CR3","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/s002360050163","volume":"36","author":"R.J.R. Back","year":"1999","unstructured":"Back, R.J.R., von Wright, J.: Reasoning algebraically about loops. Acta Informatica\u00a036(4), 295\u2013334 (1999)","journal-title":"Acta Informatica"},{"key":"10_CR4","unstructured":"Bovet, D., Cesati, M.: Understanding the Linux Kernel, 3rd edn. OReilly (2005)"},{"key":"10_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/3-540-44898-5_4","volume-title":"Static Analysis","author":"J. Boyland","year":"2003","unstructured":"Boyland, J.: Checking interference with fractional permissions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol.\u00a02694, pp. 55\u201372. Springer, Heidelberg (2003)"},{"key":"10_CR6","doi-asserted-by":"crossref","unstructured":"Burckhardt, S., Alur, R., Martin, M.M.K.: Checkfence: Checking consistency of concurrent data types on relaxed memory models. In: PLDI, pp. 12\u201321 (2007)","DOI":"10.1145\/1273442.1250737"},{"key":"10_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/978-3-642-28869-2_5","volume-title":"Programming Languages and Systems","author":"S. Burckhardt","year":"2012","unstructured":"Burckhardt, S., Gotsman, A., Musuvathi, M., Yang, H.: Concurrent library correctness on the TSO memory model. In: Seidl, H. (ed.) Programming Languages and Systems. LNCS, vol.\u00a07211, pp. 87\u2013107. Springer, Heidelberg (2012)"},{"key":"10_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1007\/978-3-642-11970-5_7","volume-title":"Compiler Construction","author":"S. Burckhardt","year":"2010","unstructured":"Burckhardt, S., Musuvathi, M., Singh, V.: Verifying local transformations on relaxed memory models. In: Gupta, R. (ed.) CC 2010. LNCS, vol.\u00a06011, pp. 104\u2013123. Springer, Heidelberg (2010)"},{"key":"10_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1007\/978-3-642-14052-5_28","volume-title":"Interactive Theorem Proving","author":"E. Cohen","year":"2010","unstructured":"Cohen, E., Schirmer, B.: From total store order to sequential consistency: A practical reduction theorem. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol.\u00a06172, pp. 403\u2013418. Springer, Heidelberg (2010)"},{"key":"10_CR10","doi-asserted-by":"crossref","unstructured":"Dongol, B., Derrick, J.: Data refinement for true concurrency. In: Derrick, J., Boiten, E.A., Reeves, S. (eds.) Refine. EPTCS, vol.\u00a0115, pp. 15\u201335 (2013)","DOI":"10.4204\/EPTCS.115.2"},{"key":"10_CR11","unstructured":"Dongol, B., Derrick, J., Hayes, I.J.: Fractional permissions and non-deterministic evaluators in interval temporal logic. ECEASST\u00a053 (2012)"},{"issue":"11","key":"10_CR12","doi-asserted-by":"publisher","first-page":"2047","DOI":"10.1016\/j.scico.2012.07.008","volume":"78","author":"B. Dongol","year":"2013","unstructured":"Dongol, B., Hayes, I.J.: Deriving real-time action systems in a sampling logic. Sci. Comput. Program.\u00a078(11), 2047\u20132063 (2013)","journal-title":"Sci. Comput. Program."},{"issue":"Pt. B","key":"10_CR13","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1016\/j.scico.2013.08.009","volume":"85","author":"B. Dongol","year":"2014","unstructured":"Dongol, B., Hayes, I.J., Derrick, J.: Deriving real-time action systems with multiple time bands using algebraic reasoning. Sci. of Comp. Prog.\u00a085(Pt. B), 137\u2013165 (2014)","journal-title":"Sci. of Comp. Prog."},{"key":"10_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/978-3-642-33314-9_4","volume-title":"Relational and Algebraic Methods in Computer Science","author":"B. Dongol","year":"2012","unstructured":"Dongol, B., Hayes, I.J., Meinicke, L., Solin, K.: Towards an algebra for real-time programs. In: Kahl, W., Griffin, T.G. (eds.) RAMICS 2012. LNCS, vol.\u00a07560, pp. 50\u201365. Springer, Heidelberg (2012)"},{"key":"10_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/978-3-642-39718-9_11","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2013","author":"B. Dongol","year":"2013","unstructured":"Dongol, B., Travkin, O., Derrick, J., Wehrheim, H.: A high-level semantics for program execution under total store order memory. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) ICTAC 2013. LNCS, vol.\u00a08049, pp. 177\u2013194. Springer, Heidelberg (2013)"},{"key":"10_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/978-3-642-33651-5_3","volume-title":"Distributed Computing","author":"A. Gotsman","year":"2012","unstructured":"Gotsman, A., Musuvathi, M., Yang, H.: Show no weakness: Sequentially consistent specifications of TSO libraries. In: Aguilera, M.K. (ed.) DISC 2012. LNCS, vol.\u00a07611, pp. 31\u201345. Springer, Heidelberg (2012)"},{"issue":"6","key":"10_CR17","doi-asserted-by":"publisher","first-page":"741","DOI":"10.1093\/comjnl\/bxt005","volume":"56","author":"I.J. Hayes","year":"2013","unstructured":"Hayes, I.J., Burns, A., Dongol, B., Jones, C.B.: Comparing degrees of non-determinism in expression evaluation. Comput. J.\u00a056(6), 741\u2013755 (2013)","journal-title":"Comput. J."},{"issue":"9","key":"10_CR18","doi-asserted-by":"publisher","first-page":"690","DOI":"10.1109\/TC.1979.1675439","volume":"28","author":"L. Lamport","year":"1979","unstructured":"Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Computers\u00a028(9), 690\u2013691 (1979)","journal-title":"IEEE Trans. Computers"},{"key":"10_CR19","doi-asserted-by":"crossref","unstructured":"Moszkowski, B.C.: A complete axiomatization of Interval Temporal Logic with infinite time. In: LICS, pp. 241\u2013252 (2000)","DOI":"10.1109\/LICS.2000.855773"},{"key":"10_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"478","DOI":"10.1007\/978-3-642-14107-2_23","volume-title":"ECOOP 2010 \u2013 Object-Oriented Programming","author":"S. Owens","year":"2010","unstructured":"Owens, S.: Reasoning about the implementation of concurrency abstractions on x86-TSO. In: D\u2019Hondt, T. (ed.) ECOOP 2010. LNCS, vol.\u00a06183, pp. 478\u2013503. Springer, Heidelberg (2010)"},{"key":"10_CR21","doi-asserted-by":"crossref","unstructured":"Park, S., Dill, D.L.: An executable specification, analyzer and verifier for RMO (relaxed memory order). In: SPAA, pp. 34\u201341 (1995)","DOI":"10.1145\/215399.215413"},{"issue":"7","key":"10_CR22","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. Commun. ACM\u00a053(7), 89\u201397 (2010)","journal-title":"Commun. ACM"},{"key":"10_CR23","doi-asserted-by":"crossref","unstructured":"Sorin, D.J., Hill, M.D., Wood, D.A.: A Primer on Memory Consistency and Cache Coherence. Synthesis Lectures on Computer Architecture. Morgan & Claypool (2011)","DOI":"10.2200\/S00346ED1V01Y201104CAC016"},{"key":"10_CR24","unstructured":"Spivey, J.M.: The Z Notation: A Reference Manual. Prentice Hall (1992)"},{"key":"10_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/978-3-319-03077-7_21","volume-title":"Hardware and Software: Verification and Testing","author":"O. Travkin","year":"2013","unstructured":"Travkin, O., M\u00fctze, A., Wehrheim, H.: SPIN as a linearizability checker under weak memory models. In: Bertacco, V., Legay, A. (eds.) HVC 2013. LNCS, vol.\u00a08244, pp. 311\u2013326. Springer, Heidelberg (2013)"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2014"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-10882-7_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,4]],"date-time":"2025-05-04T15:44:33Z","timestamp":1746373473000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-10882-7_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319108810","9783319108827"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-10882-7_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}