Concurrency Formalisms

Why?

Theories organize knowledge so that we have a consistent and well-understood vocabulary to explain and predict phenomena. When accompanied by formalisms, the language of a theory becomes precise and (hopefully) unambiguous.

Because concurrent systems are so complex, and the cost of achieving correctness and security so high, good theories and formalisms are essential to better understand and design such systems.

Let’s divide theoretical and formal approaches to concurrent system design and verification into four parts:

• Temporal Logics (for philosophy, math, and computer science)
• Process algebras and process calculi (for computer science)
• Design notations such as Petri Nets, Statecharts, and UML (useful for engineers and hardware and software architects)
• Model checkers and similar verification systems (useful for developers and QA and security engineers)

Temporal Logics

A temporal logic is a kind of modal logic that helps us talk about time. It gives rigorous syntax and semantics for terms such as now, before, after, always, never, until, henceforth.

Temporal logics are covered on this page, though you may want to start with an overview of logic itself first.

Process Calculi

Temporal logic lets us talk about time from a philosophical or mathematical perspective. When we begin to focus on computation, we have the need to talk not just about events, but of processes. We need something more than a logic to describe computations in time. We need an algebra or calculus of processes.

Nomenclature

In case you are wondering: there is no difference between a process algebra and a process calculus. Those terms denote the same idea. Wikipedia’s article is entitled Process calculus. If you go to the Process algebra page, it will redirect you to the Process calculus page. Same thing.

Process algebras provide mathematical notations and methods to model and precisely analyze and verify the behavior of concurrent and distributed systems. The processes themselves, and the interactions between them, are entities which are manipulated and reasoned about. Some allow us to say that two processes are equivalent, while others allow us to refine one process into another, more complex one, aiding proofs of correctness and security.

Here are some of the big ones:

A few are covered in these notes.

Other Formalisms

Now we move from the philosophical-mathematical-theoretical domain to something that engineers will enjoy. Real practical notations, with circles, boxes, arrows, and other shapes! Graphical formalisms that describe the intended structure and behavior of real-world systems.

Two classic models are:

• Petri Nets, created by Carl Adam Petri in 1939, are a graphical and mathematical modeling tool for describing and analyzing systems with concurrent, asynchronous, distributed, parallel, nondeterministic, and stochastic behaviors.
• Statecharts, a visual formalism for complex systems created by David Harel in 1987. They extend finite state machines with hierarchy, concurrency, and communication. You can read Harel's original paper online. Wikipedia covers them in a small section within its State Diagram article.

Statecharts were a big influence on UML’s state diagrams. As UML is a bit more modern (not to mention standardized), it’s best to familiarize yourself with the various UML diagrams for modeling concurrent systems—especially state, communication, activity, and sequence diagrams—and read about statecharts for their historical influence.

See these notes for more.

Model Checking

Let’s not forget about the QA and security people, and the really cool developers and architects that actually care about correctness and security, and bring in the tools for system verification. A model checker is a tool for verifying that a (state-based) system satisfies certain requirements (such as correctness, safety, and liveness).

Wikipedia references:

• Model Checking
• List of Model Checking Tools

Recall Practice

Here are some questions useful for your spaced repetition learning. Many of the answers are not found on this page. Some will have popped up in lecture. Others will require you to do your own research.

1. What is a theory?
   An organized body of knowledge with explanatory and predictive powers
2. What is a formalism?
   A precise and unambiguous language for a theory
3. What are the four areas of study within concurrency formalisms?
   Temporal logics, process algebras, design notations, and model checkers
4. What is a process algebra?
   A mathematical notation and method to model and analyze concurrent and distributed systems
5. What is the difference between a Process Algebra and a Process Calculus?
   There is no difference; they are the same thing
6. What are Robin Milner’s two big contributions to process algebras?
   Calculus of Communicating Systems (CCS) and Pi Calculus
7. Who invented Petri Nets and in what year?
   Carl Adam Petri, in 1939
8. Who invented Statecharts and in what year?
   David Harel, in 1987
9. What are some modern notations for concurrent systems?
   UML state, communication, activity, and sequence diagrams
10. What is a model checker?
    A tool for verifying that a system satisfies certain requirements (such as correctness, safety, and liveness)

Summary