Comment by octoberfranklin
3 hours ago
So far, I've proven that about 12% of the code behaves the same when executed single-threaded.
Dude, this is a database.
Concurrency is the source of all the hard stuff in databases.
Databases without concurrency are super-trivial.
I don't see any fundamental limitation that would prevent this from scaling up further.
The fact that you've dodged all the hard stuff is a pretty fundamental limitation.
Proving the code works single threaded is a stepping stone to eventually proving the code works under concurrency. It may be surprising, but very little of the Postgres code deals with concurrency. For the most part they've isolated the parts that deal with concurrency to a small number of subsystems. At least by volume of code, the vast majority of it is single threaded
the code is either single threaded or multi threaded. not partially...
so either you verify the whole thing or basically you didnt verify anything.
remember what verification is for. its great your query parser is functionally correct but verification is meant to prove something.
say you have a car. and its got safety requirements. those need to be verified. But now they say we've verified its safe only for the rear seat passengers. or, only the engine block is verified itll keep running safely.. it completely negates what is being done if its not done completely to the entire car.
and then ofc another driver just prangs into you anyway with their uncerified car, or suddenly the unverified road (OS) turns into a sinkhole and all ur verification still goes out the window..
there are limits already to verification if done properly and skipping the hard/important parts is really a big issue... u might aswell not do it.
(i do respect that there is a road to fully verified, u wont slap out those 9 million lines in one go. but saying you're winning halfway through the race.... nope)