Details
-
Task
-
Resolution: Unresolved
-
Major
-
None
-
Cheshire-Cat
-
None
Description
Description:
Previously, there were plans to remove the transactions related code from Jepsen as it didn't really fit under the Jepsen project in the context of producing histories which would then be analysed by the linearizability checker.
However, it looks like Jepsen comes with the Elle checker as a dependency:
https://github.com/jepsen-io/jepsen/blob/main/jepsen/project.clj
Furthermore, there is a checker which works with transactions and uses Elle to detect cycles:
https://github.com/jepsen-io/jepsen/blob/5628ee5ff308885670cc854575a6a24967d4c32c/jepsen/src/jepsen/tests/cycle.clj#L16
The transactions look like the following
{:type :ok, :value [[:append :x 2] [:append :y 1]]}
|
{:type :ok, :value [[:append :x 1] [:r :y [1]]]}
|
Variables such as :x and :y are lists and there’s an append operation and a read operation which returns the list.
In which case it might make more sense to repurpose the transactions code and more generally produce histories which can be accepted by Elle.
Side note: We're currently 'read committed.