Verified Scheduling Via High-Level Scheduling Rewrites
I propose a lightweight Coq framework for optimizing tensor kernels written in a pure, functional array language. Optimizations rely on user scheduling using series of verified, semantics-preserving rewrites. Unusually for compilation targeting imperative code with arrays and nested loops, all rewri...
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Thesis |
| Published: |
Massachusetts Institute of Technology
2022
|
| Online Access: | https://hdl.handle.net/1721.1/144722 https://orcid.org/ 0000-0001-5549-9177 |
| _version_ | 1826199165571432448 |
|---|---|
| author | Liu, Amanda |
| author2 | Chlipala, Adam |
| author_facet | Chlipala, Adam Liu, Amanda |
| author_sort | Liu, Amanda |
| collection | MIT |
| description | I propose a lightweight Coq framework for optimizing tensor kernels written in a pure, functional array language. Optimizations rely on user scheduling using series of verified, semantics-preserving rewrites. Unusually for compilation targeting imperative code with arrays and nested loops, all rewrites are source-to-source within a purely functional language. This language comprises a set of core constructs for expressing high-level computation detail and a set of what we call reshape operators, which can be derived from core constructs but trigger low-level decisions about storage patterns and ordering. We will demonstrate that not only is this system capable of deriving the optimizations of existing state-of-the-art languages like Halide and generating comparably performant code, it is also able to schedule a family of useful program transformations beyond what is reachable in Halide. |
| first_indexed | 2024-09-23T11:15:46Z |
| format | Thesis |
| id | mit-1721.1/144722 |
| institution | Massachusetts Institute of Technology |
| last_indexed | 2024-09-23T11:15:46Z |
| publishDate | 2022 |
| publisher | Massachusetts Institute of Technology |
| record_format | dspace |
| spelling | mit-1721.1/1447222022-08-30T03:43:03Z Verified Scheduling Via High-Level Scheduling Rewrites Liu, Amanda Chlipala, Adam Ragan-Kelley, Jonathan Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science I propose a lightweight Coq framework for optimizing tensor kernels written in a pure, functional array language. Optimizations rely on user scheduling using series of verified, semantics-preserving rewrites. Unusually for compilation targeting imperative code with arrays and nested loops, all rewrites are source-to-source within a purely functional language. This language comprises a set of core constructs for expressing high-level computation detail and a set of what we call reshape operators, which can be derived from core constructs but trigger low-level decisions about storage patterns and ordering. We will demonstrate that not only is this system capable of deriving the optimizations of existing state-of-the-art languages like Halide and generating comparably performant code, it is also able to schedule a family of useful program transformations beyond what is reachable in Halide. S.M. 2022-08-29T16:07:12Z 2022-08-29T16:07:12Z 2022-05 2022-06-21T19:25:47.865Z Thesis https://hdl.handle.net/1721.1/144722 https://orcid.org/ 0000-0001-5549-9177 In Copyright - Educational Use Permitted Copyright MIT http://rightsstatements.org/page/InC-EDU/1.0/ application/pdf Massachusetts Institute of Technology |
| spellingShingle | Liu, Amanda Verified Scheduling Via High-Level Scheduling Rewrites |
| title | Verified Scheduling Via High-Level Scheduling Rewrites |
| title_full | Verified Scheduling Via High-Level Scheduling Rewrites |
| title_fullStr | Verified Scheduling Via High-Level Scheduling Rewrites |
| title_full_unstemmed | Verified Scheduling Via High-Level Scheduling Rewrites |
| title_short | Verified Scheduling Via High-Level Scheduling Rewrites |
| title_sort | verified scheduling via high level scheduling rewrites |
| url | https://hdl.handle.net/1721.1/144722 https://orcid.org/ 0000-0001-5549-9177 |
| work_keys_str_mv | AT liuamanda verifiedschedulingviahighlevelschedulingrewrites |