[bikallem]

Change

PR 4b2 of phase 4 (the plan of phase 4, section 4.3; E6 and E7). In a Tx, an atomic statement runs through the savepoint code of Tx.savepoint, with one counter and the same rules.

• Tx.exec of an atomic statement: SAVEPOINT cistern_sp_<n>, the commands, then RELEASE SAVEPOINT. in_savepoint is the body of Tx.savepoint. Each command checks the margin of the statement deadline, has the statement deadline as its flow deadline, and emits its own event.
• The error of a command goes through the rules of Tx.exec (command_error):
  • An error after which the server keeps the transaction (1062, 1406) gives ROLLBACK TO SAVEPOINT, and the Tx continues.
  • An error of the class Fails (1213, 1020 of MariaDB, a broken connection), an implicit commit and the margin of the Tx deadline fail the Tx, with no ROLLBACK TO SAVEPOINT.
  • The margin of an earlier statement deadline fails only the statement.
• A cancel between SAVEPOINT and RELEASE fails the Tx. A cancel in a command breaks the connection, and the end aborts it. Between two commands the connection stays usable: the cancel goes up, and the end of Db.transaction aborts the connection. If the callback catches the cancel, the end sends ROLLBACK on the usable connection. The first error is then Connection_lost on a healthy connection: it tells only "not committed".
• Exec.scope gets error: the rules of the caller emit the event of a command and give its error.
• DESIGN.md: "Execution of one statement", "Transactions", "Tests" and "Status".

Tests

• Sim rows (test_tx.ml, "atomic statements in a Tx"):
  • The commands and their events.
  • A 1406 and a 1062 of a child: ROLLBACK TO, and the Tx continues.
  • A 1213, a 1020 on MariaDB 11.8 and an implicit commit of a child: the Tx fails, with no ROLLBACK TO.
  • A lost reply of a child.
  • Two atomic statements and a Tx.savepoint use one counter.
  • A failed RELEASE SAVEPOINT.
  • The margin of a statement deadline and of the Tx deadline.
  • The flow deadline of a command.
  • A cancel in a command, and a cancel between two commands.
  • The deadline of the Tx in a command: Timeout, with no ROLLBACK, ROLLBACK TO or RELEASE.
  • A value with no literal: Invalid_value, no SAVEPOINT, and the Tx continues.
  • An atomic statement leaves the connection clean: no reset at the next checkout.
• The Tx storm: 1 step of 10 is an atomic statement of two commands, and its second command can be a deadlock. Each command that the fake server got has one event. Each seed runs atomic statements (with KILL, the sum over the seeds).
• make mutate against origin/main: 34 mutants, 34 killed.
• Each check passes on the commit: nix flake check, dune build and dune build @fmt with no output, the opam diff, dune runtest --force, nix fmt -- --check, check-scope and check-ocaml55. make sim-slow passes.
• The integration suite on the three servers: MySQL 8.4 89, and MariaDB 11.4 and 11.8 88 each. The new row is an atomic statement in a Tx: ROLLBACK TO SAVEPOINT after a duplicate key of a child, and the Tx commits its other rows.
• Planted bugs: the 11 plants of the worker and the 15 of the reviewer all fail. They include the 5 plants of 4b2 in the plan: START TRANSACTION in a Tx, a counter of its own, no ROLLBACK TO after a 1406, ROLLBACK TO after a 1213, and a Tx that continues after a cancel.

Reviews

A correctness review at a high effort, which judged the code correct and safe, also the choice not to abort the connection after a caught cancel between two commands: the Tx fails, no command is in flight, and the end sends ROLLBACK or discards the connection. Its fixes are test rows and documentation: the deadline of the Tx in a command, a value with no literal, a clean connection after an atomic statement, and the meaning of the caught cancel.