queue.org

A simple queue example

As an example, let’s test a mutable queue (a PersistentQueue in an atom). Our queue will have three operations: new, push and pop. Before we get started, though, let’s import some things which we’ll need later.

(ns stateful-check.example
  (:require [clojure.test :refer [is]]
            [clojure.test.check.generators :as gen]
            [stateful-check.core :refer [specification-correct?]]))

Defining

new-queue

The implementation for the new-queue function is quite simple:

(defn new-queue [] (atom clojure.lang.PersistentQueue/EMPTY))

In order to use it with stateful-check we also need to model its semantics:

(def new-queue-specification
  {:requires (fn [state] (nil? state))
   :command #'new-queue
   :next-state (fn [state _ result] {:queue result, :elements []})})

This specification contains three elements:

• :requires specifies that this command is only valid if the state of the system is nil (which in this case means: nothing has been done to the system yet)
• :command specifies what to do to actually run this command. For this command we want to allocate a new queue.
• :next-state denotes the effect that running this command will have on the state of the system. In this case running the new-queue function will initialise the state. :elements is set to the empty vector because our queue starts off empty. :queue is set to the result of calling the :command function to store it for later operations.

In this instance the :next-state function is called when performing both the abstract and the real evaluation. This means that :result could be a symbolic value, and thus cannot be operated on directly in :next-state. When a symbolic value is used as an argument to a later command, however, it will be replaced by its corresponding concrete value (as can be seen below, where :queue is used as an argument to push-queue and pop-queue).

push-queue

Similarly, push-queue is fairly simple to implement.

(defn push-queue [queue val]
  (swap! queue conj val)
  nil)

Then its semantics:

(def push-queue-specification
  {:requires (fn [state] state)
   :args (fn [state] [(:queue state) gen/nat])
   :command #'push-queue
   :next-state (fn [state [_ val] _] (update-in state [:elements] conj val))})

This specification has one additional element over new-queue-specification:

• :args specifies a function which will provide a generator to generate arguments for push-queue. What we pass is converted into a generator where possible. In this case we are returning the queue under test ((:queue state)) as well as a generated natural number (gen/nat).

In addition to this, we can see that :requires merely requires that there be something truthy in the state, and :next-state simply adds the command to the end of the :elements vector in the state map.

pop-queue

Lastly, pop-queue:

(defn pop-queue [queue]
  (swap! queue pop))

(def pop-queue-specification
  {:requires (fn [state] (seq (:elements state)))
   :args (fn [state] [(:queue state)])
   :command #'pop-queue
   :next-state (fn [state [queue] _] (update-in state [:elements] (comp vec next)))
   :postcondition (fn [state _ [_] val] (= (first (:elements state)) val))})

This specification has one more element from push-queue-specification:

• :postcondition determines whether the result of performing this action correctly matches the expectation (from the abstract state). In our case: we expect the value returned by pop-queue to be the first value in the :elements vector.

Running

Now we want to run our specification. In order to do this we first need to assemble each of our command specifications into a full model specification.

(def queue-spec
  {:commands {:new #'new-queue-specification
              :push #'push-queue-specification
              :pop #'pop-queue-specification}})

The :commands key just contains a map of each command spec we are using for this model.

Let’s see what happens when we run this specification:

(is (specification-correct? queue-spec {:run {:seed 1438362541481}}))
;; 
;; FAIL in () (form-init4764932752973424260.clj:1)
;; Sequential prefix:
;;   #<1> = (:new) = #atom[#object[clojure.lang.PersistentQueue 0x9060190 "clojure.lang.PersistentQueue@1"] 0x766dbf8c]
;;   #<2> = (:push #<1> 0) = nil
;;   #<3> = (:pop #<1>) = #object[clojure.lang.PersistentQueue 0x13952b4e "clojure.lang.PersistentQueue@1"]
;; 
;; expected: all executions to match specification
;;   actual: the above execution did not match the specification

Whoops! It failed! We must have a bug somewhere.

Okay, we seem to have an error when we create a queue, then push a value into it, then pop the value back out. So it could be a problem with any of our operations.

Looking at the return value of the :pop step, though, we can see that it’s returning the wrong thing! It’s returning us a queue, not a value from the queue. We have a bug!

So, let’s fix our error.

(defn pop-queue [queue]
  (let [val (peek @queue)]
    (swap! queue pop)
    val))

Now let’s try running our tests again.

(is (specification-correct? queue-spec))

No output? That means the test passed! Success!

Running tests to find race conditions

Now that we’ve fixed our tests in the sequential case, let’s check to see if we have any race conditions in our data structure! To do this, we just add a few more options to our command. We’re going to add a :gen option to change the behaviour of our command generator to generate two threads, and we’ll add a :run option to run each tests a maximum of ten times, in an attempt to provoke an error.

(is (specification-correct? queue-spec {:gen {:threads 2}
                                        :run {:max-tries 10}}))
;;
;; FAIL in () (form-init4764932752973424260.clj:1)
;; Sequential prefix:
;;   #<1> = (:new) = #atom[#object[clojure.lang.PersistentQueue 0x9060190 "clojure.lang.PersistentQueue@1"] 0x48cf3d4c]
;;   #<2> = (:push #<1> 0) = nil
;;   #<3> = (:push #<1> 1) = nil
;; 
;; Thread a:
;;   #<1a> = (:pop #<1>) = 0
;; 
;; Thread b:
;;   #<1b> = (:pop #<1>) = 0
;; 
;; expected: all executions to match specification
;;   actual: the above execution did not match the specification

One again, our test is failing! We have a race condition!

The above output tells us that the race condition can be provoked by allocating a new queue and pushing a 0 and a 1 into it. Then, in two parallel threads, pop the top value of the thread. Now there are two possible ways this should go: either Thread a should get a 0 and Thread b should get a 1, or the other way around. We can see in the output above that both threads got a 0 when they popped the queue. That’s not right!

If you run this test multiple times, you’ll notice that it gives a different output. This is because race condition tests are non-deterministic (at least at the moment). They attempt to reproduce failures by trying many times (hence the :max-tries option), but this isn’t reliable. You may need to experiment to find values which work for your use-case.

Given we have shown that our queue is correct when we tested it sequentially, this should make us suspicious of our pop operation. Let’s have a look at its implementation again:

(defn pop-queue [queue]
  (let [val (peek @queue)]
    (swap! queue pop)
    val))

In our haste to fix the earlier problem that we had with pop-queue, we accidentally introduced a race condition. It’s possible for two threads to each execute (peek @queue) before either of them has run (swap! queue pop). This will result the first value in the queue being returned in two separate threads, and one being silently dropped.

To fix this we’re going to have to use a lower level operation: compare-and-set!. The details of this are beyond the scope of this example, so I will provide an implementation without further explanation.

(defn pop-queue [queue]
  (let [value @queue]
    (if (compare-and-set! queue value (pop value))
      (peek value)
      (recur queue))))

Re-running our tests, we can see that stateful-check is no longer able to find a counterexample:

(is (specification-correct? queue-spec {:gen {:threads 2}
                                        :run {:max-tries 10}}))