{ "nbformat": 4, "nbformat_minor": 5, "metadata": { "kernelspec": { "display_name": "Python 3", "language": "python", "name": "python3" }, "language_info": { "name": "python", "version": "3.10" } }, "cells": [ { "cell_type": "markdown", "metadata": {}, "source": [ "# What Quorum Arithmetic Leaves Out\n", "\n", "Exhaustive finite-set checks and deterministic replica traces. The results show protocol counterexamples, not observed production failure frequencies. The code models fixed quorums, sloppy respondents, and the read write-back mechanism.\n", "\n", "Extract the complete package and run from this directory. Python 3.10+, standard library. No network calls." ], "id": "cell-01" }, { "cell_type": "code", "metadata": {}, "source": [ "from pathlib import Path\n", "import runpy, json, csv\n", "ROOT = Path.cwd()\n", "assert (ROOT / 'experiment.py').is_file(), 'Open this notebook from its extracted topic folder.'\n", "experiment = runpy.run_path(str(ROOT / 'experiment.py'))" ], "execution_count": 1, "outputs": [], "id": "cell-02" }, { "cell_type": "markdown", "metadata": {}, "source": [ "## Run and check\n", "The script executes the experiment and its assertions, then writes the data and figures." ], "id": "cell-03" }, { "cell_type": "code", "metadata": {}, "source": [ "summary = experiment['run'](ROOT)\n", "print(json.dumps(summary, indent=2))" ], "execution_count": 2, "outputs": [ { "output_type": "stream", "name": "stdout", "text": [ "{\n", " \"strict_pairs\": 9,\n", " \"strict_disjoint\": 0,\n", " \"expanded_pairs\": 100,\n", " \"expanded_disjoint\": 30,\n", " \"theorem_configurations_checked\": 140,\n", " \"theorem_pairs_checked\": 21343,\n", " \"writeback_pairs_checked\": 9,\n", " \"sloppy_read_before_handoff\": 0,\n", " \"sloppy_read_after_handoff\": 1,\n", " \"sequential_reads_without_writeback\": [\n", " 1,\n", " 0\n", " ],\n", " \"sequential_reads_with_writeback\": [\n", " 1,\n", " 1\n", " ],\n", " \"measurement\": \"Exhaustive finite-set model plus explicit deterministic traces, not a database benchmark or failure probability\",\n", " \"python\": \"3.12.14\",\n", " \"run_date\": \"2026-11-06\"\n", "}\n" ] } ], "id": "cell-04" }, { "cell_type": "markdown", "metadata": {}, "source": [ "## Inspect disjoint respondent pairs\n", "The 30 disjoint pairs are structural counterexamples, not a probability estimate." ], "id": "cell-05" }, { "cell_type": "code", "metadata": {}, "source": [ "rows = experiment['pairs']('ABCDE')\n", "disjoint = [row for row in rows if row['overlap'] == 0]\n", "print('Disjoint pairs:', len(disjoint))\n", "print(disjoint[:10])\n", "assert len(disjoint) == 30" ], "execution_count": 3, "outputs": [ { "output_type": "stream", "name": "stdout", "text": [ "Disjoint pairs: 30\n", "[{'write': 'AB', 'read': 'CD', 'intersection': '', 'overlap': 0}, {'write': 'AB', 'read': 'CE', 'intersection': '', 'overlap': 0}, {'write': 'AB', 'read': 'DE', 'intersection': '', 'overlap': 0}, {'write': 'AC', 'read': 'BD', 'intersection': '', 'overlap': 0}, {'write': 'AC', 'read': 'BE', 'intersection': '', 'overlap': 0}, {'write': 'AC', 'read': 'DE', 'intersection': '', 'overlap': 0}, {'write': 'AD', 'read': 'BC', 'intersection': '', 'overlap': 0}, {'write': 'AD', 'read': 'BE', 'intersection': '', 'overlap': 0}, {'write': 'AD', 'read': 'CE', 'intersection': '', 'overlap': 0}, {'write': 'AE', 'read': 'BC', 'intersection': '', 'overlap': 0}]\n" ] } ], "id": "cell-06" }, { "cell_type": "markdown", "metadata": {}, "source": [ "## Compare the read protocol\n", "One pending write reaches A only. Without write-back, sequential reads AB then BC return 1 then 0. Synchronous majority write-back before returning changes this trace to 1 then 1." ], "id": "cell-07" }, { "cell_type": "code", "metadata": {}, "source": [ "for repair in [False, True]:\n", " print('Synchronous write-back:', repair)\n", " for row in experiment['inversion_trace'](repair):\n", " print(row)" ], "execution_count": 4, "outputs": [ { "output_type": "stream", "name": "stdout", "text": [ "Synchronous write-back: False\n", "{'step': 0, 'event': 'Initial state', 'A': 0, 'B': 0, 'C': 0, 'result': ''}\n", "{'step': 1, 'event': 'Write v1 reaches A only; write is still pending', 'A': 1, 'B': 0, 'C': 0, 'result': ''}\n", "{'step': 2, 'event': 'Read 1 obtains A,B and selects newest version', 'A': 1, 'B': 0, 'C': 0, 'result': 'selected v1'}\n", "{'step': 4, 'event': 'Read 1 completes', 'A': 1, 'B': 0, 'C': 0, 'result': 'returns v1'}\n", "{'step': 5, 'event': 'Read 2 starts later and obtains B,C', 'A': 1, 'B': 0, 'C': 0, 'result': 'returns v0'}\n", "Synchronous write-back: True\n", "{'step': 0, 'event': 'Initial state', 'A': 0, 'B': 0, 'C': 0, 'result': ''}\n", "{'step': 1, 'event': 'Write v1 reaches A only; write is still pending', 'A': 1, 'B': 0, 'C': 0, 'result': ''}\n", "{'step': 2, 'event': 'Read 1 obtains A,B and selects newest version', 'A': 1, 'B': 0, 'C': 0, 'result': 'selected v1'}\n", "{'step': 3, 'event': 'Read 1 writes v1 back to A,B and waits for both acknowledgments', 'A': 1, 'B': 1, 'C': 0, 'result': ''}\n", "{'step': 4, 'event': 'Read 1 completes', 'A': 1, 'B': 1, 'C': 0, 'result': 'returns v1'}\n", "{'step': 5, 'event': 'Read 2 starts later and obtains B,C', 'A': 1, 'B': 1, 'C': 0, 'result': 'returns v1'}\n" ] } ], "id": "cell-08" }, { "cell_type": "markdown", "metadata": {}, "source": [ "## Generated figures" ], "id": "cell-09" }, { "cell_type": "code", "metadata": {}, "source": [ "from IPython.display import SVG, display\n", "display(SVG(filename=str(ROOT / 'figures/intersections.svg')))" ], "execution_count": 5, "outputs": [ { "output_type": "display_data", "data": { "image/svg+xml": "Fixed membership forces an overlap\n\n\nFixed membership forces an overlap\nCells list shared respondents. Write acknowledgments are rows; read respondents are columns.\nAB\nAB\nAC\nAC\nBC\nBC\n\nAB\n\nA\n\nB\n\nA\n\nAC\n\nC\n\nB\n\nC\n\nBC\nAll 9 pairs overlap when N=3 and R=W=2 use the same A,B,C.\n" }, "metadata": {} } ], "id": "cell-10" }, { "cell_type": "code", "metadata": {}, "source": [ "from IPython.display import SVG, display\n", "display(SVG(filename=str(ROOT / 'figures/read-inversion.svg')))" ], "execution_count": 6, "outputs": [ { "output_type": "display_data", "data": { "image/svg+xml": "An unfinished write can produce a read\u2013read inversion\n\n\nAn unfinished write can produce a read\u2013read inversion\nAll reads collect two home replicas. This version of the protocol omits synchronous write-back.\nA\nB\nC\n0 Initial state\n\nv0\n\nv0\n\nv0\n1 Write v1 reaches A only; write is still pending\n\nv1\n\nv0\n\nv0\n2 Read 1 obtains A,B and selects newest version\nselected v1\n\nv1\n\nv0\n\nv0\n4 Read 1 completes\nreturns v1\n\nv1\n\nv0\n\nv0\n5 Read 2 starts later and obtains B,C\nreturns v0\n\nv1\n\nv0\n\nv0\n" }, "metadata": {} } ], "id": "cell-11" }, { "cell_type": "code", "metadata": {}, "source": [ "from IPython.display import SVG, display\n", "display(SVG(filename=str(ROOT / 'figures/read-writeback.svg')))" ], "execution_count": 7, "outputs": [ { "output_type": "display_data", "data": { "image/svg+xml": "Writing back before returning prevents this inversion\n\n\nWriting back before returning prevents this inversion\nThe selected version reaches a majority before Read 1 completes.\nA\nB\nC\n0 Initial state\n\nv0\n\nv0\n\nv0\n1 Write v1 reaches A only; write is still pending\n\nv1\n\nv0\n\nv0\n2 Read 1 obtains A,B and selects newest version\nselected v1\n\nv1\n\nv0\n\nv0\n3 Read 1 writes v1 back to A,B and waits for both acknowledgments\n\nv1\n\nv1\n\nv0\n4 Read 1 completes\nreturns v1\n\nv1\n\nv1\n\nv0\n5 Read 2 starts later and obtains B,C\nreturns v1\n\nv1\n\nv1\n\nv0\n" }, "metadata": {} } ], "id": "cell-12" }, { "cell_type": "code", "metadata": {}, "source": [ "from IPython.display import SVG, display\n", "display(SVG(filename=str(ROOT / 'figures/sloppy-trace.svg')))" ], "execution_count": 8, "outputs": [ { "output_type": "display_data", "data": { "image/svg+xml": "A completed write can miss a later read\n\n\nA completed write can miss a later read\nDifferent reachability: write responds through A,D; later read responds through B,C.\nA\nB\nC\nD\nE\n0 Home replicas A,B,C start at v0; D,E are fallback nodes\n\nv0\n\nv0\n\nv0\n\nv0\n\nv0\n1 Write targets A,D,E; A,D store v1 and acknowledge\nwrite completes: W=2\n\nv1\n\nv0\n\nv0\n\nv1\n\nv0\n2 Later read coordinator receives B,C; handoff is delayed\nread returns v0: R=2\n\nv1\n\nv0\n\nv0\n\nv1\n\nv0\n3 D hands its hinted v1 to home replica B\n\nv1\n\nv1\n\nv0\n\nv1\n\nv0\n4 Read B,C again with newest-version selection\nread returns v1\n\nv1\n\nv1\n\nv0\n\nv1\n\nv0\n" }, "metadata": {} } ], "id": "cell-13" }, { "cell_type": "markdown", "metadata": {}, "source": [ "## Sources\n", "- [Dynamo: Amazon\u2019s Highly Available Key-value Store](https://cdn.amazon.science/ac/1d/eb50c4064c538c8ac440ce6a1d91/dynamo-amazons-highly-available-key-value-store.pdf)\n", "- [Sharing Memory Robustly in Message-Passing Systems](https://groups.csail.mit.edu/tds/papers/Attiya/JACM95.pdf)\n", "- [Bigtable replication overview](https://docs.cloud.google.com/bigtable/docs/replication-overview)\n", "- [How DynamoDB global tables work](https://docs.aws.amazon.com/amazondynamodb/latest/developerguide/V2globaltables_HowItWorks.html)" ], "id": "cell-14" } ] }