A [[http://clojure.org][Clojure]] library designed to help with testing stateful systems with [[https://github.com/clojure/test.check/][test.check]].
By writing a specification of how our system behaves (when you do ~X~, expect ~Y~), we can generate test cases to check that our implementation matches our specification. We can even detect the presence of some race conditions, by running commands in parallel. When a failure is encountered, shrinking can help us to see what went wrong with as few distractions as possible.
<img src="http://clojars.org/org.clojars.czan/stateful-check/latest-version.svg" alt="Clojars Project">
As an example, let's write a specification for Java's ~java.util.TreeMap~ implementation. This will allow us to find the (already known) race conditions present in its implementation.
This will be the final result, once we have assembled our specification:
;; no output, because our specification is correct when run sequentially (is (specification-correct? java-map-specification)) ;; => true
;; but a failure when run on multiple threads (is (specification-correct? java-map-specification {:gen {:threads 2} :run {:max-tries 100}})) ;; FAIL in () (form-init4244174681303601076.clj:54) ;; Sequential prefix: ;; ;; Thread a: ;; #<4a> = (:put "" 0) = nil ;; ;; Thread b: ;; #<2b> = (:put "tree" 0) = nil ;; #<4b> = (:get "tree") = nil ;; ;; expected: all executions to match specification ;; actual: the above execution did not match the specification ;; => false
~TreeMap~ fails to meet our specification (presented below) because it is possible to generate command lists which do not correspond to a sequential execution. In this case, there are three possible ways for these commands to be organised:
** Setup
To start off with we'll need to require some namespaces that we'll need later:
(require '[clojure.test :refer [is]] '[clojure.test.check.generators :as gen] '[stateful-check.core :refer [specification-correct?]])
We'll be testing a ~TreeMap~, so let's allocate one in a global variable that we'll access during our tests.
(def system-under-test (java.util.TreeMap.))
We're also going to need some keys, to insert into the map. We use a small set of keys to try to encourage the generated commands to act on the same keys. We could use a larger set (even infinitely large, such as ~gen/string~), but then we potentially lower the chance of us provoking a bug.
(def test-keys ["" "a" "house" "tree" "λ"])
** Commands
Our command to ~put~ things into the map is fairly simple. It chooses one of the keys at random, and a random integer. The ~:command~ key defines the behaviour of this command, which is to call ~.put~ on our map. We then modify our test's state to associate the key with the value. This state will then be read during ~get~ commands, so we know what to expect.
(def put-command {:args (fn [state] [(gen/elements test-keys) gen/int]) :command #(.put system-under-test %1 %2) :next-state (fn [state [k v] _] (assoc state k v))})
Our command to ~get~ things out of the map is also fairly simple. It requires that we think there's something in the map (because the test's state says so). It chooses one of the keys at random, and gets it out. The postcondition requires that the value we got out of the map matches what our state contains for that key.
(def get-command {:requires (fn [state] (seq state)) :args (fn [state] [(gen/elements test-keys)]) :command #(.get system-under-test %1) :postcondition (fn [prev-state _ [k] val] (= (get prev-state k) val))})
** Specification
Now we have to put these commands together into a specification. We also include a ~:setup~ function, which restores the map to a known state (no values). The test's state is implicitly ~nil~.
(def java-map-specification {:commands {:put #'put-command :get #'get-command} :setup #(.clear system-under-test)})
** Running
We can now run the test, as shown above.
(is (specification-correct? java-map-specification))
;; note that this call can take a long time, and may need to be run ;; multiple times to provoke a failure (is (specification-correct? java-map-specification {:gen {:threads 2} :run {:max-tries 100}})) ;; there are a few ways this can fail; the most fun failure thus far ;; was an NPE!
To view this example in one file, see [[file:test/stateful_check/java_map_test.clj][the relevant test file]].
If you'd like to read more, you can read [[file:doc/queue.org][a more complete of testing a queue]]. Alternatively you can try running the above test with a ~java.util.HashMap~ instead. Is it easier, or harder, to make it fail than the ~TreeMap~? Are the failures that you see different to the ~TreeMap~?
For a detailed description of how a ~stateful-check~ specification has to be structured, see [[file:doc/specification.org][the specification document]].
For more information about how the race condition detection works, see [[file:doc/race-conditions.org][the notes on ~stateful-check~'s race condition detection]].
Related work
[[https://github.com/clojure/test.check/][test.check]] (generative testing for Clojure, on which ~stateful-check~ is built)
[[http://www.quviq.com/index.html][QuviQ Quickcheck]] (commercial generative testing for Erlang)
[[http://proper.softlab.ntua.gr/index.html][PropEr]] (open source generative testing for Erlang)
Related talks
[[https://www.youtube.com/watch?v=zi0rHwfiX1Q][Testing the Hard Stuff and Staying Sane]] - John Hughes, 2014, the inspiration for this library
[[https://www.youtube.com/watch?v=xw8ZFU8CGdA][How to do Stateful Property Testing in Clojure]] - Magnus Kvalevåg, 2019, (~stateful-check~ is mentioned starting at [[https://www.youtube.com/watch?v=xw8ZFU8CGdA&t=571][9:31]])
Future work
hook into JVM scheduler/debugger to control scheduling to make tests reproducible
License
Copyright © 2014-2024 Carlo Zancanaro
Distributed under the MIT Licence.