Before diving into the details of our first concurrency model, it will be helpful to give an overview of how we’re going to use CSP in these posts.
At the highest level, a CSP specification consists of a set of processes, which use events to describe their behavior. We use a process to represent any vantage point that lets us talk about which events occur and in which order. Each entity in our system is a process (which might be defined using subprocesses to describe each of its components or parts). We also use processes to describe how two or more entities interact with each other, and to describe any global properties of the entire system. And lastly, because CSP verification is based on “refinement”, we also use processes to define the properties that we hope our system exhibits.
Each process has an alphabet, which is the set of events that it describes (and constrains!). The process itself is the description of when each of these events can occur (and when they cannot!). There are two ways to define a process. The first is as an automaton (called an “LTS” or “labeled transition system” in the CSP literature). This is just your standard state machine, where nodes represent the current state of the process, and edges represent which events are allowed in that state (and which state you move to if the event occurs). This kind of process description is useful because you can use automated tools (like FDR) to analyze them — for instance, proving that a particular system (described by one CSP process) satisfies a particular property (described by another).
For humans, on the other hand, we define processes using CSP operators. These operators are more high-level, and more intuitive, than the lower-level LTS representation, and they line up with common patterns that we use when describing or implementing a complex system. In particular, there are several operators for combining subprocesses into larger processes, giving you full control over how the events in each subprocess interact with each other. There is a well-defined way to translate each operator into an LTS, which is what allows tools like FDR to analyze our human-readable process specifications.
Just like the real world, CSP does not impose any global ordering on any of the events in our system. We can only talk about event ordering in the context of a single process. If we want to talk about global event orderings, we have to construct a process that includes information about how all of the entities in our system participate in those events.
To dig into this paper, then, we’re going to define a CSP process for each concurrency model. The original paper uses several axioms to collectively define the behavior of each concurrency model; the more constrained models later in the paper include more axioms. We’ll define each of those axioms as a subprocess, and use CSP operators to combine them together into a single process describing the concurrency model as a whole.
We’ll also create CSP processes for each of the reference implementations. The paper then defines and uses “operational refinement” to show that each reference implementation really does implement the concurrency model in question. We’ll do something similar with CSP; we’ll make sure to construct the CSP processes for the concurrency model and for the reference implementation in such a way that we can use an FDR refinement check to show the same thing.
Read Atomic: Internal consistency