{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:10:08Z","timestamp":1775873408855,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642314230","type":"print"},{"value":"9783642314247","type":"electronic"}],"license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"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":[[2012]]},"DOI":"10.1007\/978-3-642-31424-7_36","type":"book-chapter","created":{"date-parts":[[2012,6,21]],"date-time":"2012-06-21T10:26:49Z","timestamp":1340274409000},"page":"495-512","source":"Crossref","is-referenced-by-count":84,"title":["An Axiomatic Memory Model for POWER Multiprocessors"],"prefix":"10.1007","author":[{"given":"Sela","family":"Mador-Haim","sequence":"first","affiliation":[]},{"given":"Luc","family":"Maranget","sequence":"additional","affiliation":[]},{"given":"Susmit","family":"Sarkar","sequence":"additional","affiliation":[]},{"given":"Kayvan","family":"Memarian","sequence":"additional","affiliation":[]},{"given":"Jade","family":"Alglave","sequence":"additional","affiliation":[]},{"given":"Scott","family":"Owens","sequence":"additional","affiliation":[]},{"given":"Rajeev","family":"Alur","sequence":"additional","affiliation":[]},{"given":"Milo M. K.","family":"Martin","sequence":"additional","affiliation":[]},{"given":"Peter","family":"Sewell","sequence":"additional","affiliation":[]},{"given":"Derek","family":"Williams","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"36_CR1","doi-asserted-by":"crossref","unstructured":"Adir, A., Attiya, H., Shurek, G.: Information-flow models for shared memory with an application to the PowerPC architecture. IEEE Trans. Parallel Distrib. Syst.\u00a014(5) (2003)","DOI":"10.1109\/TPDS.2003.1199067"},{"key":"36_CR2","doi-asserted-by":"crossref","unstructured":"Alglave, J., Fox, A., Ishtiaq, S., Myreen, M.O., Sarkar, S., Sewell, P., Zappa Nardelli, F.: The semantics of Power and ARM multiprocessor machine code. In: Workshop on Declarative Aspects of Multicore Programming (January 2009)","DOI":"10.1145\/1481839.1481842"},{"key":"36_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-642-14295-6_25","volume-title":"Computer Aided Verification","author":"J. Alglave","year":"2010","unstructured":"Alglave, J., Maranget, L., Sarkar, S., Sewell, P.: Fences in Weak Memory Models. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 258\u2013272. Springer, Heidelberg (2010)"},{"key":"36_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-642-19835-9_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J. Alglave","year":"2011","unstructured":"Alglave, J., Maranget, L., Sarkar, S., Sewell, P.: Litmus: Running Tests against Hardware. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol.\u00a06605, pp. 41\u201344. Springer, Heidelberg (2011)"},{"key":"36_CR5","unstructured":"Corella, F., Stone, J.M., Barton, C.M.: A formal specification of the PowerPC shared memory architecture. Technical Report RC18638, IBM (1993)"},{"key":"36_CR6","unstructured":"Een, N., Sorensson, N.: Minisat - a SAT solver with conflict-clause minimization. In: International Conference on Theory and Applications of Satisfiability Testing (2005)"},{"key":"36_CR7","unstructured":"Gharachorloo, K.: Memory consistency models for shared-memory multiprocessors. WRL Research Report 95(9) (1995)"},{"key":"36_CR8","unstructured":"Intel. A formal specification of Intel Itanium processor family memory ordering (2002), \n                    \n                      http:\/\/developer.intel.com\/design\/itanium\/downloads\/251429.html"},{"key":"36_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/978-3-642-22863-6_27","volume-title":"Interactive Theorem Proving","author":"S. Owens","year":"2011","unstructured":"Owens, S., B\u00f6hm, P., Zappa Nardelli, F., Sewell, P.: Lem: A Lightweight Tool for Heavyweight Semantics. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol.\u00a06898, pp. 363\u2013369. Springer, Heidelberg (2011)"},{"key":"36_CR10","doi-asserted-by":"crossref","unstructured":"Stone, J.M., Fitzgerald, R.P.: Storage in the PowerPC. IEEE Micro\u00a015 (April 1995)","DOI":"10.1109\/40.372352"},{"key":"36_CR11","doi-asserted-by":"crossref","unstructured":"Sarkar, S., Memarian, K., Owens, S., Batty, M., Sewell, P., Maranget, L., Alglave, J., Williams, D.: Synchronising C\/C++ and POWER. In: Programming Language Design and Implementation (2012)","DOI":"10.1145\/2254064.2254102"},{"key":"36_CR12","doi-asserted-by":"crossref","unstructured":"Sarkar, S., Sewell, P., Alglave, J., Maranget, L., Williams, D.: Understanding POWER multiprocessors. In: Programming Language Design and Implementation (2011)","DOI":"10.1145\/1993498.1993520"},{"key":"36_CR13","unstructured":"An axiomatic memory model for Power multiprocessors \u2014 supplementary material, \n                    \n                      http:\/\/www.seas.upenn.edu\/~selama\/axiompower.html"},{"key":"36_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/978-3-540-39724-3_9","volume-title":"Correct Hardware Design and Verification Methods","author":"Y. Yang","year":"2003","unstructured":"Yang, Y., Gopalakrishnan, G.C., Lindstrom, G., Slind, K.: Analyzing the Intel Itanium Memory Ordering Rules Using Logic Programming and SAT. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol.\u00a02860, pp. 81\u201395. Springer, Heidelberg (2003)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-31424-7_36","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T20:48:01Z","timestamp":1558298881000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-31424-7_36"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642314230","9783642314247"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-31424-7_36","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}