6 ms·

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.

by ndr 5y ago

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...
      - gpderetta 5y ago
        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-interactions-with-actors-in-pony-fae59151246a https://kevinhoffman.medium.com/modeling-non-blocking-intera... [2] https://stdlib.ponylang.io/promises-Promise/ https://stdlib.ponylang.io/promises-Promise/
        ndr 5y ago
        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.
        gpderetta 5y ago
        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!

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.

by 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...
    - gpderetta 5y ago
      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-interactions-with-actors-in-pony-fae59151246a https://kevinhoffman.medium.com/modeling-non-blocking-intera... [2] https://stdlib.ponylang.io/promises-Promise/ https://stdlib.ponylang.io/promises-Promise/
      - ndr 5y ago
        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.
        gpderetta 5y ago
        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!