Re: SSI predicate locking on heap -- tuple or row?

On Wed, Jun 01, 2011 at 05:09:09PM -0500, Kevin Grittner wrote:
> I won't be shocked if Dan can come up with a shorter proof, but I'm
> confident this one is solid.

Well, so happens I wrote a proof on the airplane today, before I saw
your mail. It's actually quite straightforward... (well, at least more
so than I was expecting)

> From many academic papers, there is well-established proof that
> serialization anomalies can only occur under snapshot isolation when
> there is a cycle in the graph of apparent order of execution of the
> transactions, and that in such a cycle the following pattern of
> rw-dependencies always occurs:
>
> Tin - - -> Tpivot - - -> Tout
>
> A rw-dependency (also called a rw-conflict) exists when a read by
> one transaction doesn't see the write of another transaction because
> the two transactions overlap, regardless of whether the read or the
> write actually happens first. Since the reader doesn't see the work
> of the writer, the reader appears to have executed first, regardless
> of the actual order of snapshot acquisition or commits. The arrows
> show the apparent order of execution of the transactions -- Tin
> first, Tout last. Published papers have further proven that the
> transaction which appears to have executed last of these three must
> actually commit before either of the others for an anomaly to occur.

We can actually say something slightly stronger than that last
sentence: Tout has to commit before *any* other transaction in the
cycle. That doesn't help us implement SSI, because we never try to look
at an entire cycle, but it's still true and useful for proofs like this.

Now, supposing Tin is read-only...

Since there's a cycle, there must also be a transaction that precedes
Tin in the serial order. Call it T0. (T0 might be the same transaction
as Tout, but that doesn't matter.) There's an edge in the graph from
T0 to Tin. It can't be a rw-conflict, because Tin was read-only, so it
must be a ww- or wr-dependency. Either means T0 committed before Tin
started.

Because Tout committed before any other transaction in the cycle, Tout
has to commit before T0 commits -- and thus before Tin starts.

Dan

--
Dan R. K. Ports MIT CSAIL http://drkp.net/