About Me Blog Papers

Exocompilation for Productive Programming of Hardware Accelerators

Thu 09 June 2022

Published at PLDI 2022.

Link to paper

High-performance kernel libraries are critical to exploiting accelerators and specialized instructions in many applications. Because compilers are difficult to extend to support diverse and rapidly-evolving hardware targets, and automatic optimization is often insufficient to guarantee state-of-the-art performance, these libraries are commonly still coded …

Continue reading »

Perceus: Garbage Free Reference Counting with Reuse

Mon 25 January 2021

PLDI 2021 Distinguished Paper

Link to paper

We introduce Perceus, an algorithm for precise reference counting with reuse and specialization. Starting from a functional core language with explicit control-flow, Perceus emits precise reference counting instructions such that programs are garbage-free, where only live references are retained.This enables further optimizations …

Continue reading »

Formal Semantics for the Halide Language

Fri 01 May 2020

Pre-print on arXiv

We present the first formalization and metatheory of language soundness for a user-schedulable language, the widely used array processing language Halide. User-schedulable languages strike a balance between abstraction and control in high-performance computing by separating the specification of what a program should compute from a schedule for …

Continue reading »

A Type-Directed Approach to Program Repair

Thu 16 July 2015

Published at CAV 2015.

Link to paper

Developing enterprise software often requires composing several libraries together with a large body of in-house code. Large APIs introduce a steep learning curve for new developers as a result of their complex object-oriented underpinnings. While the written code in general reflects a programmer …

Continue reading »