I am a fourth-year PhD student in the Computer Science department at UC Santa Barbara. I am fortunate to be advised by Professor Ben Hardekopf and Jonathan Balkind.
My interests primarily lie in the areas of software engineering and programming languages. At present, I am focused on utilizing these techniques to solve problems related to hardware design.
Education
Ph.D., Computer Science
2022-present
University of California, Santa Barbara
Advisors: Ben Hardekopf and Jonathan Balkind
Research
Conference Papers
Fungible Memories for Automated Technology Mapping and Re-targeting
Improving Equality Saturation for EDA via Semantic E-Graphs
* Equal contribution
Refinement Types for Visualization
Abstract
Visualizations have become crucial in the contemporary data-driven world as they aid in exploring, verifying, and sharing insights obtained from data. In this paper, we propose a new paradigm of visualization synthesis based on refinement types. Besides input-output examples, users can optionally use refinement-type annotations to constrain the range of valid values in the example visualization or to express complex interactions between different visual components. Our system's outputs include both data transformation and visualization programs that are consistent with refinement-type specifications. To mitigate the scalability challenge during the synthesis process, we introduce a new visualization synthesis algorithm that uses lightweight bidirectional type checking to prune the search space. As we demonstrate experimentally, this new synthesis algorithm results in significant speed-up compared to prior work. We have implemented the proposed approach in a tool called Calico and evaluated it on 40 visualization tasks collected from online forums and tutorials. Our experiments show that Calico can solve 98% of these benchmarks and, among those benchmarks that can be solved, the desired visualization is among the top-1 output generated by Calico. Furthermore, Calico takes an average of 1.56 seconds to generate the visualization, which is 50 times faster than Viser, a state-of-the-art synthesizer for data visualization.ALGO: Synthesizing Algorithmic Programs with Generated Oracle Verifiers
Abstract
Large language models (LLMs) excel at implementing code from functionality descriptions but struggle with algorithmic problems that require not only implementation but also identification of the suitable algorithm. Moreover, LLM-generated programs lack guaranteed correctness and require human verification. To address these challenges, we propose ALGO, a framework that synthesizes Algorithmic programs with LLM-Generated Oracles to guide the generation and verify their correctness. ALGO first generates a reference oracle by prompting an LLM to exhaustively enumerate all the combinations of relevant variables. This oracle is then utilized to guide an arbitrary search strategy in exploring the algorithm space and to verify the synthesized algorithms. Our study shows that the LLM-generatedoracles are correct for 88% of the cases. With the oracles as verifiers, ALGO can be integrated with any existing code generation model in a model-agnostic manner to enhance its performance. Experiments show that when equipped with ALGO, we achieve an 8× better one-submission pass rate over the Codex model and a 2.6× better one-submission pass rate over CodeT, the current state-of-the-art model on CodeContests. We can also get 1.3× better pass rate over the ChatGPT Code Interpreter on unseen problems. The problem set we used for testing, the prompts we used, the verifier and solution programs, and the test cases generated by ALGOare available at https://github. com/zkx06111/ALGO.Generalizable Synthesis Through Unification.
Abstract
The generalizability of PBE solvers is the key to the empirical synthesis performance. Despite the importance of generalizability, related studies on PBE solvers are still limited. In theory, few existing solvers provide theoretical guarantees on generalizability, and in practice, there is a lack of PBE solvers with satisfactory generalizability on important domains such as conditional linear integer arithmetic (CLIA). In this paper, we adopt a concept from the computational learning theory, Occam learning, and perform a comprehensive study on the framework of synthesis through unification (STUN), a state-of-the-art framework for synthesizing programs with nested if-then-else operators. We prove that Eusolver, a state-of-the-art STUN solver, does not satisfy the condition of Occam learning, and then we design a novel STUN solver, PolyGen, of which the generalizability is theoretically guaranteed by Occam learning. We evaluate PolyGen on the domains of CLIA and demonstrate that PolyGen significantly outperforms two state-of-the-art PBE solvers on CLIA, Eusolver and Euphony, on both generalizability and efficiency.Workshop Papers
Implementing Cache Coherence with Coroutines: A Case Study
Abstract
Hardware description languages must offer more productive abstractions without sacrificing low-level control. Coroutines are an expressive control construct that naturally describe the progression of a protocol as a sequence of steps separated by yield statements. In this report, we describe our experience modeling a hardware description language with coroutines to implement the MSI cache coherence protocol.Unifying HLS and RTL with Timeline Types
Abstract
Hardware design today is divided between two paradigms: RTL offers precise control over timing and resources but demands substantial manual effort, while HLS provides automation at the cost of predictability and fine-grained control. We argue that this dichotomy is unnecessary. This paper proposes a unifying design approach for latency-sensitive and latency-abstract hardware based on timeline types. By extending Filament’s timeline type system with scheduler-determined parameters, denoted by question marks, designers can selectively leave binding and scheduling decisions partially open to automation while retaining explicit control where needed. This enables a continuous spectrum between fully manual RTL design and fully automated HLS design within a single language framework, making it possible to combine fine-grained control with automation.There and Back Again: A Netlist's Tale with Much Egraphin'
Abstract
EDA toolchains are notoriously unpredictable, incomplete, and error-prone; the generally-accepted remedy has been to re-imagine EDA tasks as compilation problems. However, any compiler framework we apply must be prepared to handle the wide range of EDA tasks, including not only compilation tasks like technology mapping and optimization (the "there" in our title), but also decompilation tasks like loop rerolling (the "back again"). In this paper, we advocate for equality saturation -- a term rewriting framework -- as the framework of choice when building hardware toolchains. Through a series of case studies, we show how the needs of EDA tasks line up conspicuously well with the features equality saturation provides.Teaching
- CS32: Object-Oriented Design (Fall’24, Winter’26, Spring’26)
- CS138: Automata and Formal Languages (Spring’24, Fall’25)
- CS9: Intermediate Python (Fall’23, Winter’24)
- CS160: Translation of Computer Programs (Spring’23)
- CS162: Programming Languages (Winter’23)
Service
- PLDI’24 AEC