A Peek into Concurrency and Distributed Systems through the Lens of

The shared memory consistency model is the critical hardware-software interface in multiprocessors that specifies what value a read must return. However, this seemingly simple interface has been facing a number of notorious challenges including: (1) unclear specification; (2) implementation riddled with bugs; (3) tension between programmability and efficiency.

In this talk, I will first overview the work we've been doing for the past decade in addressing these challenges. Midway into our research, we realised a couple of key insights: (1) Hardware design for shared memory should not be guided by ad-hoc informal specifications. Instead, we advocate for implementations to be derived from the specification through a series of refinements. This not only leads to designs that are correct but also (somewhat surprisingly) to designs that are efficient. (2) Although today's distributed systems (e.g. a distributed key-value-store in a datacentre) don't look anything like "shared memory", they fundamentally share state and hence there is an opportunity of the exchange of ideas between distributed systems and computer architecture communities.

Based on these realisations, I will outline our vision for synthesizing efficient and correct-by-construction distributed systems---a problem that has had a rich history including at Edinburgh---but one whose time has come.