4
$\begingroup$

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?

$\endgroup$
3
  • 1
    $\begingroup$ Pi calculus is Turing Complete: cnd.mcgill.ca/~ivan/functions_as_processes_BFb0032030.pdf $\endgroup$
    – jmite
    Oct 3, 2016 at 3:22
  • $\begingroup$ Sure I was aware of that fact when writing this. I'm not sure that it matters or at least how it matters is very obscure to me. I'm specifically interested in programs in which the computation is a continuous reaction to a set of streams not a function on naturals. I'd wager this falls under higher type computability just for that reason alone. Either way I'd need more than just that fact. $\endgroup$
    – Jake
    Oct 3, 2016 at 3:28
  • 1
    $\begingroup$ The title you have chosen is not well suited to representing your question. Please take some time to improve it; we have collected some advice here. Thank you! $\endgroup$
    – Raphael
    Oct 3, 2016 at 7:15

1 Answer 1

5
$\begingroup$

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.

  • D. Gorla, Towards a Unified Approach to Encodability and Separation Results for Process Calculi.
  • D. Gorla, Comparing Communication Primitives via their Relative Expressive Power.
$\endgroup$
10
  • $\begingroup$ This looks promising. So a better way to ask my question might be "does lacking deadlock decrease expressiveness?". $\endgroup$
    – Jake
    Oct 3, 2016 at 21:58
  • $\begingroup$ @Jake it really depends on what you mean by deadlock, for example is $\mathbf{Nil}$, the process that does nothing, deadlocked for you or not? There are elaborate conceptions of the role of deadlocks and livelocks in process calculi. $\endgroup$ Oct 4, 2016 at 8:36
  • $\begingroup$ Yea. Part of my question was about exactly this. How does one formally define deadlock. As for the nil program I'd say it isn't deadlocked. In operational semantics I'd say its a value and thus "it doesn't get stuck" it's one of the programs for which it's OK not to have an evaluation step forward. Deadlock occurs when any non value program doesn't have a step forward I think. I'm probably missing something in that definition but I think the general idea is there. $\endgroup$
    – Jake
    Oct 4, 2016 at 13:49
  • $\begingroup$ @Jake There is terminological confusion between the concurrent/distributed systems community and the process theorists. The former thinks of a deadlock as a cycle in the waits-for graph, while the latter see a process $P$ as deadlocked if $P$ has no transitions whatsoever. Hence $Nil$ is deadlocked in process theory but not for the concurrent/distributed systems community. You can model cycle in the waits-for graph with processes, e.g. $(\nu ab)(a.\overline{b}.P \ |\ b.\overline{a}.Q)$. $\endgroup$ Oct 4, 2016 at 14:57
  • $\begingroup$ @Jake There has been a lot of work on types for concurrent processes where types gurantee certain liveness properties of processes. In such typing systems, the notion of linear (output) channel is key. If a typing systems guarantees linearity at (output) channel $x$, then an output will eventually be sent on this channel. This is a good generalisation of absence-of-deadlock in my experience. Note that in this approach it's not processes that are or are not deadlocked, but (output) channels. $\endgroup$ Oct 4, 2016 at 14:59

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.