Formal Semantics for the Halide Language

Alex Reinking and Gilbert Bernstein and Jonathan Ragan-Kelley

EECS Department, University of California, Berkeley

Technical Report No. UCB/EECS-2020-40

May 1, 2020

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2020/EECS-2020-40.pdf

<p>Halide is a domain-specific language for building and optimizing numerical pipelines for applications in image processing, neural networks, and linear algebra. Its distinctive separation of what to compute &#8212; the <em>algorithm</em> &#8212; from the organization of that computation &#8212; the <em>schedule</em> &#8212; enables programmers to focus on the optimization of their programs without reasoning about loop index edge cases, concurrency issues, or portability. Halide then ensures memory safety through a <em>bounds inference</em> engine that determines safe sizes for every buffer in the generated code.</p> <p>In this paper, we present the Halide language in a formal setting, provide semantics for every part and proofs of correctness for the scheduling directives, and define the bounds inference problem in terms of program synthesis. We believe this precision will bolster future work in extending Halide to support a broader computational model, assist validating the implementation against a formal specification, and inspire the design of new languages and tools that apply programmer-controlled scheduling to other domains.</p>

Advisors: Jonathan Ragan-Kelley

BibTeX citation:

@mastersthesis{Reinking:EECS-2020-40,
    Author= {Reinking, Alex and Bernstein, Gilbert and Ragan-Kelley, Jonathan},
    Title= {Formal Semantics for the Halide Language},
    School= {EECS Department, University of California, Berkeley},
    Year= {2020},
    Month= {May},
    Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2020/EECS-2020-40.html},
    Number= {UCB/EECS-2020-40},
    Abstract= {<p>Halide is a domain-specific language for building and optimizing numerical pipelines for applications in image processing, neural networks, and linear algebra. Its distinctive separation of what to compute &#8212; the <em>algorithm</em> &#8212; from the organization of that computation &#8212; the <em>schedule</em> &#8212; enables programmers to focus on the optimization of their programs without reasoning about loop index edge cases, concurrency issues, or portability. Halide then ensures memory safety through a <em>bounds inference</em> engine that determines safe sizes for every buffer in the generated code.</p>
<p>In this paper, we present the Halide language in a formal setting, provide semantics for every part and proofs of correctness for the scheduling directives, and define the bounds inference problem in terms of program synthesis. We believe this precision will bolster future work in extending Halide to support a broader computational model, assist validating the implementation against a formal specification, and inspire the design of new languages and tools that apply programmer-controlled scheduling to other domains.</p>},
}

EndNote citation:

%0 Thesis
%A Reinking, Alex 
%A Bernstein, Gilbert 
%A Ragan-Kelley, Jonathan 
%T Formal Semantics for the Halide Language
%I EECS Department, University of California, Berkeley
%D 2020
%8 May 1
%@ UCB/EECS-2020-40
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2020/EECS-2020-40.html
%F Reinking:EECS-2020-40