4 ms·

I have successfully used TLA+ to clear my 2-phase "put a thread to sleep" protocol from deadlock and livelocks. I also proved that one of the nasty deadlock bu

I have successfully used TLA+ to clear my 2-phase "put a thread to sleep" protocol from deadlock and livelocks. I also proved that one of the nasty deadlock bugs I was fighting on Linux (but not on Windows or Mac) was actually glibc missing condition variables wakeup signals from time to time. 100% convinced it's worth learning to debug or verify any kind of distributed or multithreaded synchronization primitive. I was bug hunting for a couple weeks before deciding to learn formal verification / model checking via TLA+. Writeup: https://github.com/mratsim/weave/issues/56 https://github.com/mratsim/weave/issues/56

MaxBarraclough 6y ago
Perhaps I'm missing something but shouldn't that bug be filed with the glibc project rather than with the weave project? Has glibc since fixed the issue?
- mratsim 6y ago
  Weave is my multithreading library. It's just a recap of what I went through for future reference. I unfortunately didn't have time to go through: - compiling glibc from source - converting my code to C - trying to reduce multithreaded synchronization code to a minimal example given how non-deterministic any of those bugs are - do a write-up That said, it seems like people went through the motions 4 months after me in this bug: - https://sourceware.org/bugzilla/show_bug.cgi?id=25847 https://sourceware.org/bugzilla/show_bug.cgi?id=25847 which affects C#, OCaml, Python Someone also fully reimplemented Glibc condition variable in TLA+ to prove that the glibc code was buggy: - https://probablydance.com/2020/10/31/using-tla-in-the-real-world-to-understand-a-glibc-bug/ https://probablydance.com/2020/10/31/using-tla-in-the-real-w... (at the bottom)
  - vinay_ys 6y ago
    This is beautiful and satisfying.
  - pmarreck 6y ago
    Wow. I'd normally respond with (when looking at the very complex relevant glibc code), "complexity is a code smell", but I don't understand the problem space enough to legitimately suggest that here, other than to say that in my experience programming thus far, if you require this much complexity for any part of your system, it is in all likelihood reflective of a design flaw (possibly elsewhere).
    - MaxBarraclough 6y ago
      High-performance concurrency is just the kind of problem that may well require a complex solution.
    - grayhatter 6y ago
      Why do so many people use the word smell to disparage code? The human part of me always feels it's super douchy and elitist, and the engineer part hates it because it's inaccurate and misleading.
      - Jtsummers 6y ago
        It's an analogy to the way we detect things like food spoilage or gas leaks by smell. For the vast majority of us most code smells are actually observed visually (Why is this nested 10 levels deep? Why are there 20 parameters to this method?) so I suppose we could start saying code eyesores, but that often has the wrong sense (even more strongly negative) than smell. It's really only douchy or elitist if it's strictly used in an insulting or disparaging way. Most of the time when people talk about code smells it's meant to indicate, just like with real-world odd, bad, or unexpected smells: Something doesn't seem right. I could be wrong, but it warrants investigation. Using the examples above, deep nesting and large numbers of parameters are indications of a potential problem, but are not necessarily problems. It could be that a refactoring is in order, but it may also be that everything is fine (just not pretty).
        grayhatter 6y ago
        I understand the point of the analogy, my question was more why is such a bad one so popular. something something makes my hair stand up, as alternative that's actually good; used to mean the feeling of anxiety. No one mentions smells when they're talking about good code. Similar to normal american english conversations, if someone mentions a smell unprovoked, it's normally a disgusting smell. So when used against code, it's implying the code is repulsive. Which to me at least feels super insulting to respond to code (text on a screen) with such a vicseral response, of distrust/dislike.
bogomipz 6y ago
>"100% convinced it's worth learning to debug or verify any kind of distributed or multithreaded synchronization primitive." Might you or anyone else have some resources you could recommend for learning TLA+?
- cloogshicer 6y ago
  Check out the video course from Leslie Lamport (the creator of TLA+) himself: https://lamport.azurewebsites.net/tla/learning.html https://lamport.azurewebsites.net/tla/learning.html
  - macintux 6y ago
    Leslie is one of those ridiculously over-accomplished people in computer science. I think it's safe to say you've earned respect when people can legitimately recognize your name for multiple, mostly-unrelated achievements, without realizing everything else you've done.
mratsim 6y ago
I have compiled my research in formal verification tools and papers here, there are a couple dozens: - https://github.com/mratsim/weave/issues/18 https://github.com/mratsim/weave/issues/18
thraway123412 6y ago
I find it suspicious that glibc and musl should have the same bug. Double check your code?
- mratsim 6y ago
  I checked my code dozens of times over days. I thought I had bugs in my code for sure, I couldn't believe glibc and musl had a bug. Then I decided to spend a couple days to learn formal verification, solved all the bugs it found. It worked on my Mac, it worked on Windows, it was still deadlocking on Linux. I replaced my code with raw futexes, no deadlock anymore. And I added logs that showed signaling happened but the thread signaled wasn't unblocked. The futex<->condvar swap is pretty simple. - https://github.com/mratsim/weave/blob/f41a562/weave/cross_thread_com/event_notifiers.nim#L144-L148 https://github.com/mratsim/weave/blob/f41a562/weave/cross_th...
  - thraway123412 6y ago
    Yes, I saw your screenshots, and I think they demonstrate lack of understanding of how condition variables work. Any use of condition variables where the lock is "never used" screams fundamentally broken to me. No amount of atomics and memory orderings or manually inserted fences/memory barriers can help you if you leave a race window open between checking your predicate and starting to wait on a signal. Condvar signals are not sticky. If nobody is waiting for a signal when you signal, that signal is lost. There is nothing between your atomics and lock & wait to prevent such loss. Also your TLA+ (or rather PlusCal) does not model a condition variable correctly, so it would obviously not detect this issue. You have a sticky boolean variable and await, which blocks the procedure until the condition becomes true. This detects lockups of the class where the condition is never signalled at all, but it does not model the possibility of losing a signal because nobody was waiting for it. I don't believe you discovered a bug in glibc and musl.

MaxBarraclough 6y ago

Perhaps I'm missing something but shouldn't that bug be filed with the glibc project rather than with the weave project? Has glibc since fixed the issue?

mratsim 6y ago
Weave is my multithreading library. It's just a recap of what I went through for future reference. I unfortunately didn't have time to go through: - compiling glibc from source - converting my code to C - trying to reduce multithreaded synchronization code to a minimal example given how non-deterministic any of those bugs are - do a write-up That said, it seems like people went through the motions 4 months after me in this bug: - https://sourceware.org/bugzilla/show_bug.cgi?id=25847 https://sourceware.org/bugzilla/show_bug.cgi?id=25847 which affects C#, OCaml, Python Someone also fully reimplemented Glibc condition variable in TLA+ to prove that the glibc code was buggy: - https://probablydance.com/2020/10/31/using-tla-in-the-real-world-to-understand-a-glibc-bug/ https://probablydance.com/2020/10/31/using-tla-in-the-real-w... (at the bottom)
- vinay_ys 6y ago
  This is beautiful and satisfying.
- pmarreck 6y ago
  Wow. I'd normally respond with (when looking at the very complex relevant glibc code), "complexity is a code smell", but I don't understand the problem space enough to legitimately suggest that here, other than to say that in my experience programming thus far, if you require this much complexity for any part of your system, it is in all likelihood reflective of a design flaw (possibly elsewhere).
  - MaxBarraclough 6y ago
    High-performance concurrency is just the kind of problem that may well require a complex solution.
  - grayhatter 6y ago
    Why do so many people use the word smell to disparage code? The human part of me always feels it's super douchy and elitist, and the engineer part hates it because it's inaccurate and misleading.
    - Jtsummers 6y ago
      It's an analogy to the way we detect things like food spoilage or gas leaks by smell. For the vast majority of us most code smells are actually observed visually (Why is this nested 10 levels deep? Why are there 20 parameters to this method?) so I suppose we could start saying code eyesores, but that often has the wrong sense (even more strongly negative) than smell. It's really only douchy or elitist if it's strictly used in an insulting or disparaging way. Most of the time when people talk about code smells it's meant to indicate, just like with real-world odd, bad, or unexpected smells: Something doesn't seem right. I could be wrong, but it warrants investigation. Using the examples above, deep nesting and large numbers of parameters are indications of a potential problem, but are not necessarily problems. It could be that a refactoring is in order, but it may also be that everything is fine (just not pretty).
      - grayhatter 6y ago
        I understand the point of the analogy, my question was more why is such a bad one so popular. something something makes my hair stand up, as alternative that's actually good; used to mean the feeling of anxiety. No one mentions smells when they're talking about good code. Similar to normal american english conversations, if someone mentions a smell unprovoked, it's normally a disgusting smell. So when used against code, it's implying the code is repulsive. Which to me at least feels super insulting to respond to code (text on a screen) with such a vicseral response, of distrust/dislike.

bogomipz 6y ago

>"100% convinced it's worth learning to debug or verify any kind of distributed or multithreaded synchronization primitive." Might you or anyone else have some resources you could recommend for learning TLA+?

cloogshicer 6y ago
Check out the video course from Leslie Lamport (the creator of TLA+) himself: https://lamport.azurewebsites.net/tla/learning.html https://lamport.azurewebsites.net/tla/learning.html
- macintux 6y ago
  Leslie is one of those ridiculously over-accomplished people in computer science. I think it's safe to say you've earned respect when people can legitimately recognize your name for multiple, mostly-unrelated achievements, without realizing everything else you've done.

mratsim 6y ago

I have compiled my research in formal verification tools and papers here, there are a couple dozens: - https://github.com/mratsim/weave/issues/18 https://github.com/mratsim/weave/issues/18

thraway123412 6y ago

I find it suspicious that glibc and musl should have the same bug. Double check your code?

mratsim 6y ago
I checked my code dozens of times over days. I thought I had bugs in my code for sure, I couldn't believe glibc and musl had a bug. Then I decided to spend a couple days to learn formal verification, solved all the bugs it found. It worked on my Mac, it worked on Windows, it was still deadlocking on Linux. I replaced my code with raw futexes, no deadlock anymore. And I added logs that showed signaling happened but the thread signaled wasn't unblocked. The futex<->condvar swap is pretty simple. - https://github.com/mratsim/weave/blob/f41a562/weave/cross_thread_com/event_notifiers.nim#L144-L148 https://github.com/mratsim/weave/blob/f41a562/weave/cross_th...
- thraway123412 6y ago
  Yes, I saw your screenshots, and I think they demonstrate lack of understanding of how condition variables work. Any use of condition variables where the lock is "never used" screams fundamentally broken to me. No amount of atomics and memory orderings or manually inserted fences/memory barriers can help you if you leave a race window open between checking your predicate and starting to wait on a signal. Condvar signals are not sticky. If nobody is waiting for a signal when you signal, that signal is lost. There is nothing between your atomics and lock & wait to prevent such loss. Also your TLA+ (or rather PlusCal) does not model a condition variable correctly, so it would obviously not detect this issue. You have a sticky boolean variable and await, which blocks the procedure until the condition becomes true. This detects lockups of the class where the condition is never signalled at all, but it does not model the possibility of losing a signal because nobody was waiting for it. I don't believe you discovered a bug in glibc and musl.