PLSE Blog RSS Feed

Exploring In-Synthesis Verification of Hardware

keywords: #synthesis #verification #hardware #compilers

Getting hardware right is crucial – without correct hardware, there’s no way to guarantee that software will work as intended. To raise the stakes even higher, hardware designers really only have one shot to get it right – once the hardware’s made, you can’t really patch it! To address this importance, there are many tools which use formal methods to give strong guarantees that hardware is correct. In practice, this often entails writing equivalence proofs showing that hardware behaves the same as some high-level model. In this post, we’ll take a look at the challenges I ran into while making Gator, a project I worked on which explored how to make these proofs easier!

Read More

Partial Rely—Guarantee Reasoning for Pluggable Types

keywords: #type-checking #type-inference #pluggable-types

Every programmer loves writing tests, but tests can’t say much about the correctness of your program. Wait a minute, what? You mean I’ve been writing tests all this time for absolutely nothing? I’ve been lied to in my undergrad software engineering course? Unfortunately, it seems like we’ve known this fact since at least 1969. A transcript from a conference on software engineering techniques sponsored by the NATO science committee contains the following quote by Edsger W. Dijkstra:

Read More

Weaving Compilers

keywords: #weaving #compilers

The past few weeks, I’ve been learning more about a few different kinds of weaving. One form of weaving is card weaving (also called tablet weaving), where the loom is instead replaced by square pieces of cardboard with holes punched in each corner. You may be wondering: how does a bunch of pieces of cardboard with holes weave cloth? I wondered the same thing myself! It seemed bonkers to think that you could do something with a bunch of cards that produced anything like fabric.

Read More

Herbie, the Numerical Compiler

keywords: #floating-point #compiler

Ten years since its inception, the Herbie project remains an active source of research and is a marquee project of PLSE. It directly spawned four publications: Herbie at PLDI 2015, Pareto-Herbie (Pherbie) at ARITH 2021, Rival at ARITH 2023, and Odyssey at UIST 2023, and influenced many more papers (an incomplete list can be found here). However, as with any long-standing project, we must question the fundamental idea behind it to inspire new directions of work. Previously, we pitched Herbie as a numerical analyst’s companion, a tool that automatically improves the accuracy of floating-point expressions. Now, we reenvision Herbie as a numerical compiler for programmers, lowering real expressions to floating-point implementations that are optimized for a given platform.

Read More

Simplifying Addition and Multiplication in Polynomials

keywords: #computer-algebra #polynomial

In my own research on Computer Algebra Systems (CAS), I often work some pretty cool data structures 😎. In this post, I want to show off one that’s responsible for simplifying polynomials. But first, I have a little secret…In high-school, I thought polynomials were boring! The hours I spent finding roots dragged on and on. They didn’t make pretty graphs like the trig functions. It’s only at this point in my life that I more fully appreciate them.

Read More

Assembly transformations against side channels

keywords: #hardware #security #side-channels

Have you ever wondered why hardware security isn’t a solved problem? It’s been six years since Spectre and Meltdown sent tech companies scrambling to fix the vulnerabilities that hardware manufacturers created with their own optimizations. Everyone involved–chip manufacturers, big tech, the security community–seems to agree that hardware security bugs are Bad and To Be Avoided. So if everyone believes that these vulnerabilies shouldn’t happen, why do they keep happening?

Read More

Designing Knitted Illusions

keywords: #knitting #design #fabrication

One of the great joys of being a researcher is observing an interesting phenomenon and deciding that you want to understand it and recreate it. Then there’s the additional joy of being a knitting researcher, and having that phenomenon be a cool object you can also display in your house or wear!

Read More

The Science of Code Formatting (Part I)

keywords: #code-formatting #pretty-printing

Code formatters are tools to make source code in a programming language easy to read. This series of blog posts presents a systematic analysis of code formatters. We aim to answer the following questions: What are the advantages and disadvantages of different kinds of code formatters (for both users and implementers)? How do they work? And what are some open problems in this space?

Read More