> I found 4 different Postgres bugs.
Bugs in the upstream Postgres C implementations? Did you report them or submit patches? I'm curious to see what you found!
Bugs in the upstream Postgres C implementations? Did you report them or submit patches? I'm curious to see what you found!
0) When parsing a macaddr[0], Postgres uses sscanf with %x. %x can wraparound. This means SELECT '10000000aa:bb:cc:dd:ee:ff'::macaddr; will return aa:bb:cc:dd:ee:ff.
1) When parsing a tid[1], Postgres uses strtoul. The return value of strtoul is different across platform for the empty string. This means on some platforms Postgres SELECT '(,5)'::tid; will error and others will accept it.
2) Postgres missed an overflow check in it's cash type[2]. When running SELECT '-92233720368547758.08'::money / (-1)::int8; some platforms will error and other's will return the MIN value. Postgres does check for this for some of the other cash related functions, but it missed it for one of them.
3) When hashing the "char" type Postgres will cast a char to an integer[3]. On some platforms char is signed and on others it's unsigned. This means the hash of a char can be different depending on the platform. If you are using a hash index or hash partitioning on a char and move your DB from x86 to arm, the hashes will differ and your index/partitioned tables become corrupted. Note that this is special char type that you have to refer to by "char" that is separate from the typically used CHAR(n) type which is what you typically use, hence this would never come up under real usage.
The common pattern with all of these is they rely on C behavior that differs across platform (integer overflow, char signedness, strtoul). Rust is better about having more consistent behavior across platforms so these cases get flagged when the Rust code and the C code differ.
[0] https://github.com/postgres/postgres/blob/REL_18_3/src/backe...
[1] https://github.com/postgres/postgres/blob/REL_18_3/src/backe...
[2] https://github.com/postgres/postgres/blob/REL_18_3/src/backe...
[3] https://github.com/postgres/postgres/blob/REL_18_3/src/backe...
Without knowing anything about the pg team, I would assume they would be hesitant to even consider an under the hood switch, just from a risk management perspective, regardless of test coverage and formal verification. But I could be wrong.
My goal is to build the best database possible. I'm trying to imagine what Postgres would be like if it were built today. I've been able to make a bunch of big architectural changes that the Postgres team has been talking about but hasn't yet made. For example, threads instead of processes and a vectorized executor.
I think everyone would agree the types of changes I'm making are good ones. The challenge Postgres faces is there's millions and millions of Postgres databases out there so they are focused on minimizing the risk of breaking any existing functionality over doing a big high risk rearchitecture.
I could see ideas from what I'm doing gradually making their way into Postgres, but I think the odds that pgrust (or any Rust code for that matter) gets merged into Postgres is close to zero.
My basic understanding was to verify high level abstractions (e.g. transport ACK, fsyncs and so on), but verifying this deep probably requires complete verification of stdlib methods used by Postgres, otherwise how can you pinpoint culprit is the sscanf?
[0] https://github.com/model-checking/kani
[1] https://model-checking.github.io/cbmc-training/cbmc/overview...
Did you have a look at why3 and generating verification conditions from Rust or C code (as frama-c does) ?
I would be very surprised by that because that means replicating a database between the two platforms would lead to corruption.
btw, this bug breaks dump-and-reload too. If you use partitioning, each partition is dumped and restored individually. In this case though, you'll get an error when you try to restore the data because it's trying to put data in the wrong partition. That's better corruption, but still an issue.