I'm interested in knowing things about the computability of concurrent programs. If you had a Turing complete language that also let you branch off new programs but had no means of communication between them there would be programs that you couldn't write. Namely those that required communication between concurrently running programs. At the other extreme it seems like the $\pi$-calculus can pretty well compute any program and has the power to implement almost any synchronization primitive I've ever heard of. But it also has deadlock much like Turing complete programs have infinite loops. So there seem to be degrees of power in synchronization/communication primitives although all I have figured out are extremes. This however seems analogous to programs without any kind of iteration or recursion and full Turing complete programs. One in-between would be mutexs that have levels to them at the type level. Every mutex could have levels to them at the type level. Every mutex could only be acquired if a higher mutex level had already been acquired by that thread. This would prevent deadlock but it would probably restrict some kinds of communication from occurring because the type system couldn't encode all well orderings on the mutexs (this is a bet, I have no proof). This feels analogous to something like primitive recursion or some other limited form of repeating computation (in fact, it's the kinda same problem of finding a well-ordering on objects in a program)
It's also easy to prove that a sufficiently strong language with a way to cause deadlock would not have decidable deadlock. Just replace infinite loops for dead lock in the standard proof of the halting problem. So yet again deadlock seems to have the kinds of properties that infinite looping has. On the other hand there is no way (that I know of, please tell me if this is possible) to detect infinite loops at run time but you can detect deadlock at run time. So dead lock also seems like an easier problem in a way as well.
Say I define a notion of total-program equality that goes something like "two languages are equal IFF every total program that can be written in one can be written in the other" where "total program" here is a function from naturals to naturals. More clearly stated if the set of total computable functions two languages can compute are the same then I'll call them "total-program equal". Every Turing complete language is total program equal and another neat fact is that have language that is total-program equal to a Turing complete language is not a total language! Assume that such a language existed, then an interpreter for it would be a total program that could be interpreted by a Turing complete language. Thus the supposed language could interpret itself. But such a total language (namely one which definitely has composition and paring and such) can't interpret itself so we have a contradiction. This is to say, there is no way to define a language that isn't going to contain non-total members.
I'd like to define something similar but for deadlock and the pi-calculus. Deadlock is tricky however. Separating deadlock from livelock is tricky to work with. Moreover I don't have a notion of the semantics of elements of a concurrent language. Certainly $\mathbb{N} \to \mathbb{N}$ doesn't really capture this because the programs were interested in keep outputting data on various channels as new data comes in. So there are some things that need to be formalized but basically I want a notion of "deadlock-free equivalent" languages. That is two languages are deadlock-free equivalent if the set of programs that they can define that never dead lock is the same set. Then I'd like to ask "is there a dead-lock free language that is deadlock-free equivalent to the pi-calculus?".
I don't really expect this exact question to have been answered but I was wondering if anyone has done work in this vain that I could look at? What are good models of process calculi like how $\mathbb{N} \to \mathbb{N}$ models computation. How do you formalize the difference between deadlock lock and livelock? Does being deadlock free cause such a language to not be able to interpret itself? Is there some other reason a dead lock free language as good as the pi-calculus can't exist? Answers to these questions here would be fantastic but I mainly just want to be pointed in the right direction to read further.
In a nutshell, lack of infinite loops means that you can't compute some programs even though they don't have infinite loops in them. Is the same true for deadlock? That is, will any language that never deadlocks have some programs that it can't compute?
