[flagged]
Hunting a 16-year-old SQLite WAL bug with TLA+
11–20 of 37 posts
Re: Hunting a 16-year-old SQLite WAL bug with TLA+
#12[flagged]
Re: Hunting a 16-year-old SQLite WAL bug with TLA+
#13[flagged]
Re: Hunting a 16-year-old SQLite WAL bug with TLA+
#14[flagged]
wut
Re: Hunting a 16-year-old SQLite WAL bug with TLA+
#15Author of the article here. I am surprised to see the post was submitted and made it to the front page! Happy to answer any questions
Thanks for the nice article. The SQLite docs that explain this bug are emphatic about how utterly rare, even irreproducible it is. How, then, was it found, one wonders?
Re: Hunting a 16-year-old SQLite WAL bug with TLA+
#16Author of the article here. I am surprised to see the post was submitted and made it to the front page! Happy to answer any questions
Thanks for the nice article. The SQLite docs that explain this bug are emphatic about how utterly rare, even irreproducible it is. How, then, was it found, one wonders?
My guess is that they noticed something was not quite right when inspecting the code and then tested their hypothesis manually to see if it was actually a real bug.
Something similar happened to me when I was working on some code that should clear the state and, by inspection, I noticed some field was not properly cleared under specific circumstances. Then I tested the hypothesis and indeed found a bug. Sometimes intuition and guessing is what it takes.
Re: Hunting a 16-year-old SQLite WAL bug with TLA+
#17I don't like the title. The article actually describes the process of proving that dqlite does not have the same bug as SQLite, using a TLA+ specification. The SQLite bug fix was entirely separate from what is described here.
Re: Hunting a 16-year-old SQLite WAL bug with TLA+
#18Author of the article here. I am surprised to see the post was submitted and made it to the front page! Happy to answer any questions
You’re in a desert walking along in the sand when all of the sudden you look down, and you see a tortoise, it’s crawling toward you. You reach down, you flip the tortoise over on its back. The tortoise lays on its back, its belly baking in the hot sun, beating its legs trying to turn itself over, but it can’t, not without your help. But you’re not helping. Why is that?
Re: Hunting a 16-year-old SQLite WAL bug with TLA+
#19Earlier quoted context omitted.
So there's \in, \subseteq and probably many others that are written just like in Latex. Notably \cap and \cup were also copied from Latex, which describe the shape of the symbol instead of its meaning. But not \to, \mapsto, \Vee and \Wedge, they're written as ASCII art ->, |->, \/ and /\. Then there's SUBSET, which means power set ... yeah. -_-
Leslie Lamport is also the original creator of LaTeX.
Where LaTeX[0] is the collection of Lamports macros over Knuths[1] TeX[2].
[0] https://en.wikipedia.org/wiki/LaTeX
Re: Hunting a 16-year-old SQLite WAL bug with TLA+
#20Author of the article here. I am surprised to see the post was submitted and made it to the front page! Happy to answer any questions
You’re in a desert walking along in the sand when all of the sudden you look down, and you see a tortoise, it’s crawling toward you. You reach down, you flip the tortoise over on its back. The tortoise lays on its back, its belly baking in the hot sun, beating its legs trying to turn itself over, but it can’t, not without your help. But you’re not helping. Why is that?
Because that would reverse flipping it over the first time, and our universe's physics are not reversible. Thermodynamics demands the turtle stay flipped.