···3131- [ ] Fault injection
3232 - [ ] Kill/Restart nodes repeatedly
3333 - [ ] Silently and randomly drop messages between nodes
3434-- [ ] Add a full model-checker workload to verify strict-serializability of all operations
3434+- [X] Add a full model-checker workload to verify strict-serializability of all operations
3535- [ ] Add liveness tests (check cluster still responds after nodes are restored)
36363737### Documentation
+14-34
lib/workloads/model.ex
···22 alias Hobbes.Transaction
33 alias Hobbes.Transaction.TxnState
44 alias Hobbes.Structs.Cluster
55- alias Hobbes.Construct.SimServer
66-77- @behaviour Hobbes.Workloads.Workload
88-99- defmodule HistoryTxn do
1010- @enforce_keys [
1111- :status,
1212-1313- :read_version,
1414- :commit_version,
1515- :batch_index,
1616-1717- :read_results,
1818- :mutations,
1919- ]
2020- defstruct @enforce_keys
2152222- def new(status, %TxnState{} = txn, read_results, mutations)
2323- when is_atom(status) and is_list(read_results) and is_list(mutations) do
2424- %HistoryTxn{
2525- status: status,
66+ alias Hobbes.Construct.SimServer
2672727- read_version: txn.read_version,
2828- commit_version: txn.commit_version,
2929- batch_index: txn.batch_index,
88+ alias Hobbes.Workloads.Model.DatabaseModel
99+ alias Hobbes.Workloads.Model.DatabaseModel.HistoryTxn
30103131- read_results: read_results,
3232- mutations: mutations,
3333- }
3434- end
3535- end
1111+ @behaviour Hobbes.Workloads.Workload
36123713 defmodule Client do
3814 use Hobbes.Construct.SimServer
···9167 {:error, :timeout} -> raise "Timeout not supported"
9268 end
9369 else
9494- # TODO: new() errors, read() errors
9595- error -> raise "Error: #{inspect(error)}"
7070+ # Transaction.new() timed out
7171+ {:error, :timeout} -> state
7272+7373+ # Read errors
7474+ # TODO: we still want to check these reads
7575+ {:error, {%TxnState{} = _txn, _results}} -> state
9676 end
9777 end
9878···195175 results =
196176 clients
197177 |> Enum.map(&SimServer.send_request(&1, :stop))
198198- |> Enum.map(&SimServer.receive_response/1)
178178+ |> Enum.map(&SimServer.receive_response(&1, 300_000))
199179 |> Enum.map(fn {:reply, reply} -> reply end)
200180201181 history =
202182 results
203183 |> Enum.map(fn %{history: history} -> history end)
204184 |> Enum.concat()
205205- |> Enum.sort_by(fn %HistoryTxn{} = ht ->
206206- {ht.commit_version, ht.batch_index}
207207- end)
185185+186186+ db_model = DatabaseModel.new()
187187+ DatabaseModel.validate_history(db_model, history)
208188209189 {
210190 :ok,
+124
lib/workloads/model/database_model.ex
···11+defmodule Hobbes.Workloads.Model.DatabaseModel do
22+ alias Hobbes.Transaction.TxnState
33+ alias Hobbes.Structs.RangeResult
44+ alias Hobbes.KV.TestKV
55+66+ alias Hobbes.Workloads.Model.DatabaseModel
77+88+ import ExUnit.Assertions, only: [assert: 1]
99+1010+ defmodule HistoryTxn do
1111+ @enforce_keys [
1212+ :status,
1313+1414+ :read_version,
1515+ :commit_version,
1616+ :batch_index,
1717+1818+ :read_results,
1919+ :mutations,
2020+ ]
2121+ defstruct @enforce_keys
2222+2323+ def new(status, %TxnState{} = txn, read_results, mutations)
2424+ when is_atom(status) and is_list(read_results) and is_list(mutations) do
2525+ %HistoryTxn{
2626+ status: status,
2727+2828+ read_version: txn.read_version,
2929+ commit_version: txn.commit_version,
3030+ batch_index: txn.batch_index,
3131+3232+ read_results: read_results,
3333+ mutations: mutations,
3434+ }
3535+ end
3636+ end
3737+3838+ @type t :: %__MODULE__{
3939+ kv: TestKV.t,
4040+ }
4141+ @enforce_keys [:kv]
4242+ defstruct @enforce_keys
4343+4444+ def new do
4545+ %DatabaseModel{
4646+ kv: TestKV.new(),
4747+ }
4848+ end
4949+5050+ def validate_history(%DatabaseModel{kv: kv} = _dbm, history) when is_list(history) do
5151+ history =
5252+ Enum.sort_by(history, fn %HistoryTxn{} = ht ->
5353+ {ht.commit_version, ht.batch_index}
5454+ end)
5555+5656+ Enum.reduce(history, kv, fn %HistoryTxn{} = txn, kv ->
5757+ validate_transaction(kv, txn)
5858+ end)
5959+ end
6060+6161+ defp validate_transaction(%TestKV{} = kv, %HistoryTxn{} = txn) do
6262+ :ok = validate_reads(kv, txn)
6363+6464+ kv =
6565+ case txn.status do
6666+ :committed ->
6767+ apply_mutations(kv, txn)
6868+6969+ # TODO: validate :read_conflict and :transaction_too_old are correct
7070+ _ -> kv
7171+ end
7272+7373+ kv
7474+ end
7575+7676+ defp apply_mutations(%TestKV{} = kv, %HistoryTxn{} = txn) do
7777+ assert txn.status == :committed
7878+ assert txn.commit_version
7979+8080+ commit_version = txn.commit_version
8181+8282+ Enum.reduce(txn.mutations, kv, fn
8383+ {:write, k, v}, kv -> TestKV.put(kv, commit_version, k, v)
8484+ end)
8585+ end
8686+8787+ defp validate_reads(%TestKV{} = kv, %HistoryTxn{} = txn) do
8888+ read_version = txn.read_version
8989+9090+ Enum.each(txn.read_results, fn
9191+ {{:read, keys}, results} ->
9292+ Enum.each(keys, fn key ->
9393+ expected = Map.fetch!(results, key)
9494+ received = TestKV.get(kv, read_version, key)
9595+9696+ if expected != received do
9797+ read_error(kv, txn, key, expected, received)
9898+ end
9999+ end)
100100+101101+ {{:read_range, {sk, ek} = range}, expected} ->
102102+ %RangeResult{pairs: received} = TestKV.scan(kv, read_version, sk, ek)
103103+104104+ if expected != received do
105105+ read_error(kv, txn, range, expected, received)
106106+ end
107107+ end)
108108+109109+ :ok
110110+ end
111111+112112+ defp read_error(%TestKV{} = _kv, %HistoryTxn{} = txn, read, expected, received) do
113113+ raise """
114114+ Error while validating transaction: read results do not match!
115115+116116+ Read version: #{inspect(txn.read_version)}
117117+118118+ Key/Range: #{inspect(read)}
119119+120120+ Expected: #{inspect(expected, pretty: true)}
121121+ Received: #{inspect(received, pretty: true)}
122122+ """
123123+ end
124124+end