On Fri, Mar 7, 2025 at 5:08 PM Alexander Korotkov <aekorotkov@gmail.com> wrote:
> On Sun, Mar 2, 2025 at 1:58 PM Alexander Korotkov <aekorotkov@gmail.com> wrote:
> >
> > On Fri, Feb 28, 2025 at 3:13 PM Álvaro Herrera <alvherre@alvh.no-ip.org> wrote:
> > > On 2025-Feb-28, Michael Paquier wrote:
> > >
> > > > Saying that, I have also done similar tests with your v12 for a couple
> > > > of hours and this looks stable under installcheck-world. I can see
> > > > that you've reworked quite a bit the surroundings of InitializedFrom
> > > > in this one. If you apply that once again at some point, the
> > > > buildfarm will be judge in the long-term, but I am rather confident by
> > > > saying that the situation looks better here, at least.
> > >
> > > Heh, no amount of testing can prove lack of bugs; but for sure "it looks
> > > different now, so it must be correct" must be the weakest proof of
> > > correctness I've heard of!
> >
> > Michael just volunteered to help Yura and me with testing. He wan't
> > intended to be reviewer. And he reported that tests looks much more
> > stable now. I think he is absolutely correct with this.
>
> Nevertheless, I don't think the bug has gone in v12. I managed to
> reproduce it on my local Raspberry PI 4. The attached version of
> patch fixes the bug for me. It adds memory barriers surrounding
> pg_atomic_compare_exchange_u64(). That certainly not right given this
> function should already provide full memory barrier semantics. But my
> investigation shows it doesn't. I'm going to start a separate thread
> about this.
>
> Also, new version of patch contains fix of potential integer overflow
> during OldPageRqstPtr computation sent off-list my me by Yura.
So, as we finally clarified CAS doesn't guarantee full memory barrier
on failure. Also, it's not clear when barriers are guaranteed on
success. In ARM without LSE implementation, read barrier is provided
before change of value and write barrier after change of value. So,
it appears that both explicit barriers I've added are required. This
revision also comes with format proof of the algorithm.
------
Regards,
Alexander Korotkov
Supabase
