{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,11,7]],"date-time":"2023-11-07T23:29:33Z","timestamp":1699399773996},"reference-count":25,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2017,9,26]],"date-time":"2017-09-26T00:00:00Z","timestamp":1506384000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Parallel Prog"],"published-print":{"date-parts":[[2018,12]]},"DOI":"10.1007\/s10766-017-0518-x","type":"journal-article","created":{"date-parts":[[2017,9,26]],"date-time":"2017-09-26T04:55:32Z","timestamp":1506401732000},"page":"1157-1183","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["GPS$$+$$+: Reasoning About Fences and Relaxed Atomics"],"prefix":"10.1007","volume":"46","author":[{"given":"Mengda","family":"He","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Viktor","family":"Vafeiadis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shengchao","family":"Qin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jo\u00e3o F.","family":"Ferreira","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,9,26]]},"reference":[{"key":"518_CR1","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 \u201911, pp. 55\u201366. ACM, New York (2011)","DOI":"10.1145\/1926385.1926394"},{"key":"518_CR2","doi-asserted-by":"crossref","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: International Conference on Theorem Proving in Higher Order Logics (TPHOLs \u201909), pp. 23\u201342 (2009)","DOI":"10.1007\/978-3-642-03359-9_2"},{"key":"518_CR3","doi-asserted-by":"crossref","unstructured":"da Rocha Pinto, P., Dinsdale-Young, T., Gardner, P.: TaDA: a logic for time and data abstraction. In: ECOOP, pp. 207\u2013231 (2014)","DOI":"10.1007\/978-3-662-44202-9_9"},{"key":"518_CR4","doi-asserted-by":"crossref","unstructured":"Dinsdale-Young, T., Dodds, M., Gardner, P., Parkinson, M.J., Vafeiadis, V.: Concurrent abstract predicates. In: ECOOP, pp. 504\u2013528 (2010)","DOI":"10.1007\/978-3-642-14107-2_24"},{"key":"518_CR5","doi-asserted-by":"crossref","unstructured":"Dinsdale-Young, T., Birkedal, L., Gardner, P., Parkinson, M.J., Yang, H.: Views: compositional reasoning for concurrent programs. In: ACM POPL, pp. 287\u2013300 (2013)","DOI":"10.1145\/2480359.2429104"},{"key":"518_CR6","doi-asserted-by":"crossref","unstructured":"Dodds, M., Feng, X., Parkinson, M., Vafeiadis, V.: Deny-guarantee reasoning. In: ESOP, pp. 363\u2013377 (2009)","DOI":"10.1007\/978-3-642-00590-9_26"},{"key":"518_CR7","doi-asserted-by":"crossref","unstructured":"Doko, M., Vafeiadis, V.: A Program Logic for C11 Memory Fences, pp. 413\u2013430. Springer, Berlin (2016)","DOI":"10.1007\/978-3-662-49122-5_20"},{"key":"518_CR8","doi-asserted-by":"crossref","unstructured":"Feng, X.: Local rely-guarantee Reasoning. In: ACM POPL, pp. 315\u2013327 (2009)","DOI":"10.1145\/1594834.1480922"},{"key":"518_CR9","unstructured":"He, M., Vafeiadis, V., Qin, S., Ferreira, J.F.: GPS+: Reasoning About Fences and Relaxed Atomics (Technical Report) (2017). http:\/\/pls.tees.ac.uk\/gpsp\/report.pdf, School of Computing, Teesside University"},{"key":"518_CR10","unstructured":"ISO\/IEC 9899:2011. Programming Language C (2011)"},{"key":"518_CR11","doi-asserted-by":"crossref","unstructured":"Jensen, J.B., Birkedal, L.: Fictional separation logic. In: ESOP, pp. 377\u2013396 (2012)","DOI":"10.1007\/978-3-642-28869-2_19"},{"key":"518_CR12","doi-asserted-by":"crossref","first-page":"596","DOI":"10.1145\/69575.69577","volume":"5","author":"CB Jones","year":"1983","unstructured":"Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM TOPLAS 5, 596\u2013619 (1983)","journal-title":"ACM TOPLAS"},{"key":"518_CR13","doi-asserted-by":"crossref","unstructured":"Jung, R., Swasey, D., Sieczkowski, F., Svendsen, K., Turon, A., Birkedal, L., Dreyer, D.: Iris: monoids and invariants as an orthogonal basis for concurrent reasoning. In: ACM POPL, pp. 637\u2013650 (2015)","DOI":"10.1145\/2775051.2676980"},{"issue":"9","key":"518_CR14","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."},{"key":"518_CR15","doi-asserted-by":"crossref","unstructured":"Leino, K.R., M\u00fcller, P., Smans, J.: Verification of concurrent programs with Chalice. In: Foundations of Security Analysis and Design V, pp. 195\u2013222 (2009)","DOI":"10.1007\/978-3-642-03829-7_7"},{"key":"518_CR16","doi-asserted-by":"crossref","unstructured":"Ley-Wild, R., Nanevski, A.: Subjective auxiliary state for coarse-grained concurrency. In: ACM POPL, pp. 561\u2013574 (2013)","DOI":"10.1145\/2480359.2429134"},{"key":"518_CR17","doi-asserted-by":"crossref","unstructured":"Manson, J., Pugh, W., Adve, S.V.: The Java memory model. In: ACM POPL, pp. 378\u2013391 (2005)","DOI":"10.1145\/1047659.1040336"},{"key":"518_CR18","doi-asserted-by":"crossref","unstructured":"Nanevski, A., Ley-Wild, R., Sergey, I., Delbianco, G.: Communicating state transition systems for fine-grained concurrent resources. In: ESOP, pp. 290\u2013310 (2014)","DOI":"10.1007\/978-3-642-54833-8_16"},{"issue":"1\u20133","key":"518_CR19","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1016\/j.tcs.2006.12.035","volume":"375","author":"PW O\u2019Hearn","year":"2007","unstructured":"O\u2019Hearn, P.W.: Resources, concurrency, and local reasoning. Theor. Comput. Sci. 375(1\u20133), 271\u2013307 (2007)","journal-title":"Theor. Comput. Sci."},{"key":"518_CR20","doi-asserted-by":"crossref","unstructured":"Svendsen, K., Birkedal, L.: Impredicative concurrent abstract predicates. In: ESOP, pp. 149\u2013168 (2014)","DOI":"10.1007\/978-3-642-54833-8_9"},{"key":"518_CR21","doi-asserted-by":"crossref","unstructured":"Tassarotti, J., Dreyer, D., Vafeiadis, V.: Verifying read-copy-update in a logic for weak memory. In: ACM PLDI, Portland, OR, USA (2015)","DOI":"10.1145\/2737924.2737992"},{"key":"518_CR22","doi-asserted-by":"crossref","unstructured":"Turon, A., Dreyer, D., Birkedal, L.: Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency. In: ICFP, pp. 377\u2013390 (2013)","DOI":"10.1145\/2544174.2500600"},{"key":"518_CR23","doi-asserted-by":"crossref","unstructured":"Turon, A., Vafeiadis, V., Dreyer, D.: GPS: Navigating weak memory with ghosts, protocols, and separation. In: ACM OOPSLA, pp. 691\u2013707 (2014)","DOI":"10.1145\/2714064.2660243"},{"key":"518_CR24","doi-asserted-by":"crossref","unstructured":"Vafeiadis, V., Parkinson, M.J.: A marriage of rely\/guarantee and separation logic. In: 18th International Conference on Concurrency Theory (CONCUR\u201907), volume 4703 of Lecture Notes in Computer Science, pp. 256\u2013271 (2007)","DOI":"10.1007\/978-3-540-74407-8_18"},{"key":"518_CR25","doi-asserted-by":"crossref","unstructured":"Vafeiadis, V., Narayan, C.: Relaxed separation logic: a program logic for C11 concurrency. In: ACM OOPSLA, pp. 867\u2013884 (2013)","DOI":"10.1145\/2544173.2509532"}],"container-title":["International Journal of Parallel Programming"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10766-017-0518-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10766-017-0518-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10766-017-0518-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,3]],"date-time":"2019-10-03T23:39:46Z","timestamp":1570145986000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10766-017-0518-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,9,26]]},"references-count":25,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2018,12]]}},"alternative-id":["518"],"URL":"https:\/\/doi.org\/10.1007\/s10766-017-0518-x","relation":{},"ISSN":["0885-7458","1573-7640"],"issn-type":[{"value":"0885-7458","type":"print"},{"value":"1573-7640","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,9,26]]}}}