Many verification-oriented programming languages have built-in support for attaching loop invariants to loops. A loop invariant is a condition that holds in four different places: immediately before the loop, at the start of each iteration (before evaluating the test condition), at the end of each iteration, and immediately after the loop. Usually, the invariants are… Continue reading Loop invariants – where should we put them?
It was great to have Patrick Sittel visit our group earlier this year. This blog post is about the work he and I did during his visit, which has been accepted as a paper (co-authored with Martin Kumm and Peter Zipf) at ASP-DAC 2020. Suppose we wish to fit a row of tiles to a… Continue reading Modulo scheduling with rational initiation intervals
A huge number of academic papers, particularly in the fields of computer systems/architecture, use some sort of block diagram to give readers an overview of the solution being presented. For instance, about two thirds of the papers presented this year at ASPLOS contained at least one of these diagrams, usually towards the start of the paper.… Continue reading How to draw block diagrams
UK housebuilding specifications require all doors that lead from a habitable room to the outside to meet certain "fire door" criteria. These include having a self-closing mechanism, since fire doors are only effective when they are closed. Housebuilders typically implement this specification using a simple and discreet spring that pulls the door closed. This is… Continue reading A rant about fire doors
The music for this little-known James Bond song doesn't appear in any of the official songbooks, or indeed anywhere else on the internet as far as I can tell. So here's my attempt to rectify that. Never Say Never Again (1983) Music: Michel Legrand Lyrics: Lani Hall ----------------------------- Intro: Cm, F, etc. Cm F You… Continue reading Never Say Never Again – chords
I had a great time at PLDI 2018 last week. Here is my take on a few of the papers that stood out for me. John Vilk presented a tool called BLeak for finding memory leaks in web browsers. One might think that leak detection is not important in a garbage-collected setting, but Vilk explained… Continue reading Greatest hits of PLDI 2018
I've been working in an Electrical and Electronic Engineering department for more than three years now, but I admit that it's only quite recently that I find myself properly understanding the difference between latency and throughput. These are terms that are used all the time when talking about an electronic circuit. The distinction between them… Continue reading What is the difference between latency and throughput?
I had a great time in Boulder, Colorado at the FCCM 2018 conference last week. Here are a few of the papers that I found particularly interesting: Siddhartha and Kapre's paper, Hoplite-Q: Priority-Aware Routing in FPGA Overlay NoCs, was about how to build a "network-on-chip"; that is, a miniature network that allows the various components of… Continue reading Greatest Hits of FCCM 2018
What follows is a summary of the main contributions of a paper by Nadesh Ramanathan, George Constantinides, and myself that will be presented at the FCCM 2018 conference. If you want to compute something, you have two broad options: do it in software, or do it in hardware. A custom piece of hardware can give you… Continue reading Concurrency-aware scheduling for high-level synthesis
