From 36aa05a586c0411e027d6e63a1ece975bf060eef Mon Sep 17 00:00:00 2001 From: CWen Date: Fri, 20 Jul 2018 12:59:57 +0800 Subject: [PATCH] ConcurrentPercolator: remove the pre rollback (#23) --- ConcurrentPercolator/ConcurrentPercolator.tla | 72 ++++++++++++++++--- 1 file changed, 62 insertions(+), 10 deletions(-) diff --git a/ConcurrentPercolator/ConcurrentPercolator.tla b/ConcurrentPercolator/ConcurrentPercolator.tla index 1b78aa9..80bb717 100644 --- a/ConcurrentPercolator/ConcurrentPercolator.tla +++ b/ConcurrentPercolator/ConcurrentPercolator.tla @@ -64,8 +64,7 @@ Range(m) == {m[i] : i \in DOMAIN m} -------------------------------------------------------------------------------- -\* Checks whether there is a lock of key $k$, whose $ts$ is less or equal than -\* $ts$. +\* Checks whether there is a lock of key $k$, whose $ts$ is less than or equal to $ts$. hasLockLE(k, ts) == \E l \in key_lock[k] : l.ts <= ts @@ -90,10 +89,24 @@ findWriteWithStartTS(k, ts) == findWriteWithCommitTS(k, ts) == {w \in Range(key_write[k]) : (w.type = "write" /\ w.ts = ts)} -\* Returns TRUE if there is a rollback for key $k$ at timestamp $ts$. +\* Returns TRUE if there is a rollback for key $k$ that is not deleted logically at timestamp $ts$. +hasRollbackNotDeleted(k, ts) == + {r \in Range(key_write[k]) : (r.type = "rollback" /\ r.is_deleted = FALSE /\ r.ts = ts )} # {} + +\* Returns TRUE if there is a rollback for key $k$ at timestamp $ts$ hasRollback(k, ts) == {r \in Range(key_write[k]) : (r.type = "rollback" /\ r.ts = ts)} # {} +\* Returns TRUE if the write is rollback with ts equal to $ts$ +\* and this rollback is marked as deleted. +isRollbackWithDeleted(w, ts) == + (w.type = "rollback" /\ w.ts = ts /\ w.is_deleted = TRUE) + +\* Returns TRUE if there is a rollback at timestamp $ts$ +\* and this rollback is marked as deleted. +hasRollbackWithDeleted(ws, ts) == + {r \in Range(ws) : isRollbackWithDeleted(r, ts)} # {} + \* Updates $key_si$ for key $k$. If a new version of key $k$ is committed with \* $commit_ts$ < last read timestamp, consider the snapshot isolation invariant \* for key $k$ has been violated. @@ -104,6 +117,45 @@ checkSnapshotIsolation(k, commit_ts) == ELSE UNCHANGED <> +\* Returns the writes with ts less than or equal to $ts$ and is not deleted logically +findWriteLessEqualTS(kw, ts) == + {w \in Range(kw) : (w.ts <= ts /\ w.is_deleted = FALSE)} + +\* Returns the write whose $ts$ is the max in all writes +getWriteWithMaxTS(w) == CHOOSE x \in w : \A y \in w : x.ts >= y.ts + +\* Deletes element from $seq$ logically +logicalDeleteElement(seq, e)== + [i \in 1..Len(seq)|->IF seq[i] # e THEN seq[i] ELSE [ts |-> seq[i].ts, type |-> seq[i].type, is_deleted |-> TRUE]] + +\* Removes the pre rollback, whose ts is less than or equal to $ts$. +collapsePreRollback(w, ts) == + LET + writes == findWriteLessEqualTS(w, ts) + IN + IF writes # {} + THEN + LET + maxTsWrite == getWriteWithMaxTS(writes) + IN + IF maxTsWrite.type = "rollback" + THEN + logicalDeleteElement(w, maxTsWrite) + ELSE + w + ELSE + w + +\* Writes rollback record to key write. +\* If the rollback with the ts equal to $ts$ exists and is marked as deleted, +\* which will be overwritten by the new rollback. +writeRollback(ws, ts) == + IF hasRollbackWithDeleted(ws, ts) + THEN + [i \in 1..Len(ws)|->IF isRollbackWithDeleted(ws[i], ts) THEN ws[i] ELSE [ts |-> ws[i].ts, type |-> ws[i].type, is_deleted |-> FALSE]] + ELSE + Append(collapsePreRollback(ws, ts), [ts |-> ts, type |-> "rollback", is_deleted |-> FALSE]) + \* Cleans up a stale lock and its data. \* If the lock is a secondary lock, and the assoicated primary lock is cleaned \* up, we can clean up the lock and do, @@ -115,8 +167,7 @@ cleanupStaleLock(k, ts) == eraseLock(key, l) == /\ 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"])] + /\ key_write' = [key_write EXCEPT ![key] = writeRollback(key_write[key], l.ts)] IN \E l \in key_lock[k] : /\ isStaleLock(l, ts) @@ -134,7 +185,7 @@ cleanupStaleLock(k, ts) == \* the primary key is not committed, clean up the data. \* Note we should always clean up the corresponding primary \* lock first, then this secondary lock. - IF hasRollback(l.primary, l.ts) = FALSE + IF hasRollbackNotDeleted(l.primary, l.ts) = FALSE THEN /\ eraseLock(l.primary, l) /\ UNCHANGED <> @@ -218,7 +269,8 @@ commitPrimary(c) == /\ key_write' = [key_write EXCEPT ![primary] = Append(@, [ts |-> commit_ts, type |-> "write", - start_ts |-> start_ts])] + start_ts |-> start_ts, + is_deleted |-> FALSE])] /\ key_lock' = [key_lock EXCEPT ![primary] = @ \ {[ts |-> start_ts, primary |-> primary]}] /\ checkSnapshotIsolation(primary, commit_ts) @@ -330,8 +382,8 @@ KeyLockTypeInv == key_lock \in [KEY -> SUBSET [ts : Nat, primary : KEY]] KeyWriteTypeInv == - key_write \in [KEY -> Seq([ts : Nat, type : {"write"}, start_ts : Nat] \union - [ts : Nat, type : {"rollback"}]) + key_write \in [KEY -> Seq([ts : Nat, type : {"write"}, start_ts : Nat, is_deleted: BOOLEAN] \union + [ts : Nat, type : {"rollback"}, is_deleted: BOOLEAN]) ] KeyLastReadTsTypeInv == @@ -387,7 +439,7 @@ CommittedConsistency == commit_ts == client_ts[c].commit_ts primary == client_key[c].primary secondary == client_key[c].secondary - w == [ts |-> commit_ts, type |-> "write", start_ts |-> start_ts] + w == [ts |-> commit_ts, type |-> "write", start_ts |-> start_ts, is_deleted |-> FALSE] IN client_state[c] = "committed" => \* The primary key lock must be cleaned up, and no any older lock.