{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T13:18:40Z","timestamp":1725887920595},"publisher-location":"Cham","reference-count":43,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319596464"},{"type":"electronic","value":"9783319596471"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-59647-1_11","type":"book-chapter","created":{"date-parts":[[2017,5,13]],"date-time":"2017-05-13T02:53:30Z","timestamp":1494644010000},"page":"133-148","source":"Crossref","is-referenced-by-count":0,"title":["Locality and Singularity for Store-Atomic Memory Models"],"prefix":"10.1007","author":[{"given":"Egor","family":"Derevenetc","sequence":"first","affiliation":[]},{"given":"Roland","family":"Meyer","sequence":"additional","affiliation":[]},{"given":"Sebastian","family":"Schweizer","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,5,14]]},"reference":[{"key":"11_CR1","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":"PA 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. 7214, pp. 204\u2013219. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-28756-5_15"},{"key":"11_CR2","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). doi: 10.1007\/978-3-662-46669-8_13"},{"key":"11_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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 \u2013 a static analysis approach to automatic fence insertion. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 508\u2013524. Springer, Cham (2014). doi: 10.1007\/978-3-319-08867-9_33"},{"key":"11_CR4","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). doi: 10.1007\/978-3-642-37036-6_28"},{"key":"11_CR5","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\u00a0concurrent\u00a0software. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 141\u2013157. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-39799-8_9"},{"key":"11_CR6","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: 10.1007\/978-3-642-22110-1_6"},{"key":"11_CR7","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. 6174, pp. 258\u2013272. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-14295-6_25"},{"issue":"2","key":"11_CR8","doi-asserted-by":"crossref","first-page":"7:1","DOI":"10.1145\/2627752","volume":"36","author":"J Alglave","year":"2014","unstructured":"Alglave, J., Maranget, L., Tautschnig, M.: Herding cats: modelling, simulation, testing, and data mining for weak memory. ACM TOPLAS 36(2), 7:1\u20137:74 (2014)","journal-title":"ACM TOPLAS"},{"key":"11_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1007\/978-3-642-28869-2_2","volume-title":"Programming Languages and Systems","author":"MF Atig","year":"2012","unstructured":"Atig, M.F., Bouajjani, A., Burckhardt, S., Musuvathi, M.: What\u2019s Decidable about Weak Memory Models? In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 26\u201346. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-28869-2_2"},{"key":"11_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-642-22110-1_9","volume-title":"Computer Aided Verification","author":"MF Atig","year":"2011","unstructured":"Atig, M.F., Bouajjani, A., Parlato, G.: Getting rid of store-buffers in TSO analysis. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 99\u2013115. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-22110-1_9"},{"key":"11_CR11","unstructured":"Bonachea, D.: GASNet specification, v1.1. Technical report UCB\/CSD-02-1207, University of California, Berkeley (2002)"},{"key":"11_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/978-3-662-46675-9_18","volume-title":"Fundamental Approaches to Software Engineering","author":"A Bouajjani","year":"2015","unstructured":"Bouajjani, A., Calin, G., Derevenetc, E., Meyer, R.: Lazy TSO reachability. In: Egyed, A., Schaefer, I. (eds.) FASE 2015. LNCS, vol. 9033, pp. 267\u2013282. Springer, Heidelberg (2015). doi: 10.1007\/978-3-662-46675-9_18"},{"key":"11_CR13","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: 10.1007\/978-3-642-37036-6_29"},{"key":"11_CR14","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. LNCS, vol. 6756, pp. 428\u2013440. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-22012-8_34"},{"key":"11_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"489","DOI":"10.1007\/11817963_45","volume-title":"Computer Aided Verification","author":"S Burckhardt","year":"2006","unstructured":"Burckhardt, S., Alur, R., Martin, M.M.K.: Bounded model checking of concurrent data types on relaxed memory models: a case study. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 489\u2013502. Springer, Heidelberg (2006). doi: 10.1007\/11817963_45"},{"key":"11_CR16","doi-asserted-by":"crossref","unstructured":"Burckhardt, S., Alur, R., Martin, M.: Checkfence: checking consistency of concurrent data types on relaxed memory models. In: PLDI, pp. 12\u201321. ACM (2007)","DOI":"10.1145\/1250734.1250737"},{"key":"11_CR17","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). doi: 10.1007\/978-3-540-70545-1_12"},{"key":"11_CR18","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. 6605, pp. 11\u201325. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-19835-9_3"},{"key":"11_CR19","unstructured":"Calin, G., Derevenetc, E., Majumdar, R., Meyer, R.: A theory of partitioned global address spaces. In: FSTTCS, pp. 127\u2013139 (2013)"},{"key":"11_CR20","doi-asserted-by":"crossref","unstructured":"Chapman, B., Curtis, T., Pophale, S., Poole, S., Kuehn, J., Koelbel, C., Smith, L.: Introducing OpenSHMEM: SHMEM for the PGAS community. In: PGAS, p. 2. ACM (2010)","DOI":"10.1145\/2020373.2020375"},{"key":"11_CR21","doi-asserted-by":"crossref","unstructured":"UPC Consortium. UPC language specification v1.2. Technical report (2005)","DOI":"10.2172\/862127"},{"key":"11_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"449","DOI":"10.1007\/978-3-662-46081-8_25","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A Dan","year":"2015","unstructured":"Dan, A., Meshman, Y., Vechev, M., Yahav, E.: Effective abstractions for verification under relaxed memory models. In: D\u2019Souza, D., Lal, A., Larsen, K.G. (eds.) VMCAI 2015. LNCS, vol. 8931, pp. 449\u2013466. Springer, Heidelberg (2015). doi: 10.1007\/978-3-662-46081-8_25"},{"key":"11_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/978-3-662-43951-7_14","volume-title":"Automata, Languages, and Programming","author":"E Derevenetc","year":"2014","unstructured":"Derevenetc, E., Meyer, R.: Robustness against power is PSPACE-complete. In: Esparza, J., Fraigniaud, P., Husfeldt, T., Koutsoupias, E. (eds.) ICALP 2014. LNCS, vol. 8573, pp. 158\u2013170. Springer, Heidelberg (2014). doi: 10.1007\/978-3-662-43951-7_14"},{"key":"11_CR24","unstructured":"Derevenetc, E., Meyer, R., Schweizer, S.: Locality and singularity for store-atomic memory models (2017). arXiv:1703.04603"},{"key":"11_CR25","doi-asserted-by":"crossref","unstructured":"Fang, X., Lee, J., Midkiff, S.: Automatic fence insertion for shared memory multiprocessing. In: SC, pp. 285\u2013294. ACM (2003)","DOI":"10.1145\/782814.782854"},{"key":"11_CR26","unstructured":"Global address space programming interface. http:\/\/www.gaspi.de\/"},{"key":"11_CR27","doi-asserted-by":"crossref","unstructured":"Hilfinger, P.N., Bonachea, D.O., Datta, K., Gay, D., Graham, S.L., Liblit, B.R., Pike, G., Su, J.Zh., Yelick, K.A.: Titanium language reference manual, version 2.19. Technical report UCB\/EECS-2005-15, UC Berkeley (2005)","DOI":"10.2172\/1511296"},{"key":"11_CR28","unstructured":"Kuperstein, M., Vechev, M., Yahav, E.: Automatic inference of memory fences. In: FMCAD, pp. 111\u2013119. IEEE (2010)"},{"key":"11_CR29","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\/1993498.1993521"},{"issue":"2","key":"11_CR30","doi-asserted-by":"crossref","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 43(2), 108\u2013123 (2012)","journal-title":"SIGACT News"},{"issue":"7","key":"11_CR31","doi-asserted-by":"crossref","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. CACM 21(7), 558\u2013565 (1978)","journal-title":"CACM"},{"issue":"9","key":"11_CR32","doi-asserted-by":"crossref","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. Comput. 28(9), 690\u2013691 (1979)","journal-title":"IEEE Trans. Comput."},{"issue":"3\u20134","key":"11_CR33","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1007\/s00450-009-0088-2","volume":"23","author":"R Machado","year":"2009","unstructured":"Machado, R., Lojewski, C.: The Fraunhofer virtual machine: a communication library and runtime system based on the RDMA model. Comput. Sci. Res. Dev. 23(3\u20134), 125\u2013132 (2009)","journal-title":"Comput. Sci. Res. Dev."},{"key":"11_CR34","doi-asserted-by":"crossref","unstructured":"Marino, D., Singh, A., Millstein, T., Musuvathi, M., Narayanasamy, S.: A case for an SC-preserving compiler. In: PLDI, pp. 199\u2013210. ACM (2011)","DOI":"10.1145\/1993498.1993522"},{"key":"11_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/978-3-319-10936-7_15","volume-title":"Static Analysis","author":"Y Meshman","year":"2014","unstructured":"Meshman, Y., Dan, A., Vechev, M., Yahav, E.: Synthesis of memory fences via refinement propagation. In: M\u00fcller-Olm, M., Seidl, H. (eds.) SAS 2014. LNCS, vol. 8723, pp. 237\u2013252. Springer, Cham (2014). doi: 10.1007\/978-3-319-10936-7_15"},{"key":"11_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"533","DOI":"10.1007\/BFb0097937","volume-title":"Parallel and Distributed Processing","author":"J Nieplocha","year":"1999","unstructured":"Nieplocha, J., Carpenter, B.: ARMCI: a portable remote memory copy library for distributed array libraries and compiler run-time systems. In: Rolim, J., et al. (eds.) IPPS 1999. LNCS, vol. 1586, pp. 533\u2013546. Springer, Heidelberg (1999). doi: 10.1007\/BFb0097937"},{"key":"11_CR37","doi-asserted-by":"crossref","unstructured":"Numrich, R.W., Reid, J.: Co-array Fortran for parallel programming. In: ACM Sigplan Fortran Forum, vol. 17, pp. 1\u201331. ACM (1998)","DOI":"10.1145\/289918.289920"},{"key":"11_CR38","doi-asserted-by":"crossref","unstructured":"Sarkar, S., Sewell, P., Alglave, J., Maranget, L., Williams, D.: Understanding POWER multiprocessors. In: PLDI, pp. 175\u2013186. ACM (2011)","DOI":"10.1145\/1993498.1993520"},{"key":"11_CR39","doi-asserted-by":"crossref","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 53, 89\u201397 (2010)","journal-title":"CACM"},{"issue":"2","key":"11_CR40","doi-asserted-by":"crossref","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 10(2), 282\u2013312 (1988)","journal-title":"ACM TOPLAS"},{"key":"11_CR41","doi-asserted-by":"crossref","unstructured":"Singh, A., Narayanasamy, S., Marino, D., Millstein, T., Musuvathi, M.: End-to-end sequential consistency. In: ISCA, pp. 524\u2013535. IEEE (2012)","DOI":"10.1109\/ISCA.2012.6237045"},{"key":"11_CR42","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. 6887, pp. 146\u2013162. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-23702-7_14"},{"volume-title":"The SPARC Architecture Manual Version 9","year":"1994","key":"11_CR43","unstructured":"Weaver, D., Germond, T. (eds.): The SPARC Architecture Manual Version 9. PTR Prentice Hall, Upper Saddle River (1994)"}],"container-title":["Lecture Notes in Computer Science","Networked Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-59647-1_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,24]],"date-time":"2019-09-24T15:58:02Z","timestamp":1569340682000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-59647-1_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319596464","9783319596471"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-59647-1_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}