search

jepsen-io / elle

Black-box transactional safety checker based on cycle detection
Eclipse Public License 2.0
644 stars 34 forks source link

Add check for mismatch of operations in history #10

Closed aquarhead closed 3 years ago

aquarhead commented 3 years ago

This is intended to fix https://github.com/jepsen-io/maelstrom/issues/14

I can see the result by injecting the op-mismatch as :internal anomalies, which will (cause maelstrom to) output like this if I simply use append for all µ-op functions:

 :workload {:valid? false,
            :anomaly-types (:internal),
            :anomalies {:internal (([[:r 6 nil] [:append 6 nil]])
                                   ([[:r 9 nil] [:append 9 [1]]]
                                    [[:r 9 nil] [:append 9 [1]]])
                                   ([[:r 9 nil] [:append 9 nil]]
                                    [[:r 8 nil] [:append 8 nil]])
                                   ([[:r 8 nil] [:append 8 nil]]))},

I still need to find a place to let the checker realize the :op-mismatch anomalies though, it seems I would need to add it somewhere in consistency_model.clj? And at this point I'm not sure if this should be considered as a "consistency model", or which one (I'm interested in this field but I'm not fluent in the terminologies). Could you point out where I should add it?

Also this is my first time contributing to Clojure projects (actually first time working on any Clojure projects), so kindly inform me if there're better ways to approach things. There're also probably some excessive comments, let me know if they should be removed.

And obviously the error message/return should be improved.

aphyr commented 3 years ago

Hey, thanks for this! I think you're on the right track here, but Elle's checkers are complicated and I'm gonna need to look at this carefully (and get tests in place) before merging. Might be a little bit--I've got a bunch of unfinished Elle work in progress that I gotta button up first, and that's waiting on me getting time off from client work.

aphyr commented 3 years ago

So this breaks... 28 different tests, haha--mostly because we were relying on not needing to generate completely well-formed histories in the test code. Not a huge deal, but it does create a lot of work for me. In the future, I'd appreciate it if you could run the tests first!

aquarhead commented 3 years ago

Sorry about that xD

I'm completely new to Clojure projects but will keep this in mind in the future :)

aphyr commented 3 years ago

Errrgh, okay, this is gonna take me several hours to fix, and I'm on the clock for a client. I'm gonna revert this for now, but you're welcome to take a pass at fixing the tests yourself!