The Hoare Cube – Wickopedia
I wrote earlier this year about my attempt to understand the repercussions of toggling $latex \subseteq$ and $latex \supseteq$ when giving a semantics to Hoare triples. In response to that post, Ya…| Wickopedia
Ilan Iwumbwe and Benny Liu did undergraduate research placements with me this summer, and I’m very pleased that they will be presenting their work at the Programming Languages for Quantum Computing (PLanQC) workshop at POPL next month. Ilan and Benny built a tool called QuteFuzz that randomly generates descriptions of quantum circuits. The idea is… Continue reading Fuzzing Quantum Compilers→| Wickopedia
I wrote earlier this year about my attempt to understand the repercussions of toggling $latex \subseteq$ and $latex \supseteq$ when giving a semantics to Hoare triples. In response to that post, Ya…| Wickopedia
The UK government imposes a tax on people’s income, and, as is quite conventional, the rate at which a person pays this tax increases as their income increases. However, I was surprised to notice recently that this rate does not increase monotonically with income. Here is how the UK government explains the calculation of income… Continue reading Fun with income tax→| Wickopedia
This post provides a short introduction to a paper that will be presented at DVCon in Munich next month by my PhD student Michalis Pardalos about work we have done with collaborators Alastair Donaldson, Emi Morini and Laura Pozzi. Hardware engineers take great care to ensure that their designs are correct. Unlike bugs in software,… Continue reading Who checks the equivalence checkers?→| Wickopedia
I’m delighted that Quentin Corradi, a PhD student I jointly supervise with George Constantinides, will be presenting his work to improve the reliability of hardware design tools next week at …| Wickopedia
I was singing Freddy, My Love as a lullaby for my toddler last night, and enjoying the nifty rhyming triplets (catches–patches–matches, and so on), when I suddenly realised that the song has almost…| Wickopedia
I’ve used Santander Cycles to get from King’s Cross to Imperial College hundreds of times over the last couple of years, and I’d like to think that I’m pretty close to finding the fastest possible route now. The basic route is to aim for New Cavendish Street and then cross Hyde Park, but I’ve found… Continue reading Cycling from King’s Cross to Imperial College London→| Wickopedia
Yann Herklotz has added hyperblock scheduling to his verified high-level synthesis (HLS) tool called Vericert, and I’m very pleased that our paper about this work has been accepted to appear at PLDI 2024 this June. This paper was our “difficult second album”, in the sense that we’d already published a paper about the first version… Continue reading Verified high-level synthesis – now with hyperblocks!→| Wickopedia
The Hoare triple has a very simple meaning, namely: . That is: if the precondition is satisfied in some state , and can transform into , then must satisfy the postcondition . (We’ll allow non-deterministic commands, so need not be uniquely determined by and .) Or, more concisely: if holds before executing , then will… Continue reading What is the other Incorrectness logic?→| Wickopedia
The world of computer architecture is quite excited these days about something called Compute Express Link (CXL). It’s a new standard that allows the various components of a datacentre computer to communicate large amounts of data efficiently with each other. In this article, I’ll explain what CXL is, and why there is so much excitement… Continue reading CXL: What’s all the fuss about?→| Wickopedia
I’ve commuted via King’s Cross St Pancras to Imperial College’s South Kensington Campus for about a decade now, but have only recently discovered what I believe to be the fastest possible route between those two London stations. King’s Cross St Pancras to South Kensington takes me about 20 minutes, and the return journey takes about… Continue reading The fastest route between King’s Cross St Pancras and South Kensington→| Wickopedia
When writing multi-word adjectives, hyphens can be important. But many writers use either too many or too few. This blog post is my attempt to clarify the situation (as I understand it). The basic issue is that “adjective noun noun” can be hard for readers to parse. The default is to understand it as (adjective… Continue reading Hyphenation: when and why?→| Wickopedia
My friend and colleague George Constantinides wrote an interesting post on his blog recently where he formalises St Anselm’s argument for the existence of God. Since I’m teaching a course on the Isabelle proof assistant this term, I thought I’d see if I could recreate that argument using Isabelle. Here goes… As can be seen… Continue reading Proving the existence of God using a computer→| Wickopedia
A little old lady worked all on her own On a paper about a result she had shown. A wise old man heard her grumble and rage: "There’s not enough room on my page! Wise old man, won’t you help me, please? My paper’s a squash and a squeeze."… Continue reading “A Squash and a Squeeze” – Academic Edition→| Wickopedia
FCCM 2022 in New York City has just drawn to a close, so I thought I’d put down some thoughts about my experience while it’s fresh in my mind. As my first in-person conference since covid, my expectations were sky high, and I’m very pleased to report that my expectations were well and truly met… Continue reading Some reflections on FCCM 2022→| Wickopedia
When playing the board game Cluedo (also known as Clue in North America), you make a series of hypotheses that consist of a murderer, a weapon, and a room. In each hypothesis, the room has to be the room your piece is currently in, and the player to your left always has the first opportunity… Continue reading The “Cluedo” effect in randomised testing→| Wickopedia
This post is about a paper by Yann Herklotz, James Pollard, Nadesh Ramanathan, and myself that will be presented shortly at OOPSLA 2021. High-level synthesis (HLS) is an increasingly popular way to design hardware. It appeals to software developers because it allows them to exploit the performance and energy-efficiency of custom hardware without having to learn… Continue reading High-level synthesis, but correct→| Wickopedia
Originally posted on Thinking: At FPL 2021, my PhD student Jianyi Cheng (jointly supervised by John Wickerson) will present our short paper “Exploiting the Correlation between Dependence Distance and Latency in Loop Pipelining for HLS”. In this post, I explain the simple idea behind this paper and how it can significantly accelerate certain neglected corner…| Wickopedia
If you’ve ever attended a seminar about weak memory models, chances are good that you’ve been shown a small concurrent program and asked to ponder what is allowed to happen if its threads are executed on two or three different cores of a multicore CPU. For instance, you might be shown this program: and asked… Continue reading Understanding the memory semantics of multi-threaded CPU/FPGA programs→| Wickopedia
This post is about a paper by Matt Windsor, Ally Donaldson, and myself that will presented shortly at the ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA) conference, in the tool demonstrations track. Compilers are a central pillar of our computing infrastructure, so it’s really important that they work correctly. There’s been a… Continue reading Introducing C4: the C Compiler Concurrency Checker→| Wickopedia
High-level synthesis – the automatic compilation of a software program into a custom hardware design – is an increasingly important technology. It’s attractive because it lets software engineers harness the computational power and energy-efficiency of custom hardware devices such as FPGAs. It’s also attractive to hardware designers because it allows them to enter their designs… Continue reading Fuzzing High-Level Synthesis Tools→| Wickopedia
Your task is to write down a sequence of English words that, after possibly moving around the spaces between the words, become their German translations. As stated, this is pretty easy: for instance, I could write down the single English word SAND which translates to the single German word SAND. Or I could be a… Continue reading A translation puzzle→| Wickopedia
T-diagrams (or tombstone diagrams) are widely used by teachers to explain how compilers and interpreters can be composed together to build and execute software. In this blog post, Paul Brunet and I revisit these diagrams, and show how they can be redesigned for better readability. We demonstrate how they can be applied to explain compiler… Continue reading Diagrams for Composing Compilers→| Wickopedia
Originally posted on Dan's Blog: If I visit an exotic destination, I would surely do some sightseeing. I would cycle to that destination and I would use Google Maps for navigation. At most crossroads, I need to know in which direction I should turn. Other apps running on my phone might delay the indications…| Wickopedia
Here are a few personal highlights from the FPGA 2020 conference, which took place this week in Seaside, California. (Main photo credit: George Constantinides.) Jakub Szefer‘s invited talk on “Thermal and Voltage Side Channels and Attacks in Cloud FPGAs” described a rather nifty side-channel through which secrets could be leaked in the context of cloud-based… Continue reading Highlights from FPGA 2020→| Wickopedia
The concept of “odd” and “even” functions is quite important in areas such as Fourier analysis. An odd function is one that has 2-fold rotational symmetry around the origin;…| Wickopedia
When you want to do some computation on an FPGA, it is traditional to enter your design in a language like Verilog, and then to use automatic synthesis tools to turn your Verilog design into a “configuration bitstream” that can be fed to your FPGA to make it perform the computation you want. These synthesis… Continue reading Fuzzing FPGA synthesis tools→| Wickopedia
In this post, I’d like to share some thoughts I’ve accumulated over the past few years about how to draw better graphs. To get straight to the point, I have two concrete recommendations: normalised data should usually be plotted on a logarithmic scale, and scatter plots can be easier to understand than bar charts. I’ll… Continue reading A plot twist! Drawing better graphs in PL papers→| Wickopedia
A lot of papers include a graph that benchmarks the performance of a new technique against a technique from previous work. Such a graph might look like this: The graph is rather straightforward to read: when the green bar is higher, the old technique is faster, and when the red bar is higher, the new… Continue reading In praise of scatter plots→| Wickopedia
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?→| Wickopedia
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→| Wickopedia
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→| Wickopedia
| Wickopedia
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→| Wickopedia
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→| Wickopedia
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→| Wickopedia
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?→| Wickopedia
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→| Wickopedia
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→| Wickopedia
I’m delighted that Luke Geeson’s work on “mix testing” (a collaboration with James Brotherston, Wilco Dijkstra, Alastair Donaldson, Lee Smith, Tyler Sorensen, and myself) will app…| Wickopedia
