Hyphenation: when and why?

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?


Proving the existence of God using a computer

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... theory God imports Main… Continue reading Proving the existence of God using a computer

High-level synthesis, but correct

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

What’s the Rush?


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 cases in high-level synthesis (HLS).

By far the most significant way to extract high performance from a hardware accelerator in high-level synthesis is to use loop pipelining. Loop pipelining is the idea of starting the next iteration of a loop before the previous one finishes, allowing multiple iterations to be executing simultaneously. However, some loop iterations may need a result produced by earlier loop iterations, limiting the extent to which this can be done. HLS tools generally determine a ‘safe’ initiation interval – the number of clock cycles between starting two adjacent loop iterations – and…

View original post 349 more words

Understanding the memory semantics of multi-threaded CPU/FPGA programs

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: // Thread… Continue reading Understanding the memory semantics of multi-threaded CPU/FPGA programs

Introducing C4: the C Compiler Concurrency Checker

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

Fuzzing High-Level Synthesis Tools

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