6 ms·

Is there a language where deadlocks are not possible ?

by qaq 5y ago

ndr 5y ago
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 https://www.ponylang.io/discover/#what-makes-pony-different
- camkego 5y ago
  Now that's something remarkable about a language. Definitely going to check out Pony now.
- masklinn 5y ago
  > 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.
  - ndr 5y ago
    > 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.
    - gpderetta 5y ago
      > 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.
      - ndr 5y ago
        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.
        masklinn 5y ago
        > 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).
        gpderetta 5y ago
        > 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).
        ndr 5y ago
        > 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 :)
  - ergl 5y ago
    > 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.
  - MaxBarraclough 5y ago
    > 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?
hnlmorg 5y ago
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.
zaphirplane 5y ago
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
scatters 5y ago
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 https://www.type-driven.org.uk/edwinb/papers/fi-cbc.pdf (free; 2009) 2. https://livebook.manning.com/book/type-driven-development-with-idris/chapter-15/ https://livebook.manning.com/book/type-driven-development-wi... (registration wall; 2017) 3. https://research-repository.st-andrews.ac.uk/handle/10023/23560 https://research-repository.st-andrews.ac.uk/handle/10023/23... (free; 2021)

Is there a language where deadlocks are not possible ?

by qaq 5y ago

Is there a language where deadlocks are not possible ?

ndr 5y ago

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 https://www.ponylang.io/discover/#what-makes-pony-different

camkego 5y ago
Now that's something remarkable about a language. Definitely going to check out Pony now.
masklinn 5y ago
> 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.
- ndr 5y ago
  > 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.
  - gpderetta 5y ago
    > 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.
    - ndr 5y ago
      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.
      - masklinn 5y ago
        > 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).
      - gpderetta 5y ago
        > 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).
        ndr 5y ago
        > 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 :)
- ergl 5y ago
  > 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.
- MaxBarraclough 5y ago
  > 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?

hnlmorg 5y ago

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.

zaphirplane 5y ago

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

scatters 5y ago

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 https://www.type-driven.org.uk/edwinb/papers/fi-cbc.pdf (free; 2009) 2. https://livebook.manning.com/book/type-driven-development-with-idris/chapter-15/ https://livebook.manning.com/book/type-driven-development-wi... (registration wall; 2017) 3. https://research-repository.st-andrews.ac.uk/handle/10023/23560 https://research-repository.st-andrews.ac.uk/handle/10023/23... (free; 2021)