tl;dr CSP is a formal method that lets you describe and reason about the behavior of concurrent systems. CSP is composable; you write simple processes, and then use special operators to combine them together into larger, more complex processes. A process is a summary of some system; it uses events to describe how that system works, and to synchronously communicate with other processes. You can compare two processes using a refinement check; this lets us check, for instance, whether a real-world system satisfies some important safety or liveness property. CSP has good tool support, which lets us perform these refinement checks quickly and automatically.
Well that was easy, wasn’t it? You can boil just about anything down to a single paragraph. Let’s look at each of those key points in more detail.
CSP is a formal method, which means that the language has a very precise mathematical definition. This is what allows us to reason about a system that has been described in CSP: the language defines several different semantics, which are mathematical rules that describe how a CSP model behaves. Those rules let us verify whether the model satisfies some property that you care about. If your model accurately describes your real-world system, then any conclusions that we can draw about your model also apply to your system.
Of course, it’s up to you to create a CSP model that accurately describes your real-world system. For a large and complex system, it might not be immediately obvious how to describe the system in CSP. That said, the language’s operators line up pretty well with the techniques we use to implement real-world systems, so once you’ve learned the language, it’s usually straightforward to construct a CSP model for the system you want to analyze.
CSP is also a process calculus, which is a particular kind of formal method that focuses on concurrent systems. A concurrent system is one that is divided into several smaller parts or subsystems. For the most part, each of these subsystems operate independently; however, they can also collaborate by sending messages to each other.
This modeling approach is very similar to how we actually design complex systems: we create small, highly focused subsystems that are responsible for portions of the overall behavior, and we keep the interaction points small so that we can understand how the parts work together to implement the whole.
Note that concurrency is a design technique, which you think about while architecting and implementing your system. It’s not the same as parallelism, which is an optimization technique. Concurrency lets you simplify your design by dividing up responsibilities among different subsystems. Parallelism only comes into play when your system is up and running: you try to do multiple things simultaneously (or “in parallel”) so that you can finish the overall job faster. The two are definitely related — you can’t execute two things in parallel unless they were already concurrent — but they’re not the same thing. Since CSP is a modeling language, it’s focused on concurrency, not parallelism.
In CSP, each system and subsystem is modeled by a process, which describes a particular pattern of events that can occur. These events provide a summary of the internal behavior of the process. Processes are very similar to state machines; you can think of events as evidence of a process moving from one state to another. Events usually correspond to a real-world condition that you want to detect or action that you want to control. When modeling a system using CSP, one of your most important steps will be deciding which events to use, and what those events represent.
CSP is composable — once you’ve defined the CSP processes for your small subsystems, you use one of CSP’s composition operators to join those subsystems together into a larger, more complex process. There are several composition operators to choose from, depending on how each of the subsystems should interact with each other.
This approach makes it much easier to model and reason about a complex system: each subsystem is small enough that you can understand how it works, and the composition operators provide well-defined rules for how those smaller pieces work together to produce some more complex behavior.
CSP events not only describe the behavior of individual processes; they also allow multiple processes to communicate with each other. If two processes both include the same event, then when you compose those processes together, that event becomes a communications channel that links the two processes.
For example, a CSP process that models a vending machine might use an event
called coin to detect when someone has inserted a coin into the machine. A
second CSP process that models the person using the machine would use this same
coin event to represent the act of inserting a coin into the machine. When we
compose these two processes together, we get a new process that represents the
interaction between the person and the machine.
One of the most important features of CSP is that all communication is synchronous. When two processes communicate via an event, that event will either occur simultaneously in both processes, or it won’t occur in either. In our example, this means that the machine won’t detect a coin if the person never inserted one; and vice versa, that the person can’t insert a coin without the machine detecting it.
The main reason for using a formal method to model a real-world system is so that you can verify some properties of that system. For instance, with our vending machine, we might want to make sure that “if you insert a coin, you either get a drink or you get your coin back.”
In CSP, you do this using a refinement check. “Refinement” is the mathematical term for the particular way that we compare the behavior of two processes. If you have a CSP process describing your system, and another describing the property you want to verify, then a refinement tells you whether the system satisfies that property. More importantly, the refinement doesn’t just tell you “yes” or “no”; it also provides a proof or a counterexample automatically.
This is true of all formal methods — the entire reason for using a formal method is so you can perform these rigorous checks using well-defined rules, which give you proofs about the properties that you care about. That said, CSP differs from most other formal methods in that you use the same language to describe your system and the properties that you want your system to have. In other formal methods, you use one language to describe your system, and a completely different language to describe the properties that you want to check. In CSP, you use processes and events to describe both.
Refinement checks are nice, but they’d be rather pointless if we had to do them by hand. Our real-world systems are usually too large and complex for that to be practical. If you have to write hundreds of pages of detailed mathematical proof to convince yourself that your system satsifies a safety property, then the benefit of having that mathematical proof isn’t worth the cost of producing it.
That means that to be useful, a formal method needs to have good tool support. For CSP, the tool of choice is FDR. You provide machine-readable descriptions of your CSP processes, and ask it perform refinement checks for you. It also provides a nice user interface for viewing counterexamples, to help you identify which parts of your system violate the properties that you’re checking.