4 ms·

I admit to curiosity as to whether static analysis could have caught this. E.g., Rust's type system (yeah yeah I know) catches all data races, unless they origi

I admit to curiosity as to whether static analysis could have caught this. E.g., Rust's type system (yeah yeah I know) catches all data races, unless they originate in unsafe code, which this one might or might not have; a hypothetical Rust SQLite would probably need a lot of unsafe (https://github.com/tursodatabase/turso https://github.com/tursodatabase/turso has 556 unsafe blocks in the core), and I don't have a sense of whether the particular part that contained this bug would be included in that.

jhhh 2mo ago
There was a post recently using TLA to model this issue and (re)discover the bug: https://news.ycombinator.com/item?id=48730953 https://news.ycombinator.com/item?id=48730953.
- ameliaquining 2mo ago
  Interesting. I don't think this kind of technique could realistically have caught the bug in advance, though; you're not going to model the entire codebase in TLA+, so the investigation in that post modeled just the parts that turned out in hindsight to be relevant.
  - fragmede 2mo ago
    > you're not going to model the entire codebase in TLA+ Not by hand in the olden days but with AI to help with it, why not?
    - j16sdiz 2mo ago
      Because AI have a recall of 80% or 90% at best. While it might be better than some human, it won't hit the 100% TLA+ modeling aims
    - ameliaquining 2mo ago
      LLMs are not at the point where they can reliably complete this kind of task without making mistakes. The model checker can tell you whether the formal design specification contradicts itself, but it can't tell you whether it matches the implementation, nor whether it matches the programmers' intentions. And it's too much for humans to review by hand. This is importantly different from formal code verification, in which the specification that needs to match the programmers' intentions is small enough to review, while the bulk of the LLM's output is proof tactics and such, which don't need human review because the verifier guarantees* that they're right. I suppose you could just tell Fable "hey try using TLA+ to look for bugs in this code" and see whether it finds any. * Uh, usually. https://leodemoura.github.io/blog/2026-8-1-postmortem-for-kernel-soundness-bug-14576/ https://leodemoura.github.io/blog/2026-8-1-postmortem-for-ke...
andai 2mo ago
>Rust's type system (yeah yeah I know) What do you know?
- 1over137 2mo ago
  Presumably he is referring to rust fanboys' tiresome criticisms of everything C.
IsTom 2mo ago
It sounds like it was a bug caused by pushing on performance/safety ratio, it could easily have been avoided by adding enough mutexes in the code, but for performance reasons (I assume) they don't do that. To write it like that in Rust you'd have to use unsafe blocks and then you don't gain much from the typesystem in this case.
inigyou 2mo ago
I don't think they could. This is probably a memory-mapped file, which would be unsafe.
computerfriend 2mo ago
I wouldn't think so, but Go also has a data race detector: https://go.dev/doc/articles/race_detector https://go.dev/doc/articles/race_detector.
- ameliaquining 2mo ago
  That's dynamic, not static; it doesn't help much with a race that's hard to trigger.

jhhh 2mo ago

There was a post recently using TLA to model this issue and (re)discover the bug: https://news.ycombinator.com/item?id=48730953 https://news.ycombinator.com/item?id=48730953.

ameliaquining 2mo ago
Interesting. I don't think this kind of technique could realistically have caught the bug in advance, though; you're not going to model the entire codebase in TLA+, so the investigation in that post modeled just the parts that turned out in hindsight to be relevant.
- fragmede 2mo ago
  > you're not going to model the entire codebase in TLA+ Not by hand in the olden days but with AI to help with it, why not?
  - j16sdiz 2mo ago
    Because AI have a recall of 80% or 90% at best. While it might be better than some human, it won't hit the 100% TLA+ modeling aims
  - ameliaquining 2mo ago
    LLMs are not at the point where they can reliably complete this kind of task without making mistakes. The model checker can tell you whether the formal design specification contradicts itself, but it can't tell you whether it matches the implementation, nor whether it matches the programmers' intentions. And it's too much for humans to review by hand. This is importantly different from formal code verification, in which the specification that needs to match the programmers' intentions is small enough to review, while the bulk of the LLM's output is proof tactics and such, which don't need human review because the verifier guarantees* that they're right. I suppose you could just tell Fable "hey try using TLA+ to look for bugs in this code" and see whether it finds any. * Uh, usually. https://leodemoura.github.io/blog/2026-8-1-postmortem-for-kernel-soundness-bug-14576/ https://leodemoura.github.io/blog/2026-8-1-postmortem-for-ke...

andai 2mo ago

>Rust's type system (yeah yeah I know) What do you know?

1over137 2mo ago
Presumably he is referring to rust fanboys' tiresome criticisms of everything C.

IsTom 2mo ago

It sounds like it was a bug caused by pushing on performance/safety ratio, it could easily have been avoided by adding enough mutexes in the code, but for performance reasons (I assume) they don't do that. To write it like that in Rust you'd have to use unsafe blocks and then you don't gain much from the typesystem in this case.

inigyou 2mo ago

I don't think they could. This is probably a memory-mapped file, which would be unsafe.

computerfriend 2mo ago

I wouldn't think so, but Go also has a data race detector: https://go.dev/doc/articles/race_detector https://go.dev/doc/articles/race_detector.

ameliaquining 2mo ago
That's dynamic, not static; it doesn't help much with a race that's hard to trigger.