{
  "model": "finite deterministic FaRM commit-path model",
  "not_modeled": [
    "real RDMA or NIC acknowledgements",
    "NVRAM or SSD power-failure behavior",
    "ZooKeeper membership and lease timing",
    "arbitrary schedules or production FaRM"
  ],
  "recovery": {
    "all_backup_records": {
      "decision": "commit",
      "votes": {
        "r1": "commit-backup",
        "r2": "commit-backup"
      }
    },
    "locks_only_before_decision": {
      "decision": "abort",
      "votes": {
        "r1": "lock",
        "r2": "lock"
      }
    },
    "mutant_skipped_r2_backup_then_primaries_failed": {
      "atomic_durability_preserved": false,
      "decision": "abort",
      "previously_exposed": {
        "r1": 1,
        "r2": 1
      },
      "recoverable": {
        "r1": 1,
        "r2": null
      },
      "votes": {
        "r1": "commit-backup",
        "r2": "abort"
      }
    },
    "one_primary_commit_survives": {
      "decision": "commit",
      "votes": {
        "r1": "commit-primary",
        "r2": "commit-backup"
      }
    }
  },
  "write_skew_correct": {
    "final": {
      "x": 0,
      "y": 1
    },
    "ignore_lock_bits_during_validation": false,
    "serializable": true,
    "status": {
      "T1": "aborted",
      "T2": "committed"
    },
    "validation": {
      "T1": false,
      "T2": true
    }
  },
  "write_skew_mutant": {
    "final": {
      "x": 1,
      "y": 1
    },
    "ignore_lock_bits_during_validation": true,
    "serializable": false,
    "status": {
      "T1": "committed",
      "T2": "committed"
    },
    "validation": {
      "T1": true,
      "T2": true
    }
  },
  "write_write_conflict": {
    "final": {
      "counter": 1
    },
    "lock": {
      "T1": true,
      "T2": false
    },
    "status": {
      "T1": "committed",
      "T2": "aborted"
    }
  }
}