PLSE Research Group
Various Presenters (Allen School)
Colloquium
Thursday, October 6, 2022, 3:30 pm
Abstract
Speaker: Oliver Flatt
Title: Small Proofs from Congruence Closure
Satisfiability Modulo Theory (SMT) solvers and equality saturation engines must generate proof certificates from e-graph-based congruence closure procedures to enable verification and conflict clause generation. Smaller proof certificates speed up these activities. Though the problem of generating proofs of minimal size is known to be NP-complete, existing proof minimization algorithms for congruence closure generate unnecessarily large proofs and introduce asymptotic overhead over the core congruence closure procedure. In this paper, we introduce an O(n^5) time algorithm which generates optimal proofs under a new relaxed "proof tree size" metric that directly bounds proof size. We then relax this approach further to a practical O(n \log(n)) greedy algorithm which generates small proofs with no asymptotic overhead. We implemented our techniques in the egg equality saturation toolkit, yielding the first certifying equality saturation engine. We show that our greedy approach in egg quickly generates substantially smaller proofs than the state-of-the-art Z3 SMT solver on a corpus of 3760 benchmarks.
Speaker: Gus Smith
Title: Synthesizing FPGA ISA Implementations with Lakeroad
Compiling hardware designs to FPGAs -- flexible hardware platforms composed of configurable hardware units -- has long been a frustrating task. Legacy compilers developed in the early days of FPGAs have not kept up with the increasing complexity of modern FPGAs. To address this, FPGA compilers are becoming more and more like software compilers, in which a program (i.e. a hardware design) is gradually lowered through increasingly fine-grained levels of abstraction, with the goal of eventually converting the entire program into a list of instructions in a low-level instruction set architecture (ISA). Currently, state-of-the-art FPGA compilers implement their ISAs by hand for each FPGA backend they would like to target. In this work, we present a tool, Lakeroad, which uses program synthesis to implement an ISA given just a high-level description of the FPGA architecture. We demonstrate how Lakeroad is able to implement a rich ISA across a diverse set of FPGAs.
Speaker: Sirui Lu
Title: Grisette: Symbolic Compilation as a Monadic Library
The development of constraint solvers has enabled automated reasoning about programs, shifting the engineering burden to implementing symbolic compilation tools that translate programs into efficient constraints. It is desirable to have reusable symbolic compilation tools to reduce this engineering burden, and such reusable tools should be both efficient and user-friendly. We describe a new formulation of a reusable symbolic compiler architecture, Grisette. Internally, Grisette is based on a novel algorithm that efficiently merges and normalizes program states, improving symbolic compilation speed and reducing constraint size. For the user, it provides a functional, statically-typed, and monadic interface, allowing the user to easily implement high-performance symbolic compilers by configuring our system with domain knowledge.
Speaker: Dan Cascaval
Title: Referencing CAD Programs
In order to write programs that generate geometry and represent spaces of possible Computer-Aided Design (CAD) models, a programmer must refer to geometric elements that might appear or disappear depending on model inputs. We give a domain specific language for defining such CAD references that is safe, unambiguous, and does not duplicate code.