stateful-check

A Clojure library designed to help with testing stateful systems with 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.

Example

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:

• 4a, 2b, then 4b
• 2b, 4a, then 4b
• 2b, 4b, then 4a

but none of these sequential executions match the output that we have seen. In any of them, we would expect 4b to have returned 0 instead of nil. Thus, we have found a race condition in java.util.TreeMap.

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 the relevant test file.

If you’d like to read more, you can read 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?

Specifications

For a detailed description of how a stateful-check specification has to be structured, see the specification document.

Race condition detection

For more information about how the race condition detection works, see the notes on stateful-check’s race condition detection.

Related work

• test.check (generative testing for Clojure, on which stateful-check is built)
• QuviQ Quickcheck (commercial generative testing for Erlang)
• PropEr (open source generative testing for Erlang)

Related talks

• Testing the Hard Stuff and Staying Sane - John Hughes, 2014, the inspiration for this library
• How to do Stateful Property Testing in Clojure - Magnus Kvalevåg, 2019, (stateful-check is mentioned starting at 9:31)

Future work

• hook into JVM scheduler/debugger to control scheduling to make tests reproducible

License

Copyright © 2020 Carlo Zancanaro

Distributed under the MIT Licence.