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.
Tuesday, May 24, 2011
Friday, May 20, 2011
Algebraic Theory of Concurrency
The last thing I posted about a year ago was the beginning of work I've subsequently pursued to a concrete result. That result is an algebraic theory of concurrency, which I can use to construct a logic, and from that, a type system, both of which can reason about concurrency. There's a very strong connection to quantum theory in all this, which I'll discuss later on.
For now, I'll give an overview of the algebra. What I'm describing represents some of what is, and some of the directions I'd like to take things, so it's not necessarily mathematically rigorous. This is meant to introduce the basics of the algebra; the complete equational theory is in the tech report I wrote.
First, we need to describe states. I do this in a manner that is compatible with linear algebra. A state space is a collection of distinct elements called "states", which are closed under scalar multiplication by identity and zero. We write states using notation similar to Dirac's notation: | s > and < s |. The inner product < s | s' > is a mapping from two states to identity or zero (which I write using id and ⊥ instead of 1 and 0) such that < s | s' > = id iff s = s' and ⊥ otherwise. We can describe any memory state over a fixed address space by taking the elements of the state space to be maps from addresses to values. Also, note that any inner-product vector space can also give rise to a state space.
For any two state spaces S and T, there exists a product space S ⊗ T. We write elements of the product space using the tensor product s ⊗ t. This allows us to reason about disjoint portions of a state.
Actions represent the single, atomic actions that make up concurrent programs (such as atomic reads, writes, and more complex primitives). The algebra of actions gives us a way to sequentially compose actions into larger actions. We will use this to reason about how processes behave when running in isolation. An action is a set of strict, (Scott-)continuous functions from a given state space onto itself. I'll discuss the constructors for actions briefly.
The most basic action is the outer product, | s >< s' |, which represents a mapping some state t to the state < t | s > s'. Note that if t = s, then the result will be s', otherwise, it will be ⊥. As with quantum mechanics, we can thus reason about the composition of outer products using inner products in a straightforward manner. For example | s >< s' | composed with | t >< t ' | is | s >< s' | t >< t '|, which we can reduce by evaluating < s' | t >.
There exists an identity action id which maps each state onto itself. We will be able to give a precise definition of this later on. The empty function space is represented by ⊥ (this is distinct from the scalar ⊥, but scalar multiplication of any action by ⊥ yields the ⊥ action). The total function space is represented by ⊤.
As with states, actions are closed under tensor products. Tensor products distribute with respect to outer products as one would expect, ie. | s ⊗ t >< s' ⊗ t' | = | s >< s' | ⊗ | t >< t' |. Tensor products also have the identity property with id, ie. A ⊗ id = A.
We can represent branching and "intelligent" nondeterminism using the pointwise join of the function spaces represented by two actions. We write this as A ⊔ B. Not surprisingly, A ⊔ ⊥ = A and A ⊔ ⊤ = ⊤. The pointwise meet of two function spaces models the behavior one sees in real parallelism (or what theorists call "alternation), where if any possibility can fail, then the system can fail. We write this as A ⊓ B. Not surprisingly, A ⊓ ⊥ = ⊥, and A ⊓ ⊤ = A. Both meet and join distribute over eachother, and both distribute with tensor products. The rules for distribution with outer products are more intricate. In essence, we have that (A ⊔ B)(A' ⊓ B') = (A ⊓ B)(A' ⊔ B') = (AA' ⊔ AB' ) ⊓ (BA' ⊔ BB').
Lastly, it is often useful to talk about the differences of actions. We can model these as set differences, and the algebraic rules are exactly those from the algebra of sets (with meet and join substituted for intersection and union).
Finally, we model actual concurrent programs with processes. The main purpose of processes is to reason about how actions interleave, and to permit some notion of reasoning about isolation of portions of state. For starters, every action is also a process. There are also constructors for processes that correspond to the constructors for actions. There are meet and join constructors, tensor products, and a sequence constructor ⋅ (which corresponds to composition). These are not the same as the operators on actions, however; we cannot reduce processes by the action rules unless we know the state on which it operates to be isolated.
We represent this notion of isolation with closure. The closure operator is written as Cl[P] (normally I write a superscript denoting the state space being closed over). Closure maps processes to actions by substituting corresponding constructors. We can think of the process versions of the constructors as "frozen".
We can model recursion with recursively-defined processes. More importantly, we can model real concurrency with a derived operator ⋈, which is defined as (P1 ⋅ P2) ⋈ P = P ⋈ (P1 ⋅ P2) = ((P1 ⋈ P) ⋅ P2) ⊓ (P1 ⋅ (P ⋈ P2)) and A ⋈ A' = (A ⋅ A') ⊓ (A' ⋅ A). In other words, ⋈ represents all possible interleavings.
This finally gets us an acceptable notion of bisimilarity. Formally, we write it as follows P1 ≈ P2 iff ∀P. Cl[P1 ⋈ P] = Cl[P2 ⋈ P]. In other words, P1 is bisimilar to P2 if it behaves the same when running beside all other possible processes.
It is possible to formulate a similar reasoning system in a higher-order predicate logic (such as ECC), which can then be incorporated into a type system to allow reasoning about concurrency. I will discuss this later.
For now, I'll give an overview of the algebra. What I'm describing represents some of what is, and some of the directions I'd like to take things, so it's not necessarily mathematically rigorous. This is meant to introduce the basics of the algebra; the complete equational theory is in the tech report I wrote.
First, we need to describe states. I do this in a manner that is compatible with linear algebra. A state space is a collection of distinct elements called "states", which are closed under scalar multiplication by identity and zero. We write states using notation similar to Dirac's notation: | s > and < s |. The inner product < s | s' > is a mapping from two states to identity or zero (which I write using id and ⊥ instead of 1 and 0) such that < s | s' > = id iff s = s' and ⊥ otherwise. We can describe any memory state over a fixed address space by taking the elements of the state space to be maps from addresses to values. Also, note that any inner-product vector space can also give rise to a state space.
For any two state spaces S and T, there exists a product space S ⊗ T. We write elements of the product space using the tensor product s ⊗ t. This allows us to reason about disjoint portions of a state.
Actions represent the single, atomic actions that make up concurrent programs (such as atomic reads, writes, and more complex primitives). The algebra of actions gives us a way to sequentially compose actions into larger actions. We will use this to reason about how processes behave when running in isolation. An action is a set of strict, (Scott-)continuous functions from a given state space onto itself. I'll discuss the constructors for actions briefly.
The most basic action is the outer product, | s >< s' |, which represents a mapping some state t to the state < t | s > s'. Note that if t = s, then the result will be s', otherwise, it will be ⊥. As with quantum mechanics, we can thus reason about the composition of outer products using inner products in a straightforward manner. For example | s >< s' | composed with | t >< t ' | is | s >< s' | t >< t '|, which we can reduce by evaluating < s' | t >.
There exists an identity action id which maps each state onto itself. We will be able to give a precise definition of this later on. The empty function space is represented by ⊥ (this is distinct from the scalar ⊥, but scalar multiplication of any action by ⊥ yields the ⊥ action). The total function space is represented by ⊤.
As with states, actions are closed under tensor products. Tensor products distribute with respect to outer products as one would expect, ie. | s ⊗ t >< s' ⊗ t' | = | s >< s' | ⊗ | t >< t' |. Tensor products also have the identity property with id, ie. A ⊗ id = A.
We can represent branching and "intelligent" nondeterminism using the pointwise join of the function spaces represented by two actions. We write this as A ⊔ B. Not surprisingly, A ⊔ ⊥ = A and A ⊔ ⊤ = ⊤. The pointwise meet of two function spaces models the behavior one sees in real parallelism (or what theorists call "alternation), where if any possibility can fail, then the system can fail. We write this as A ⊓ B. Not surprisingly, A ⊓ ⊥ = ⊥, and A ⊓ ⊤ = A. Both meet and join distribute over eachother, and both distribute with tensor products. The rules for distribution with outer products are more intricate. In essence, we have that (A ⊔ B)(A' ⊓ B') = (A ⊓ B)(A' ⊔ B') = (AA' ⊔ AB' ) ⊓ (BA' ⊔ BB').
Lastly, it is often useful to talk about the differences of actions. We can model these as set differences, and the algebraic rules are exactly those from the algebra of sets (with meet and join substituted for intersection and union).
Finally, we model actual concurrent programs with processes. The main purpose of processes is to reason about how actions interleave, and to permit some notion of reasoning about isolation of portions of state. For starters, every action is also a process. There are also constructors for processes that correspond to the constructors for actions. There are meet and join constructors, tensor products, and a sequence constructor ⋅ (which corresponds to composition). These are not the same as the operators on actions, however; we cannot reduce processes by the action rules unless we know the state on which it operates to be isolated.
We represent this notion of isolation with closure. The closure operator is written as Cl[P] (normally I write a superscript denoting the state space being closed over). Closure maps processes to actions by substituting corresponding constructors. We can think of the process versions of the constructors as "frozen".
We can model recursion with recursively-defined processes. More importantly, we can model real concurrency with a derived operator ⋈, which is defined as (P1 ⋅ P2) ⋈ P = P ⋈ (P1 ⋅ P2) = ((P1 ⋈ P) ⋅ P2) ⊓ (P1 ⋅ (P ⋈ P2)) and A ⋈ A' = (A ⋅ A') ⊓ (A' ⋅ A). In other words, ⋈ represents all possible interleavings.
This finally gets us an acceptable notion of bisimilarity. Formally, we write it as follows P1 ≈ P2 iff ∀P. Cl[P1 ⋈ P] = Cl[P2 ⋈ P]. In other words, P1 is bisimilar to P2 if it behaves the same when running beside all other possible processes.
It is possible to formulate a similar reasoning system in a higher-order predicate logic (such as ECC), which can then be incorporated into a type system to allow reasoning about concurrency. I will discuss this later.
Restarting
I've not posted in this logbook in quite some time. I've been extremely busy, first as a research intern with IBM Research last summer, and then working on a project which serves as a Ph.D qualifier. However, after lunch yesterday here at IBM (I'm an intern again this summer), I've decided I'm going to start writing again.
It'll probably take me a while to write out all the various ideas I've had over the past year, but hopefully it should be interesting.
It'll probably take me a while to write out all the various ideas I've had over the past year, but hopefully it should be interesting.
Subscribe to:
Posts (Atom)