diff --git a/Percolator/Concurrent/ConcurrentPercolator.cfg b/Percolator/Concurrent/ConcurrentPercolator.cfg index e13d0a2..8fe03ad 100644 --- a/Percolator/Concurrent/ConcurrentPercolator.cfg +++ b/Percolator/Concurrent/ConcurrentPercolator.cfg @@ -17,4 +17,6 @@ INVARIANT LockConsistency CommittedConsistency AbortedConsistency + RollbackConsistency + UniqueWrite SnapshotIsolation diff --git a/Percolator/Concurrent/ConcurrentPercolator.tla b/Percolator/Concurrent/ConcurrentPercolator.tla index 784bf28..4fc6768 100644 --- a/Percolator/Concurrent/ConcurrentPercolator.tla +++ b/Percolator/Concurrent/ConcurrentPercolator.tla @@ -35,8 +35,10 @@ VARIABLES key_data VARIABLES key_lock \* $key_write[k]$ is a sequence of committed version of the key. -\* A committed version of the key is a record of [ts: commit_ts, -\* start_ts: start_ts]. +\* A committed version of the key is a record of [ts: ts, type: type, +\* start_ts: start_ts]. $type$ can be "write" or "rollback" depending on record +\* type. $start_ts$ field only exists if type is "write". For "write" record, +\* $ts$ denotes commit_ts; for "rollback" record, $ts$ denotes start_ts. VARIABLES key_write \* Two auxiliary variables for verifying snapshot isolation invariant. These @@ -78,11 +80,15 @@ hasStaleLock(k, ts) == \* Returns the writes with start_ts equals to $ts$. findWriteWithStartTS(k, ts) == - {w \in Range(key_write[k]) : w.start_ts = ts} + {w \in Range(key_write[k]) : (w.type = "write" /\ w.start_ts = ts)} \* Returns the writes with commit_ts equals to $ts$. findWriteWithCommitTS(k, ts) == - {w \in Range(key_write[k]) : w.ts = 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$. +hasRollback(k, ts) == + {r \in Range(key_write[k]) : (r.type = "rollback" /\ r.ts = 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 @@ -100,39 +106,44 @@ checkSnapshotIsolation(k, commit_ts) == \* 1. If the primary key is committed, we must also commit the secondary key. \* 2. Otherwise, clean up the stale data too. cleanupStaleLock(k, ts) == - \E l \in key_lock[k] : - /\ isStaleLock(l, ts) - /\ UNCHANGED <> - /\ \/ /\ l.primary = k \* this is a primary key, always rollback - \* because it is not committed. - /\ key_data' = [key_data EXCEPT ![k] = @ \ {[ts |-> l.ts]}] - /\ key_lock' = [key_lock EXCEPT ![k] = @ \ {l}] - /\ UNCHANGED <> - \/ /\ l.primary # k \* this is a secondary key. - /\ LET - writes == findWriteWithStartTS(l.primary, l.ts) - IN - IF writes = {} - THEN - \* 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 hasLockEQ(l.primary, l.ts) + LET + \* Erases the lock by removing data and lock, and write a rollback record. + 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"])] + IN + \E l \in key_lock[k] : + /\ isStaleLock(l, ts) + /\ UNCHANGED <> + /\ \/ /\ l.primary = k \* this is a primary key, always rollback + \* because it is not committed. + /\ eraseLock(k, l) + /\ UNCHANGED <> + \/ /\ l.primary # k \* this is a secondary key. + /\ LET + ws == findWriteWithStartTS(l.primary, l.ts) + IN + IF ws = {} THEN - /\ key_data' = [key_data EXCEPT ![l.primary] = @ \ {[ts |-> l.ts]}] - /\ key_lock' = [key_lock EXCEPT ![l.primary] = @ \ {l}] - /\ UNCHANGED <> + \* 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 + THEN + /\ eraseLock(l.primary, l) + /\ UNCHANGED <> + ELSE + /\ eraseLock(k, l) + /\ UNCHANGED <> ELSE - /\ key_data' = [key_data EXCEPT ![k] = @ \ {[ts |-> l.ts]}] - /\ key_lock' = [key_lock EXCEPT ![k] = @ \ {l}] - /\ UNCHANGED <> - ELSE - \* the primary key is committed, commit the secondary key. - \E w \in writes : - /\ key_lock' = [key_lock EXCEPT ![k] = @ \ {l}] - /\ key_write' = [key_write EXCEPT ![k] = Append(@, w)] - /\ checkSnapshotIsolation(k, w.ts) - /\ UNCHANGED <> + \* the primary key is committed, commit the secondary key. + \E w \in ws : + /\ key_lock' = [key_lock EXCEPT ![k] = @ \ {l}] + /\ key_write' = [key_write EXCEPT ![k] = Append(@, w)] + /\ checkSnapshotIsolation(k, w.ts) + /\ UNCHANGED <> \* Cleans up a stale lock when the client encounters one. cleanup(c) == @@ -160,14 +171,14 @@ readKey(c) == /\ key_last_read_ts' = [key_last_read_ts EXCEPT ![k] = start_ts] /\ UNCHANGED <> -\* Returns TRUE if there is no lock for key $k$, and no any newer write than +\* Returns TRUE if there is no lock for key $k$, and no any newer writes than \* $ts$. canLockKey(k, ts) == LET writes == {w \in DOMAIN key_write[k] : key_write[k][w].ts >= ts} IN /\ key_lock[k] = {} \* no any lock for the key. - /\ writes = {} \* no any newer write. + /\ writes = {} \* no any newer writes or rollbacks. \* Locks the key and places the data. lockKey(k, start_ts, primary) == @@ -182,18 +193,15 @@ lock(c) == primary == client_key[c].primary pending == client_key[c].pending IN - IF primary \in pending - THEN \* primary key is not locked, lock it first. - /\ canLockKey(primary, start_ts) - /\ lockKey(primary, start_ts, primary) - /\ client_key' = [client_key EXCEPT ![c].pending = @ \ {primary}] + \* Different from normal percolator protocol, which issues a prewrite on + \* primary lock first, then secondary locks, hereby we issues prewrites + \* on both primary and secondary locks concurrently. Rollback mechanism + \* ensures its correctness. + \E k \in pending : + /\ canLockKey(k, start_ts) + /\ lockKey(k, start_ts, primary) + /\ client_key' = [client_key EXCEPT ![c].pending = @ \ {k}] /\ UNCHANGED <> - ELSE \* primary key has already been locked, choose a secondary key to lock. - \E k \in pending : - /\ canLockKey(k, start_ts) - /\ lockKey(k, start_ts, primary) - /\ client_key' = [client_key EXCEPT ![c].pending = @ \ {k}] - /\ UNCHANGED <> \* Commits the primary key. commitPrimary(c) == @@ -203,8 +211,12 @@ commitPrimary(c) == primary == client_key[c].primary IN /\ hasLockEQ(primary, start_ts) - /\ key_write' = [key_write EXCEPT ![primary] = Append(@, [ts |-> commit_ts, start_ts |-> start_ts])] - /\ key_lock' = [key_lock EXCEPT ![primary] = @ \ {[ts |-> start_ts, primary |-> primary]}] + /\ key_write' = [key_write EXCEPT ![primary] = + Append(@, [ts |-> commit_ts, + type |-> "write", + start_ts |-> start_ts])] + /\ key_lock' = [key_lock EXCEPT ![primary] = @ \ {[ts |-> start_ts, + primary |-> primary]}] /\ checkSnapshotIsolation(primary, commit_ts) /\ UNCHANGED <> @@ -314,7 +326,9 @@ KeyLockTypeInv == key_lock \in [KEY -> SUBSET [ts : Nat, primary : KEY]] KeyWriteTypeInv == - key_write \in [KEY -> Seq([ts : Nat, start_ts : Nat])] + key_write \in [KEY -> Seq([ts : Nat, type : {"write"}, start_ts : Nat] \union + [ts : Nat, type : {"rollback"}]) + ] KeyLastReadTsTypeInv == key_last_read_ts \in [KEY -> Nat] @@ -339,11 +353,15 @@ TypeInvariant == \* start_ts. WriteConsistency == /\ \A k \in KEY : - \A n \in 1..Len(key_write[k]) - 1 : - key_write[k][n].ts < key_write[k][n + 1].start_ts + \A i, j \in 1..Len(key_write[k]) : + (/\ i < j + /\ key_write[k][i].type = "write" + /\ key_write[k][j].type = "write" + ) => + key_write[k][i].ts < key_write[k][j].start_ts /\ \A k \in KEY : - \A n \in 1..Len(key_write[k]) : - key_write[k][n].start_ts < key_write[k][n].ts + \A w \in Range(key_write[k]) : + w.type = "write" => w.start_ts < w.ts LockConsistency == \* There should be at most one lock for each key. @@ -365,7 +383,7 @@ CommittedConsistency == commit_ts == client_ts[c].commit_ts primary == client_key[c].primary secondary == client_key[c].secondary - w == [ts |-> commit_ts, start_ts |-> start_ts] + w == [ts |-> commit_ts, type |-> "write", start_ts |-> start_ts] IN client_state[c] = "committed" => \* The primary key lock must be cleaned up, and no any older lock. @@ -394,6 +412,28 @@ AbortedConsistency == ) => findWriteWithCommitTS(client_key[c].primary, client_ts[c].commit_ts) = {} +\* For each transaction, we cannot have both committed and rolled back keys. +RollbackConsistency == + \A c \in CLIENT : + LET + start_ts == client_ts[c].start_ts + hasWriteKey == \E k \in KEY : findWriteWithStartTS(k, start_ts) # {} + hasRollbackKey == \E k \in KEY : hasRollback(k, start_ts) + IN + start_ts > 0 => ~ (hasWriteKey /\ hasRollbackKey) + +\* For each key, each write or rollback record in write column should have a +\* unique start_ts. +UniqueWrite == + LET + getStartTs(w) == + IF w.type = "write" + THEN w.start_ts + ELSE w.ts + IN + \A k \in KEY : + Cardinality({getStartTs(w) : w \in Range(key_write[k])}) = Len(key_write[k]) + \* Snapshot isolation invariant should be preserved. SnapshotIsolation == \A k \in KEY : diff --git a/Percolator/Concurrent/ConcurrentPercolator.toolbox/ConcurrentPercolator___ConcurrentPercolatorModel.launch b/Percolator/Concurrent/ConcurrentPercolator.toolbox/ConcurrentPercolator___ConcurrentPercolatorModel.launch index a1dce55..0721fee 100644 --- a/Percolator/Concurrent/ConcurrentPercolator.toolbox/ConcurrentPercolator___ConcurrentPercolatorModel.launch +++ b/Percolator/Concurrent/ConcurrentPercolator.toolbox/ConcurrentPercolator___ConcurrentPercolatorModel.launch @@ -28,6 +28,8 @@ + +