Hacker News Reader

Comment by mratsim | Hacker News Reader

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

View on HN

I have compiled my research in formal verification tools and papers here, there are a couple dozens:

- https://github.com/mratsim/weave/issues/18

>"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+?

Check out the video course from Leslie Lamport (the creator of TLA+) himself:

https://lamport.azurewebsites.net/tla/learning.html

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.

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?

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 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-w... (at the bottom)

This is beautiful and satisfying.

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).

High-performance concurrency is just the kind of problem that may well require a complex solution.

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.

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).

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.

I don't think everyone, let alone most people, makes the leap from "smell" to "repulsive". "My fridge smells funny" is not the same as "My fridge smells so bad it makes me want to puke". The first is a cause for investigation, the second is a cause for real concern.

Most code "smells" are in the former category, they are not describing the code as "repulsive" but "off". If you're making that leap then you're going to need to supply (or find) another term for what is described, for now over 20 years, as a code smell. Since most people don't have the same visceral reaction you do, they won't care.

It's a qualitative word for a qualitative assessment.

For example, it is quite possible that code that is nested 30 levels deep is provably correct. Since we are humans, is that likely? No, it is not. Or at least, it is certainly less likely than 3-level-deep code. So you look at some code and without doing any deep analysis you can make some "probably valid" assumptions which come from your experience.

If you're so bent on accurate engineering, answer me this: Why are technology choices often "fashion-driven", without any significant empirical data to support their choice over other alternatives? (My latest pet peeve in this space is widespread use of Docker.) And where data DOES exist (such as to support the statement "Functional languages produce far fewer bugs per LOC written"), why don't more programmers/engineers heed that?

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

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_th...

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.

Reply on news.ycombinator.com