## Greatest hits of PLDI 2018

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

## Concurrency-aware scheduling for high-level synthesis

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

## What do you get if you cross Weak Memory with Transactional Memory?

What follows is a summary of the main contributions of a paper I wrote with Nathan Chong and Tyler Sorensen for the PLDI 2018 conference. This project studies two features of a modern computer, one called out-of-order execution and one called transactional memory. Out-of-order execution is where a computer chooses, for performance reasons, to perform its instructions in an order… Continue reading What do you get if you cross Weak Memory with Transactional Memory?

## Ribbon Diagrams for Weak Memory

In their POPL'17 paper, Shaked Flur, Susmit Sarkar, Christopher Pulte, Kyndylan Nienhuis, Luc Maranget, Kathy Gray, Ali Sezgin, Mark Batty, and Peter Sewell describe a semantics of weakly-consistent memory that copes (for the first time) with mixed-size memory accesses. In this blog post, I describe how their semantics can be explained rather nicely with some graphical… Continue reading Ribbon Diagrams for Weak Memory

## Translating lock-free, relaxed concurrency from software into hardware

What follows is a summary of the main contributions of a paper I wrote with Nadesh Ramanathan, Shane Fleming, and George Constantinides for the FPGA 2017 conference. Languages like C and C++ allow programmers to write concurrent programs. These are programs whose instructions are partitioned into multiple threads, all of which can be run at the same time.… Continue reading Translating lock-free, relaxed concurrency from software into hardware

## Memory Consistency Models, and how to compare them automatically

My POPL 2017 paper with Mark Batty, Tyler Sorensen, and George Constantinides is all about memory consistency models, and how we can use an automatic constraint solver to compare them. In this blog post, I will discuss: What are memory consistency models, and why do we want to compare them? Why is comparing memory consistency… Continue reading Memory Consistency Models, and how to compare them automatically

## cppreference.com gets acquire/release instructions wrong

It is quite well-known that the memory operations and fences provided by the C/C++11 languages are pretty complicated and confusing. For instance, my OOPSLA 2015 paper (joint with Batty, Beckmann, and Donaldson) explains that a proposed implementation of these instructions for next-generation AMD graphics cards is faulty because the designers misunderstood how they worked. And… Continue reading cppreference.com gets acquire/release instructions wrong

## Why we should plot normalised data on a logarithmic scale

I believe that normalised data should be plotted on a logarithmic scale. (By "normalised data", I refer to data that is the ratio between two measurements that have the same dimension. Examples of such data include the ratio between the execution time of a program before a proposed compiler optimisation has been applied and the execution time of that program… Continue reading Why we should plot normalised data on a logarithmic scale

## Partial and total correctness as greatest and least fixpoints

This short note explains how partial and total correctness triples can be characterised as the greatest and least fixpoints, respectively, of the same function. Suppose we have a small-step transition relation $latex \rightarrow$ between configurations. Configurations comprise a command $latex C$ and a state $latex \sigma$. Given an initial configuration $latex (C_0,\sigma_0)$, we can produce… Continue reading Partial and total correctness as greatest and least fixpoints

## “Concurrent Buns” – A chef’s guide to concurrency verification

Sequential recipes Consider the recipe for making breakfast that is presented in Figure 1, below. An arrow from one step to another indicates that the first step must be completed before the second may commence. The recipe, as presented, fails to convey the fact that many of the steps can be swapped around. For instance,… Continue reading “Concurrent Buns” – A chef’s guide to concurrency verification