{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,24]],"date-time":"2026-02-24T16:53:06Z","timestamp":1771951986792,"version":"3.50.1"},"reference-count":57,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T00:00:00Z","timestamp":1718841600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000038","name":"NSERC","doi-asserted-by":"crossref","award":["RGPIN-06516, DGECR00303"],"award-info":[{"award-number":["RGPIN-06516, DGECR00303"]}],"id":[{"id":"10.13039\/501100000038","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,6,20]]},"abstract":"<jats:p>\n            We present S\n            <jats:sc>p<\/jats:sc>\n            EQ, a quick and correct strategy for detecting semantics in sparse codes and enabling automatic translation to high-performance library calls or domain-specific languages (DSLs). When sparse linear algebra codes contain implicit preconditions about how data is stored that hamper direct translation, S\n            <jats:sc>p<\/jats:sc>\n            EQ identifies the high-level computation along with storage details and related preconditions. A run-time check guards the translation and ensures that required preconditions are met.\n          <\/jats:p>\n          <jats:p>\n            We implement S\n            <jats:sc>p<\/jats:sc>\n            EQ using the LLVM framework, the Z3 solver, and\n            <jats:monospace>egglog<\/jats:monospace>\n            library and correctly translate sparse linear algebra codes into two high-performance libraries, NVIDIA cuSPARSE and Intel MKL, and OpenMP (OMP). We evaluate S\n            <jats:sc>p<\/jats:sc>\n            EQ on ten diverse benchmarks against two state-of-the-art translation tools. S\n            <jats:sc>p<\/jats:sc>\n            EQ achieves geometric mean speedups of\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:mrow>\n                  <mml:mn>3.25<\/mml:mn>\n                  <mml:mo>\u00d7<\/mml:mo>\n                  <mml:mo>,<\/mml:mo>\n                  <mml:mn>5.09<\/mml:mn>\n                  <mml:mo>\u00d7<\/mml:mo>\n                  <mml:mo>,<\/mml:mo>\n                <\/mml:mrow>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            and\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:mrow>\n                  <mml:mn>8.04<\/mml:mn>\n                  <mml:mo>\u00d7<\/mml:mo>\n                <\/mml:mrow>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            on OpenMP, MKL, and cuSPARSE backends, respectively. S\n            <jats:sc>p<\/jats:sc>\n            EQ is the only tool that can guarantee the correct translation of sparse computations.\n          <\/jats:p>","DOI":"10.1145\/3656445","type":"journal-article","created":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T16:27:20Z","timestamp":1718900840000},"page":"1680-1703","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["SpEQ: Translation of Sparse Codes using Equivalences"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9063-6018","authenticated-orcid":false,"given":"Avery","family":"Laird","sequence":"first","affiliation":[{"name":"University of Toronto, Toronto, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9943-6941","authenticated-orcid":false,"given":"Bangtian","family":"Liu","sequence":"additional","affiliation":[{"name":"University of Toronto, Toronto, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1695-2810","authenticated-orcid":false,"given":"Nikolaj","family":"Bj\u00f8rner","sequence":"additional","affiliation":[{"name":"Microsoft Research, Redmond, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2719-8788","authenticated-orcid":false,"given":"Maryam Mehri","family":"Dehnavi","sequence":"additional","affiliation":[{"name":"University of Toronto, Toronto, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,6,20]]},"reference":[{"key":"e_1_3_1_2_1","unstructured":"2023. MemorySSA. https:\/\/llvm.org\/docs\/MemorySSA.html. Accessed: 2023-11-13."},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3183713.3196891"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3355089.3356549"},{"key":"e_1_3_1_5_1","article-title":"Compilers: Principles, Techniques, and Tools (2nd Edition)","author":"V. Aho Alfred","year":"2006","unstructured":"Alfred V. Aho , Monica S. Lam, Ravi Sethi, and Jeffrey D. Ullman. 2006. Compilers: Principles, Techniques, and Tools (2nd Edition). Addison-Wesley Longman Publishing Co., Inc., USA.","journal-title":"Addison-Wesley Longman Publishing Co., Inc., USA."},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","unstructured":"Andrew W. Appel . 1998. SSA is functional programming. SIGPLAN Not. 33 4 (apr 1998) 17-20. https:\/\/doi.org\/10.1145\/278283.278285 10.1145\/278283.278285","DOI":"10.1145\/278283.278285"},{"key":"e_1_3_1_7_1","unstructured":"OpenMP ARB. 2023. OpenMP. https:\/\/www.openmp.org\/."},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863581"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60299-2_37"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/567806.567807"},{"key":"e_1_3_1_11_1","unstructured":"Alvin Cheung. 2023. MetaLift.https:\/\/github.com\/metalift\/metalift."},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276493"},{"key":"e_1_3_1_13_1","unstructured":"cuSPARSE [n. d.]. Basic Linear Algebra for Sparse Matrices on NVIDIA GPUs. https:\/\/developer.nvidia.com\/cusparse."},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75280"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1137\/1.9780898718881"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3459010"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73595-3_13"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1066100.1066102"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1155\/2001\/527931"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/Correctness49594.2019.00010"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3377555.3377893"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3173162.3173182"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408974"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908117"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/360032.360048"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2017.8115709"},{"key":"e_1_3_1_28_1","unstructured":"Thomas Koehler Phil Trinder and Michel Steuwer. 2022. Sketch-Guided Equality Saturation."},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","unstructured":"Avery Laird. 2024. SpEQ: Translation of Sparse Codes using Equivalences https:\/\/doi.org\/10.5281\/zenodo.10906216 10.5281\/zenodo.10906216","DOI":"10.5281\/zenodo.10906216"},{"key":"e_1_3_1_30_1","first-page":"75","article-title":"LLVM: A Compilation Framework for Lifelong Program Analysis and Transformation","author":"Lattner Chris","year":"2004","unstructured":"Chris Lattner and Vikram Adve. 2004. LLVM: A Compilation Framework for Lifelong Program Analysis and Transformation. In CGO. San Jose, CA, USA, 75-88.","journal-title":"In CGO. San Jose, CA, USA,"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/CGO51591.2021.9370308"},{"key":"e_1_3_1_32_1","unstructured":"LCSSA 2023. Loop Closed SSA (LCSSA). https:\/\/llvm.org\/docs\/LoopTerminology.html#loop-closed-ssa-lcssa."},{"key":"e_1_3_1_33_1","unstructured":"Loop Simplify 2023. Loop Simplify Form. https:\/\/llvm.org\/docs\/LoopTerminology.html#loop-simplify-form."},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.future.2021.07.021"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/PACT.2011.68"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","unstructured":"Zohar Manna and Amir Pnueli. 2012. Temporal verification of reactive systems: safety. Springer Science & Business Media. https:\/\/doi.org\/10.1007\/978-1-4612-4222-2 10.1007\/978-1-4612-4222-2","DOI":"10.1007\/978-1-4612-4222-2"},{"key":"e_1_3_1_37_1","first-page":"85","article-title":"Matching linear algebra and tensor code to specialized hardware accelerators","author":"Martinez Pablo Antonio","year":"2023","unstructured":"Pablo Antonio Martinez, Jackson Woodruff, Jordi Armengol-Estape, Gregorio Bernabe, Jose Manuel Garcia, and Michael FP O\u2019Boyle. 2023. Matching linear algebra and tensor code to specialized hardware accelerators. In Proceedings of the 32nd ACM SIGPLAN International Conference on Compiler Construction. 85-97.","journal-title":"In Proceedings of the 32nd ACM SIGPLAN International Conference on Compiler Construction"},{"key":"e_1_3_1_38_1","unstructured":"MKL [n.d.]. Intel\u00ae oneAPI Math Kernel Library. https:\/\/www.intel.com\/content\/www\/us\/en\/developer\/tools\/oneapi\/onemkl.html."},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314646"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38856-9_17"},{"key":"e_1_3_1_41_1","article-title":"Techniques for program verification","author":"Nelson Charles Gregory","year":"1980","unstructured":"Charles Gregory Nelson. 1980. Techniques for program verification. Stanford University.","journal-title":"Stanford University"},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-17473-0_9"},{"key":"e_1_3_1_43_1","unstructured":"Louis-Noel Pouchet and Tomofumi Yuki. 2019. Polyhedral Benchmark suite. http:\/\/polybench.sf.net\/."},{"key":"e_1_3_1_44_1","unstructured":"Roldan Pozo. 2000. SciMark 2.0. http:\/\/math.nist.gov\/scimark2\/ (2000)."},{"key":"e_1_3_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/1460299.1460314"},{"key":"e_1_3_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2714064.2660228"},{"key":"e_1_3_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3460969"},{"key":"e_1_3_1_48_1","doi-asserted-by":"publisher","unstructured":"Davide Sangiorgi. 2011. Introduction to bisimulation and coinduction. Cambridge University Press. https:\/\/doi.org\/10.1017\/CBO9780511777110 10.1017\/CBO9780511777110","DOI":"10.1017\/CBO9780511777110"},{"key":"e_1_3_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2858949.2784754"},{"key":"e_1_3_1_50_1","doi-asserted-by":"publisher","DOI":"10.1109\/CGO.2017.7863730"},{"key":"e_1_3_1_51_1","article-title":"Parboil: A revised benchmark suite for scientific and commercial throughput computing","author":"Stratton John A","year":"2012","unstructured":"John A Stratton, Christopher Rodrigues, I-Jui Sung, Nady Obeid, Li-Wen Chang, Nasser Anssari, Geng Daniel Liu, and Wen-mei W Hwu. 2012. Parboil: A revised benchmark suite for scientific and commercial throughput computing.Center for Reliable and High-Performance Computing 127 (2012), 27.","journal-title":"Center for Reliable and High-Performance Computing 127 (2012), 27"},{"key":"e_1_3_1_52_1","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2018.2857721"},{"key":"e_1_3_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/1594834.1480915"},{"key":"e_1_3_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2738003"},{"key":"e_1_3_1_55_1","doi-asserted-by":"publisher","DOI":"10.1109\/SC.2016.40"},{"key":"e_1_3_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/2544137.2544141"},{"key":"e_1_3_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434304"},{"key":"e_1_3_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591239"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656445","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3656445","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:40:52Z","timestamp":1751661652000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656445"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6,20]]},"references-count":57,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2024,6,20]]}},"alternative-id":["10.1145\/3656445"],"URL":"https:\/\/doi.org\/10.1145\/3656445","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,6,20]]},"assertion":[{"value":"2024-06-20","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}