So when programming with locks as a synchronization primitives you can ensure no deadlock by ensuring that an ordering exists on the locks and that all acquires of the locks happen in that order (which really just needs to be a well founded quasi-order). This lends itself to lots of different kinds of solutions to dead lock. You can bake this into the type system itself by demanding that locks have a number associated with them at the type level and that acquiring a lock demands that an already acquired lock of a higher level be passed to it.

Deadlock can also occur when working with channels however. For instance I could wait on receiving something on a channel and never ever get it. I could also, in the case of $\pi$-calculus get stuck waiting on something to send too. Additionally cycles of waiting to receive things can occur which is more like the deadlock that occurs with locks. This leads me to think that some kind of ordering constraint plus a constraint that rules there not being an active sender/reciver on the other side might be helpful.

Is there a similarly helpful condition one can impose on channels to disallow deadlock? Is there a process algebra (weather it uses channels or not) that does not have dead lock?

  • $\begingroup$ Have you looked at the session types literature (Honda, Yoshida and many others) ? A few other keywords: global types, choreographies, behavio(u)ral types. These can guarantee progress in distributed computations. $\endgroup$ – chi Jul 11 '16 at 17:09
  • $\begingroup$ That gives me a lot to look at! Thanks! Could you give me a tl;dr on these different topics or some links to good introductory literature? I can't seem to get a feel for these things by reading sporadic literature that usually is expanding upon these ideas not introducing them. $\endgroup$ – Jake Jul 12 '16 at 4:36

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.