4 ms·

> 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 sti

by 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 :)
      - gpderetta 5y ago
        > 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.
        ndr 5y ago
        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/ https://www.infoq.com/presentations/pony-type-system/ [1] https://qconlondon.com/london-2017/system/files/presentation-slides/qcon_london_2017_2.pdf https://qconlondon.com/london-2017/system/files/presentation... [2] https://www.infoq.com/podcasts/sylvan-clebsch-pony-formal-verification/ https://www.infoq.com/podcasts/sylvan-clebsch-pony-formal-ve...

by ndr 5y ago

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 :)
    - gpderetta 5y ago
      > 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.
      - ndr 5y ago
        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/ https://www.infoq.com/presentations/pony-type-system/ [1] https://qconlondon.com/london-2017/system/files/presentation-slides/qcon_london_2017_2.pdf https://qconlondon.com/london-2017/system/files/presentation... [2] https://www.infoq.com/podcasts/sylvan-clebsch-pony-formal-verification/ https://www.infoq.com/podcasts/sylvan-clebsch-pony-formal-ve...