{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T03:23:35Z","timestamp":1743132215497,"version":"3.40.3"},"publisher-location":"Cham","reference-count":14,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319296128"},{"type":"electronic","value":"9783319296135"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-29613-5_9","type":"book-chapter","created":{"date-parts":[[2016,1,28]],"date-time":"2016-01-28T02:47:34Z","timestamp":1453949254000},"page":"142-164","source":"Crossref","is-referenced-by-count":3,"title":["A Simpler Reduction Theorem for x86-TSO"],"prefix":"10.1007","author":[{"given":"Jonas","family":"Oberhauser","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"9_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1007\/978-3-662-46669-8_13","volume-title":"Programming Languages and Systems","author":"PA Abdulla","year":"2015","unstructured":"Abdulla, P.A., Atig, M.F., Ngo, T.-P.: The best of both worlds: trading efficiency and optimality in fence insertion for TSO. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 308\u2013332. Springer, Heidelberg (2015)"},{"key":"9_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"533","DOI":"10.1007\/978-3-642-37036-6_29","volume-title":"Programming Languages and Systems","author":"A Bouajjani","year":"2013","unstructured":"Bouajjani, A., Derevenetc, E., Meyer, R.: Checking and enforcing robustness against TSO. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 533\u2013553. Springer, Heidelberg (2013)"},{"key":"9_CR3","series-title":"Lecture Notes in Computer Science","first-page":"117","volume-title":"Verified Software: Theories, Tools and Experiments","author":"G Chen","year":"2014","unstructured":"Chen, G., Cohen, E., Kovalev, M.: Store buffer reduction with MMUs. In: Giannakopoulou, D., Kroening, D. (eds.) VSTTE 2014. LNCS, vol. 8471, pp. 117\u2013132. Springer, Heidelberg (2014)"},{"key":"9_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-03359-9_2","volume-title":"Theorem Proving in Higher Order Logics","author":"E Cohen","year":"2009","unstructured":"Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: a practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 23\u201342. Springer, Heidelberg (2009)"},{"key":"9_CR5","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. 6172, pp. 403\u2013418. Springer, Heidelberg (2010)"},{"key":"9_CR6","doi-asserted-by":"crossref","unstructured":"Crary, K., Sullivan, M.J.: A calculus for relaxed memory. In: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 623\u2013636. ACM (2015)","DOI":"10.1145\/2775051.2676984"},{"issue":"7","key":"9_CR7","doi-asserted-by":"publisher","first-page":"558","DOI":"10.1145\/359545.359563","volume":"21","author":"L Lamport","year":"1978","unstructured":"Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21(7), 558\u2013565 (1978). \n                    http:\/\/doi.acm.org\/10.1145\/359545.359563","journal-title":"Commun. ACM"},{"issue":"1","key":"9_CR8","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1145\/103727.103729","volume":"9","author":"JM Mellor-Crummey","year":"1991","unstructured":"Mellor-Crummey, J.M., Scott, M.L.: Algorithms for scalable synchronization on shared-memory multiprocessors. ACM Trans. Comput. Syst. (TOCS) 9(1), 21\u201365 (1991)","journal-title":"ACM Trans. Comput. Syst. (TOCS)"},{"key":"9_CR9","unstructured":"Oberhauser, J.: A simpler store buffer reduction theorem. Technical report, Saarland University (2015). \n                    http:\/\/www-wjp.cs.uni-saarland.de\/publikationen\/OberhauserSB.pdf"},{"key":"9_CR10","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. 6183, pp. 478\u2013503. Springer, Heidelberg (2010)"},{"key":"9_CR11","unstructured":"Paul, W.J., Baumann, C., Lutsyk, P., Schmaltz, S.: System Architecture as an Ordinary Engineering Discipline. Springer (in press)"},{"key":"9_CR12","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/978-1-4615-3604-8_2","volume-title":"Scalable Shared Memory Multiprocessors","author":"PS Sindhu","year":"1992","unstructured":"Sindhu, P.S., Frailong, J.M., Cekleov, M.: Formal specification of memory models. In: Dubois, M., Thakkar, S. (eds.) Scalable Shared Memory Multiprocessors, pp. 25\u201341. Springer, New York (1992). \n                    http:\/\/dx.doi.org\/10.1007\/978-1-4615-3604-8_2"},{"key":"9_CR13","doi-asserted-by":"publisher","first-page":"524","DOI":"10.1145\/2366231.2337220","volume":"40","author":"A Singh","year":"2012","unstructured":"Singh, A., Narayanasamy, S., Marino, D., Millstein, T., Musuvathi, M.: End-to-end sequential consistency. ACM SIGARCH Comput. Archit. News 40, 524\u2013535 (2012). IEEE Computer Society","journal-title":"ACM SIGARCH Comput. Archit. News"},{"key":"9_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-642-23702-7_14","volume-title":"Static Analysis","author":"V Vafeiadis","year":"2011","unstructured":"Vafeiadis, V., Zappa Nardelli, F.: Verifying fence elimination optimisations. In: Yahav, E. (ed.) Static Analysis. LNCS, vol. 6887, pp. 146\u2013162. Springer, Heidelberg (2011)"}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools, and Experiments"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-29613-5_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T07:47:18Z","timestamp":1559375238000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-29613-5_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319296128","9783319296135"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-29613-5_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}