                                                                                                                 QuickerCheck
                                                                          Implementing and Evaluating a Parallel Run-Time for QuickCheck
                                                                            Robert Krook                                                                       Nicholas Smallbone
                                                                    krookr@chalmers.se                                                                       nicsma@chalmers.se
                                                              Chalmers University of Technology                                                        Chalmers University of Technology
                                                                    Gothenburg, Sweden                                                                       Gothenburg, Sweden

                                                                         Bo Joel Svensson                                                                           Koen Claessen
                                                                   bo.joel.svensson@gmail.com                                                                 koen@chalmers.se
                                                                      Lind Art & Technology                                                            Chalmers University of Technology
arXiv:2404.16062v1 [cs.PL] 17 Apr 2024




                                                                        Stockholm, Sweden                                                                    Gothenburg, Sweden

                                         ABSTRACT                                                                                        1    INTRODUCTION
                                         This paper introduces a new parallel run-time for QuickCheck, a                                 QuickCheck [5] is a widely known Haskell tool for property-based
                                         Haskell library and EDSL for specifying and randomly testing prop-                              random testing of programs. First, the programmer writes a prop-
                                         erties of programs. The new run-time can run multiple tests for a                               erty of the program under test that they expect to always hold.
                                         single property in parallel, using the available cores. Moreover, if a                          Then, to check the property, QuickCheck generates a number of
                                         counterexample is found, the run-time can also shrink the test case                             random test cases to exercise the property. If the property always
                                         in parallel, implementing a parallel search for a locally minimal                               held, the check is reported as successful. If a test case makes the
                                         counterexample.                                                                                 property fail, a process called shrinking is invoked, which consists
                                            Our experimental results show a 3–9× speed-up for testing                                    of a greedy search for a (locally) minimal failing test case.
                                         QuickCheck properties on a variety of heavy-weight benchmark                                       For example, we may be testing an implementation of System F
                                         problems. We also evaluate two different shrinking strategies; deter-                           [6], where we have the following types and functions:
                                         ministic shrinking, which guarantees to produce the same minimal                            1   type Expr −− expressions
                                         test case as standard sequential shrinking, and greedy shrinking,                           2   type Type −− types
                                         which does not have this guarantee but still produces a locally                             3
                                         minimal test case, and is faster in practice.                                               4   reduce :: Expr −> Maybe Expr
                                                                                                                                     5   typeOf :: Expr −> Type
                                         CCS CONCEPTS                                                                                    The types Expr and Type stand for expressions and types of expres-
                                         • Computing methodologies → Concurrent algorithms; Shared                                       sions in System F. The function reduce takes one evaluation step, if
                                         memory algorithms; • Theory of computation → Shared                                             possible. The function typeOf computes the type of an expression.
                                         memory algorithms; • Software and its engineering → Soft-                                       Subject reduction is a property that says that evaluation of expres-
                                         ware testing and debugging.                                                                     sions does not cause their type to change. This can be expressed as
                                                                                                                                         a QuickCheck property as follows:
                                         KEYWORDS                                                                                    1 prop_Preservation :: Expr −> Property
                                         property-based testing, quickcheck, testing, parallel functional pro-                       2 prop_Preservation e =
                                         gramming, haskell                                                                           3   isJust r ==> typeOf e == typeOf (fromJust r )
                                                                                                                                     4   where
                                         ACM Reference Format:                                                                       5     r = reduce e
                                         Robert Krook, Nicholas Smallbone, Bo Joel Svensson, and Koen Claessen.                          Here, the operator ==> specifies a precondition: only tests satisfying
                                         2023. QuickerCheck: Implementing and Evaluating a Parallel Run-Time for                         isJust r are of interest.
                                         QuickCheck. In The 35th Symposium on Implementation and Application of                             To run QuickCheck, the user must also supply an Arbitrary
                                         Functional Languages (IFL 2023), August 29–31, 2023, Braga, Portugal. ACM,
                                                                                                                                         instance describing how to generate random well-typed Exprs1 (a
                                         New York, NY, USA, 12 pages. https://doi.org/10.1145/3652561.3652570
                                                                                                                                         non-trivial task studied in e.g. [7]). QuickCheck will then generate
                                                                                                                                         a configurable amount of random expressions, which by default is
                                                                                                                                         100, and evaluate the property for them. In fact, QuickCheck will
                                         Permission to make digital or hard copies of part or all of this work for personal or           typically evaluate the property even more times, because:
                                         classroom use is granted without fee provided that copies are not made or distributed
                                         for profit or commercial advantage and that copies bear this notice and the full citation
                                                                                                                                              • QuickCheck discards any test case not satisfying the pre-
                                         on the first page. Copyrights for third-party components of this work must be honored.                 condition isJust r, and continues until it has executed 100
                                         For all other uses, contact the owner/author(s).                                                       tests satisfying the precondition.
                                         IFL 2023, August 29–31, 2023, Braga, Portugal
                                                                                                                                         1 There is no requirement by QuickCheck itself that the generator has to generate
                                         © 2023 Copyright held by the owner/author(s).
                                         ACM ISBN 979-8-4007-1631-7/23/08.                                                               well-formed terms. This is primarily required to meaningfully exercise the property in
                                         https://doi.org/10.1145/3652561.3652570                                                         question.
IFL 2023, August 29–31, 2023, Braga, Portugal                                                     Robert Krook, Nicholas Smallbone, Bo Joel Svensson, and Koen Claessen


     • If a test case fails (for example if the function reduce contains              total number of successful tests3 . So, the distribution of sizes during
       a bug), shrinking searches for a smaller counterexample by                     testing only depends on the total number of successful tests so far,
       executing the property on many smaller test cases.                             not on the total number of tests in general. This introduces a small
                                                                                      but significant data dependency preventing parallel evaluations of
    All this happens sequentially at the moment in QuickCheck. If
                                                                                      tests; when a worker runs a test it must know the appropriate size
the evaluation of the property takes a long time, QuickChecking
                                                                                      of the test case to run, and the appropriate size depends on whether
it (and possibly shrinking the counterexample) will take an even
                                                                                      the previous tests were successful or not. This dependency needs
longer time. This is time often spent waiting by the programmer,
                                                                                      to be dealt with somehow in the parallelization.
perhaps wondering why their computer is roaring like a spaceship
while only one core is in use. The contribution of this paper is                         Shrinking. When a failing test case is found, QuickCheck
to propose and practically evaluate a way of performing both the                      searches for a smaller failing test case by applying a process called
testing phase as well as the shrinking phase of QuickCheck in                         shrinking [10]. The goal of shrinking is to produce a locally minimal
parallel2 .                                                                           failing test case. Shrinking first produces a list of shrink candidates,
    Note that our work aims to reduce waiting time for the program-                   variants of the test case that have been reduced in size in a vari-
mer while checking a single property. There exist frameworks (for                     ety of ways. This list is traversed from left to right until we find
example tasty [4]) that allow testing of multiple properties and unit                 a new failing test case. Shrinking is then applied recursively on
tests in parallel or even distributed on a cluster. These are typically               the new failing test case until the current failing test case cannot
used in regression tests or continuous integration. Our work can                      be reduced anymore. Shrinking does not backtrack in search of a
not only speed up testing in these settings but also during active                    globally minimal counterexample, but only promises to yield a local
development, where programmers typically run QuickCheck on a                          minimum.
single property and wait for the result.                                                 To use shrinking, the user must define a shrink function. For a
                                                                                      type T, this is a function shrink :: T -> [T] which, given a test
2    WHAT ARE THE CHALLENGES?                                                         case, produces a list of shrink candidates, i.e. smaller or simpler
                                                                                      test cases to try. For example, suppose that we are testing System F
Even though running each test is supposed to be independent,
                                                                                      again, and the type of expressions is defined as follows:
and as such testing a property 100 times should be a so-called
embarrassingly parallel task, in practice parallelizing testing is not            1 data Expr
so easy. For one, individual tests may interact with each other, but              2   = Var String    −− variable
luckily in Haskell, we often get the independence guarantees we                   3   | App Expr Expr −− application
need from pure (or at least thread-safe) code. In this paper, we                  4   | ...           −− other constructors
assume that the property itself is thread-safe.                                          Then we can define a shrink function as follows:
   But the biggest problem is that QuickCheck’s algorithm is in-                  1 shrink :: Expr −> [Expr]
herently sequential. This is not at all obvious at first glance. The              2 shrink (Var _) = []
problem comes from two features in QuickCheck – adjustment of                     3 shrink (App t u) =
test size, and shrinking. As we will see, these features introduce a              4   concat [ [ t , u ]
data dependency: the test case that we should try next depends on                 5           , [ App t ' u | t ' <− shrink t ]
the result of the previous test. Addressing these dependencies was                6           , [ App t u' | u' <− shrink u ]
one of the main challenges in parallelizing QuickCheck.                           7           ]
                                                                                  8 shrink ( ... ) = ... −− other constructors
   Test size. Many times it is enough to generate a small test input
to falsify a property. QuickCheck tries to generate smaller inputs                    A Var can not be shrunk further, so we return an empty list of can-
early on, and gradually increases the size as more and more tests                     didates. A function application App t u, however, can be shrunk
are passed. This is achieved by QuickCheck supplying the test-data                    further. We can remove the App constructor and one of the subex-
generator with a size. The generators are free to disregard the size                  pressions, leaving just t or u, which if successful may shrink the
completely but may use it if they wish to. As an example, the default                 expression considerably. We can also keep the App constructor but
generator for lists uses the size as an upper bound of the length                     shrink the subexpressions.
of the generated list. The size of the first test is always 0, while                     Note that QuickCheck always tries the shrink candidates in the
the default upper bound is 100. If the user specifies that 100 tests                  order they appear in the list, from left to right. Hence it is com-
should be executed, QuickCheck will make sure that the generator                      mon to return the greedy candidates first, those that remove large
has been provided with all sizes between 0 and 99. The authors                        parts of the value, as we do in this case. Ordering the shrink list
point out that so far everything discussed is easily parallelisable.                  appropriately can greatly improve the speed of shrinking.
   However, properties in QuickCheck can not only succeed or fail,                       We propose to parallelize shrinking in two ways:
but also discard, which means that a pre-condition in the property                       (1) Greedy shrinking evaluates as many shrinking candidates
was not fulfilled. A discarded test case is not counted towards the                          in parallel as possible, and as soon as a candidate fails, it
                                                                                             recursively continues with that candidate. It may be that a
                                                                                      3 The reason for this is that if the precondition of a property is more likely to succeed
2 The implementation can be found at https://github.com/Rewbert/quickcheck. The       for small test data sizes, we still want to make sure that we exercise the property on
authors intend to eventually merge this work into mainline QuickCheck.                larger sizes.
    QuickerCheck                                                                                                      IFL 2023, August 29–31, 2023, Braga, Portugal


            candidate earlier in the shrink list (corresponding to a more         1 prop_metamorphic :: Program −> Property
            aggressive shrink step) would also have failed if we had              2 prop_metamorphic program = ioProperty $ do
            waited, and in that case, we may perform a smaller shrink             3    writeFile "p.c" (render program)
            step than necessary.                                                  4    writeFile "q.c" (render $ mutateInput program)
        (2) Deterministic shrinking speculatively evaluates test cases in         5   output1 <− compileAndRun "p.c"
            the search before we know we will need to, but always makes           6   output2 <− compileAndRun "q.c"
            the same choices as in the sequential case. That is, when a           7   mapM removeFile ["p.c", "q.c" , "p.exe" , "q.exe"]
            shrink candidate fails, it waits until it knows that no earlier       8   return (mutateOutput output1 == output2)
            candidate fails                                                              The property executes both the original and modified programs
    In our evaluation, greedy shrinking is usually faster than determin-              after having first written them to the file system. The file system is
    istic shrinking.                                                                  cleaned up, after which the outputs are compared. The output of
                                                                                      the unmodified program is modified to reflect the change described
    3    QUICKERCHECK                                                                 by the metamorphic relation.
    We present QuickerCheck via two examples. We point out that the                      Unfortunately, running this property with quickCheckPar will
    QuickCheck API for writing generators, shrinkers, and properties                  produce extremely strange test failures. The reason is that the prop-
    remains unchanged, and only the internal evaluation of a property                 erty, while innocent-looking, is not thread-safe. There is an implic-
    is modified.                                                                      itly shared resource, the file system: if multiple instances of the
                                                                                      property execute in parallel, they will all write to the same files p.c
       System F. In Section 1, we saw the property prop_Preservation
                                                                                      and q.c. This leads to obvious race conditions. There are different
    :: Expr -> Property for testing subject reduction in System F.
                                                                                      ways to modify the property such that there are no race conditions,
    To test this property with sequential QuickCheck we run:
                                                                                      one of which is to let the property create a temporary directory to
    > quickCheck prop_Preservation                                                    which intermediary files are written.
    +++ OK! Passed 100 tests.
                                                                                  1   −− create a fresh temporary directory based on a baseline name
       As the property is pure, it is safe to test in parallel using Quick-       2   −− withSystemTempDirectory :: String −> ( FilePath −> IO a) −> IO a
    erCheck. To do so, we must compile the code with the -threaded                3
    and -rtsopts flags and pass in the -N option to the run-time sys-             4 prop_metamorphic :: Program −> Property
    tem, to enable parallelism in GHC. Then all we have to do is invoke           5 prop_metamorphic program = ioProperty $ do
    quickCheckPar instead of quickCheck.                                          6   withSystemTempDirectory "compiler_output" $ \ dir −> do
       The output (assuming all tests passed) is                                  7     −− rest of property , now using dir as a
    > quickCheckPar prop_Preservation                                             8     −− scratch space for temporary files
    +++ OK! Passed 100 tests.
                                                                                         If we disregard other implicitly shared resources such as CPU
      tester 0: 50
                                                                                      caches, RAM, bandwidth, etc, this property can now be evaluated
      tester 1: 50
                                                                                      in parallel by using quickCheckPar.
       The lines tester 0: 50 and tester 1: 50 show that two                             In general, using QuickerCheck requires three steps. (1) Make
    threads were used (we happened to limit GHC to using two cores)                   sure that the property is thread-safe (only for properties doing
    and that they each executed 50 test cases. What is not visible in the             I/O). (2) Compile the program with threading options. (3) Run
    output is that, since the tests were distributed among two cores,                 quickCheckPar instead of quickCheck.
    QuickerCheck ran close to twice as fast.
       Compiler testing. A function that is not necessarily embarrass-                4   QUICKERCHECK DESIGN AND
    ingly parallel is one that is effectful. To test a compiler it is necessary           IMPLEMENTATION
    to perform IO actions, such as invoking the compiler under test or                The extensions to QuickCheck described in this paper are designed
    executing the compiled binary. Testing compilers is non-trivial, but              such that as few observable behaviors as possible are changed. Some
    a well-studied approach is metamorphic testing [3]. In this approach,             design choices of QuickCheck do not lend themselves nicely to par-
    assuming a function of type Program -> IO Output that compiles                    allelism, and QuickerCheck tries to make reasonable compromises
    and runs the program, we define a function mutateProgram ::                       where possible. One notable case of this is the way QuickCheck
    Program -> Program that mutates the program in some way, and                      computes sizes for a test case. The size is derived from the number
    then specify how the output should change in response by a func-                  of tests that have passed so far, and the number of tests that have
    tion mutateOutput :: Output -> Output. Mathematically, the                        been discarded since the last passing test. This means that we can
    property that should hold is:                                                     not compute the size of a test until we have observed the outcome
1 −− compileAndRun :: Program −> IO Output                                            of all tests that came before. This sounds sub-optimal for paral-
2 compileAndRun (mutateProgram p) =                                                   lelization; below, we explain what QuickerCheck does to address
3   fmap mutateOutput (compileAndRun p)                                               this.
        In practice, we also need to perform various housekeeping tasks                  Testing. The test loop in ordinary, sequential QuickCheck is a
    such as writing the program source to a file and cleaning up output               recursive function that maintains a state containing e.g. the count
    files, so a more realistic property is:                                           of how many tests were executed so far, how many were discarded
IFL 2023, August 29–31, 2023, Braga, Portugal                                                        Robert Krook, Nicholas Smallbone, Bo Joel Svensson, and Koen Claessen


due to a failed pre-condition, etc. It also holds the random seed
used to generate the test case. It generates and executes one test at
a time, adjusting the size of the test case whenever a test succeeds,
but not when a test is discarded. Once a test fails, the test loop
terminates and a shrinking routine is invoked.
     The parallel test loop is implemented by running concurrent
instances of the sequential test loop. The main thread spawns con-
current testers that evaluate one test after another, and then goes to
sleep until the testers report that all tests have been executed, too
many tests were discarded, or a counterexample was found. The
test loop maintains a state that is updated after every test, recording                     Figure 1: An illustration of how size grows as more and more
how many tests have been passed so far, the next random seed, and                           tests are passed, and to which worker they are assigned. In
many other things. In order to facilitate multiple, concurrent testers,                     order to get a fair workload for the concurrent testers a stride
some of the state has been moved into MVars. As an example, the                             is applied when computing sizes.
integer representing the number of tests a particular thread has yet
to run resides in an MVar, enabling other threads to read it if they
wish to steal work from that thread.                                                            graceful. When a property is aborted as violently as this, by
     Communication between threads occurs as little as possible in                          raising an asynchronous exception, there is a risk that there will be
order to not incur synchronization costs. When testing is initiated,                        artifacts left from a test. If a property e.g. creates a new file on the
the number of tests to run is divided equally between the testers, and                      file system that is normally deleted at the end, an interruption by
only when one thread has exhausted its budget of tests will it inspect                      an asynchronous exception may make the file erroneously persist.
the budgets of the concurrent testers. If work-stealing is enabled, a
thread may then decrement the counter of a sibling tester and run                       1 prop :: Input −> Property
another test on its own. Each tester has its own random seed that                       2 prop ip = ioProperty $ do
it splits before running a test, as sharing a seed between all testers                  3   run $ writeFile "temp.txt " (show ip)
would incur synchronization overheads. Additionally, each tester                        4   −− do some work
computes the sizes to use for test cases based on their individual                      5   run $ deleteFile "temp.txt " −− we may never execute this
counters for how many tests they have passed, and how many                                    To address this, we introduce a combinator graceful that takes
tests they have discarded since the last passing test. In an effort to                      an IO action and a handler. The handler will run if QuickCheck
explore the same set of sizes as in sequential QuickCheck, they each                        makes the choice to terminate evaluation of the property.
apply a stride: If we have 𝑘 threads, then thread number 𝑖 uses sizes
𝑖, 𝑖 + 𝑘, 𝑖 + 2𝑘, 𝑖 + 3𝑘, . . .. This is illustrated in figure 1. A compromise          1   −− graceful :: IO a −> IO ( ) −> PropertyM IO a
is made when a thread steals a test from a sibling tester, in which                     2

case the local next size is used. This reduces synchronization costs,                   3 prop :: Input −> Property
as the thread that ran the test doesn’t need to report the result                       4 prop ip = ioProperty $ do
back to the other thread. With this approach, we explore the same                       5   run $ writeFile "temp.txt " (show ip)
set of sizes as sequential QuickCheck, except when work stealing                        6   graceful
happens.                                                                                7     (do −− do some work
     As an alternative to strides, we have also implemented a strategy                  8         deleteFile "temp.txt " )
that divides the set of sizes into contiguous segments for each of                      9     ( deleteFile "temp.txt " )
the testers, by applying an offset to the size computation. There is                           The handler is implemented by intercepting the asynchronous
a risk, however, that test cases generated by e.g. smaller sizes will                       exception before the worker is restarted and running the handler
run faster than test cases generated with larger sizes. This would                          before rethrowing the exception. graceful can only capture a spe-
lead to the concurrent testers finishing their given workloads at                           cific exception thrown internally by QuickCheck. We choose to
different times. Computing sizes with an offset is implemented and                          implement this dedicated operator like this rather than relying on
can be chosen by configuring the arguments to quickCheckWith4 ,                             existing bracket functionality, as both user code and QuickCheck
but the default behavior is to use a stride.                                                might already have code in place to deal with exceptions.
     When a thread finds a counterexample it wakes up the main                                 graceful can be used not only for shrinking but also for testing.
thread by writing the used seed and size to an MVar. The main                               When one tester finds a counterexample the concurrent testers will
thread will then terminate the remaining testers before it shrinks                          be aborted. This combinator will make sure that cleanup occurs
the counterexample, by delivering asynchronous exceptions. This                             then as well.
is very abrupt, with the exceptions delivered at the next allocation
point.                                                                                        Shrinking. The existing shrink loop continually evaluates the
                                                                                            head of the candidate list until a new counterexample is found, at
                                                                                            which point the loop recurses, or until the list is empty, at which
4 The function quickCheckWith is a variant of quickCheck that accepts a configuration       point shrinking is terminated. This is illustrated in figure 2a. The
parameter where default behavior can be overridden.                                         design of the new loop is very similar.
QuickerCheck                                                                                             IFL 2023, August 29–31, 2023, Braga, Portugal


    Rather than a single thread traversing the candidate list one ele-
ment at a time, the parallel shrink loop spawns concurrent worker
threads that cooperate and traverse the same list, now residing in
an MVar. If any of the concurrent workers finds a new counterex-
ample, they will update the shared list of candidates and signal to
their sibling workers that they should stop evaluating their current
candidate and instead pick a new one from the new list.
    The behavior of this shrink loop might return a non-deterministic
result. Whereas the previous loop will always find the first coun-
terexample in the candidate list, the parallel loop might find a                     (a) Illustration of the existing QuickCheck
counterexample other than the first one. To emulate the determin-                    shrink-loop. It guarantees to always return
istic behavior, the new loop can choose to only signal a restart                     the same locally minimal counterexample.
to those concurrent workers that are evaluating candidates that
appeared after the current one in the candidate list, and tell them
to speculatively start shrinking the new counterexample. The other
workers will keep evaluating their current candidates, and if one of
them turns out to be a counterexample, the current progress will
be discarded, and shrinking will continue with the new counterex-
ample. In this case, we might do some unnecessary work, but we
will get the same deterministic result. Figure 2b illustrates this and
how this approach may make us evaluate candidates that we don’t
need.
    Another alternative is that when any worker has found a coun-                    (b) The new deterministic shrink-loop
terexample, all concurrent workers are restarted and told to start                   promises to find the same local minimum
shrinking the new counterexample, regardless if this was the first                   every time, but it may speculatively eval-
                                                                                     uate other candidates in its search for the
counterexample or not. This might lead to a non-deterministic re-
                                                                                     final counterexample.
sult, as the path down the rose tree of shrink candidates is not the
leftmost one, as illustrated in figure 2c. Restarting a worker is done
by raising an asynchronous exception in the worker. The worker
will catch this exception and enter the shrink-loop anew, and begin
to search through the new list of candidates.
    Repeatedly accessing a shared resource may incur overhead costs.
If two workers attempt to modify a shared resource at the same
time, one will have to wait for the other. As the list of candidate
counterexamples is shared between workers, if candidates are eval-
uated very fast, it is likely that using more threads will slow down
shrinking.                                                                           (c) The greedy shrink-loop does not guar-
                                                                                     antee to find the same local minimum, po-
5     EVALUATION                                                                     tentially returning a different final coun-
We evaluate QuickerCheck to answer the following four questions                      terexample.

      • Question 1: Is the sequential performance of the new im-
                                                                         Figure 2: The three figures above illustrate how the search
        plementation comparable with QuickCheck?
                                                                         for a minimized counterexample happened. The dotted line
      • Question 2: How does the parallel run-time scale as we add
                                                                         represents the final path to the local minimum, green boxes
        more cores?
                                                                         are candidate counterexamples that turned out to not be
      • Question 3: Can we find bugs faster by using more cores?
                                                                         new counterexamples, and red boxes are counterexamples
      • Question 4: Can we shrink counterexamples faster by using
                                                                         that still falsified the property. Grey boxes are candidate
        more cores?
                                                                         counterexamples that were never evaluated.
      • Question 5: Does the choice of shrinking algorithm affect
        the quality of shrunk counterexamples?
  To answer these questions we run properties and collect infor-         intended to represent a diverse set of testing tasks. compiler testing
mation. We will refer to such properties as benchmarks, and the          and compressid are effectful tasks making use of IO facilities, while
benchmarks we use are described in the following subsection.             the other tasks are pure.
                                                                            constant. The benchmark named constant is not one that anyone
5.1     Benchmarks
                                                                         would write organically, but its inclusion as a benchmark in this
We perform all our evaluations using six distinct benchmarks. While      set has a very specific purpose. The underlying property is
the first benchmark constant is artificial, the other benchmarks are
    IFL 2023, August 29–31, 2023, Braga, Portugal                                       Robert Krook, Nicholas Smallbone, Bo Joel Svensson, and Koen Claessen


                                                                               like this will experience race conditions if multiple threads are used.
                                                                               We test two alternative implementations that make the property
                                                                               thread-safe in different ways. The first (tmpfs) generates fresh di-
                                                                               rectories for each concurrent worker to write such files to, and the
                                                                               second (nofs) uses pipes to pass values around, never using the file
                                                                               system.

                                                                                   verse. This property asserts the confluence of the rewrite system
                                                                               for the Verse Core Calculus [2]. A rewrite system is confluent if,
                                                                               regardless of which rewrite rules are applied in each step, the result
                                                                               is always the same, single, normal form.
                                                                                   The property generates an arbitrary term and applies two arbi-
                                                                               trary sequences of rewrite rules. If the two resulting normal forms
    Figure 3: A high-level description of the internal testing loop.           are different, the rewrite system is not confluent and the property
    The loop begins by generating input and then invoking the                  is falsified.
    property. After this, the loop inspects the outcome before it
                                                                                  system f. The system f benchmark is a pure property that gen-
    either reports having found a counterexample, or loops back
                                                                               erates arbitrary lambda terms and asserts the subject reduction
    to repeat all steps. The bottom box and all arrows are part of
                                                                               property, described in section 1, which states that the type of a
    the internal testing loop, while the top two boxes are defined
                                                                               term should not change after performing one reduction of said
    by the user.
                                                                               term. The code was taken from Etna, an evaluation platform for
                                                                               Property-based testing frameworks[8].
    prop_constant :: ( ) −> Bool
                                                                                  twee. Twee [9] is a high-performance theorem prover for equa-
1

    prop_constant ( ) = True
                                                                               tional logic written in Haskell. A key component is the term index,
2


       The cost in execution time of running a test consists of three          a data structure for finding equations matching a given term. The
    parts – generating input, running the property, and the machinery          twee benchmark is a pure property stating that, after any sequence
    of the internal testing loop. This is illustrated in figure 3. As Quick-   of update operations on a term index, the data structure’s invariant
    erCheck only changes the workings of the testing loop, we want             is preserved.
    to measure the change in cost of just the testing loop. The above
    property minimizes the execution time of both the generation of            5.2    Results and Discussion
    test data and evaluation of the property. Generation and evaluation
                                                                               Evaluation is done using an Intel I7-10700 8-core CPU with turbo-
    are constant time as there are no random choices to make dur-
                                                                               boost turned off. The evaluation system is equipped with 64GB of
    ing generation and evaluation of the property is trivial. Measured
                                                                               2933MT/s RAM.
    changes in the execution speed of QuickCheck vs QuickerCheck on
                                                                                  We use GHC to compile and execute Haskell code, using
    this benchmark should primarily be a result of the different testing
                                                                               the compile-time flags -threaded, -feager-blackholing, and
    loops.
                                                                               -rtsopts. We don’t try to mitigate garbage collection costs by in-
       compiler testing. The underlying property of the compiler test-         creasing the nursery size or try to improve the performance in any
    ing benchmark asserts that a compiler for an imperative language           other way, as we believe most people use QuickCheck without do-
    generates correct output. The property is stated as a metamorphic          ing this. All invocations of QuickCheck are made with the chatty
    relation as described in section 3.                                        flag set to False as printing would otherwise affect the results. In
       In practice, the property does significantly more work than the         appendix A it is illustrated how chatty affects experimentation.
    other benchmarks. It generates a type-correct imperative program
                                                                                  Is the sequential performance of the new implementation compara-
    and produces several executables that are invoked to assert the
                                                                               ble with QuickCheck? We answer this by executing each benchmark
    correctness. The generated programs may include non-terminating
                                                                               several times both with QuickCheck and QuickerCheck, using only
    loops, so the property might require some time to execute. Such
                                                                               one core. We compute the median execution times and compare
    loops are eventually broken by the property itself after consuming
                                                                               them. The results are presented in figure 4.
    too many resources. During evaluation, the property will spend a
                                                                                  Something that immediately stands out is the huge overhead ex-
    significant amount of time in external processes.
                                                                               perienced by the constant benchmark. This benchmark is intended
        compressid. This benchmark composes the two Unix commands              to act as a worst-case property and illustrate precisely what the
    gzip and gunzip and verifies that the composition behaves as the           overhead of the new testing loop is. The results indicate that, in
    identity function. It generates an arbitrary string and invokes gzip,      the worst case, QuickerCheck will incur a penalty of 70%.
    passes the compressed result to gunzip, and asserts that the final            The other benchmarks all perform some actual workload and
    output is identical to the input.                                          experience much more modest changes in performance. The system
        This benchmark comes in three flavors – one is a naive imple-          f property, just like the constant property, is very fast. By running
    mentation (naive) that writes intermediary values directly to the          many more tests it interacts much more with the new testing loop,
    file system. Since the file system is a shared resource a property         incurring more of the new costs. This shows up by QuickerCheck
QuickerCheck                                                                                           IFL 2023, August 29–31, 2023, Braga, Portugal




Figure 4: The performance of sequential QuickerCheck com-
pared to that of QuickCheck. A number of 1 means that
                                                                         Figure 5: The acquired speedup relative to the sequential
there was no difference in performance, whereas a num-
                                                                         execution time when running tests.
ber less than 1 indicates that QuickerCheck was faster than
QuickCheck (e.g. 0.5 shows that QuickerCheck finished in
half the time). A number greater than 1 indicates that Quick-
erCheck was slower than QuickCheck.



requiring 11% more execution time to finish the same workload.
Some of the workloads experienced no change at all or even got
slightly faster.
   Not accounting for the constant benchmark, it appears that there
is no major change in performance by using sequential Quick-
erCheck instead of QuickCheck.

   How does the parallel run-time scale as we add more cores? Each
of the benchmarks is executed several times for each core config-
uration, the median execution time is computed and the speedup
relative to the sequential running time is computed. The results are
presented in figure 5.
   We first observe that many of the benchmarks scale very well
until the point where we exhaust the number of physical cores. The
highest speedup was achieved by the compiler testing benchmark
                                                                         Figure 6: The acquired speedup relative to the sequential
which got more than eight times faster. The verse property is not
                                                                         execution time when searching for a planted bug.
far behind.
   The twee benchmark initially scales very well but starts to lose
momentum when we approach the limit of physical resources.
                                                                         tests in the same time frame. The results seem to indicate that the
When hyper-threading is active performance slowly but surely de-
                                                                         more time a property spends inside the body of the property, the
grades. The twee benchmark is very data-intensive and frequently
                                                                         greater the potential speedup.
moves data around. While two hyper-threads appear to the operat-
ing system as two CPUs, they are actually two logical threads that          Can we find bugs faster by using more cores? To evaluate this we
share hardware components required to execute machine instruc-           plant a bug in 4 of the 6 benchmarks and let QuickerCheck run
tions, such as caches and the system bus. One potential explanation      until it finds the bug. This is repeated 300 times after which the
for this degradation is that the different testers affect the cache in   median execution time is computed. Figure 6 illustrates the speedup
unfavorable ways.                                                        acquired relative to the sequential execution time.
   One noticeable difference between e.g. the compiler testing and          We first note that the system f benchmark doesn’t reach as high
system f benchmark is that the compiler testing property is signifi-     of a speedup as when we are running tests without a bug enabled.
cantly slower. The property may spend over a second evaluating           While we can’t say with certainty what to attribute this to, we
a single test while the system f benchmark may run thousands of          have a pretty good guess of what is happening. The shape of the
IFL 2023, August 29–31, 2023, Braga, Portugal                                      Robert Krook, Nicholas Smallbone, Bo Joel Svensson, and Koen Claessen


curve is the same, except that it is pushed down towards lower
multiples. There are some new costs associated with starting up the
parallel test loop, and when we run tests without a bug enabled the
benchmark is allowed to run for a few seconds, running hundreds of
thousands of tests. The cost of starting up the test loop is amortized
over all these tests, while when a bug is enabled there are many
fewer tests. The bug was found after roughly 200 tests, running for
just a couple of milliseconds.
   The overall shape of the twee benchmark is the same, but not
reaching quite as high of a speedup as when just running tests. The
compiler testing benchmark acquires a 10x increase in performance,
outperforming all other evaluated benchmarks. We believe this
speedup is higher than that achieved in figure 5 because many
concurrently running tests are aborted when a counterexample
is found. When evaluating speedup for question two, every test
that we began evaluating was expected to finish, whereas when we
evaluated question three, we terminated concurrent testers when
one of them found a counterexample. We will thus do slightly less         Figure 7: The speedups acquired when using two cores to
work. We observe the inverse behavior in the system f property,           shrink the compiler testing tests, using the deterministic
where the concurrent testers have time to run many additional tests       algorithm.
before they are terminated by a tester who found a counterexample.

   Can we shrink counterexamples faster by using more cores? We
generate 200 random seeds that we know trigger bugs, such that
we can replay them to deterministically see the same counterexam-
ples. We replay the seeds and measure how long it takes to shrink
them, varying the number of cores and the choice of strategy (de-
terministic or greedy shrinking). We have done this for the three
benchmarks compiler testing, twee, and verse. Because it is imprac-
tical to show all the results, we have picked some subsets of data
that we find representative of the overall results.
   The compiler testing results are presented in figure 7, 8, and
9. Figures 7 and 8 illustrate the relationship between sequential
and parallel execution time, using two cores. The red dots got
slower when two cores were used, whereas the blue dots achieved
a speedup. The further from the line a point lies, the more extreme
the achieved effect is. From the two figures, we can see that the
greedy algorithm appears to benefit more experiments and that
the achieved effects are greater. The blue dots in figure 7 appear to
tangent a line. This line traces the execution time that is twice as      Figure 8: The speedups acquired when using two cores to
fast as the sequential one and illustrates the upper bound defined        shrink the compiler testing tests, using the greedy algorithm.
by Amdahl’s law[1]. The results in figure 8 show some experiments
crossing this boundary, which is explained by the greedy algorithm
being able to return a completely different counterexample.
   As more and more cores are added, the results indicate that more          Figure 9 shows that there is a clear trend of counterexamples with
and more experiments got slower, while the remaining ones that            a good efficiency not benefiting from parallel shrinking. If there
achieved a speedup achieved a much greater speedup.                       was not that much extra work to be done from the beginning, the
   To try and answer which counterexamples may benefit from               existence of more cores does not offer any substantial performance
parallel shrinking, we plot the efficiency of the shrunk counterex-       improvements.
amples. The efficiency of a single counterexample is defined as              The results observed from twee (figures 10, 11, and 12) tell a
the fraction of evaluated candidates that successfully shrunk the         different story. The twee property finishes shrinking in a couple
counterexample, and as such is a number between 0 and 1. It is            of milliseconds, and using more cores quickly makes all observed
clear that if the efficiency is one, there is nothing to be gained        counterexamples shrink slower. The efficiency appears to make no
from parallelism as shrinking becomes a sequential search. As an          difference and we believe that the overhead of the parallel search
example, the total number of evaluated candidates in figures 2a,          overshadows any benefits of using more cores. The advantage of
2b, and 2c are 5, 7, and 8 respectively. In all 3 cases the number of     having more cores at one’s disposal appears to mainly be beneficial
successful shrinks was 3, so the efficiencies are 0.6, 0.42, and 0.375.   in cases where execution will require a non-trivial amount of time.
QuickerCheck                                                                                            IFL 2023, August 29–31, 2023, Braga, Portugal




Figure 9: This figure illustrates that the closer the efficiency is       Figure 11: The greedy algorithm appears to perform roughly
to one, the higher the probability that the test will get slower          the same as the deterministic one, with the exception of some
when shrinking. It also appears that the relative speedup is              tests that did indeed shrink faster.
higher the lower the efficiency.




                                                                          Figure 12: While the efficiency turned out to be an excellent
Figure 10: The results indicate that most tests finished shrink-          indicator for whether a test got faster or not for the compiler
ing very fast when only two cores was used.                               testing benchmark, the same can not be said for twee. Using
                                                                          16 cores and the greedy algorithm, all tests got slower and
                                                                          there was quite a spread of efficiencies. The overall efficiency
   The verse benchmark, much like the compiler testing one, achieves
                                                                          appears to be much lower, but there is still nothing to be
a noticeable speedup for the majority of candidates. This is illus-
                                                                          gained by additional cores.
trated in figures 13 and 14. The efficiency of the shrinker is depicted
in figure 15, and shows that there is a slight trend towards can-
didates with a lower efficiency being more likely to benefit from
                                                                          distribution of sizes of shrunk counterexamples is different for the
multiple cores. This benchmark shrinks quite rapidly, and as we
                                                                          two algorithms. We evaluate this on two benchmarks, compiler
add more cores, more and more candidates become slower, with the
                                                                          testing and verse. We collect 300 seeds from the compiler testing
final number at 16 cores showing that roughly half of the candidates
                                                                          benchmark and 500 from the verse benchmark. These seeds imme-
experienced a slowdown.
                                                                          diately falsify the property, allowing us to shrink them and record
   Does the choice of shrinking algorithm affect the quality of shrunk    the size using both algorithms. We define the size of a counterex-
counterexamples? The deterministic shrinking algorithm will al-           ample as the number of constructors in it. We point out that both
ways yield the same locally minimal counterexample, while the             algorithms produce identical results when only one core is used.
greedy algorithm may return another local minimum, of a poten-               To compare the results from the two algorithms, we model the
tially different size. We are interested in finding out whether the       measured sizes as negative binomial distributions. Whereas we
IFL 2023, August 29–31, 2023, Braga, Portugal                                   Robert Krook, Nicholas Smallbone, Bo Joel Svensson, and Koen Claessen




Figure 13: The speedups acquired with two cores using the               Figure 15: The efficiency of the verse shrinker shows that
deterministic algorithm, for the verse benchmark.                       there is a slight trend of lower efficiency indicating that there
                                                                        is a speedup to have by using more cores.




Figure 14: The speedups acquired with two cores using the
greedy algorithm, for the verse benchmark. It can be observed           Figure 16: The measured sizes are rendered as a histogram,
that the number of candidates that achieved a speedup in-               together with a model that represents the distribution from
creased, compared to using the deterministic algorithm.                 which they were drawn.


only have one baseline model (the deterministic algorithm), we
have 16 models representing the greedy algorithm (one for each          that the choice of algorithm does not impact the quality of shrunk
core configuration). The authors note that in the single-core case,     counterexamples at all.
the two algorithms are identical. Figure 16 illustrates both the
measured sizes of the deterministic algorithm, as well as the model     6   RELATED WORK
representing them.                                                      QuickCheck, having proven itself an extremely useful framework
   We compare the models representing the greedy algorithm to the       for testing software, has been re-implemented in many program-
baseline model by computing the entropy between them. Figures           ming languages. It appears that most other implementations don’t
17 and 18 illustrate the baseline model and the greedy model with       support parallel execution of properties. The only other imple-
the highest relative entropy. In both measured benchmarks the           mentation we could find that supports parallelism is fsCheck, a
difference is very small. While the verse benchmark shows little        QuickCheck implementation for testing .NET code. The parallel
to no difference at all, the compiler testing benchmark has a small     run-time is not described in any paper and the documentation is
but noticeable difference. This difference is not large enough to say   sparse, but the implementation is discussed in a merge request
whether the distributions are different or not. The results indicate    introducing the work. The discussion indicates that they initially
QuickerCheck                                                                                            IFL 2023, August 29–31, 2023, Braga, Portugal


                                                                           The Haskell package tasty [4] lets the user define test suites with
                                                                        individual tests in a suite being of different kinds. A test suite can
                                                                        simultaneously include e.g. QuickCheck tests, SmallCheck tests,
                                                                        and unit tests. This is possible by tasty using different test drivers
                                                                        to execute the tests. tasty can execute individual tests in a test suite
                                                                        in parallel, but it will not introduce parallelism in the underlying
                                                                        test drivers. If a test suite contains many tests, with all but one test
                                                                        terminating very quickly, the majority of execution time will be
                                                                        sequential, waiting for the longest running test to terminate.




                                                                        7   CONCLUSIONS AND FUTURE WORK
                                                                        Our results show that parallel testing is beneficial. If the property
                                                                        being tested is slow to run the expected performance increase is
                                                                        high, whereas a fast property stands to gain less (but not nothing).
Figure 17: The figure illustrates the distribution of the base-            Thanks to the natural division of effectful and pure code in
line samples, as well as the greedy distribution with the high-         Haskell, many properties are immediately able to benefit from
est relative entropy, from the compiler testing benchmark.              the parallel run-time. We found that with slight modifications to
                                                                        effectful properties, we could run them in a thread-safe manner.
                                                                           Parallel shrinking is not as universally beneficial, but can still
                                                                        yield good results. For all benchmarks evaluated, individual coun-
                                                                        terexamples could go either way, either experiencing a slowdown
                                                                        or a speedup. We can not conclude that parallel shrinking is always
                                                                        beneficial. It depends on not only the property but also the specific
                                                                        test case. As more cores are added, some counterexamples will get
                                                                        significantly faster, while the likelihood of your counterexample
                                                                        shrinking slower increases. There seems to be a good compromise
                                                                        around using multiple cores, but a lower number. The greedy al-
                                                                        gorithm appears to offer a greater speedup than the deterministic
                                                                        one, without compromising on the quality of the counterexamples.
                                                                           While the work presented in this paper represents a considerable
                                                                        engineering effort, there are still many lines of future work to
                                                                        pursue. While implementing the work described in this paper, it
                                                                        became clear that the ad-hoc way of computing sizes in QuickCheck
                                                                        does not lend itself nicely to parallelism. It imposes a sequential
                                                                        ordering to test cases and is tricky to distribute over multiple cores.
Figure 18: The figure illustrates the distribution of the base-         While we have implemented a best-effort attempt to maintain the
line samples, as well as the greedy distribution with the high-         previous behavior, it is not a perfect imitation. The authors would
est relative entropy, from the verse benchmark. The distribu-           like to implement and evaluate several different ways of computing
tions are practically the same.                                         sizes and reach some conclusions about which strategies are most
                                                                        efficient.
                                                                           While the greedy algorithm is allowed to search for the fastest
used an offset to compute sizes for tests but switched to using a       path to a counterexample, there may well be more efficient algo-
stride after observing an uneven workload between workers.              rithms still. There is still a bias towards finding earlier paths. It
   The largest framework for property-based testing by number           would be interesting to see how a random walk would perform.
of users is the Python package Hypothesis. They have explicitly            Currently, the user must explicitly request parallel QuickCheck
chosen not to provide support for parallel evaluation of properties     by using quickCheckPar instead of quickCheck. This choice was
as it can not be determined beforehand whether the function being       made because properties involving I/O can not always be safely ex-
tested is thread-safe or not. In a non-pure language like Python,       ecuted in parallel. It would be possible to instead have QuickCheck
this might be a concern, but we believe that this concern is not as     automatically execute tests in parallel when it is safe to do so. For
severe when it comes to Haskell code. Haskell code is usually split     example, pure properties (not using 𝑖𝑜𝑃𝑟𝑜𝑝𝑒𝑟𝑡𝑦) can always be par-
up into its pure parts and effectful parts, with the pure parts being   allelized. Properties doing I/O could be marked as thread-safe using
embarrassingly parallel from the get-go. Effectful code can in many     a special combinator.
cases be refactored to be thread-safe, such that parallel testing may      We are also working together with the QuickCheck maintainers
yield positive results.                                                 towards merging this line of work into mainline QuickCheck.
IFL 2023, August 29–31, 2023, Braga, Portugal                                                       Robert Krook, Nicholas Smallbone, Bo Joel Svensson, and Koen Claessen


REFERENCES                                                                                  of an effect this has on a sequential workload. The constant and
 [1] Gene M. Amdahl. 1967. Validity of the single processor approach to achieving           system f properties run extremely fast, and we observe that with
     large scale computing capabilities. In American Federation of Information Process-     the chatty flag set to True, QuickerCheck is significantly faster.
     ing Societies: Proceedings of the AFIPS ’67 Spring Joint Computer Conference, April
     18-20, 1967, Atlantic City, New Jersey, USA (AFIPS Conference Proceedings, Vol. 30).   The constant property finished evaluating in one-fifth of the time
     AFIPS / ACM / Thomson Book Company, Washington D.C., New York, NY, USA,                that QuickCheck required.
     483–485. https://doi.org/10.1145/1465482.1465560
 [2] Lennart Augustsson, Joachim Breitner, Koen Claessen, Ranjit Jhala, Simon
                                                                                               As we add cores, it appears that chatty might make the bench-
     Peyton Jones, Olin Shivers, Guy L. Steele Jr., and Tim Sweeney. 2023. The              marks scale slightly worse, but not a lot, as indicated in figure
     Verse Calculus: A Core Calculus for Deterministic Functional Logic Program-            20.
     ming. Proc. ACM Program. Lang. 7, ICFP, Article 203 (aug 2023), 31 pages.
     https://doi.org/10.1145/3607845
 [3] Tsong Yueh Chen, S. C. Cheung, and Siu-Ming Yiu. 2020. Metamorphic Testing:
     A New Approach for Generating Next Test Cases. CoRR abs/2002.12543 (2020).
     arXiv:2002.12543 https://arxiv.org/abs/2002.12543
 [4] Roman Cheplyaka. 2013. tasty. https://hackage.haskell.org/package/tasty
 [5] Koen Claessen and John Hughes. 2000. QuickCheck: a lightweight tool for
     random testing of Haskell programs. In Proceedings of the Fifth ACM SIGPLAN
     International Conference on Functional Programming (ICFP ’00), Montreal, Canada,
     September 18-21, 2000, Martin Odersky and Philip Wadler (Eds.). ACM, New York,
     NY, USA, 268–279. https://doi.org/10.1145/351240.351266
 [6] Jean-Yves Girard. 1972. Interprétation fonctionnelle et élimination des coupures de
     l’arithmétique d’ordre supérieur. Ph. D. Dissertation.
 [7] Michał H Pałka, Koen Claessen, Alejandro Russo, and John Hughes. 2011. Testing
     an optimising compiler by generating random lambda terms. In Proceedings of
     the 6th International Workshop on Automation of Software Test. 91–97.
 [8] Jessica Shi, Alperen Keles, Harrison Goldstein, Benjamin C Pierce, and Leonidas
     Lampropoulos. 2023. Etna: An Evaluation Platform for Property-Based Testing
     (Experience Report). Proceedings of the ACM on Programming Languages 7, ICFP
     (2023), 878–894.
 [9] Nicholas Smallbone. 2021. Twee: An Equational Theorem Prover. In Automated
     Deduction - CADE 28 - 28th International Conference on Automated Deduction,
     Virtual Event, July 12-15, 2021, Proceedings (Lecture Notes in Computer Science,
     Vol. 12699), André Platzer and Geoff Sutcliffe (Eds.). Springer, New York, NY, USA,
     602–613. https://doi.org/10.1007/978-3-030-79876-5_35
[10] Andreas Zeller and Ralf Hildebrandt. 2002. Simplifying and Isolating Failure-
     Inducing Input. IEEE Trans. Software Eng. 28, 2 (2002), 183–200. https://doi.org/      Figure 19: The sequential performance of QuickerCheck rel-
     10.1109/32.988498                                                                      ative to QuickCheck, evaluated with the chatty flag turned
                                                                                            on and off. The (c) suffix indicates that Chatty was set to True.
A     THE EFFECT OF CHATTY
The chatty flag in QuickCheck controls whether QuickCheck
should continuously print what it is doing or not. While printing
is helpful in assessing the current progress, it can be a bottleneck
when it comes to performance.
   QuickCheck prints the current progress before every test. If you
run just a few tests every second this is of no concern, but if your
property is a very fast one it has a huge effect on performance.
Running 10000 tests per second means that you will print 10000
times per second, which is significantly more than a human eye
can observe.
   QuickerCheck takes a different approach to printing. Since the
new run-time is multi-threaded anyway, QuickerCheck will spawn
a separate worker thread whose sole purpose is to periodically
print the progress to the terminal. The duration of the period can
be configured, and the default is 200 milliseconds.
   While the property that now runs 10000 tests in one second
would previously have printed 10000 times, QuickerCheck would                               Figure 20: The speedup relative to sequential execution time,
only have printed 5 times. In figure 19 it can be observed how much                         when chatty is enabled.
