Transaction specs may be not as solid as expected

[sticnarf]

I try to reproduce the bug which is fixed by tikv/tikv#5673. The bug is introduced by the new check_txn_status API, which is a cleanup API substitution. We forgot to write rollback when there is no lock.

To reproduce the problem in TLA+, I change the eraseLock in CollapseRollbacks by:

eraseLock(key, l) == 
        IF l \in key_lock[key]
        THEN
            /\ key_data' = [key_data EXCEPT ![key] = @ \ {[ts |-> l.ts]}]
            /\ key_lock' = [key_lock EXCEPT ![key] = @ \ {l}]
            /\ key_write' = [key_write EXCEPT ![key] =
                         Append(@, [ts |-> l.ts, type |-> "rollback"])]
        ELSE
            UNCHANGED <<key_data, key_lock, key_write>>

This demonstrates the wrong implementation in tikv/tikv#5390. However, the tests still pass.

[sticnarf]

#29 can successfully reproduce this problem.

Changing rollback(k, ts) to:

rollback(k, ts) ==
  IF key_lock[k] # {}
  THEN
      \* If the existing lock has the same ts, unlock it.
      /\ IF \E l \in key_lock[k] : l.ts = ts
         THEN key_lock' = [key_lock EXCEPT ![k] = {}]
         ELSE UNCHANGED key_lock
      /\ key_data' = [key_data EXCEPT ![k] = @ \ {[ts |-> ts]}]
      \* Write a rollback in the write column.
      /\ key_write' = [key_write EXCEPT
           ![k] = (@ \ {w \in latestHistoryWrite(k, ts) : w.type = "rollback"}) \* collapse rollback
                     \union {[ts |-> ts, type |-> "rollback", start_ts |-> ts]}]
  ELSE
    UNCHANGED <<key_lock, key_data, key_write>>

It's quite easy to get Invariant CommittedTxnConsistency is violated.

[IANTHEREAL]

@sticnarf can you improve the invariants in https://github.com/pingcap/tla-plus/blob/master/CollapseRollbacks/CollapseRollbacks.tla#L167