Hacker News Reader

Comment by qaq | Hacker News Reader

Is there a language where deadlocks are not possible ?

Yes, Idris. Dependent types in an effect system allow you to prove that deadlock cannot occur, such that a potential deadlock in user code is a compile time error. Edwin Brady has been working on this for decades[1], and Idris 2[2] has finally made it a reality[3].

1. https://www.type-driven.org.uk/edwinb/papers/fi-cbc.pdf (free; 2009)

2. https://livebook.manning.com/book/type-driven-development-wi... (registration wall; 2017)

3. https://research-repository.st-andrews.ac.uk/handle/10023/23... (free; 2021)

Avoiding deadlocks is easy if you're lockfree (or otherwise non-blocking), the interesting bit is being data-race free:

https://www.ponylang.io/discover/#what-makes-pony-different

> Avoiding deadlocks is easy if you're lockfree (or otherwise non-blocking)

Only if you’re also concurrency free.

If you can still have two actors waiting on one another, you’re letter-of-the-law deadlock-free, but your program is still in effect deadlocked.

> the interesting bit is being data-race free:

Data race freedom is much weaker (and easier) than deadlock freedom, or race condition freedom.

Safe rust is free of data races for instance. But still subject to deadlocks, and other race conditions.

> Only if you’re also concurrency free. If you can still have two actors waiting on one another, you’re letter-of-the-law deadlock-free, but your program is still in effect deadlocked.

I'm not sure we're using the same definitions. If you're non-blocking you have system wide progress, I'm not sure your examples of two actors mutually waiting on each other qualify.

In any case I think Pony qualifies as wait-free too, which avoids this scenario. Of course one can still have an infinite for loop, or an infinite ping-pong between actors.

> I'm not sure your examples of two actors mutually waiting on each other qualify

Of course it qualifies, that's a classical text book example of deadlock.

Isn't that a live lock?

Can anything really shield you from that? It seems nothing can, in the same way nothing can really shield you from an infinite loop.

> Isn't that a live lock?

If they are blocked it is not a live lock. If they are spinning in a try_read then it would be a live lock.

> Can anything really shield you from that? It seems nothing can, in the same way nothing can really shield you from an infinite loop

Non-Turing Complete languages can be proven to terminate(they do exist, see total functional programming). Similarly I think there are programming paradigms that might be truly deadlock free but my recollection is fuzzy. IIRC writes must never block and reads must handle all blocking conditions with guarded commands. I think you can still livelock (by failing to do something when woken up for example).

> If they are blocked it is not a live lock.

If they're blocked then we are no longer talking about non-blocking, did we go full circle?

> Non-Turing Complete languages can be proven to terminate [...]

Of course, and while I appreciate the point for sake of argument, these languages have very limited applicability.

> Similarly I think there are programming paradigms that might be truly deadlock free but my recollection is fuzzy.

Look up Pony, from an earlier message in this thread :)

> Look up Pony, from an earlier message in this thread :)

after 5 minutes of googling, pony has non-blocking reads and uses promises with continuations. The CPS transform of a program that can deadlock will still deadlock. Just because you reify your wait queue does not mean you are free from deadlocks. They are just much harder to debug as you do not have a clean stackframe and process identity.

edit: to be more clear, to say that a program that uses promises and continuations can't deadlock is equivalent to saying that a C program running on linux can't deadlock because the kernel is still able to make progress. From the kernel point of view the C program looks exactly like the pony program, with continuations suspended on wait queues.

My understanding is that it doesn't use promises with continuations, what source suggests it does? The message queues are unbounded, do not block on writes, and only one can actor can read. There's no blocking nor waiting, so I'm not sure you can get into two actors waiting on each other at all. Infinite loops, sort-of live locks, and OOM are all still possible.

More in this presentation[0] (slides here [1]) and this [2].

[0] https://www.infoq.com/presentations/pony-type-system/

[1] https://qconlondon.com/london-2017/system/files/presentation...

[2] https://www.infoq.com/podcasts/sylvan-clebsch-pony-formal-ve...

From a cursory look and from my understanding of [1] and [2], promise next takes the continuation to apply to the future (elsewhere known as 'then').

[1] https://kevinhoffman.medium.com/modeling-non-blocking-intera...

[2] https://stdlib.ponylang.io/promises-Promise/

I think that's just normal code, nothing that affects the runtime, that Promise is just a pony actor and abides to the same rules, with the same causal messaging guarantees.

Let's say I'm writing a trivial proxy which simply forwards data unchanged between two sockets. This is my pseudocode:

   while true:
       x = read s1
       write s2, x
       y = read s2
       write s1, y

This can deadlock. If for example s1 stops sending data, read(s1) blocks, so the proxy won't forward any data from s2 back to s1, potentially leading to a full pipeline deadlock.

Now, the above can be expressed in purely non blocking fashion as follow :

   letrec f = async_read s1, \x ->
              async_write s2, x \->
              async_read s2, \y ->
              async_write s1, y, f

It still deadlocks exactly as the previous program.

I'm not going to learn pony for the sake of an example, but I'm 97.5% sure you can express the above in Pony, except you do not pass the continuation directly to read and writes but to the returned promise. Sure, the pony runtime will still work and technically the actor could potentially handle other messages, but that's not very useful for the end user that has to deal with a deadlocked pipeline.

So claiming that pony is deadlock-free might be true in a trivial sense, but in practice it is at the very least misleading and potentially dangerous.

edit: it is of course possible to write the program in such a way that it doesn't deadlock, the point is that if pony was truly deadlock free it would reject all programs that can deadlock.

edit2: and of course, if one were to show that the above program is in fact not expressible in pony, it would be a great result and I would want to know about!

I think you might not be able to write that program, there simply is no way to block in Pony (modulo FFI).

The scheduler wakes up actors that have messages (in their local/private queue) to process, all actors can do is to consume their queue and send (wait-free) messages to other actors if they want to.

From your example "read X" would be reading from the actor's queue, so it would not be blocking. If the message queue is empty that actor won't be scheduled, no blocking there.

That "while true" would not be writeable as such, you'd have to have two "behaviors" (in Pony terms, you can imagine it's an event handler) one that process the writing of s1 and one for the writing of s2, and "on read" they'd do the write. There'd be no "while true".

> I'm not going to learn pony for the sake of an example ... > edit2: and of course, if one were to show that the above program is in fact not expressible in pony, it would be a great result and I would want to know about!

I might have misunderstood what your example was supposed to do, but I suspect you'd find it interesting to try it out.

The async_{read,write} variant never blocks nor has a while loop, it is just a four continuations recursively tail calling each other. Yet it deadlocks (as it is a purely mechanical transformation of the synchronous variant). It still might be possible that the precise pony scoping rules for closures prevent writing that variant, but I would be surprised.

> in the same way nothing can really shield you from an infinite loop.

Fwiw that’s possible with dependent typing, the compiler can require a proof of progress (and thus termination).

> If you can still have two actors waiting on one another

There's no way to actively wait for another actor (except for using callbacks). The only way for your situation to occur would be if one of the actors receives a message with an included callback, but decides to never call it.

> If you can still have two actors waiting on one another, you’re letter-of-the-law deadlock-free, but your program is still in effect deadlocked.

How is it letter-of-the-law deadlock-free?

Now that's something remarkable about a language. Definitely going to check out Pony now.

None that I've used. But some are better than others for mitigating such scenarios. Go is pretty poor in that regard. I don't think it helped that the early releases were single threaded by default -- the argument being to help with developer onboarding. But really pain points like these need to be flushed out while the language was still being defined rather than hidden away.

Unlikely in a general purpose language

I expect you have to go out of your way to make it happen in erlang and actor based systems

Reply on news.ycombinator.com