Re: Potential G2-item cycles under serializable isolation

On 6/5/20 6:44 PM, Peter Geoghegan wrote:

> Hopefully this helps you, Kyle. Would you mind repeating the exercise
> from earlier with this new log file/execution?

Here's a quick runthrough of G2-item #0:

Let:
  T1 = {:type :ok, :f :txn, :value [[:append 1468 3] [:r 1469 nil] [:append
1439 2]], :time 22408795244, :process 49, :index 10392}
  T2 = {:type :ok, :f :txn, :value [[:append 1469 1] [:append 1456 2] [:r 1468
nil]], :time 22565885165, :process 45, :index 10464}

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

Classic G2: two rw-edges, where each transaction failed to observe the other's
write. I restricted the log to just those processes:

egrep 'process (49|45)' log_rr_recording.log

I jumped to the write of 1468 with /'1468'/, then backtracked to process 45's BEGIN:

[rr 316503 580915] 1591388175.849-316503-5/231-0-SHOW-5edaa7f9.4d457-jepsen
process 45 LOG:  execute <unnamed>: SHOW TRANSACTION ISOLATION LEVEL
[rr 316503 581192] 1591388175.858-316503-5/232-0-SET-5edaa7f9.4d457-jepsen
process 45 LOG:  execute <unnamed>: SET SESSION CHARACTERISTICS AS TRANSACTION
ISOLATION LEVEL SERIALIZABLE
[rr 316503 581202] 1591388175.858-316503-5/233-0-BEGIN-5edaa7f9.4d457-jepsen
process 45 LOG:  execute <unnamed>: BEGIN

45 tries to append 1 to 1469, but fails because it found zero rows:

[rr 316503 581206] 1591388175.859-316503-5/233-0-UPDATE-5edaa7f9.4d457-jepsen
process 45 LOG:  execute <unnamed>: update txn2 set val = CONCAT(val, ',', $1)
where id = $2
 1591388175.859-316503-5/233-0-UPDATE-5edaa7f9.4d457-jepsen process 45 DETAIL: 
parameters: $1 = '1', $2 = '1469'

45 backs off to an insert:

[rr 316503 581222] 1591388175.859-316503-5/233-0-SAVEPOINT-5edaa7f9.4d457-jepsen
process 45 LOG:  execute <unnamed>: savepoint upsert

49 jumps in to start a transaction:

[rr 316514 581232] 1591388175.860-316514-13/401-0-SHOW-5edaa7f9.4d462-jepsen
process 49 LOG:  execute <unnamed>: SHOW TRANSACTION ISOLATION LEVEL
[rr 316514 581242] 1591388175.860-316514-13/402-0-SET-5edaa7f9.4d462-jepsen
process 49 LOG:  execute <unnamed>: SET SESSION CHARACTERISTICS AS TRANSACTION
ISOLATION LEVEL SERIALIZABLE
[rr 316514 581256] 1591388175.860-316514-13/403-0-BEGIN-5edaa7f9.4d462-jepsen
process 49 LOG:  execute <unnamed>: BEGIN

49 tries to update 1468, which also fails, and backs off to an insert:

[rr 316514 581350] 1591388175.864-316514-13/403-0-UPDATE-5edaa7f9.4d462-jepsen
process 49 LOG:  execute <unnamed>: update txn1 set val = CONCAT(val, ',', $1)
where id = $2
 1591388175.864-316514-13/403-0-UPDATE-5edaa7f9.4d462-jepsen process 49
DETAIL:  parameters: $1 = '3', $2 = '1468'
[rr 316514 581364]
1591388175.864-316514-13/403-0-SAVEPOINT-5edaa7f9.4d462-jepsen process 49 LOG: 
execute <unnamed>: savepoint upsert
[rr 316514 581374] 1591388175.865-316514-13/403-0-INSERT-5edaa7f9.4d462-jepsen
process 49 LOG:  execute <unnamed>: insert into txn1 (id, sk, val) values ($1,
$2, $3)
 1591388175.865-316514-13/403-0-INSERT-5edaa7f9.4d462-jepsen process 49
DETAIL:  parameters: $1 = '1468', $2 = '1468', $3 = '3'

45 performs its insert of 1469:

[rr 316503 581548] 1591388175.871-316503-5/233-0-INSERT-5edaa7f9.4d457-jepsen
process 45 LOG:  execute <unnamed>: insert into txn2 (id, sk, val) values ($1,
$2, $3)
 1591388175.871-316503-5/233-0-INSERT-5edaa7f9.4d457-jepsen process 45 DETAIL: 
parameters: $1 = '1469', $2 = '1469', $3 = '1'
[rr 316503 581562]
1591388175.872-316503-5/233-1680808-RELEASE-5edaa7f9.4d457-jepsen process 45
LOG:  execute <unnamed>: release savepoint upsert

And goes on to update 1456, which also fails, so it inserts there too:

[rr 316503 581576]
1591388175.872-316503-5/233-1680808-UPDATE-5edaa7f9.4d457-jepsen process 45
LOG:  execute <unnamed>: update txn0 set val = CONCAT(val, ',', $1) where id = $2
 1591388175.872-316503-5/233-1680808-UPDATE-5edaa7f9.4d457-jepsen process 45
DETAIL:  parameters: $1 = '2', $2 = '1456'
[rr 316503 581980]
1591388175.887-316503-5/233-1680808-SAVEPOINT-5edaa7f9.4d457-jepsen process 45
LOG:  execute <unnamed>: savepoint upsert
[rr 316503 581994]
1591388175.887-316503-5/233-1680808-INSERT-5edaa7f9.4d457-jepsen process 45
LOG:  execute <unnamed>: insert into txn0 (id, sk, val) values ($1, $2, $3)
 1591388175.887-316503-5/233-1680808-INSERT-5edaa7f9.4d457-jepsen process 45
DETAIL:  parameters: $1 = '1456', $2 = '1456', $3 = '2'
[rr 316503 582008]
1591388175.888-316503-5/233-1680808-RELEASE-5edaa7f9.4d457-jepsen process 45
LOG:  execute <unnamed>: release savepoint upsert

45 reads 1468, observing 0 rows:

[rr 316503 582018]
1591388175.888-316503-5/233-1680808-SELECT-5edaa7f9.4d457-jepsen process 45
LOG:  execute <unnamed>: select (val) from txn1 where id = $1
 1591388175.888-316503-5/233-1680808-SELECT-5edaa7f9.4d457-jepsen process 45
DETAIL:  parameters: $1 = '1468'

And 45 commits:

[rr 316503 582028]
1591388175.888-316503-5/233-1680808-COMMIT-5edaa7f9.4d457-jepsen process 45
LOG:  execute <unnamed>: COMMIT

49's insert succeeded, and it goes on to read 1469, finding 0 rows as well. This
should cause the transaction to abort, because 1469 was written by a committed
transaction performed by process 45, *and* 45 didn't observe 49's writes.

[rr 316514 582409]
1591388175.902-316514-13/403-1680806-RELEASE-5edaa7f9.4d462-jepsen process 49
LOG:  execute <unnamed>: release savepoint upsert
[rr 316514 582419]
1591388175.902-316514-13/403-1680806-SELECT-5edaa7f9.4d462-jepsen process 49
LOG:  execute <unnamed>: select (val) from txn2 where sk = $1
 1591388175.902-316514-13/403-1680806-SELECT-5edaa7f9.4d462-jepsen process 49
DETAIL:  parameters: $1 = '1469'

49 goes on to append to 1439, which, again, fails and backs off to insert:

[rr 316514 583918]
1591388175.956-316514-13/403-1680806-UPDATE-5edaa7f9.4d462-jepsen process 49
LOG:  execute <unnamed>: update txn0 set val = CONCAT(val, ',', $1) where id = $2
 1591388175.956-316514-13/403-1680806-UPDATE-5edaa7f9.4d462-jepsen process 49
DETAIL:  parameters: $1 = '2', $2 = '1439'
[rr 316514 584036]
1591388175.960-316514-13/403-1680806-SAVEPOINT-5edaa7f9.4d462-jepsen process 49
LOG:  execute <unnamed>: savepoint upsert
[rr 316514 584283]
1591388175.970-316514-13/403-1680806-INSERT-5edaa7f9.4d462-jepsen process 49
LOG:  execute <unnamed>: insert into txn0 (id, sk, val) values ($1, $2, $3)
 1591388175.970-316514-13/403-1680806-INSERT-5edaa7f9.4d462-jepsen process 49
DETAIL:  parameters: $1 = '1439', $2 = '1439', $3 = '2'[rr 316514 584299]
1591388175.971-316514-13/403-1680806-RELEASE-5edaa7f9.4d462-jepsen process 49
LOG:  execute <unnamed>: release savepoint upsert

And 49 commits, resulting in a G2-item.

[rr 316514 584309]
1591388175.971-316514-13/403-1680806-COMMIT-5edaa7f9.4d462-jepsen process 49
LOG:  execute <unnamed>: COMMIT

--Kyle