Hacker News Reader

Comment by JonChesterfield | Hacker News Reader

The visualisation of the data race in this post is superb. Worth reading just for that.

Handrolled concurrency using atomic integers in C. Without the proof system or state machine model to support it. Seems likely that's not going to be their only race condition.

View on HN

The animations also stood out to me. I took a look at the source to see if they used a library or were written completely by hand and was surprised to see that they were entirely CSS-based, no JavaScript required (although the "metadata" overwrite animation is glitched if you disable JS, for some reason not immediately apparent to me).

> for some reason not immediately apparent to me

The CSS that sets the background of the code elements (so they properly cover up the ones under them) is attached to the hljs class, which is added to those elements by highlight.js.

No JS > no classname added > no background style > jank

Thanks for pointing this out to me! I'll see if I can pre-render the syntax highlighting like I do with KaTeX and stuff. No reason to do that on the client.

This looks like the sort of bug I'd write back when I used mutexes to write I/O routines. These days, I'd use a lock-free state machine to encode something like this:

   NOT_IN_CACHE -> READING -> IN_CACHE

(the real system would need states for cache eviction, and possibly page mutation).

Readers that encounter the READING state would insert a completion handler into a queue, and readers transitioning out of the READING state would wake up all the completion handlers in the queue.

I've been working on an open source library and simple (manual) proof system that makes it easy to verify that the queue manipulation and the state machine manipulation are atomic with respect to each other:

https://docs.rs/atomic-try-update/0.0.2/atomic_try_update/

The higher level invariants are fairly obvious once you show that the interlocks are correct, and showing the interlocks are correct is just a matter of a quick skim of the function bodies that implement the interlocks for a given data type.

I've been looking for good write ups of these techniques, but haven't found any.

The existing btrfs code does use a lock-free state machine for this, `eb->bflags`, that sort of mirrors regular page flags (hence `UPTODATE`, `DIRTY`, etc.).

But Linux kernel APIs like test_bit(), set_bit(), clear_bit(), test_and_set_bit() etc. only work on one bit at a time. The advantage is they can avoid a CAS loop on many platforms. The disadvantage is you only get atomic transitions for one bit at a time. So the `READING -> UPTODATE` transition is more like

    READING -> (READING | UPTODATE) -> UPTODATE

And the `NOT_IN_CACHE -> READING` transition is not fully atomic at all:

    if (!(bflags & UPTODATE)) // atomic
                              // race could happen here
        bflags |= READING;    // atomic

The whole state machine could be made atomic with CAS, but that would be (slightly) more expensive.

That not-invented-here locking mechanism was a big shock to me. I'd be very interested to know the rationale behind that, are locking primitives somehow not available in file system code?

Locks are perfectly usable in filesystem code, but test_and_set_bit()/wait_on_bit() has lower overhead, so they'll get used as an optimization. This function is called on every metadata read, so the improved performance/scalability of raw atomics over locks can probably make a difference on fast storage.

Also the code used to use locks, and it wasn't any simpler: https://lore.kernel.org/linux-btrfs/20230503152441.1141019-2...

Anybody know how the visualisation was done?

I did it by hand with CSS: https://github.com/tavianator/tavianator.com/blob/main/src/2...

Dang, that seems like a lot of effort. It looks great though and it's such a big help for understanding something like this. I wonder if there are tools to automate this sort of thing. Like, is there a debugger that could highlight code that it passes through and when?

Reply on news.ycombinator.com