← Back to context

Comment by ameliaquining

15 days ago

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

11 comments

ameliaquining

Reply
jhhh  15 days ago

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

  • ameliaquining  15 days 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.

inigyou  14 days ago

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

IsTom  15 days 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.