Logic of Concurrency

I wrote before on an algebraic theory of concurrency. The algebraic construction I gave is good for describing the semantics of a programming language. Terms in the language are mapped onto terms in the algebra, and execution is described by the equational theory of the algebra. However, the algebra is ill-suited for constructing a type system; describing terms in algebraic terms is tedious, and it's difficult to integrate the algebra with the logic of a type system.

To build a type system which can reason about concurrency, we need to design a logic that corresponds with the algebra. More concretely, we need to describe a term language and a mapping from logical terms onto algebraic ones. We also need an equational theory of logical terms (described in logic), which corresponds with the equational theory for algebraic terms.

To be clear, we'll call logical descriptions of process behaviors patterns.

The biggest challenge in doing this is that we are dealing with a predicate logic over terms of a language (and very likely, a higher-order predicate logic). In the algebra, we had a strict notion of "state spaces", which in a memory system implies a specific address space. In the logical theory, we'll likely be using a higher-order separation logic, which is a great deal more flexible in how it can reason about states. For one, separation logic can express propositions such as "no even address points to ...", "x = 5 implies y points to ..."recursively-defined states, and propositions completely independent of any state. Additionally, the logic needs to be able to introduce variables in order to deal with value bindings.

I'll deal with the issue of value bindings first. Consider the following code fragment: "λp q. x = [p]; if x = 1 then [q] = 2 else ()" (that is, a function that takes a two pointers, and stores 2 to the second if the first points to 1). The full description of this term's behavior would be (| p ↦ 1 ⊗ q ↦ v >< p ↦ 1 ⊗ q ↦ v | ⋅ | p ↦ v1 ⊗ q ↦ v2 >< p ↦ v1 ⊗ q ↦ 2 |) ⊔ | p ↦ v1 ⊗ q ↦ v2 ∧ v1 ≠ 1 >< p ↦ v ⊗ q ↦ v2 |. Of course, this contains alot of redundant information. We'd like to be able to write something more like this: (| p ↦ 1 > ⋅ < q ↦ 2 |) ⊔ | ¬ (p ↦ v1) > (we'll stick to these kinds of minimalistic terms from here on, since this is indeed how the logic works in the end). This says we can observe that p points to 1, then cause q to point to 2, or we can simply observe that p does not point to 1 (note how the observation and effect are not done atomically). The problem is we can't construct this by looking at each part of the term individually. We'd get the following (equivalent) pattern by doing it that way: | p ↦ x > ⋅ (| x = 1 >< q ↦ 2 | ⊔ | x ≠ 1 >). The problem with this term is that in a logical system, we cannot implicitly introduce the variable x. The introduction of this issue is alot longer than its solution; in a higher-order logic system, we simply introduce a new constructor which ↑ (lift), which constructs a pattern from a function from something to a pattern. The elimination rule for lift simply replaces it with a universal quantifier, and passes the quantified variable into the function. Readers familiar with logic may recognize this as how other kinds of quantifiers are synthesized in higher-order logic using universal quantifiers.

The first issue requires a bit more work to resolve. In the algebra, we define the closure operator over a particular state space. Closing over a state space treats all processes defined over that state space as isolated (meaning, they can be reduced according to the equational theory of actions). However, we have a much fuzzier notion of state spaces in the logical theory. We can tie up this loose end by defining state spaces in terms of predicates about states. A closure applies to an individual outer product if the state predicate implies the observation predicate (meaning, the P in | P >< Q |) for all states. For sequences A1 ⋅ A2, we can close over P if we can close A1 over P, and we can find some P' such that | P > A1 = A1 | P' >, and we can close A2 over P'. The rules for the other constructors are purely compositional.

Finally, in order to facilitate simpler patterns, the rules for the formation and evaluation of actions are a bit different. For starters, we allow single observations (| P >) and effects (< Q |), and products of the form | P1 >| P2 > and < Q1 |< Q2 |. The rules for inner products are also more complex, as they are now tasked with precondition/postcondition reasoning. Lastly, an observation | P > is formed from a predicate P about a state (in higher-order logic, a function from a state to a proposition), and an effect < Q | is formed from a binary predicate Q, which expresses the difference between an initial and final state.

With these constructions, it is actually rather easy to construct a language whose types can reason about concurrency. We can use the same techniques Morrisett et al used to construct a language with Hoare-Logic types, only we use patterns instead of Hoare triples.

The remaining challenges include integrating impredicative polymorphism, recursive state predicates, and subtyping.