LATTE is a venue for discussion, debate, and brainstorming about language-oriented approaches to hardware acceleration. The focus is on new languages and tools that aim to let domain specialists, not just hardware experts, produce efficient accelerators. See the Call for Participation for more details.
LATTE '23 is co-located with ASPLOS '23. It will happen on Sunday, March 26, 2023 in Vancouver, BC, Canada.
To attend LATTE in person, please register for ASPLOS. Choose the option to attend (at least) one day of workshops/tutorials, and check the box for LATTE on the second page of the registration form.
We also invite virtual participation. To attend virtually, pre-register for the Zoom meeting (which is free). You don't need to register for ASPLOS.
The focus of LATTE is on generating discussion---before, during, and after the workshop! We have set up asynchronous discussion threads for each of the talks at the workshop. Regardless of whether you can join us in Vancouver or on Zoom, we want you to participate! Get the discussion started now.
At the workshop, we have time dedicated to an "Open Mic" to give voice to to these asynchronous discussions. As topics progress on the threads, please keep track of anything that arises that you think the broader audience should know about. You can take 60 seconds during the "Open Mic" session to summarize the point and get the synchronous discussion rolling.
|9–9:15am||Opening & Introductions|
|9:15–10:20am||Keynote by Gilbert Bernstein|
|11:10am–noon||Discussion & Open Mic|
|3:40–4pm||Discussion & Closing|
Talks in the sessions are 7 minutes, each with 1 minute of short clarification questions. Each session will have 6 minutes of shared discussion time directed toward all the authors in a given session.
Performance vs. Correctness When Writing Low-Level HPC Code
Gilbert Bernstein, University of Washington
Most applications benefiting from accelerators (especially ML accelerators) rely on hand-optimized high-performance kernel libraries to get access to new hardware, and ensure a high level of performance (e.g. BLAS, CuDNN, etc.). However, these kernel libraries are still written and optimized by hand, at great expense using low-level C and assembly code. This is because the performance engineers who write this code, (like the hardware designers on the other side of the ISA from them) require control over the design. What if we designed programming languages specially tailored to the needs of these programmers?
First, I will discuss performance and correctness. Should we think of this as a tradeoff (as the talk title implies) or two halves of the same whole? Then, I will discuss two different “user-scheduled” languages we’ve built to achieve both performance and correctness in HPC kernel programming. (1) Exo is an imperative language which turns the compiler “inside out” by externalizing control of code optimization directly to the user, and by replacing hardware-specific backends (the compiler writers’ responsibility) with user-level libraries (the performance engineers’ responsibility). (2) ATL is a simple functional tensor language, which we have embedded in Coq. Rewrites of ATL programs thereby become lemmas, and user-scheduling directives become proof tactics. These languages match the performance of highly tuned linear algebra, neural net and image processing kernels by using formal verification machinery to expedite the existing optimization process of low-level software performance engineers.
A Scalable Formal Approach for Correctness-Assured Hardware Design
Jin Yang, Intel
Correctness must be a first principle in hardware design, especially for security and safety critical applications. We will give an overview of our scalable approach for correctness-assured hardware design at behavioral level, based on formalizing microarchitecture features as program transformations in an incremental compiler design and microprocessor correctness as a refined notation of compiler correctness. We will show how our approach is applied to designing a formally verified FHE (Fully Homomorphic Encryption) accelerator.