Two years ago, I started writing a series of blog posts about CSP — Communicating Sequential Processes. That series has…let’s say “stalled”. Part of the reason is that I didn’t have a good non-trivial example to work with. The stereotypical running example is the vending machine: start with a simple one, which accepts a single coin and spits out a tea; add more detail as you introduce more of the language. I always had a hunch that I needed an example with more meat on it, but could never find one.
Fast-forward to today. I was reading through some of Christopher Meiklejohn’s work on Lasp, I came across a citation to a really nice paper by Cerone, Bernardi, and Gotsman, which adds some formal rigor to the consistency models that we use to describe modern distributed systems. Their formalism is a great combination of simple and expressive. The core of the paper is about processes accessing a transactional data store; the authors provide formal definitions of several concurrency models, and of some reference implementations that supposedly provide those concurrency models. They then use a technique called “observational refinement” to show that the reference implementations really do provide the concurrency guarantees in question.
This approach lines up very well with how you perform refinement checks in CSP to show that systems satisfy some specification. And so I finally found my meaty running example! I’m resurrecting this blog series, and plan to work through each of the consistency models and proofs described in the paper, translating them into CSP processes and refinement checks. This isn’t an attempt to replace or outdo anything in the paper! Far from it — it’s my attempt to use something more familiar to work through the details of something less familiar.
I’m not going to assume a working knowledge of CSP — or of the consistency models described in the paper! If you’re familiar with one, my hope is that you’ll be able to follow along and pick up the other. And if you’re not familiar with either…well, I guess we’ll see how good I am at writing an intro to a difficult topic!