patternMinor
How does lack of deadlock relate to computability in process calculi?
Viewed 0 times
processdeadlockcalculicomputabilityrelatelackdoeshow
Problem
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
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
Solution
I think you are asking about expressivity of concurrent programming languages. This is a deep and not well-understood field. For example you say that "the $\pi$-calculus [...] has the power to implement almost any synchronization primitive I've ever heard of". It is well known that the $\pi$-calculus cannot implement broadcasting (see e.g. here). The $\pi$-calculus can also not implement $n$-ary synchronisation (think Petri nets) for all $n > 2$, and $\pi$ can also not
implement Ambient-calculus. Moreover, full mixed choice cannot be implemented by the asynchrnous $\pi$-calcululs, this is an old result by Palamidessi. There are more such results.
What I have not said here is what it means precisely for one calculus to implement another (or being unable to do so). There is no general agreement. For more on this, I suggest to consult the following.
implement Ambient-calculus. Moreover, full mixed choice cannot be implemented by the asynchrnous $\pi$-calcululs, this is an old result by Palamidessi. There are more such results.
What I have not said here is what it means precisely for one calculus to implement another (or being unable to do so). There is no general agreement. For more on this, I suggest to consult the following.
- D. Gorla, Towards a Unified Approach to Encodability and Separation Results for Process Calculi.
- D. Gorla, Comparing Communication Primitives via their Relative Expressive Power.
Context
StackExchange Computer Science Q#64153, answer score: 5
Revisions (0)
No revisions yet.