Anti-dependency cycles & write skew with select ... for update

[aphyr]

On TiDB 2.1.7, 2.1.8, and 3.0.0-beta.1, Jepsen finds anti-dependency cycles in histories even where we use select ... for update on every read. For instance, in [http://jepsen.io.s3.amazonaws.com/analyses/tidb-2.1.7/20190503T174826-select-for-update-g2.zip](this test), we observed the following pair of transactions:

T1 : ... r(1067, nil), append(1066, 1)
T2 : ... r(1066, nil), append(1067, 1)

Since T1 observes the initial (nil) state of key 1067, it must precede T2; but since T2 observed the initial (nil) state of key 1066, it must precede T1: a contradiction. This is an anti-dependency cycle which is allowed under snapshot isolation, but which select ... for update would have prohibited, had 1066 or 1067 existed prior.

TiDB's team have stated that using select ... for update prevents read skew, but tests with 3.0.0-beta1.40 suggest that write skew is, in fact, possible:

Let:
  T1 = {:type :ok, :f :txn, :value [[:r 3 nil] [:r 4 nil] [:append 4 2]], :process 7, :time 8162397985, :index 18}
  T2 = {:type :ok, :f :txn, :value [[:r 3 nil] [:r 4 nil] [:append 3 1]], :process 3, :time 8137934433, :index 14}

Then:
  - T1 < T2, because T1 observed the initial (nil) state of 3, which T2 created by appending 1.
  - However, T2 < T1, because T2 observed the initial (nil) state of 4, which T1 created by appending 2: a contradiction!

As we discussed in chat, this occurs because TiDB's select ... for update locking mechanism can only lock records which exist. The MySQL documentation for select ... for update says:

For index records the search encounters, locks the rows and any associated index entries, the
same as if you issued an UPDATE statement for those rows. Other transactions are blocked
from updating those rows, from doing SELECT ... FOR SHARE, or from reading the data in
certain transaction isolation levels.

... which is a little ambiguous about the behavior when rows don't exist yet, but I think means that locks aren't acquired. Postgres says:

FOR UPDATE causes the rows retrieved by the SELECT statement to be locked as though for update.

... which I interpret to mean that when a row doesn't exist, it isn't locked.

This may not be a bug, but it seems worth discussing what the behavior should be for TiDB. Should select ... for update on every read make queries serializable? Or are anti-dependency cycles, including write skew, legal when they involve the first, but not subsequent, write(s) to a key?