Box calculus is a new process algebra that seems to have a relatively simple Petri net semantics. The purpose of this new algebra is to be able to translate real-life parallel programs into a set of algebraic rules and then to prove interesting properties of the programs in a mathematically rigorous fashion. The authors apply the technique to two traditional well-known mutual exclusion algorithms--Dekkar’s and Dijkstra’s--and rigorously prove that these algorithms are really deadlock-free, starvation-free, and fair. The authors also claim that this new process algebra provides more concise ways of writing parallel programs and makes it easier to make claims about properties without using operational arguments.

The paper is theoretical and should be mildly interesting to Petri net researchers. It is highly readable, lucid, and self-contained; the concepts of S-invariants and traps may be useful in analyzing other parallel programs. You do not need to know box calculus to understand the paper, but general familiarity with Petri nets and process algebras in general will enhance understanding.