{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,11,19]],"date-time":"2024-11-19T16:44:04Z","timestamp":1732034644429},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642397172"},{"type":"electronic","value":"9783642397189"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39718-9_11","type":"book-chapter","created":{"date-parts":[[2013,8,30]],"date-time":"2013-08-30T03:01:54Z","timestamp":1377831714000},"page":"177-194","source":"Crossref","is-referenced-by-count":4,"title":["A High-Level Semantics for Program Execution under Total Store Order Memory"],"prefix":"10.1007","author":[{"given":"Brijesh","family":"Dongol","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Oleg","family":"Travkin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"John","family":"Derrick","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Heike","family":"Wehrheim","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"12","key":"11_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"},{"key":"11_CR2","doi-asserted-by":"crossref","unstructured":"Alglave, J., Kroening, D., Nimal, V., Tautschnig, M.: Software verification for weak memory via program transformation. CoRR, abs\/1207.7264 (2012)","DOI":"10.1007\/978-3-642-37036-6_28"},{"issue":"2","key":"11_CR3","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1145\/1150019.1136489","volume":"34","author":"A. Arvind","year":"2006","unstructured":"Arvind, A., Maessen, J.-W.: Memory model = instruction reordering + store atomicity. SIGARCH Comput. Archit. News\u00a034(2), 29\u201340 (2006)","journal-title":"SIGARCH Comput. Archit. News"},{"key":"11_CR4","first-page":"7","volume-title":"POPL","author":"M.F. Atig","year":"2010","unstructured":"Atig, M.F., Bouajjani, A., Burckhardt, S., Musuvathi, M.: On the verification problem for weak memory models. In: POPL, pp. 7\u201318. ACM, New York (2010)"},{"key":"11_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":"11_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":"11_CR7","unstructured":"Inc. CORPORATE SPARC\u00a0International. The SPARC architecture manual: version 8. Prentice-Hall, Inc., Upper Saddle River, NJ, USA (1992)"},{"key":"11_CR8","unstructured":"Dongol, B., Derrick, J.: Proving linearisability via coarse-grained abstraction. CoRR, abs\/1212.5116 (2012)"},{"key":"11_CR9","unstructured":"Dongol, B., Derrick, J., Hayes, I.J.: Fractional permissions and non-deterministic evaluators in interval temporal logic. ECEASST\u00a053 (2012)"},{"key":"11_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/978-3-642-31113-0_7","volume-title":"Mathematics of Program Construction","author":"B. Dongol","year":"2012","unstructured":"Dongol, B., Hayes, I.J.: Deriving real-time action systems controllers from multiscale system specifications. In: Gibbons, J., Nogueira, P. (eds.) MPC 2012. LNCS, vol.\u00a07342, pp. 102\u2013131. Springer, Heidelberg (2012)"},{"key":"11_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/978-3-642-30729-4_4","volume-title":"Integrated Formal Methods","author":"B. Dongol","year":"2012","unstructured":"Dongol, B., Hayes, I.J.: Rely\/guarantee reasoning for teleo-reactive programs over multiple time bands. In: Derrick, J., Gnesi, S., Latella, D., Treharne, H. (eds.) IFM 2012. LNCS, vol.\u00a07321, pp. 39\u201353. Springer, Heidelberg (2012)"},{"key":"11_CR12","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":"11_CR13","doi-asserted-by":"crossref","unstructured":"Hayes, I.J., Burns, A., Dongol, B., Jones, C.: Comparing degrees of non-determinism in expression evaluation. The Computer Journal (accepted January 4, 2013)","DOI":"10.1093\/comjnl\/bxt005"},{"key":"11_CR14","doi-asserted-by":"crossref","unstructured":"Herlihy, M., Moss, J.E.B.: Transactional memory: Architectural support for lock-free data structures. In: Jay Smith, A. (ed.) ISCA, pp. 289\u2013300. ACM (1993)","DOI":"10.1145\/173682.165164"},{"issue":"3","key":"11_CR15","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1145\/78969.78972","volume":"12","author":"M.P. Herlihy","year":"1990","unstructured":"Herlihy, M.P., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst.\u00a012(3), 463\u2013492 (1990)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"11_CR16","unstructured":"Intel, Santa Clara, CA, USA. Intel 64 and IA-32 Architectures Software Developer\u2019s Manual Volume 3A: System Programming Guide, Part 1 (May 2012)"},{"issue":"4","key":"11_CR17","doi-asserted-by":"publisher","first-page":"596","DOI":"10.1145\/69575.69577","volume":"5","author":"C.B. Jones","year":"1983","unstructured":"Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM Trans. Prog. Lang. and Syst.\u00a05(4), 596\u2013619 (1983)","journal-title":"ACM Trans. Prog. Lang. and Syst."},{"key":"11_CR18","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/s00165-010-0156-1","volume":"23","author":"C.B. Jones","year":"2011","unstructured":"Jones, C.B., Pierce, K.: Elucidating concurrent algorithms via layers of abstraction and reification. Formal Aspects of Computing\u00a023, 289\u2013306 (2011)","journal-title":"Formal Aspects of Computing"},{"issue":"9","key":"11_CR19","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":"11_CR20","unstructured":"Morgan, C.: Programming from Specifications. Prentice-Hall (1990)"},{"key":"11_CR21","unstructured":"Moszkowski, B.C.: A complete axiomatization of Interval Temporal Logic with infinite time. In: LICS, pp. 241\u2013252 (2000)"},{"key":"11_CR22","unstructured":"AMD64 Architecture Programmer\u2019s Manual Volume 2: System Programming (2012), \n                  \n                    http:\/\/support.amd.com\/us\/Processor_TechDocs\/24593_APM_v2.pdf"},{"key":"11_CR23","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":"11_CR24","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"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2013"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-39718-9_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,20]],"date-time":"2019-05-20T01:55:37Z","timestamp":1558317337000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39718-9_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642397172","9783642397189"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39718-9_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}