{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,16]],"date-time":"2026-03-16T10:06:41Z","timestamp":1773655601650,"version":"3.50.1"},"reference-count":27,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2021,2,14]],"date-time":"2021-02-14T00:00:00Z","timestamp":1613260800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,2,14]],"date-time":"2021-02-14T00:00:00Z","timestamp":1613260800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2021,10]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>A commonly used approach to develop deterministic parallel programs is to augment a sequential program with compiler directives that indicate which program blocks may potentially be executed in parallel. This paper develops a verification technique to reason about such compiler directives, in particular to show that they do not change the behaviour of the program. Moreover, the verification technique is tool-supported and can be combined with proving functional correctness of the program. To develop our verification technique, we propose a simple intermediate representation (syntax and semantics) that captures the main forms of deterministic parallel programs. This language distinguishes three kinds of basic blocks: parallel, vectorised and sequential blocks, which can be composed using three different composition operators: sequential, parallel and fusion composition. We show how a widely used subset of OpenMP can be encoded into this intermediate representation. Our verification technique builds on the notion of iteration contract to specify the behaviour of basic blocks; we show that if iteration contracts are manually specified for single blocks, then that is sufficient to automatically reason about data race freedom of the composed program. Moreover, we also show that it is sufficient to establish functional correctness on a linearised version of the original program to conclude functional correctness of the parallel program. Finally, we exemplify our approach on an example OpenMP program, and we discuss how tool support is provided.<\/jats:p>","DOI":"10.1007\/s10009-020-00601-z","type":"journal-article","created":{"date-parts":[[2021,2,18]],"date-time":"2021-02-18T00:13:40Z","timestamp":1613607220000},"page":"741-763","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Correct program parallelisations"],"prefix":"10.1007","volume":"23","author":[{"given":"S.","family":"Blom","sequence":"first","affiliation":[]},{"given":"S.","family":"Darabi","sequence":"additional","affiliation":[]},{"given":"M.","family":"Huisman","sequence":"additional","affiliation":[]},{"given":"M.","family":"Safari","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,2,14]]},"reference":[{"key":"601_CR1","doi-asserted-by":"crossref","unstructured":"Amighi, A., Haack, C., Huisman, M., Hurlin, C.: Permission-based separation logic for multithreaded Java programs. LMCS 11(1), (2015)","DOI":"10.2168\/LMCS-11(1:2)2015"},{"key":"601_CR2","unstructured":"Aviram, A., Ford, B.: Deterministic OpenMP for Race-free Parallelism. In HotPar\u201911 (2011)"},{"key":"601_CR3","doi-asserted-by":"crossref","unstructured":"Barthe, G., Crespo, J.M., Gulwani, S., Kunz, C., Marron, M.: From relational verification to SIMD loop synthesis. In: PPoPP, pp. 123\u2013134 (2013)","DOI":"10.1145\/2517327.2442529"},{"issue":"4","key":"601_CR4","doi-asserted-by":"publisher","first-page":"414","DOI":"10.1016\/j.jpdc.2004.11.010","volume":"65","author":"MJ Berger","year":"2005","unstructured":"Berger, M.J., Aftosmis, M.J., Marshall, D.D., Murman, S.M.: Performance of a new CFD flow solver using a hybrid programming paradigm. J. Parallel Distrib. Comput. 65(4), 414\u2013423 (2005)","journal-title":"J. Parallel Distrib. Comput."},{"key":"601_CR5","doi-asserted-by":"crossref","unstructured":"Blom, S., Darabi, S., Huisman, M.: Verification of loop parallelisations. In: Egyed, A.,\u00a0Schaefer, I. (eds.) FASE, Volume 9033 of LNCS. Springer, pp. 202\u2013217 (2015)","DOI":"10.1007\/978-3-662-46675-9_14"},{"key":"601_CR6","doi-asserted-by":"crossref","unstructured":"Bornat, R., Calcagno, C., O\u2019Hearn, P., Parkinson, M.: Permission accounting in separation logic. In: POPL, pp. 259\u2013270 (2005)","DOI":"10.1145\/1047659.1040327"},{"key":"601_CR7","doi-asserted-by":"crossref","unstructured":"Botincan, M., Dodds, M., Jagannathan, S.: Resource-sensitive synchronization inference by abduction. In:\u00a0Field, J.,\u00a0Hicks, M. (eds.) Principles of Programming Languages (POPL 2012), pp. 309\u2013322 (2012)","DOI":"10.1145\/2103621.2103694"},{"key":"601_CR8","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2491522.2491525","volume":"35","author":"M Botin\u010dan","year":"2013","unstructured":"Botin\u010dan, M., Dodds, M., Jagannathan, S.: Proof-directed parallelization synthesis by separation logic. ACM Trans. Program. Lang. Syst. 35, 1\u201360 (2013)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"601_CR9","doi-asserted-by":"crossref","unstructured":"Boyland, J.: Checking interference with fractional permissions. In: SAS, Volume 2694 of LNCS. Springer, pp. 55\u201372 (2003)","DOI":"10.1007\/3-540-44898-5_4"},{"key":"601_CR10","doi-asserted-by":"crossref","unstructured":"Bubel, R., H\u00e4hnle, R., Heydari Tabar, A.: A program logic for dependence analysis. In: Ahrendt, W., Tapia Tarifa, S.L. (eds.) Integrated Formal Methods. Springer International Publishing, Cham, pp. 83\u2013100 (2019)","DOI":"10.1007\/978-3-030-34968-4_5"},{"key":"601_CR11","doi-asserted-by":"crossref","unstructured":"Che, S., Boyer, M., Meng, J., Tarjan, D., Sheaffer, J.W., Lee, S.-H., Skadron, K.: Rodinia: A benchmark suite for heterogeneous computing. In Workload Characterization. IISWC 2009, pp. 44\u201354 (2009)","DOI":"10.1109\/IISWC.2009.5306797"},{"key":"601_CR12","doi-asserted-by":"crossref","unstructured":"Darabi, S., Blom, S., Huisman, M.: A verification technique for deterministic parallel programs. In: Barrett, C.,\u00a0Davies, M.,\u00a0Kahsai, T. (eds.) NASA Formal Methods (NFM), Volume 10227 of LNCS, pp. 247\u2013264 (2017)","DOI":"10.1007\/978-3-319-57288-8_17"},{"key":"601_CR13","doi-asserted-by":"crossref","unstructured":"Dodds, M., Jagannathan, S., Parkinson, M.J.: Modular reasoning for deterministic parallelism. In ACM SIGPLAN Notices, pp. 259\u2013270 (2011)","DOI":"10.1145\/1925844.1926416"},{"issue":"2","key":"601_CR14","doi-asserted-by":"publisher","first-page":"4:1","DOI":"10.1145\/2818638","volume":"38","author":"M Dodds","year":"2016","unstructured":"Dodds, M., Jagannathan, S., Parkinson, M.J., Svendsen, K., Birkedal, L.: Verifying custom synchronization constructs using higher-order separation logic. ACM Trans. Program. Lang. Syst. 38(2), 4:1\u20134:72 (2016)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"601_CR15","doi-asserted-by":"crossref","unstructured":"Haack, C., Huisman, M., Hurlin, C.: Reasoning about Java\u2019s reentrant locks. In:\u00a0Ramalingam, G., (ed.) Programming Languages and Systems, 6th Asian Symposium, APLAS 2008, Bangalore, India, December 9\u201311, 2008. Proceedings, Volume 5356 of LNCS. Springer, pp. 171\u2013187 (2008)","DOI":"10.1007\/978-3-540-89330-1_13"},{"key":"601_CR16","unstructured":"Hurlin, C.: Specification and Verification of Multithreaded Object-Oriented Programs with Separation Logic. PhD thesis, Universit\u00e9 Nice Sophia Antipolis (2009)"},{"key":"601_CR17","unstructured":"Jin, H.-Q., Frumkin, M., Yan, J.: The OpenMP Implementation of NAS Parallel Benchmarks and its Performance (1999)"},{"key":"601_CR18","unstructured":"Leavens, G., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D.R., M\u00fcller, P., Kiniry, J., Chalin, P.: JML Reference Manual (2007). Dept. of Computer Science, Iowa State University. http:\/\/www.jmlspecs.org"},{"key":"601_CR19","doi-asserted-by":"crossref","unstructured":"M\u00fcller, P., Schwerhoff, M., Summers, A.: Viper\u2014a verification infrastructure for permission-based reasoning. In VMCAI (2016)","DOI":"10.1007\/978-3-662-49122-5_2"},{"key":"601_CR20","unstructured":"OpenMP architecture review board, OpenMP API specification for parallel programming. Last accessed 18 Oct 2016. http:\/\/openmp.org\/wp\/"},{"key":"601_CR21","unstructured":"LLNL OpenMP Benchmarks. Last accessed 28 Nov 2016. https:\/\/asc.llnl.gov\/CORAL-benchmarks\/"},{"key":"601_CR22","doi-asserted-by":"crossref","unstructured":"Parkinson, M., Summers, A.: The relationship between separation logic and implicit dynamic frames. In\u00a0Barthe, G. (ed.) Programming Languages and Systems\u201420th European Symposium on Programming, ESOP 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbr\u00fccken, Germany, March 26\u2013April 3, 2011. Proceedings, volume 6602 of LNCS. Springer, pp. 439\u2013458 (2011)","DOI":"10.1007\/978-3-642-19718-5_23"},{"key":"601_CR23","doi-asserted-by":"crossref","unstructured":"Raychev, V., Vechev, M., Yahav, E.: Automatic synthesis of deterministic concurrency. In: Static Analysis\u201420th International Symposium, SAS 2013, Seattle, WA, USA, June 20\u201322, 2013. Proceedings. Springer, pp. 283\u2013303 (2013)","DOI":"10.1007\/978-3-642-38856-9_16"},{"key":"601_CR24","doi-asserted-by":"crossref","unstructured":"Salamanca, J., Mattos, L., Araujo, G.: Loop-carried dependence verification in OpenMP. In: International Workshop on OpenMP 2014, pp. 87\u2013102 (2014)","DOI":"10.1007\/978-3-319-11454-5_7"},{"issue":"1","key":"601_CR25","doi-asserted-by":"publisher","first-page":"2:1","DOI":"10.1145\/2160910.2160911","volume":"34","author":"J Smans","year":"2012","unstructured":"Smans, J., Jacobs, B., Piessens, F.: Implicit dynamic frames. ACM Trans. Program. Lang. Syst. 34(1), 2:1\u20132:58 (2012)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"601_CR26","unstructured":"Viper project website. http:\/\/www.pm.inf.ethz.ch\/research\/viper"},{"key":"601_CR27","doi-asserted-by":"crossref","unstructured":"von Praun, C., Bordawekar, R., Cascaval, C.: Modeling optimistic concurrency using quantitative dependence analysis. In: Proceedings of the 13th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, pp. 185\u2013196 (2008)","DOI":"10.1145\/1345206.1345234"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-020-00601-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-020-00601-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-020-00601-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,26]],"date-time":"2021-11-26T12:05:25Z","timestamp":1637928325000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-020-00601-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,2,14]]},"references-count":27,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2021,10]]}},"alternative-id":["601"],"URL":"https:\/\/doi.org\/10.1007\/s10009-020-00601-z","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,2,14]]},"assertion":[{"value":"10 December 2020","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"14 February 2021","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}