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

▲

malisper 3 hours ago | parent [-]

Yep, I did submit bug reports. This was on Tuesday. I don't see a public copy of the mailing list that has my bug reports yet. The four bugs were:

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

▲

mjw1007 16 minutes ago | parent | next [-]

I think the postgresql maintainers don't claim to support moving a database from x86 to arm without a dump-and-reload. The docs tend to say "same hardware architecture". Though if they don't intend to support this case I think it's a shame if the pg_control checks allow the server to start after such a migration.

	▲	malisper 3 minutes ago \| parent [-]
		> I think the postgresql maintainers don't claim to support moving a database from x86 to arm without a dump-and-reload 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.

▲

appplication 3 hours ago | parent | prev | next [-]

Very cool project and good finds. What do you see as the end state for your project - do you think pg has a path to upstream, or would this be a fork?

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.

▲

malisper 3 hours ago | parent [-]

Thank you for the kind words!

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.

	▲	wonger_ 2 hours ago \| parent [-]
		For other interested spectators, I found this post by the author to be a good example of architectural changes in pgrust (along with motivations): https://malisper.me/the-four-horsemen-behind-thousands-of-po...

▲

throwaw12 2 hours ago | parent | prev [-]

these are impressive findings, I am curious what was your process to convert existing code to formal verification languages like TLA+.

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?

	▲	malisper 16 minutes ago \| parent [-]
		Right now I'm only doing very small simple functions. Kani[0] takes care of translating the code to an intermediate representation for me. It converts the Rust code and C code into a GOTO program[1] which verifiers can then run on top of [0] https://github.com/model-checking/kani [1] https://model-checking.github.io/cbmc-training/cbmc/overview...