jepsen-io / elle Goto Github PK

View Code? Open in Web Editor NEW

624.0 624.0 35.0 12.27 MB

Black-box transactional safety checker based on cycle detection

License: Eclipse Public License 2.0

Shell 0.04% Isabelle 50.32% TeX 0.21% Clojure 47.54% Java 1.89%

elle's People

Contributors

Stargazers

Watchers

elle's Issues

The rw-register checker succeeds on the history: wx1, rx2.

The following history succeds with the rw-register checker (with :strict-serializable model and linearisable-keys? true):

{:type :invoke, :f :txn :value [[:w :x 1]],   :process 0, :index 1}
{:type :ok,     :f :txn :value [[:w :x 1]],   :process 0, :index 2}
{:type :invoke, :f :txn :value [[:r :x nil]], :process 0, :index 3}
{:type :ok,     :f :txn :value [[:r :x 2]],   :process 0, :index 4}

Adding an other read to the history makes it fail, e.g.:

{:type :invoke, :f :txn :value [[:r :x nil]], :process 0, :index 5}
{:type :ok,     :f :txn :value [[:r :x 1]],   :process 0, :index 6}

This doesn't seem right to me, but perhaps I'm missing something?

I've captured the above in two test cases in the following PR #7.

Is there any example on how to use the gen function?

First of all, I'm not a closure programmer. So it might be a very dump question.

(ns jepsen.test
  (:require [elle.list-append :as a]
            [elle.txn :as ct]
            [jepsen.history :as h]
            [clojure.pprint :refer [pprint]]))
(defn -main
    (pprint (take 100 (ct/wr-txns {:key-count 3}))))

I'm trying to print out some txn history so that I can use the sequence to check my work. But it doesn't compile. lein run gives me this error:

Syntax error macroexpanding clojure.core/defn at (jepsen/test.clj:11:1).
pprint - failed: vector? at: [:fn-tail :arity-n :bodies :params] spec: :clojure.core.specs.alpha/param-list
(pprint (take 100 (ct/wr-txns {:key-count 3}))) - failed: vector? at: [:fn-tail :arity-1 :params] spec: :clojure.core.specs.alpha/param-list

I don't know what the error messages mean.

Publish jar files for each release

please publish jar files

Feature: add delete operation

Currently elle supports reads and writes/appends. Is there a way to add delete operations?

Could Elle tell the difference between snapshot isolation and strong-session-snapshot-isolation?

In the consistency models you provided in README, I found that you have distinguished PL-SI (snapshot-isolation), strong-session-snapshot-isolation and strong-snapshot-isolation. However, it seems that you have not implemented this in Elle?

I constructed this history of 4 transactions running in 3 processes. There is a cycle as shown in the picture above. In other words, strong-session-snapshot-isolation is violated by this history.

(def h [{:type :invoke, :value [[:r :x nil] [:r :z nil]], :process 0, :index 0}
        {:type :ok, :value [[:r :x nil] [:r :z [1]]], :process 0, :index 1}
        {:type :invoke, :value [[:append :x 1]], :process 1, :index 2}
        {:type :ok, :value [[:append :x 1]], :process 1, :index 3}
        {:type :invoke, :value [[:r :z nil]], :process 1, :index 4}
        {:type :ok, :value [[:r :z nil]], :process 1, :index 5}
        {:type :invoke, :value [[:append :z 1]], :process 2, :index 6}
        {:type :ok, :value [[:append :z 1]], :process 2, :index 7}])

However, when I cloned the latest release v0.1.5, and checked this history by Elle, the result is valid.

Did I miss any key steps or did not set any key parameters when checking?

I would appreciate it if you could give a prompt reply.

Sincerely,
Young

Build fails with `lein check`

Building with lein check fails, with a Reflection warning and a syntax warning on the current master (531ea9a).

The problem seems to be a missing variable txn/int-write-mops

$ lein check
Compiling namespace elle.graph
Reflection warning, elle/graph.clj:683:15 - call to method select can't be resolved (target class is unknown).
Compiling namespace elle.version-graph
Compiling namespace elle.history
Compiling namespace elle.util
Compiling namespace elle.set-add
Syntax error compiling at (elle/recovery.clj:102:10).
No such var: txn/int-write-mops

Full report at:
/tmp/clojure-17876742899113241601.edn
Failed.

Contents of the report:

{:clojure.main/message
 "Syntax error compiling at (elle/recovery.clj:102:10).\nNo such var: txn/int-write-mops\n",
 :clojure.main/triage
 {:clojure.error/phase :compile-syntax-check,
  :clojure.error/line 102,
  :clojure.error/column 10,
  :clojure.error/source "recovery.clj",
  :clojure.error/path "elle/recovery.clj",
  :clojure.error/class java.lang.RuntimeException,
  :clojure.error/cause "No such var: txn/int-write-mops"},
 :clojure.main/trace
 {:via
  [{:type clojure.lang.Compiler$CompilerException,
    :message "Syntax error compiling at (elle/recovery.clj:102:10).",
    :data
    {:clojure.error/phase :compile-syntax-check,
     :clojure.error/line 102,
     :clojure.error/column 10,
     :clojure.error/source "elle/recovery.clj"},
    :at [clojure.lang.Compiler analyze "Compiler.java" 6808]}
   {:type java.lang.RuntimeException,
    :message "No such var: txn/int-write-mops",
    :at [clojure.lang.Util runtimeException "Util.java" 221]}],
  :trace
  [[clojure.lang.Util runtimeException "Util.java" 221]
   [clojure.lang.Compiler resolveIn "Compiler.java" 7388]
   [clojure.lang.Compiler resolve "Compiler.java" 7358]
   [clojure.lang.Compiler analyzeSymbol "Compiler.java" 7319]
   [clojure.lang.Compiler analyze "Compiler.java" 6768]
   [clojure.lang.Compiler analyze "Compiler.java" 6745]
   [clojure.lang.Compiler$InvokeExpr parse "Compiler.java" 3888]
   [clojure.lang.Compiler analyzeSeq "Compiler.java" 7109]
   [clojure.lang.Compiler analyze "Compiler.java" 6789]
   [clojure.lang.Compiler analyze "Compiler.java" 6745]
   [clojure.lang.Compiler$InvokeExpr parse "Compiler.java" 3888]
   [clojure.lang.Compiler analyzeSeq "Compiler.java" 7109]
   [clojure.lang.Compiler analyze "Compiler.java" 6789]
   [clojure.lang.Compiler analyze "Compiler.java" 6745]
   [clojure.lang.Compiler$InvokeExpr parse "Compiler.java" 3888]
   [clojure.lang.Compiler analyzeSeq "Compiler.java" 7109]
   [clojure.lang.Compiler analyze "Compiler.java" 6789]
   [clojure.lang.Compiler analyzeSeq "Compiler.java" 7095]
   [clojure.lang.Compiler analyze "Compiler.java" 6789]
   [clojure.lang.Compiler analyze "Compiler.java" 6745]
   [clojure.lang.Compiler$BodyExpr$Parser parse "Compiler.java" 6120]
   [clojure.lang.Compiler$LetExpr$Parser parse "Compiler.java" 6436]
   [clojure.lang.Compiler analyzeSeq "Compiler.java" 7107]
   [clojure.lang.Compiler analyze "Compiler.java" 6789]
   [clojure.lang.Compiler analyzeSeq "Compiler.java" 7095]
   [clojure.lang.Compiler analyze "Compiler.java" 6789]
   [clojure.lang.Compiler analyze "Compiler.java" 6745]
   [clojure.lang.Compiler$BodyExpr$Parser parse "Compiler.java" 6120]
   [clojure.lang.Compiler$FnMethod parse "Compiler.java" 5467]
   [clojure.lang.Compiler$FnExpr parse "Compiler.java" 4029]
   [clojure.lang.Compiler analyzeSeq "Compiler.java" 7105]
   [clojure.lang.Compiler analyze "Compiler.java" 6789]
   [clojure.lang.Compiler analyzeSeq "Compiler.java" 7095]
   [clojure.lang.Compiler analyze "Compiler.java" 6789]
   [clojure.lang.Compiler access$300 "Compiler.java" 38]
   [clojure.lang.Compiler$DefExpr$Parser parse "Compiler.java" 596]
   [clojure.lang.Compiler analyzeSeq "Compiler.java" 7107]
   [clojure.lang.Compiler analyze "Compiler.java" 6789]
   [clojure.lang.Compiler analyze "Compiler.java" 6745]
   [clojure.lang.Compiler eval "Compiler.java" 7181]
   [clojure.lang.Compiler load "Compiler.java" 7636]
   [clojure.lang.RT loadResourceScript "RT.java" 381]
   [clojure.lang.RT loadResourceScript "RT.java" 372]
   [clojure.lang.RT load "RT.java" 459]
   [clojure.lang.RT load "RT.java" 424]
   [clojure.core$load$fn__6839 invoke "core.clj" 6126]
   [clojure.core$load invokeStatic "core.clj" 6125]
   [clojure.core$load doInvoke "core.clj" 6109]
   [clojure.lang.RestFn invoke "RestFn.java" 408]
   [clojure.core$load_one invokeStatic "core.clj" 5908]
   [clojure.core$load_one invoke "core.clj" 5903]
   [clojure.core$load_lib$fn__6780 invoke "core.clj" 5948]
   [clojure.core$load_lib invokeStatic "core.clj" 5947]
   [clojure.core$load_lib doInvoke "core.clj" 5928]
   [clojure.lang.RestFn applyTo "RestFn.java" 142]
   [clojure.core$apply invokeStatic "core.clj" 667]
   [clojure.core$load_libs invokeStatic "core.clj" 5989]
   [clojure.core$load_libs doInvoke "core.clj" 5969]
   [clojure.lang.RestFn applyTo "RestFn.java" 137]
   [clojure.core$apply invokeStatic "core.clj" 667]
   [clojure.core$require invokeStatic "core.clj" 6007]
   [clojure.core$require doInvoke "core.clj" 6007]
   [clojure.lang.RestFn invoke "RestFn.java" 457]
   [elle.set_add$eval568$loading__6721__auto____569
    invoke
    "set_add.clj"
    1]
   [elle.set_add$eval568 invokeStatic "set_add.clj" 1]
   [elle.set_add$eval568 invoke "set_add.clj" 1]
   [clojure.lang.Compiler eval "Compiler.java" 7177]
   [clojure.lang.Compiler eval "Compiler.java" 7166]
   [clojure.lang.Compiler load "Compiler.java" 7636]
   [clojure.lang.RT loadResourceScript "RT.java" 381]
   [clojure.lang.RT loadResourceScript "RT.java" 372]
   [clojure.lang.RT load "RT.java" 459]
   [clojure.lang.RT load "RT.java" 424]
   [clojure.core$load$fn__6839 invoke "core.clj" 6126]
   [clojure.core$load invokeStatic "core.clj" 6125]
   [clojure.core$load doInvoke "core.clj" 6109]
   [clojure.lang.RestFn invoke "RestFn.java" 408]
   [user$eval140$fn__151 invoke "form-init12736845212758803140.clj" 1]
   [user$eval140 invokeStatic "form-init12736845212758803140.clj" 1]
   [user$eval140 invoke "form-init12736845212758803140.clj" 1]
   [clojure.lang.Compiler eval "Compiler.java" 7177]
   [clojure.lang.Compiler eval "Compiler.java" 7167]
   [clojure.lang.Compiler load "Compiler.java" 7636]
   [clojure.lang.Compiler loadFile "Compiler.java" 7574]
   [clojure.main$load_script invokeStatic "main.clj" 475]
   [clojure.main$init_opt invokeStatic "main.clj" 477]
   [clojure.main$init_opt invoke "main.clj" 477]
   [clojure.main$initialize invokeStatic "main.clj" 508]
   [clojure.main$null_opt invokeStatic "main.clj" 542]
   [clojure.main$null_opt invoke "main.clj" 539]
   [clojure.main$main invokeStatic "main.clj" 664]
   [clojure.main$main doInvoke "main.clj" 616]
   [clojure.lang.RestFn applyTo "RestFn.java" 137]
   [clojure.lang.Var applyTo "Var.java" 705]
   [clojure.main main "main.java" 40]],
  :cause "No such var: txn/int-write-mops",
  :phase :compile-syntax-check}}

Cannot run on the latest version of Clojure on Ubuntu 22.04: reducers.clj is not found

Run has failed with latest Clojure on Ubuntu 22.04:

[0] ~/sources/elle-cli/elle$ lein deps                                                                                                  
Retrieving com/gfredericks/test.chuck/0.2.14/test.chuck-0.2.14.pom from clojars                                                         
Retrieving com/gfredericks/test.chuck/0.2.14/test.chuck-0.2.14.jar from clojars                                                         
[0] ~/sources/elle-cli/elle$ lein uberjar                                                                                               
Compiling 3 source files to /home/sergeyb/sources/elle-cli/elle/target/classes                                                          
warning: [options] bootstrap class path not set in conjunction with -source 8                                                           
Note: Some input files use unchecked or unsafe operations.                                                                              
Note: Recompile with -Xlint:unchecked for details.                                                                                      
1 warning                                                                                                                               
Created /home/sergeyb/sources/elle-cli/elle/target/elle-0.1.8.jar                                                                       
Created /home/sergeyb/sources/elle-cli/elle/target/elle-0.1.8-standalone.jar                                                            
[0] ~/sources/elle-cli/elle$ java -jar ./target/elle-0.1.8-standalone.jar                                                               
Clojure 1.2.1                                                                                                                           
user=> (require '[elle.list-append :as a]                                                                                               
            '[jepsen.history :as h])                                                                                                    
java.io.FileNotFoundException: Could not locate clojure/core/reducers__init.class or clojure/core/reducers.clj on classpath:  (list_append.clj:1)

Is it possible to somehow check minimal version before start? Otherwise, it is not clear why reducers.clj is not found. (Hint: required Clojure version is 1.11.1 according to project.clj).

Ubuntu 22.04 x86_64, Clojure 1.10.2

Modeling linearizable keys with the list-append workload

I'm trying to test our database with jepsen, and having trouble to model our (probably unusual) guarantees. Currently our transactions guarantee serializable isolation, but additionally non-stale reads (all committed changes must be visible in subsequent transactions), and due to implementation it's probably per key (or even per shard) linearizable. Due to single-shard optimizations we are not yet strict-serializable however: independent single-key writes may be assigned local shard timestamps, which appear reordered from the global time perspective.

Example of a possible history:

(require '[elle.list-append :as a]
         '[jepsen.history :as h])

(def h (h/history
        [{:process 0, :time 1000, :type :invoke, :f :txn, :value [[:r :x nil] [:r :y nil]]}
         {:process 1, :time 1001, :type :invoke, :f :txn, :value [[:append :x 1]]}
         {:process 1, :time 1010, :type :ok, :f :txn, :value [[:append :x 1]]}
         {:process 1, :time 1011, :type :invoke, :f :txn, :value [[:append :y 2]]}
         {:process 1, :time 1020, :type :ok, :f :txn, :value [[:append :y 2]]}
         {:process 0, :time 1030, :type :ok, :f :txn, :value [[:r :x []] [:r :y [2]]]}]))

(pprint (a/check {:consistency-models [:serializable]} h))
(pprint (a/check {:consistency-models [:strict-serializable]} h))

This history is obviously serializable, but not strict serializable.

Consider this history however:

(def h (h/history
        [{:process 1, :time 1001, :type :invoke, :f :txn, :value [[:append :x 1]]}
         {:process 1, :time 1010, :type :ok, :f :txn, :value [[:append :x 1]]}
         {:process 1, :time 1011, :type :invoke, :f :txn, :value [[:r :x nil]]}
         {:process 1, :time 1020, :type :ok, :f :txn, :value [[:r :x []]]}]))

This history is also serializable, and not strict serializable. But it also shows stale read, and is not per key linearizable.

Unfortunately, both :strong-read-committed and :linearizable show this history as valid for some reason:

...=> (pprint (a/check {:consistency-models [:strong-read-committed]} h))
{:valid? true}
nil
...=> (pprint (a/check {:consistency-models [:linearizable]} h))
{:valid? true}
nil

I'm not sure whether it's because :strong-read-committed and :linearizable are not implemented, or whether I misunderstand what they mean. Unfortunately testing with :strict-serializable shows G-single-item-realtime and G-nonadjacent-item-realtime anomalies, which appear to be due to reordered writes. And :serializable is too weak.

I'm a novice in clojure, so don't quite understand how to extend elle to do what I want, can you please point me in the right direction on how to check for additional realtime restrictions over serializable isolation?

Could I check a history that with real-time order

suppose I have a history like this

(def his 
[{:type :ok, :process 1, :value [[:r 0 nil] [:w 0 1]], :time 0}
 {:type :ok, :process 2, :value [[:w 0 2]], :time 1}
 {:type :ok, :process 3, :value [[:r 0 1]], :time 2}])

processes 1 and 2 are concurrent.
process 3 is executed when processes 1 and 2 finish.
Obviously, this history is not serializable, but elle could not work due to missing real-time order

Elle may miss two types of transaction anomalies:

During my testing, I found the following two anomalies may be ignored by elle.

Cycle of wr-process-wr
This case comes from transactional causal consistency:

(def h
  [{:process 1, :type :invoke, :f :txn, :value [[:r :x] [:append :y 1]], :index 0}
   {:process 1, :type :ok, :f :txn, :value [[:r :x [1]] [:append :y 1]], :index 1}
   {:process 2, :type :invoke, :f :txn, :value [[:r :y]], :index 2}
   {:process 2, :type :ok, :f :txn, :value [[:r :y [1]]], :index 3}
   {:process 2, :type :invoke, :f :txn, :value [[:append :x 1]], :index 4}
   {:process 2, :type :ok, :f :txn, :value [[:append :x 1]], :index 5}])

Here is my REPL screenshot

It is obvious that there is a cycle and I think this cycle should be prohibited by stong-session-snapshot-isolation

Future Read
This case is about the internal consistency for a transaction.

I know elle do something special for internal-cases for read-your-writes condition, but maybe elle does not check for the future read.

I would appreciate it if you could give a prompt reply.

Sincerely,
Young

PL-2L(monotonic-view) G-monotonic: experiment with adding the anomaly

Hi,

I'm working on using Elle as a checker for causal consistency.
Yes, the CRDTs are finally coming in the form of local first sync layers. :)

While testing with :consistency-models [:consistent-view], it seemed like lots of anomalies were not being caught.
Looking at the graphs and cycle-anomalies, consistent-view was:

missing the process-order graph
reporting anomalies at higher consistency levels, e.g. strong-session-snapshot-isolation

Looking at how elle.txn used -process, reportable-anomalies, etc lead to looking at Adya's Weak Consistency to see where process order and the expected anomalies were introduced. And in 4.2.2 PL-2L:

G-monotonic: Monotonic Reads. A history H exhibits phenomenon G-monotonic for transaction Ti if there exists a cycle in USG(H, Ti ) containing exactly one anti-dependency edge from a read node ri (xj ) (or ri (P: xj )) to some transaction node Tk (and any number of order or dependency edges).

Which Elle expresses as:

:G-single {:rels        (rels/union ww wwp wr wrp)
           :single-rels (rels/union rw rwp)
           :type        :G-single}

And if we test using G-single-process as additional :anomalies [:G-single-process]:

(def opts
  {:consistency-models [:consistent-view] ; Adya formalism for causal consistency
   :sequential-keys? true                 ; infer version order from elle/process-graph
   :wfr-keys? true                        ; rw/wfr-version-graph within txns
   })

(def mono-writes-anomaly
  (->> [{:process 0 :value [[:w :x 0]]   :type :ok :f :txn}
        {:process 0 :value [[:w :y 0]]   :type :ok :f :txn}
        {:process 1 :value [[:r :y 0]]   :type :ok :f :txn}
        {:process 1 :value [[:r :x nil]] :type :ok :f :txn}]
       h/history))

(rw/check opts mono-writes-anomaly)
{:valid? true}

(rw/check (assoc opts :anomalies [:G-single-process]) mono-writes-anomaly)
{:valid? false,
 :anomaly-types [:G-single-item-process],
 :anomalies {:G-single-item-process [{:cycle [{:index 3, :time -1, :type :ok, :process 1, :f :txn, :value [[:r :x nil]]}
                                              {:index 0, :time -1, :type :ok, :process 0, :f :txn, :value [[:w :x 0]]}
                                              {:index 1, :time -1, :type :ok, :process 0, :f :txn, :value [[:w :y 0]]}
                                              {:index 2, :time -1, :type :ok, :process 1, :f :txn, :value [[:r :y 0]]}
                                              {:index 3, :time -1, :type :ok, :process 1, :f :txn, :value [[:r :x nil]]}],
                                      :steps [{:key :x, :value nil, :value' 0, :type :rw, :a-mop-index 0, :b-mop-index 0}
                                              {:type :process, :process 0}
                                              {:type :wr, :key :y, :value 0, :a-mop-index 0, :b-mop-index 0}
                                              {:type :process, :process 1}], :type :G-single-item-process}]},
 :not #{:strong-session-snapshot-isolation},
 :also-not #{:strong-serializable :strong-session-serializable :strong-snapshot-isolation}}

🎉
It also catches more writes-follow-reads in other tests too.

But if G-single-process is added to the direct-proscribed-anomalies:

:monotonic-view [:G1 :G-monotonic   ; Adya
                 :G-single-process]

We no longer find the G-single-item-process, but only the stronger consistency strong-session-snapshot-isolation-cycle-exists:

(et/reportable-anomaly-types opts)
#{:G-cursor :G-monotonic :G-single :G-single-item :G-single-item-process :G-single-process :G0 :G1 :G1a :G1b :G1c :PL-1-cycle-exists :PL-2-cycle-exists :cycle-search-timeout :cyclic-versions :dirty-update :duplicate-elements :empty-transaction-graph :future-read :incompatible-order :lost-update}

(rw/check opts mono-writes-anomaly)
{:valid? true}

(:anomalies (et/cycles! opts (partial rw/graph opts) mono-writes-anomaly))
{:strong-session-snapshot-isolation-cycle-exists [{:type :strong-session-snapshot-isolation-cycle-exists,
                                                   :not :strong-session-snapshot-isolation,
                                                   :subgraph [:extension [:union :ww :wwp :wr :wrp :process] [:union :rw :rwp]],
                                                   :scc-size 3,
                                                   :scc #{0 1 2}}]}

I've looked at opts :anomalies handling in prohibited-anomaly-types, cycle identification in cycle-explainer, and a few other places and I can't find anything anomalous. :)

I do think that:

monotonic-view's G-monotonic needs to be expressed, it's currently a no-op
causal, consistent-view, has to end up with process order
G-monotonic, as G-single-process, would:
- more correctly identify what consistency level you are and :not :also-not
- catch some of the tests labeled not possible to catch at the given consistency level as they are actually writes-follows-reads and/or monotonic-writes anomalies.

Was hoping you would be able to confirm that this is generally a good idea, desired?
And if so, any ideas on where to look to understand and change the behavior?

Thanks!

(P.S. This is my first time really trying to understand DAGs, cycles, etc and Elle is a wonderful teaching tool. I keep thinking, Wow! It's as if Elle was designed for this, then remembering it most certainly was. 😆

list-append/sorted-values might be broken with history object

I am running a Jepsen test from Jepsen-io/mongodb and using [jepsen "0.3.3-SNAPSHOT"], I am seeing this error below. Can anyone help? Thanks
here is the lein run command
lein run test-all -w list-append -n n1 -n n2 -n n3 -n n4 -n n5 -n n6 -n n7 -n n8 -n n9 -r 1000 --concurrency 3n --time-limit 240 --max-writes-per-key 128 --read-concern majority --write-concern majority --txn-read-concern snapshot --txn-write-concern majority --nemesis-interval 1 --nemesis partition --test-count 1

here is the error message:

[2023/08/24 00:06:52.509] INFO [2023-08-24 00:06:52,428] jepsen test runner - jepsen.core Analyzing...
[2023/08/24 00:06:52.509] WARN [2023-08-24 00:06:52,508] clojure-agent-send-off-pool-78 - jepsen.checker Error while checking history:
[2023/08/24 00:06:52.509] java.lang.ClassCastException: class clojure.lang.LazySeq cannot be cast to class jepsen.history.IHistory (clojure.lang.LazySeq and jepsen.history.IHistory are in unnamed module of loader 'app')
[2023/08/24 00:06:52.509] at elle.list_append$sorted_values.invokeStatic(list_append.clj:257)
[2023/08/24 00:06:52.509] at elle.list_append$sorted_values.invoke(list_append.clj:223)
[2023/08/24 00:06:52.509] at jepsen.mongodb.list_append$divergence_stats_checker$reify__2906.check(list_append.clj:174)
[2023/08/24 00:06:52.509] at jepsen.checker$check_safe.invokeStatic(checker.clj:86)
[2023/08/24 00:06:52.509] at jepsen.checker$check_safe.invoke(checker.clj:79)
[2023/08/24 00:06:52.509] at jepsen.checker$compose$reify__10709$fn__10711.invoke(checker.clj:102)
[2023/08/24 00:06:52.509] at clojure.core$pmap$fn__8552$fn__8553.invoke(core.clj:7089)
[2023/08/24 00:06:52.509] at clojure.core$binding_conveyor_fn$fn__5823.invoke(core.clj:2047)
[2023/08/24 00:06:52.509] at clojure.lang.AFn.call(AFn.java:18)
[2023/08/24 00:06:52.509] at java.base/java.util.concurrent.FutureTask.run(FutureTask.java:264)
[2023/08/24 00:06:52.509] at java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1128)
[2023/08/24 00:06:52.509] at java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:628)
[2023/08/24 00:06:52.509] at java.base/java.lang.Thread.run(Thread.java:829)
[2023/08/24 00:06:54.572] INFO [2023-08-24 00:06:54,572] jepsen test runner - jepsen.core Analysis complete

Example for running test-cases with Elle?

Hello Jepsen developers,

I'm currently working as a researcher in a company project that is inventing a new key-value store, and I have found this Jepsen I/O, which can be an excellent benchmark for checking the anomalies.

I'm checking the scope of the workload that needs to be done so that the Elle can be used to the company's new key-value store. For now, what I see from the provided test directory is that Elle can run the consistency model using the history hand-created by the developer.

Are there any good examples that I can follow to run Elle with Jepsen I/O and a database as a whole? (not the unit-test) I have read the amazing papers that Elle is actually applied in many different databases, and I want to see how the test case is done, so I can propose the Jepsen I/O as the main benchmark for checking the anomalies.

Example with list-append history is broken in 0.1.6

In a new version 0.1.6 example described in a README ¹ is broken:

elle.core=> (require '[elle.list-append :as a])
nil
elle.core=> h
[{:type :ok, :value [[:append :x 1] [:r :y [1]]]} {:type :ok, :value [[:append :x 2] [:append :y 1]]} {:type :ok, :value [[:r :x [1 2]]]}]
elle.core=> (pprint (a/check {:consistency-models [:serializable], :directory "out"} h))
Execution error (ExceptionInfo) at jepsen.history/filter (history.clj:1143).
Assert failed:
{:type :jepsen.history/not-history,
 :history-type clojure.lang.PersistentVector}


elle.core=>

This is probably due to significant changes in history format, https://github.com/jepsen-io/jepsen/releases/tag/v0.3.0

https://github.com/jepsen-io/elle#demo ↩

Elle checks :fail results?

I'm working on a test with Elle to verify serializable transactions.
I have a question about checking anomalies.

Does Elle check the anomalies with :fail results?
I tried Elle via Jepsen (jepsen.tests.cycle.append/test), but I had anomalies for :fail results.
I'd like to ignore these :fail results for checking anomalies.

{:clock {:valid? true},
 :stats
 {:valid? true,
  :count 1504,
  :ok-count 318,
  :fail-count 1184,
  :info-count 2,
  :by-f
  {:txn
   {:valid? true,
    :count 1504,
    :ok-count 318,
    :fail-count 1184,
    :info-count 2}}},
 :exceptions {:valid? true},
 :workload
 {:valid? false,
  :anomaly-types (:G1a :G1b :dirty-update),
  :anomalies
  {:G1a
   ({:op
     {:type :ok,
      :f :txn,
      :value [[:r 18 [1]] [:r 17 [3]] [:append 6 10] [:append 17 9]],
      :time 24868956077,
      :process 0,
      :index 101},
     :mop [:r 18 [1]],
     :writer
     {:type :fail,
      :f :txn,
      :value
      [[:append 14 6]
       [:append 18 1]
       [:r 17 nil]
       [:r 17 nil]
       [:r 17 nil]
       [:append 14 7]
       [:append 18 2]],
      :time 24441252230,
      :process 1,
      :error [:crud-error "rollback is toward non-prepared record"],
      :index 91},
     :element 1}
...

Elle couldn't check list-append example described in a paper

There is a regression in comparison to previous Elle version.
Elle cannot check example described in paper ¹:

elle.core=>  (require '[elle.list-append :as a]
       #_=>             '[jepsen.history :as h])
nil
elle.core=>  (def h (h/history
       #_=>             [{:index 0 :type :invoke  :value [[:append 253 1] [:append 253 3] [:append 253 4] [:append 255 2] [:append 255 3] [:append 255 4] [:append 255 5] [:append 256 1] [:append 256 2]]}
       #_=> {:index 1 :type :ok      :value [[:append 253 1] [:append 253 3] [:append 253 4] [:append 255 2] [:append 255 3] [:append 255 4] [:append 255 5] [:append 256 1] [:append 256 2]]}
       #_=> {:index 2 :type :invoke, :value [[:append 255 8] [:r 253 nil]]}
       #_=> {:index 3 :type :ok,     :value [[:append 255 8] [:r 253 [1 3 4]]]}
       #_=> {:index 4 :type :invoke, :value [[:append 256 4] [:r 255 nil] [:r 256 nil] [:r 253 nil]]}
       #_=> {:index 5 :type :ok,     :value [[:append 256 4] [:r 255 [2 3 4 5 8]] [:r 256 [1 2 4]] [:r 253 [1 3 4]]]}
       #_=> {:index 6 :type :invoke, :value [[:append 250 10] [:r 253 nil] [:r 255 nil] [:append 256 3]]}
       #_=> {:index 7 :type :ok      :value [[:append 250 10] [:r 253 [1 3 4]] [:r 255 [2 3 4 5]] [:append 256 3]]}]))
#'elle.core/h
elle.core=> (pprint (a/check {:consistency-models [:serializable], :directory "out"} h))
{:valid? :unknown,
 :anomaly-types (:empty-transaction-graph),
 :anomalies {:empty-transaction-graph true},
 :not #{},
 :also-not #{}}
nil
elle.core=>

Version: 49a209f

https://github.com/jepsen-io/elle/blob/main/histories/paper-example.edn ↩

jepsen-io / elle Goto Github PK

elle's People

Contributors

Stargazers

Watchers

Forkers

elle's Issues

Footnotes

Footnotes

Recommend Projects

Recommend Topics

Recommend Org