{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,26]],"date-time":"2026-02-26T15:27:33Z","timestamp":1772119653617,"version":"3.50.1"},"reference-count":44,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2024,6,19]],"date-time":"2024-06-19T00:00:00Z","timestamp":1718755200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,6,19]],"date-time":"2024-06-19T00:00:00Z","timestamp":1718755200000},"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":["J Autom Reasoning"],"published-print":{"date-parts":[[2024,9]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>We present a stepwise refinement approach to develop verified parallel algorithms, down to efficient LLVM code. The resulting algorithms\u2019 performance is competitive with their counterparts implemented in C++. Our approach is backwards compatible with the Isabelle Refinement Framework, such that existing sequential formalizations can easily be adapted or re-used. As case study, we verify a parallel quicksort algorithm that is competitive to unverified state-of-the-art algorithms.<\/jats:p>","DOI":"10.1007\/s10817-024-09701-w","type":"journal-article","created":{"date-parts":[[2024,6,19]],"date-time":"2024-06-19T07:01:52Z","timestamp":1718780512000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Refinement of Parallel Algorithms Down to LLVM: Applied to Practically Efficient Parallel Sorting"],"prefix":"10.1007","volume":"68","author":[{"given":"Peter","family":"Lammich","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,6,19]]},"reference":[{"key":"9701_CR1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/s11265-020-01534-1","volume":"93","author":"M Asiatici","year":"2021","unstructured":"Asiatici, M., Maiorano, D., Ienne, P.: How many CPU cores is an FPGA worth? Lessons learned from accelerating string sorting on a CPU-FPGA system. J. Signal Process. Syst. 93, 1\u201313 (2021)","journal-title":"J. Signal Process. Syst."},{"issue":"1","key":"9701_CR2","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1145\/3505286","volume":"9","author":"M Axtmann","year":"2022","unstructured":"Axtmann, M., Witt, S., Ferizovic, D., Sanders, P.: Engineering in-place (shared-memory) sorting algorithms. ACM Trans. Parallel Comput. 9(1), 2\u20131262 (2022). https:\/\/doi.org\/10.1145\/3505286","journal-title":"ACM Trans. Parallel Comput."},{"key":"9701_CR3","volume-title":"Interactive Theorem Proving and Program Development: Coq\u2019Art The Calculus of Inductive Constructions","author":"Y Bertot","year":"2010","unstructured":"Bertot, Y., Castran, P.: Interactive Theorem Proving and Program Development: Coq\u2019Art The Calculus of Inductive Constructions, 1st edn. Springer, Heidelberg (2010)","edition":"1"},{"key":"9701_CR4","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/978-3-319-66845-1_7","volume-title":"Integrated Formal Methods","author":"S Blom","year":"2017","unstructured":"Blom, S., Darabi, S., Huisman, M., Oortwijn, W.: The vercors tool set: verification of parallel and concurrent software. In: Polikarpova, N., Schneider, S. (eds.) Integrated Formal Methods, pp. 102\u2013110. Springer, Cham (2017)"},{"key":"9701_CR5","unstructured":"Boost C++ Libraries Sorting Algorithms. https:\/\/www.boost.org\/doc\/libs\/1_77_0\/libs\/sort\/doc\/html\/index.html"},{"key":"9701_CR6","unstructured":"Boost C++ Libraries. https:\/\/www.boost.org\/"},{"key":"9701_CR7","doi-asserted-by":"publisher","unstructured":"Bornat, R., Calcagno, C., O\u2019Hearn, P., Parkinson, M.: Permission accounting in separation logic. In: Proc. of POPL, pp. 259\u2013270. ACM, New York, NY, USA (2005). https:\/\/doi.org\/10.1145\/1040305.1040327","DOI":"10.1145\/1040305.1040327"},{"issue":"1","key":"9701_CR8","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10817-017-9418-4","volume":"60","author":"J Brunner","year":"2018","unstructured":"Brunner, J., Lammich, P.: Formal verification of an executable LTL model checker with partial order reduction. J. Autom. Reasoning 60(1), 3\u201321 (2018). https:\/\/doi.org\/10.1007\/s10817-017-9418-4","journal-title":"J. Autom. Reasoning"},{"key":"9701_CR9","doi-asserted-by":"crossref","unstructured":"Calcagno, C., O\u2019Hearn, P.W., Yang, H.: Local action and abstract separation logic. In: LICS 2007, pp. 366\u2013378 (2007)","DOI":"10.1109\/LICS.2007.30"},{"issue":"2","key":"9701_CR10","doi-asserted-by":"publisher","first-page":"1313","DOI":"10.14778\/1454159.1454171","volume":"1","author":"J Chhugani","year":"2008","unstructured":"Chhugani, J., Nguyen, A.D., Lee, V.W., Macy, W., Hagog, M., Chen, Y.-K., Baransi, A., Kumar, S., Dubey, P.: Efficient implementation of sorting on multi-core SIMD CPU architecture. Proc. VLDB Endow. 1(2), 1313\u20131324 (2008)","journal-title":"Proc. VLDB Endow."},{"key":"9701_CR11","doi-asserted-by":"crossref","unstructured":"Esparza, J., Lammich, P., Neumann, R., Nipkow, T., Schimpf, A., Smaus, J.-G.: A fully verified executable LTL model checker. In: CAV. LNCS, vol. 8044, pp. 463\u2013478. Springer, Saint Petersburg (2013)","DOI":"10.1007\/978-3-642-39799-8_31"},{"key":"9701_CR12","doi-asserted-by":"publisher","unstructured":"Fleury, M., Lammich, P.: A more pragmatic CDCL for isasat and targetting LLVM (short paper). In: Pientka, B., Tinelli, C. (eds.) Automated Deduction - CADE 29 - 29th International Conference on Automated Deduction, Rome, Italy, July 1\u20134, 2023, Proceedings. Lecture Notes in Computer Science, vol. 14132, pp. 207\u2013219. Springer, Rome, Italy (2023). https:\/\/doi.org\/10.1007\/978-3-031-38499-8_12","DOI":"10.1007\/978-3-031-38499-8_12"},{"key":"9701_CR13","doi-asserted-by":"crossref","unstructured":"Fleury, M., Blanchette, J.C., Lammich, P.: A verified SAT solver with watched literals using Imperative HOL. In: Proc. of CPP, pp. 158\u2013171 (2018)","DOI":"10.1145\/3176245.3167080"},{"key":"9701_CR14","doi-asserted-by":"publisher","DOI":"10.1184\/R1\/6608258.v1","volume-title":"Parallel Neighbor-Sort","author":"AN Habermann","year":"1972","unstructured":"Habermann, A.N.: Parallel Neighbor-Sort. Carnegie Mellon University, Pittsburgh (1972). https:\/\/doi.org\/10.1184\/R1\/6608258.v1"},{"key":"9701_CR15","doi-asserted-by":"publisher","unstructured":"Haslbeck, M.P.L., Lammich, P.: For a few dollars more-verified fine-grained algorithm analysis down to LLVM. In: Yoshida, N. (ed.) Proc. of ESOP. LNCS, vol. 12648, pp. 292\u2013319. Springer, Luxemburg (2021). https:\/\/doi.org\/10.1007\/978-3-030-72019-3_11","DOI":"10.1007\/978-3-030-72019-3_11"},{"key":"9701_CR16","unstructured":"Haslbeck, M.P.L., Lammich, P.: For a few dollars more - verified fine-grained algorithm analysis down to LLVM. TOPLAS, S.I. ESOP\u201921"},{"key":"9701_CR17","doi-asserted-by":"publisher","DOI":"10.1145\/3371074","author":"JK Hinrichsen","year":"2019","unstructured":"Hinrichsen, J.K., Bengtson, J., Krebbers, R.: Actris: session-type based reasoning in separation logic. Proc. ACM Program. Lang. (2019). https:\/\/doi.org\/10.1145\/3371074","journal-title":"Proc. ACM Program. Lang."},{"key":"9701_CR18","doi-asserted-by":"publisher","unstructured":"Huffman, B., Kuncar, O.: Lifting and transfer: A modular design for quotients in isabelle\/hol. In: Gonthier, G., Norrish, M. (eds.) Proc. of CPP. LNCS, vol. 8307, pp. 131\u2013146. Springer, Melbourne (2013). https:\/\/doi.org\/10.1007\/978-3-319-03545-1_9","DOI":"10.1007\/978-3-319-03545-1_9"},{"key":"9701_CR19","unstructured":"Intel oneAPI Threading Building Blocks. https:\/\/software.intel.com\/en-us\/intel-tbb"},{"key":"9701_CR20","volume-title":"The C++ Standard Library: A Tutorial and Reference","author":"NM Josuttis","year":"2012","unstructured":"Josuttis, N.M.: The C++ Standard Library: A Tutorial and Reference, 2nd edn. Addison-Wesley Professional, Boston (2012)","edition":"2"},{"key":"9701_CR21","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1017\/S0956796818000151","volume":"28","author":"R Jung","year":"2018","unstructured":"Jung, R., Krebbers, R., Jourdan, J., Bizjak, A., Birkedal, L., Dreyer, D.: Iris from the ground up: a modular foundation for higher-order concurrent separation logic. J. Funct. Program. 28, 20 (2018). https:\/\/doi.org\/10.1017\/S0956796818000151","journal-title":"J. Funct. Program."},{"key":"9701_CR22","first-page":"149","volume-title":"TPHOLs","author":"F Kamm\u00fcller","year":"1999","unstructured":"Kamm\u00fcller, F., Wenzel, M., Paulson, L.C.: Locales a sectioning concept for Isabelle. In: Bertot, Y., Dowek, G., Th\u00e9ry, L., Hirschowitz, A., Paulin, C. (eds.) TPHOLs, pp. 149\u2013165. Springer, Nice (1999)"},{"key":"9701_CR23","doi-asserted-by":"crossref","unstructured":"Klein, G., Kolanski, R., Boyton, A.: Mechanised separation algebra. In: ITP, pp. 332\u2013337. Springer, Princeton (2012)","DOI":"10.1007\/978-3-642-32347-8_22"},{"key":"9701_CR24","doi-asserted-by":"crossref","unstructured":"Lammich, P.: Automatic data refinement. In: ITP. LNCS, vol. 7998, pp. 84\u201399. Springer, Rennes (2013)","DOI":"10.1007\/978-3-642-39634-2_9"},{"key":"9701_CR25","doi-asserted-by":"crossref","unstructured":"Lammich, P.: Verified efficient implementation of Gabow\u2019s strongly connected component algorithm. In: International Conference on Interactive Theorem Proving, pp. 325\u2013340 (2014). Springer","DOI":"10.1007\/978-3-319-08970-6_21"},{"key":"9701_CR26","doi-asserted-by":"crossref","unstructured":"Lammich, P.: Refinement to Imperative\/HOL. In: ITP. LNCS, vol. 9236, pp. 253\u2013269. Springer, Nanjing (2015)","DOI":"10.1007\/978-3-319-22102-1_17"},{"key":"9701_CR27","doi-asserted-by":"crossref","unstructured":"Lammich, P.: Efficient verified (UN)SAT certificate checking. In: Proc. of CADE. Springer, Gothenburg (2017)","DOI":"10.1007\/978-3-319-63046-5_15"},{"key":"9701_CR28","doi-asserted-by":"crossref","unstructured":"Lammich, P.: The GRAT tool chain-efficient (UN)SAT certificate checking with formal correctness guarantees. In: SAT, pp. 457\u2013463 (2017)","DOI":"10.1007\/978-3-319-66263-3_29"},{"key":"9701_CR29","doi-asserted-by":"publisher","first-page":"22","DOI":"10.4230\/LIPIcs.ITP.2019.22","volume-title":"ITP","author":"P Lammich","year":"2019","unstructured":"Lammich, P.: Generating Verified LLVM from Isabelle\/HOL. In: Harrison, J., O\u2019Leary, J., Tolmach, A. (eds.) ITP, vol. 141, pp. 22\u201312219. Dagstuhl Publishing, Portland (2019). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2019.22"},{"key":"9701_CR30","doi-asserted-by":"publisher","unstructured":"Lammich, P.: Efficient verified implementation of introsort and pdqsort. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) Proc. of IJCAR (II). LNCS, vol. 12167, pp. 307\u2013323. Springer, Paris (2020). https:\/\/doi.org\/10.1007\/978-3-030-51054-1_18","DOI":"10.1007\/978-3-030-51054-1_18"},{"key":"9701_CR31","doi-asserted-by":"publisher","unstructured":"Lammich, P.: Refinement of parallel algorithms down to LLVM. In: Andronick, J., Moura, L. (eds.) ITP. LIPIcs, vol. 237, pp. 24\u201312418. Dagstuhl Publishing, Haifa (2022). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2022.24","DOI":"10.4230\/LIPIcs.ITP.2022.24"},{"key":"9701_CR32","doi-asserted-by":"publisher","unstructured":"Lammich, P., Fleury, M.: lammich\/isabelle_llvm: parallel sorting: artefact release. https:\/\/doi.org\/10.5281\/zenodo.10869631","DOI":"10.5281\/zenodo.10869631"},{"key":"9701_CR33","doi-asserted-by":"crossref","unstructured":"Lammich, P., Lochbihler, A.: The Isabelle Collections Framework. In: ITP 2010. LNCS, vol. 6172, pp. 339\u2013354. Springer, Edinburgh (2010)","DOI":"10.1007\/978-3-642-14052-5_24"},{"key":"9701_CR34","doi-asserted-by":"crossref","unstructured":"Lammich, P., Sefidgar, S.R.: Formalizing the Edmonds-Karp algorithm. In: Proc. of ITP, pp. 219\u2013234 (2016)","DOI":"10.1007\/978-3-319-43144-4_14"},{"issue":"2","key":"9701_CR35","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/s10817-017-9442-4","volume":"62","author":"P Lammich","year":"2019","unstructured":"Lammich, P., Sefidgar, S.R.: Formalizing network flow algorithms: a refinement approach in Isabelle\/HOL. J. Autom. Reasoning 62(2), 261\u2013280 (2019). https:\/\/doi.org\/10.1007\/s10817-017-9442-4","journal-title":"J. Autom. Reasoning"},{"key":"9701_CR36","series-title":"LNCS","first-page":"166","volume-title":"ITP 2012","author":"P Lammich","year":"2012","unstructured":"Lammich, P., Tuerk, T.: Applying data refinement for monadic programs to Hopcroft\u2019s algorithm. In: Beringer, L., Felty, A.P. (eds.) ITP 2012. LNCS, vol. 7406, pp. 166\u2013182. Springer, Princeton (2012)"},{"key":"9701_CR37","doi-asserted-by":"publisher","DOI":"10.1145\/3473571","author":"G M\u00e9vel","year":"2021","unstructured":"M\u00e9vel, G., Jourdan, J.-H.: Formal verification of a concurrent bounded queue in a weak memory model. Proc. ACM Program. Lang. (2021). https:\/\/doi.org\/10.1145\/3473571","journal-title":"Proc. ACM Program. Lang."},{"issue":"8","key":"9701_CR38","first-page":"983","volume":"27","author":"DR Musser","year":"1997","unstructured":"Musser, D.R.: Introspective sorting and selection algorithms. Software 27(8), 983\u2013993 (1997)","journal-title":"Software"},{"key":"9701_CR39","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-540-28644-8_4","volume-title":"CONCUR 2004-Concurrency Theory","author":"PW O\u2019Hearn","year":"2004","unstructured":"O\u2019Hearn, P.W.: Resources, concurrency and local reasoning. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004-Concurrency Theory, pp. 49\u201367. Springer, Berlin (2004)"},{"key":"9701_CR40","doi-asserted-by":"crossref","unstructured":"Safari, M., Huisman, M.: A generic approach to the verification of the permutation property of sequential and parallel swap-based sorting algorithms. In: International Conference on Integrated Formal Methods, pp. 257\u2013275 (2020). Springer","DOI":"10.1007\/978-3-030-63461-2_14"},{"key":"9701_CR41","doi-asserted-by":"crossref","unstructured":"Spies, S., G\u00e4her, L., Gratzer, D., Tassarotti, J., Krebbers, R., Dreyer, D., Birkedal, L.: Transfinite iris: Resolving an existential dilemma of step-indexed separation logic. In: Proc. of PLDI, pp. 80\u201395 (2021)","DOI":"10.1145\/3453483.3454031"},{"key":"9701_CR42","unstructured":"The GNU C++ Library 3.4.28. https:\/\/gcc.gnu.org\/onlinedocs\/libstdc++\/"},{"key":"9701_CR43","unstructured":"Verified Software Toolchain Project Web Page. https:\/\/vst.cs.princeton.edu\/"},{"key":"9701_CR44","doi-asserted-by":"crossref","unstructured":"Wimmer, S., Lammich, P.: Verified model checking of timed automata. In: TACAS 2018, Thessaloniki, pp. 61\u201378 (2018)","DOI":"10.1007\/978-3-319-89960-2_4"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-024-09701-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-024-09701-w\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-024-09701-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T05:08:15Z","timestamp":1725599295000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-024-09701-w"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6,19]]},"references-count":44,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2024,9]]}},"alternative-id":["9701"],"URL":"https:\/\/doi.org\/10.1007\/s10817-024-09701-w","relation":{"has-preprint":[{"id-type":"doi","id":"10.21203\/rs.3.rs-2733052\/v1","asserted-by":"object"}]},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,6,19]]},"assertion":[{"value":"24 March 2023","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"30 April 2024","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"19 June 2024","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare no conflict of interest.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}}],"article-number":"14"}}