Beginnings of a Theory of Concurrent Processes

First post in a very long time. I've been working on things that will be turned into intellectual property one day, so I can't post in the clear about them. However, this pertains to my first potential PhD thesis topic...

I'm pulling ideas together for a general theory of concurrent processes. First, background. One of my older interests, π-calculus and its predecessor, CPS both describe concurrent execution using synchronous channels, which are a very peculiar construction. They are peculiar in that they effectively step two threads (processes) at once. I was actually able to use this property to set up two separate proofs (which I have yet to successfully publish). The primary shortcoming of π-calculus is that it cannot describe the more common model of shared-heap interactions. This is where I'm trying to go, of course.

The theory I'm developing thus far is actually very general. I'm hoping that by taking this approach, I can avoid getting entangled in the nastiness of memory semantics. Also, quantum mechanics has been an excellent source of ideas for my efforts thus far. Entanglement, operators, tensor products, the Quantum Cloning Theorem, and others all seem to have analogs in concurrent execution. This of course makes sense; quantum mechanics describes general physical systems; my theory will describe general computational systems. The remainder here will be very much scrawled notes, interspersed with more coherent thoughts, as are my thoughts at this point.

In general, states are sets of propositions. I'm unsure about the exact details. There's several ways I can go here. One approach is to model them as a kind of "value space": that is, a mapping from coordinates (which, in computing will be one-dimensional and discrete (and total-ordered, with multiply and add and the ring laws, blah blah) but nothing prohibits more exotic constructions) to values of some kind, and with more general properties providing more abstract reasoning ability. This is nicely close to computation. Another approach is simply "sets of truthful propositions", or "truth assignments of propositions". This is nice because it can reason about anything, not just computation. But it begs for a minimal basis set (and computational states are notoriously high-dimensional). It also raises the question of relevance. Logic-as-space is to my knowledge unexplored, relevance logic is quite well explored (it's basic substructural logic, probably the least-used variation). Somewhere in the middle might be the best approach.

I've made more progress with regard to semantics. I'd like to get away with not tying my theory to any one representation of processes, but I've managed to redesign programming language semantics in a way that enables this, and gives rise to a very elegant construction of synchronization as well.

You can also apply quantum mechanics' tensor products and entanglement to the descriptions of state. Separation logic is invaluable when it comes to describing propositional states. It permits isolation. The tensor product ⊗ in quantum mechanics is completely analogous. The Quantum Cloning Theory also comes to bear. In quantum mechanics, you cannot "split" a quantum state without having it be entangled with its original. A similar theorem applies to states. You can easily split a state with a separating conjunction, so as to reason about how two processes act upon it, assuming you can cleanly separate it. However, if you can't then you get two states which affect eachother (quantum entanglement).

I call it differential semantics. Most semantic descriptions of stateful languages simply include the state in their operational semantics. The differential semantic approach is to describe the possible observations and effects that a given process can cause on state. This makes building a type system for describing concurrent effects easier, and it also removes the state from all semantic descriptions. The semantics are blind to any real state; they reason only about what might possibly happen. Extend this to synchronization, and you get another elegant description of something that's usually very messy: possible future semantics. We can describe synchronization in terms of possible outcomes, rather than getting into the ugly details of how it might be implemented (and losing generality). The huge advantage of this approach is that it can turn synchronization problems into classical computing problems, and then you can reason about their difficulty. I used this to show that combining synchronous channels and transactions yields a synchronization problem equivalent to solving SAT problems. A very useful result would be finding the point at which a system requires global synchronization (which is bad)

I've described a language using differential semantics, but I've not yet extended the approach to general possible-future semantics. This is largely because my type system can't reason about the behavior of multiple threads.

To pull this off, I really need four things: a way to reason from sequences of observation/effect pairs to possible futures, a way to treat groups of threads as a single thread, a way to describe the interactions of possible futures without getting bogged down in a mess, and design a type theory that can reason about the interactions amongst multiple threads.

If I can pull all this off, and wrap it up in a nice package, with all the theoretical heavy-lifting done, then I may very well have a thesis topic...