PLSE Blog

As a follow up to Alexandra’s recent post about speculative execution and how your mental model of a computer is probably wrong, I thought I’d follow up with another example of how our programming abstraction has drifted from the underlying hardware implementation—this time with respect to when shared memory operations are visible to another program. These specifications, called memory consistency models (also just memory models or MCMs), are unfortunately tricky to understand and are famously ambiguously specified.

As part of my responsibilities as an industrial PhD student with PLSE and Intel, I develop and maintain, alongside my colleague and PLSE alumni Bill Zorn, a reference implementation of floating-point arithmetic. Hardware designers use this reference model to formally specify the behavior of floating point in hardware designs and verify the correctness of their implementations of these designs. Our library must not only have reasonable performance while simulating these designs and be consumable by formal verification tools for equivalence checking or property verification; but it must also correctly answer the often difficult question about floating point: “but what do it do?” With the prevalence of machine learning and its demand for ever smaller number formats for increased performance, we explored the interesting and often ridiculous world of small floating-point formats.

Speculative execution, aka speculation, is a form of computation that increasingly underlies every program our computers run. If your mental model of a CPU is a device that runs every instruction given to it, in the order given, with all prerequisite inputs gathered beforehand—wipe that model from your head, because we live in the world of speculation and Spectre.

When choosing a programming language to use for a project—or when implementing one—there are many considerations to keep in mind. One of those is whether or not the programming language uses any sort of garbage collection. Today, I’m going to talk about one method of garbage collection that we can implement ourselves fairly easily: two-space copying garbage collection.

In this post, I will relate some of the key findings and lessons learned in our 2024 ISSTA publication Equivalent Mutants In The Wild: Identifying and Efficiently Suppressing Equivalent Mutants for Java Programs (that’s a mouthful so I’ll just call it EMIW). In EMIW, my co-authors and I performed an extensive manual analysis of mutants generated for Java programs to gain insight into the types of equivalent mutants generated for real-world code. We found that a number of equivalent mutants follow simple patterns. We used these patterns to write simple, efficient static analyses, which we call suppression rules, to suppress equivalent mutants before the are ever generated. We added the suppression rules to the Major mutation framework and will refer to Major with suppression rules as EMS.

Hi friends! I’m back to discuss more accessibility improvements we’ve made to the PLSE website: how we found more issues, how we fixed them, and how we’ll (hopefully) not make these same mistakes in the future! In particular, this post touches on running automated browser tests across our entire website to flag specific types of accessibility issues. Along the way, we’ll learn about some specific web accessibility standards and how to implement them not-poorly!

Do you wonder what it’s like to do research at PLSE? If you are a student without prior research experience, the PLSE lab may seem intimidating at first. However, PLSE supports a diverse body of undergraduates working on various research topics, from software engineering questions like “How good is a test suite” all the way to compilers for hardware. Our undergrads play an integral part in the PLSE community, growing with the lab and constantly making PLSE a better place.

For the last 8 months, I’ve been working on Odyssey, a tool for analyzing floating point expressions by integrating floating point tools into one dynamic workbench. One of our big milestones is approaching, as we’ll present Odyssey at the Supercomputing Conference (SC 2024) in less than a week.

I recently submitted a data reproduction artifact accompanying our paper “Verifying the Option Type with Rely-Guarantee Reasoning.” There are things that I wish I had done from the get-go next time, so I’m writing them down in this post. Hopefully, you’ll find some of the things I write here useful in creating your own data artifacts!

Before I ever started my PhD, I could have recited to you the Curry-Howard Isomorphism: proofs are programs, and programs are proofs. But it was only when I started working on proof compilation in the interactive theorem prover Rocq (formerly known as Coq) that I feel that I truly understood it – along with why it works, why theorem provers work, and all sorts of cool tricks and connections you can use.