{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,18]],"date-time":"2026-09-18T16:21:14Z","timestamp":1789748474454,"version":"4.0.1"},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642370359","type":"print"},{"value":"9783642370366","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-37036-6_29","type":"book-chapter","created":{"date-parts":[[2013,2,18]],"date-time":"2013-02-18T19:35:55Z","timestamp":1361216155000},"page":"533-553","source":"Crossref","is-referenced-by-count":94,"title":["Checking and Enforcing Robustness against TSO"],"prefix":"10.1007","author":[{"given":"Ahmed","family":"Bouajjani","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Egor","family":"Derevenetc","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Roland","family":"Meyer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"29_CR1","unstructured":"Trencher: a tool for checking and enforcing robustness against TSO, http:\/\/concurrency.cs.uni-kl.de\/trencher.html"},{"key":"29_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1007\/978-3-642-28756-5_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P.A. Abdulla","year":"2012","unstructured":"Abdulla, P.A., Atig, M.F., Chen, Y.-F., Leonardsson, C., Rezine, A.: Counter-Example Guided Fence Insertion under TSO. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol.\u00a07214, pp. 204\u2013219. Springer, Heidelberg (2012)"},{"issue":"6","key":"29_CR3","doi-asserted-by":"publisher","first-page":"613","DOI":"10.1109\/71.242161","volume":"4","author":"S.V. Adve","year":"1993","unstructured":"Adve, S.V., Hill, M.D.: A unified formalization of four shared-memory models. IEEE Trans. Parallel Distrib. Syst.\u00a04(6), 613\u2013624 (1993)","journal-title":"IEEE Trans. Parallel Distrib. Syst."},{"key":"29_CR4","unstructured":"Alglave, J.: A Shared Memory Poetics. PhD thesis, University Paris 7 (2010)"},{"key":"29_CR5","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.\u00a06806, pp. 50\u201366. Springer, Heidelberg (2011)"},{"key":"29_CR6","doi-asserted-by":"crossref","unstructured":"Alur, R., McMillan, K., Peled, D.: Model-Checking of Correctness Conditions for Concurrent Objects. In: LICS, pp. 219\u2013228. IEEE Computer Society Press (1996)","DOI":"10.1109\/LICS.1996.561322"},{"key":"29_CR7","doi-asserted-by":"crossref","unstructured":"Atig, M.F., Bouajjani, A., Burckhardt, S., Musuvathi, M.: On the Verification Problem for Weak Memory Models. In: POPL, pp. 7\u201318. ACM (2010)","DOI":"10.1145\/1707801.1706303"},{"key":"29_CR8","unstructured":"Bouajjani, A., Derevenetc, E., Meyer, R.: Checking and enforcing robustness against TSO. CoRR, abs\/1208.6152 (2012), http:\/\/arxiv.org\/abs\/1208.6152"},{"key":"29_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"428","DOI":"10.1007\/978-3-642-22012-8_34","volume-title":"Automata, Languages and Programming","author":"A. Bouajjani","year":"2011","unstructured":"Bouajjani, A., Meyer, R., M\u00f6hlmann, E.: Deciding Robustness against Total Store Ordering. In: Aceto, L., Henzinger, M., Sgall, J. (eds.) ICALP 2011, Part II. LNCS, vol.\u00a06756, pp. 428\u2013440. Springer, Heidelberg (2011)"},{"key":"29_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.\u00a05123, pp. 107\u2013120. Springer, Heidelberg (2008)"},{"key":"29_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1007\/978-3-642-19835-9_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J. Burnim","year":"2011","unstructured":"Burnim, J., Sen, K., Stergiou, C.: Sound and Complete Monitoring of Sequential Consistency for Relaxed Memory Models. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol.\u00a06605, pp. 11\u201325. Springer, Heidelberg (2011)"},{"key":"29_CR12","unstructured":"Dice, D.: A race in locksupport park() arising from weak memory models (November 2009), https:\/\/blogs.oracle.com\/dave\/entry\/a_race_in_locksupport_park"},{"issue":"5","key":"29_CR13","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1145\/277652.277725","volume":"33","author":"M. Frigo","year":"1998","unstructured":"Frigo, M., Leiserson, C.E., Randall, K.H.: The implementation of the Cilk-5 multithreaded language. SIGPLAN Not.\u00a033(5), 212\u2013223 (1998)","journal-title":"SIGPLAN Not."},{"key":"29_CR14","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1145\/146637.146681","volume":"39","author":"S.M. German","year":"1992","unstructured":"German, S.M., Sistla, P.A.: Reasoning about systems with many processes. JACM\u00a039, 675\u2013735 (1992)","journal-title":"JACM"},{"issue":"4","key":"29_CR15","doi-asserted-by":"publisher","first-page":"1208","DOI":"10.1137\/S0097539794279614","volume":"26","author":"P.B. Gibbons","year":"1997","unstructured":"Gibbons, P.B., Korach, E.: Testing shared memories. SIAM J. Comp.\u00a026(4), 1208\u20131244 (1997)","journal-title":"SIAM J. Comp."},{"key":"29_CR16","unstructured":"Herlihy, M., Shavit, N.: The Art of Multiprocessor Programming. MKP (2008)"},{"key":"29_CR17","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker SPIN. IEEE Tr. Soft. Eng.\u00a023, 279\u2013295 (1997)","journal-title":"IEEE Tr. Soft. Eng."},{"key":"29_CR18","doi-asserted-by":"crossref","unstructured":"Kopetz, H., Reisinger, J.: The Non-Blocking Write Protocol NBW: A Solution to a Real-Time Synchronisation Problem. In: IEEE Real-Time Systems Symposium, pp. 131\u2013137. IEEE Computer Society Press (1993)","DOI":"10.1109\/REAL.1993.393507"},{"key":"29_CR19","doi-asserted-by":"crossref","unstructured":"Kuperstein, M., Vechev, M.T., Yahav, E.: Partial-Coherence Abstractions for Relaxed Memory Models. In: PLDI, pp. 187\u2013198. ACM (2011)","DOI":"10.1145\/1993316.1993521"},{"issue":"2","key":"29_CR20","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1145\/2261417.2261438","volume":"43","author":"M. Kuperstein","year":"2012","unstructured":"Kuperstein, M., Vechev, M.T., Yahav, E.: Automatic inference of memory fences. SIGACT News\u00a043(2), 108\u2013123 (2012)","journal-title":"SIGACT News"},{"issue":"9","key":"29_CR21","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. Comp.\u00a028(9), 690\u2013691 (1979)","journal-title":"IEEE Trans. Comp."},{"key":"29_CR22","doi-asserted-by":"crossref","unstructured":"Lamport, L.: A fast mutual exclusion algorithm. ACM Tr. Comp. Sys. 5(1) (1987)","DOI":"10.1145\/7351.7352"},{"key":"29_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1007\/978-3-642-22306-8_10","volume-title":"Model Checking Software","author":"A. Linden","year":"2011","unstructured":"Linden, A., Wolper, P.: A Verification-Based Approach to Memory Fence Insertion in Relaxed Memory Systems. In: Groce, A., Musuvathi, M. (eds.) SPIN 2011. LNCS, vol.\u00a06823, pp. 144\u2013160. Springer, Heidelberg (2011)"},{"key":"29_CR24","unstructured":"Lipton, R.: The reachability problem requires exponential space. Technical Report\u00a062, Yale University (1976)"},{"key":"29_CR25","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":"29_CR26","doi-asserted-by":"crossref","unstructured":"Owens, S., Sarkar, S., Sewell, P.: A better x86 memory model: x86-TSO (extended version). Technical Report CL-TR-745, University of Cambridge (2009)","DOI":"10.1007\/978-3-642-03359-9_27"},{"key":"29_CR27","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1016\/0304-3975(78)90036-1","volume":"6","author":"C. Rackoff","year":"1978","unstructured":"Rackoff, C.: The covering and boundedness problems for vector addition systems. Theor. Comp. Sci.\u00a06, 223\u2013231 (1978)","journal-title":"Theor. Comp. Sci."},{"key":"29_CR28","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. CACM\u00a053, 89\u201397 (2010)","journal-title":"CACM"},{"issue":"2","key":"29_CR29","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 TOPLAS\u00a010(2), 282\u2013312 (1988)","journal-title":"ACM TOPLAS"},{"key":"29_CR30","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.) SAS 2011. LNCS, vol.\u00a06887, pp. 146\u2013162. Springer, Heidelberg (2011)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-37036-6_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,29]],"date-time":"2025-04-29T21:32:38Z","timestamp":1745962358000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-37036-6_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642370359","9783642370366"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-37036-6_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}