{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:46:11Z","timestamp":1742913971429,"version":"3.40.3"},"publisher-location":"Cham","reference-count":25,"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_10","type":"book-chapter","created":{"date-parts":[[2016,1,28]],"date-time":"2016-01-28T02:47:34Z","timestamp":1453949254000},"page":"165-182","source":"Crossref","is-referenced-by-count":0,"title":["Moving Around: Lipton\u2019s Reduction for TSO"],"prefix":"10.1007","author":[{"given":"Ali","family":"Sezgin","sequence":"first","affiliation":[]},{"given":"Serdar","family":"Tasiran","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"10_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"508","DOI":"10.1007\/978-3-319-08867-9_33","volume-title":"Computer Aided Verification","author":"J Alglave","year":"2014","unstructured":"Alglave, J., Kroening, D., Nimal, V., Poetzl, D.: Don\u2019t sit on the fence. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 508\u2013524. Springer, Heidelberg (2014)"},{"key":"10_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/978-3-642-37036-6_28","volume-title":"Programming Languages and Systems","author":"J Alglave","year":"2013","unstructured":"Alglave, J., Kroening, D., Nimal, V., Tautschnig, M.: Software verification for weak memory via program transformation. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 512\u2013532. Springer, Heidelberg (2013)"},{"key":"10_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/978-3-642-39799-8_9","volume-title":"Computer Aided Verification","author":"J Alglave","year":"2013","unstructured":"Alglave, J., Kroening, D., Tautschnig, M.: Partial orders for efficient bounded model checking of concurrent software. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 141\u2013157. Springer, Heidelberg (2013)"},{"key":"10_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/978-3-642-22110-1_6","volume-title":"Computer Aided Verification","author":"J Alglave","year":"2011","unstructured":"Alglave, J., Maranget, L.: Stability in weak memory models. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 50\u201366. Springer, Heidelberg (2011)"},{"doi-asserted-by":"crossref","unstructured":"Batty, M., Dodds, M., Gotsman, A.: Library abstraction for c\/c++ concurrency. In: Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2013, pp. 235\u2013248. ACM (2013)","key":"10_CR5","DOI":"10.1145\/2480359.2429099"},{"doi-asserted-by":"crossref","unstructured":"Batty, M., Owens, S., Sarkar, S., Sewell, P., Weber, T.: Mathematizing c++ concurrency. In: Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, pp. 55\u201366. ACM (2011)","key":"10_CR6","DOI":"10.1145\/1926385.1926394"},{"doi-asserted-by":"crossref","unstructured":"Boehm, H.J. and Adve, S.V.: Foundations of the c++ concurrency memory model. In: Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2008, pp. 68\u201378. ACM (2008)","key":"10_CR7","DOI":"10.1145\/1375581.1375591"},{"key":"10_CR8","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)"},{"doi-asserted-by":"crossref","unstructured":"Burckhardt, S., Alur, R., Martin, M.M.: Checkfence: Checking consistency of concurrent data types on relaxed memory models. In: Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2007, pp. 12\u201321. ACM (2007)","key":"10_CR9","DOI":"10.1145\/1250734.1250737"},{"key":"10_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-540-70545-1_12","volume-title":"Computer Aided Verification","author":"S Burckhardt","year":"2008","unstructured":"Burckhardt, S., Musuvathi, M.: Effective program verification for relaxed memory models. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 107\u2013120. Springer, Heidelberg (2008)"},{"key":"10_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-642-38856-9_7","volume-title":"Static Analysis","author":"AM Dan","year":"2013","unstructured":"Dan, A.M., Meshman, Y., Vechev, M., Yahav, E.: Predicate abstraction for relaxed memory models. In: Logozzo, F., F\u00e4hndrich, M. (eds.) Static Analysis. LNCS, vol. 7935, pp. 84\u2013104. Springer, Heidelberg (2013)"},{"doi-asserted-by":"crossref","unstructured":"Elmas, T., Qadeer, S., Tasiran, S.: A calculus of atomic actions. In: Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, pp. 2\u201315. ACM (2009)","key":"10_CR12","DOI":"10.1145\/1480881.1480885"},{"key":"10_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/978-3-642-11957-6_15","volume-title":"Programming Languages and Systems","author":"R Ferreira","year":"2010","unstructured":"Ferreira, R., Feng, X., Shao, Z.: Parameterized memory models and concurrent separation logic. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 267\u2013286. Springer, Heidelberg (2010)"},{"key":"10_CR14","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. 7611, pp. 31\u201345. Springer, Heidelberg (2012)"},{"issue":"2","key":"10_CR15","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1145\/2601339","volume":"36","author":"S Jagannathan","year":"2014","unstructured":"Jagannathan, S., Laporte, V., Petri, G., Pichardie, D., Vitek, J.: Atomicity refinement for verified compilation. ACM Trans. Program. Lang. Syst. 36(2), 6 (2014)","journal-title":"ACM Trans. Program. Lang. Syst."},{"doi-asserted-by":"crossref","unstructured":"Koskinen, E., Parkinson, M., Herlihy, M.: Coarse-grained transactions. In: Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, pp. 19\u201330. ACM (2010)","key":"10_CR16","DOI":"10.1145\/1706299.1706304"},{"issue":"12","key":"10_CR17","doi-asserted-by":"publisher","first-page":"717","DOI":"10.1145\/361227.361234","volume":"18","author":"RJ Lipton","year":"1975","unstructured":"Lipton, R.J.: Reduction: a method of proving properties of parallel programs. ACM Commun. 18(12), 717\u2013721 (1975)","journal-title":"ACM Commun."},{"key":"10_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/978-3-642-31424-7_36","volume-title":"Computer Aided Verification","author":"S Mador-Haim","year":"2012","unstructured":"Mador-Haim, S., et al.: An axiomatic memory model for POWER multiprocessors. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 495\u2013512. Springer, Heidelberg (2012)"},{"doi-asserted-by":"crossref","unstructured":"Norris, B., Demsky, B.: CDSchecker: Checking concurrent data structures written with c\/c++ atomics. In: Proceedings of the ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA 2013, pp. 131\u2013150. ACM (2013)","key":"10_CR19","DOI":"10.1145\/2544173.2509514"},{"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. 6183, pp. 478\u2013503. Springer, Heidelberg (2010)"},{"key":"10_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/978-3-642-15057-9_4","volume-title":"Verified Software: Theories, Tools, Experiments","author":"T Ridge","year":"2010","unstructured":"Ridge, T.: A rely-guarantee proof system for x86-TSO. In: Leavens, G.T., O\u2019Hearn, P., Rajamani, S.K. (eds.) VSTTE 2010. LNCS, vol. 6217, pp. 55\u201370. Springer, Heidelberg (2010)"},{"issue":"6","key":"10_CR22","doi-asserted-by":"publisher","first-page":"942","DOI":"10.1145\/267959.269969","volume":"19","author":"MC Rinard","year":"1997","unstructured":"Rinard, M.C., Diniz, P.C.: Commutativity analysis: A new analysis technique for parallelizing compilers. ACM Trans. Program. Lang. Syst. 19(6), 942\u2013991 (1997)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"7","key":"10_CR23","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. ACM Commun. 53(7), 89\u201397 (2010)","journal-title":"ACM Commun."},{"issue":"2","key":"10_CR24","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1145\/42190.42277","volume":"10","author":"D Shasha","year":"1988","unstructured":"Shasha, D., Snir, M.: Efficient and correct execution of parallel programs that share memory. ACM Trans. Program. Lang. Syst. 10(2), 282\u2013312 (1988)","journal-title":"ACM Trans. Program. Lang. Syst."},{"doi-asserted-by":"crossref","unstructured":"Vafeiadis, V., Narayan, C.: Relaxed separation logic: A program logic for c11 concurrency. In: Proceedings of the ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA 2013, pp. 867\u2013884. ACM (2013)","key":"10_CR25","DOI":"10.1145\/2544173.2509532"}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools, and Experiments"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-29613-5_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,8]],"date-time":"2020-01-08T13:52:05Z","timestamp":1578491525000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-29613-5_10"}},"subtitle":["(Regular Submission)"],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319296128","9783319296135"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-29613-5_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}