{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:39:39Z","timestamp":1740123579371,"version":"3.37.3"},"reference-count":28,"publisher":"Springer Science and Business Media LLC","issue":"7","license":[{"start":{"date-parts":[[2019,3,26]],"date-time":"2019-03-26T00:00:00Z","timestamp":1553558400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2019,3,26]],"date-time":"2019-03-26T00:00:00Z","timestamp":1553558400000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/100010663","name":"H2020 European Research Council","doi-asserted-by":"publisher","award":["801091"],"award-info":[{"award-number":["801091"]}],"id":[{"id":"10.13039\/100010663","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100003329","name":"Ministerio de Econom\u00eda y Competitividad","doi-asserted-by":"publisher","award":["TIN2016-79637-P"],"award-info":[{"award-number":["TIN2016-79637-P"]}],"id":[{"id":"10.13039\/501100003329","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Supercomput"],"published-print":{"date-parts":[[2020,7]]},"DOI":"10.1007\/s11227-019-02827-4","type":"journal-article","created":{"date-parts":[[2019,3,26]],"date-time":"2019-03-26T20:23:26Z","timestamp":1553631806000},"page":"5057-5078","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Detecting semantic violations of lock-free data structures through C++ contracts"],"prefix":"10.1007","volume":"76","author":[{"given":"Javier","family":"L\u00f3pez-G\u00f3mez","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"del Rio Astorga","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Manuel F.","family":"Dolz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8539-5491","authenticated-orcid":false,"given":"Javier","family":"Fern\u00e1ndez","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J. Daniel","family":"Garc\u00eda","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,3,26]]},"reference":[{"issue":"4","key":"2827_CR1","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1002\/stvr.281","volume":"13","author":"C Artho","year":"2003","unstructured":"Artho C, Havelund K, Biere A (2003) High-level data races. Softw Test Verif Reliab 13(4):207\u2013227","journal-title":"Softw Test Verif Reliab"},{"key":"2827_CR2","unstructured":"Blechmann T (2011) Chapter 17. Boost.Lockfree. \nhttps:\/\/www.boost.org\/doc\/libs\/1_54_0\/doc\/html\/lockfree.html"},{"key":"2827_CR3","doi-asserted-by":"publisher","unstructured":"Borkar S (2010) The exascale challenge. In: 2010 international symposium on VLSI design automation and test (VLSI-DAT), pp 2\u20133. \nhttps:\/\/doi.org\/10.1109\/VDAT.2010.5496640","DOI":"10.1109\/VDAT.2010.5496640"},{"key":"2827_CR4","doi-asserted-by":"crossref","unstructured":"Boyapati C, Lee R, Rinard M (2002) Ownership types for safe programming: preventing data races and deadlocks. In: ACM SIGPLAN notices, vol 37, no. 11. ACM, pp 211\u2013230","DOI":"10.1145\/583854.582440"},{"key":"2827_CR5","doi-asserted-by":"publisher","unstructured":"Choi J, Dukhan M, Liu X, Vuduc R (2014) Algorithmic time, energy, and power on candidate HPC compute building blocks. In: 2014 IEEE 28th international on Parallel and distributed processing symposium, pp 447\u2013457. \nhttps:\/\/doi.org\/10.1109\/IPDPS.2014.54","DOI":"10.1109\/IPDPS.2014.54"},{"key":"2827_CR6","doi-asserted-by":"publisher","DOI":"10.1002\/cpe.4114","author":"MF Dolz","year":"2017","unstructured":"Dolz MF, Del Rio Astorga D, Fern\u00e1ndez J, Torquati M, Garc\u00eda JD, Garc\u00eda-Carballeira F, Danelutto M (2017) Enabling semantics to improve detection of data races and misuses of lock-free data structures. Concurr Comput Pract Exp. \nhttps:\/\/doi.org\/10.1002\/cpe.4114","journal-title":"Concurr Comput Pract Exp"},{"key":"2827_CR7","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1007\/11901433_16","volume-title":"Formal methods and software engineering","author":"B Dongol","year":"2006","unstructured":"Dongol B (2006) Formalising progress properties of non-blocking programs. In: Liu Z, He J (eds) Formal methods and software engineering. Springer, Berlin, pp 284\u2013303"},{"issue":"5","key":"2827_CR8","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1145\/1165389.945468","volume":"37","author":"D Engler","year":"2003","unstructured":"Engler D, Ashcraft K (2003) RacerX: effective, static detection of race conditions and deadlocks. SIGOPS Oper Syst Rev 37(5):237\u2013252. \nhttps:\/\/doi.org\/10.1145\/1165389.945468","journal-title":"SIGOPS Oper Syst Rev"},{"key":"2827_CR9","doi-asserted-by":"publisher","unstructured":"Giacomoni J, Moseley T, Vachharajani M (2008) Fastforward for efficient pipeline parallelism: a cache-optimized concurrent lock-free queue. In: Proceedings of the 13th ACM SIGPLAN symposium on principles and practice of parallel programming, PPoPP \u201908. ACM, NY, pp 43\u201352. \nhttps:\/\/doi.org\/10.1145\/1345206.1345215","DOI":"10.1145\/1345206.1345215"},{"key":"2827_CR10","unstructured":"Intel: Inspector XE 2017. \nhttps:\/\/software.intel.com\/en-us\/intel-inspector-xe"},{"issue":"1","key":"2827_CR11","doi-asserted-by":"publisher","first-page":"17:1","DOI":"10.1145\/3158105","volume":"2","author":"M Kokologiannakis","year":"2017","unstructured":"Kokologiannakis M, Lahav O, Sagonas K, Vafeiadis V (2017) Effective stateless model checking for c\/c++ concurrency. Proc ACM Program Lang 2(1):17:1\u201317:32. \nhttps:\/\/doi.org\/10.1145\/3158105","journal-title":"Proc ACM Program Lang"},{"issue":"7","key":"2827_CR12","doi-asserted-by":"publisher","first-page":"558","DOI":"10.1145\/359545.359563","volume":"21","author":"L Lamport","year":"1978","unstructured":"Lamport L (1978) Time, clocks, and the ordering of events in a distributed system. Commun ACM 21(7):558\u2013565. \nhttps:\/\/doi.org\/10.1145\/359545.359563","journal-title":"Commun ACM"},{"issue":"9","key":"2827_CR13","doi-asserted-by":"publisher","first-page":"690","DOI":"10.1109\/TC.1979.1675439","volume":"28","author":"L Lamport","year":"1979","unstructured":"Lamport L (1979) How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans Comput 28(9):690\u2013691. \nhttps:\/\/doi.org\/10.1109\/TC.1979.1675439","journal-title":"IEEE Trans Comput"},{"key":"2827_CR14","doi-asserted-by":"crossref","unstructured":"Lattner C, Adve V (2004) LLVM: A compilation framework for lifelong program analysis & transformation. In: Proceedings of the international symposium on code generation and optimization: feedback-directed and runtime optimization, CGO \u201904. IEEE Computer Society, Washington, p 75","DOI":"10.1109\/CGO.2004.1281665"},{"issue":"1","key":"2827_CR15","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1145\/3093333.3009857","volume":"52","author":"C Lidbury","year":"2017","unstructured":"Lidbury C, Donaldson AF (2017) Dynamic race detection for c++11. SIGPLAN Not 52(1):443\u2013457. \nhttps:\/\/doi.org\/10.1145\/3093333.3009857","journal-title":"SIGPLAN Not"},{"key":"2827_CR16","doi-asserted-by":"publisher","unstructured":"Lu S, Park S, Seo E, Zhou Y (2008) Learning from mistakes: a comprehensive study on real world concurrency bug characteristics. In: Proceedings of the 13th International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS XIII. ACM, New York, pp 329\u2013339. \nhttps:\/\/doi.org\/10.1145\/1346281.1346323","DOI":"10.1145\/1346281.1346323"},{"key":"2827_CR17","unstructured":"Michael MM, Scott ML (1996) Simple, fast, and practical non-blocking and blocking concurrent queue algorithms. In: Proceedings of the fifteenth annual ACM symposium on principles of distributed computing, PODC \u201996. ACM, New York, pp 267\u2013275"},{"issue":"10","key":"2827_CR18","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1145\/2544173.2509514","volume":"48","author":"B Norris","year":"2013","unstructured":"Norris B, Demsky B (2013) CDSchecker: checking concurrent data structures written with C\/C++ atomics. SIGPLAN Not 48(10):131\u2013150. \nhttps:\/\/doi.org\/10.1145\/2544173.2509514","journal-title":"SIGPLAN Not"},{"issue":"3","key":"2827_CR19","doi-asserted-by":"publisher","first-page":"10:1","DOI":"10.1145\/2806886","volume":"38","author":"B Norris","year":"2016","unstructured":"Norris B, Demsky B (2016) A practical approach for model checking C\/C++11 Code. ACM Trans Program Lang Syst 38(3):10:1\u201310:51. \nhttps:\/\/doi.org\/10.1145\/2806886","journal-title":"ACM Trans Program Lang Syst"},{"issue":"10","key":"2827_CR20","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1145\/966049.781528","volume":"38","author":"R O\u2019Callahan","year":"2003","unstructured":"O\u2019Callahan R, Choi JD (2003) Hybrid dynamic data race detection. SIGPLAN Not 38(10):167\u2013178","journal-title":"SIGPLAN Not"},{"issue":"8","key":"2827_CR21","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1145\/3155284.3018749","volume":"52","author":"P Ou","year":"2017","unstructured":"Ou P, Demsky B (2017) Checking concurrent data structures under the C\/C++11 memory model. SIGPLAN Not 52(8):45\u201359. \nhttps:\/\/doi.org\/10.1145\/3155284.3018749","journal-title":"SIGPLAN Not"},{"key":"2827_CR22","unstructured":"Reis GD, Garcia JD, Lakos J, Meredith A, Myers N, Stroustrup B (2018) Support for contract based programming in C++. ISO\/IEC JTC1\/SC22\/WG21 Working Paper, June 2018"},{"issue":"4","key":"2827_CR23","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1145\/265924.265927","volume":"15","author":"S Savage","year":"1997","unstructured":"Savage S, Burrows M, Nelson G, Sobalvarro P, Anderson T (1997) Eraser: a dynamic data race detector for multithreaded programs. ACM Trans Comput Syst (TOCS) 15(4):391\u2013411","journal-title":"ACM Trans Comput Syst (TOCS)"},{"key":"2827_CR24","doi-asserted-by":"crossref","unstructured":"Schweizer H, Besta M, Hoefler T (2015) Evaluating the cost of atomic operations on modern architectures. In: 24th International Conference on Parallel Architectures and Compilation (PACT\u201915). ACM","DOI":"10.1109\/PACT.2015.24"},{"key":"2827_CR25","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/978-3-642-29860-8_9","volume-title":"Runtime verification","author":"K Serebryany","year":"2012","unstructured":"Serebryany K, Potapenko A, Iskhodzhanov T, Vyukov D (2012) Dynamic race detection with LLVM compiler. In: Khurshid S, Sen K (eds) Runtime verification. Springer, Berlin, pp 110\u2013114"},{"issue":"3","key":"2827_CR26","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1145\/1147954.1147958","volume":"53","author":"O Shalev","year":"2006","unstructured":"Shalev O, Shavit N (2006) Split-ordered lists: lock-free extensible hash tables. J ACM 53(3):379\u2013405","journal-title":"J ACM"},{"key":"2827_CR27","doi-asserted-by":"crossref","unstructured":"Xie X, Xue J (2011) Acculock: accurate and efficient detection of data races. In: Proceedings of the 9th annual IEEE\/ACM international symposium on code generation and optimization, CGO \u201911. IEEE Computer Society, Washington, pp 201\u2013212","DOI":"10.1109\/CGO.2011.5764688"},{"key":"2827_CR28","doi-asserted-by":"publisher","unstructured":"Zhou P, Teodorescu R, Zhou Y (2007) Hard: Hardware-assisted lockset-based race detection. In: Proceedings of the 2007 IEEE 13th international symposium on high performance computer architecture, HPCA \u201907. IEEE Computer Society, Washington, pp 121\u2013132. \nhttps:\/\/doi.org\/10.1109\/HPCA.2007.346191","DOI":"10.1109\/HPCA.2007.346191"}],"container-title":["The Journal of Supercomputing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11227-019-02827-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11227-019-02827-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11227-019-02827-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,5]],"date-time":"2020-06-05T08:30:00Z","timestamp":1591345800000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11227-019-02827-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,3,26]]},"references-count":28,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2020,7]]}},"alternative-id":["2827"],"URL":"https:\/\/doi.org\/10.1007\/s11227-019-02827-4","relation":{},"ISSN":["0920-8542","1573-0484"],"issn-type":[{"type":"print","value":"0920-8542"},{"type":"electronic","value":"1573-0484"}],"subject":[],"published":{"date-parts":[[2019,3,26]]},"assertion":[{"value":"26 March 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}