Merge pull request #264 from barrucadu/docs

Update website

doc/adding_a_new_primitive.rst

@@ -156,7 +156,7 @@ Now we jump over to the ``Test.DejaFu.Internal`` module.  The
 
 .. code-block:: haskell
 
-  rewind (SetMVar c _) = Just (WillSetMVar c)
+  rewind (SetMVar c _) = WillSetMVar c
 
 Finally, we need to make sure the systematic testing will treat our
 new primitive correctly.  As setting the value of an ``MVar`` may

doc/advanced.rst

@@ -11,146 +11,34 @@ provided to tweak how things work.
 Execution settings
 ------------------
 
-The ``autocheck``, ``dejafu``, and ``dejafus`` functions from
-``Test.DejaFu`` all have a variant which lets you specify the **memory
-model** used for ``CRef`` operations and the **way** in which
-schedules are explored.  These are ``autocheckWay``, ``dejafuWay``,
-and ``dejafusWay`` (plus ``IO`` variants).
-
-Memory model
-~~~~~~~~~~~~
-
-Threads running under modern multicore processors do not behave as a
-simple interleaving of the individual thread actions.  Processors do
-all sorts of complex things to increase speed, such as buffering
-writes.  For concurrent programs which make use of non-synchronised
-functions (such as ``readCRef`` coupled with ``writeCRef``) different
-memory models may yield different results.
-
-As an example, consider this program from the ``Data.IORef``
-documentation.  Two ``CRef`` variables are created, and two threads
-spawned to write to and read from both.  Each thread returns the value
-it observes.
+The ``autocheckWithSettings``, ``dejafuWithSettings``, and
+``dejafusWithSettings`` let you provide a ``Settings`` value, which
+controls some of Déjà Fu's behaviour:
 
 .. code-block:: haskell
 
-  example :: MonadConc m => m (Bool, Bool)
-  example = do
-    r1 <- newCRef False
-    r2 <- newCRef False
-    x <- spawn $ writeCRef r1 True >> readCRef r2
-    y <- spawn $ writeCRef r2 True >> readCRef r1
-    (,) <$> readMVar x <*> readMVar y
+  dejafuWithSettings mySettings "Assert the thing holds" myPredicate myAction
 
-Under a sequentially consistent memory model the possible results are
-``(True, True)``, ``(True, False)``, and ``(False, True)``.  Under
-total or partial store order, ``(False, False)`` is also a possible
-result, even though there is no interleaving of the threads which can
-lead to this.
+The available settings are:
 
-We can see this by testing with different memory models:
+* **"Way"**, how to explore the behaviours of the program under test.
 
-.. code-block:: none
+* **Memory model**, which affects how non-synchronised operations,
+  such as ``readCRef`` and ``writeCRef`` behave.
 
-  > autocheckWay defaultWay SequentialConsistency example
-  [pass] Never Deadlocks
-  [pass] No Exceptions
-  [fail] Consistent Result
-      (False,True) S0---------S1----S0--S2----S0--
+* **Discarding**, which allows throwing away uninteresting results,
+  rather than keeping them around in memory.
 
-      (True,True) S0---------S1-P2----S1---S0---
+* **Early exit**, which allows exiting as soon as a result matching a
+  predicate is found.
 
-      (True,False) S0---------S2----S1----S0---
-  False
+* **Representative traces**, keeping only one execution trace for each
+  distinct result.
 
-  > autocheckWay defaultWay TotalStoreOrder example
-  [pass] Never Deadlocks
-  [pass] No Exceptions
-  [fail] Consistent Result
-      (False,True) S0---------S1----S0--S2----S0--
+* **Trace simplification**, rewriting execution traces into a simpler
+  form (particularly effective with the random testing).
 
-      (False,False) S0---------S1--P2----S1--S0---
-
-      (True,False) S0---------S2----S1----S0---
-
-      (True,True) S0---------S1-C-S2----S1---S0---
-  False
-
-Traces for non-sequentially-consistent memory models show where
-``CRef`` writes are committed, which makes a write visible to all
-threads rather than just the one which performed the write.
-
-The default memory model is total store order, as that is how x86
-processors behave.
-
-Schedule bounds
-~~~~~~~~~~~~~~~
-
-Schedule bounding is an optimisation which only considers schedules
-within some bound.  This sacrifices completeness outside of the bound,
-but can drastically reduce the number of schedules to test, and is in
-fact necessary for non-terminating programs.
-
-There are three supported types of bounds:
-
-Pre-emption bounding
-  Restricts the number of pre-emptive context switches.  A context
-  switch is pre-emptive if the previously executing thread is not
-  blocked and did not explicitly yield.
-
-Fair bounding
-  Restricts how many times each thread can yield, by bounding the
-  maximum difference between the thread which has yielded the most,
-  and the thread which has yielded the least.
-
-Length bounding
-  Restricts how long an execution can be, in terms of Déjà Fu's
-  "primitive actions".
-
-The standard testing mechanism uses all three bounds.  Pre-emption +
-fair bounding is useful for programs which use spinlocks or yield for
-control flow, but which are otherwise terminating.  Length bounding
-makes it possible to test potentially non-terminating programs.
-
-If you wanted to disable pre-emption bounding, for example, you can do
-so like so:
-
-.. code-block:: haskell
-
-  dejafuWay (systematically defaultBounds { boundPreemp = Nothing })
-            defaultMemType
-            myAction
-            ("Assert the thing holds", myPredicate)
-
-
-Random scheduling
-~~~~~~~~~~~~~~~~~
-
-If you don't want to find all executions within the schedule bounds,
-and instead want to test a fixed number of executions, you can use
-random scheduling.
-
-There are three variants:
-
-``randomly randomGen numExecutions``
-  Perform the given number of executions using weighted random
-  scheduling.  On creation, a thread is given a random weight, which
-  is used to perform a nonuniform random selection amongst the
-  enabled (not blocked) threads at every scheduling point.
-
-``uniformly randomGen numExecutions``
-  Like ``randomly``, but rather than a weighted selection, it's a
-  uniform selection.
-
-These are all given as the first argument to ``dejafuWay`` (and its
-ilk), like ``systematically``.  So for example you could do this:
-
-.. code-block:: haskell
-
-  dejafuWay (randomly (mkStdGen 42) 1000)
-            defaultMemType
-            myAction
-            ("Assert the thing holds", myPredicate)
+See the ``Test.DejaFu.Settings`` module for more information.
 
 
 .. _performance:
@@ -166,8 +54,8 @@ Performance tuning
 
 * Can you sacrifice completeness?
 
-    Consider using the random testing functionality. See the ``*Way``
-    functions and ``Test.DejaFu.SCT.sct{Uniform,Weighted}Random``.
+    Consider using the random testing functionality. See the ``*WithSettings``
+    functions.
 
 * Would strictness help?
 
@@ -181,7 +69,7 @@ Performance tuning
 * Do you know something about the sort of results you care about?
 
     Consider discarding results you *don't* care about. See the
-    ``*Discard`` functions in ``Test.DejaFu``, ``Test.DejaFu.SCT``,
+    ``*WithSettings`` functions in ``Test.DejaFu``, ``Test.DejaFu.SCT``,
     and ``Test.{HUnit,Tasty}.DejaFu``.
 
 For example, let's say you want to know if your test case deadlocks,
@@ -191,13 +79,15 @@ could do it like this:
 
 .. code-block:: haskell
 
-  dejafuDiscard
-    -- "efa" == "either failure a", discard everything but deadlocks
-    (\efa -> Just (if either isDeadlock (const False) efa then DiscardTrace else DiscardResultAndTrace))
-    -- try 10000 executions with random scheduling
-    (randomly (mkStdGen 42) 10000)
-    -- use the default memory model
-    defaultMemType
+  dejafuWithSettings
+    ( set ldiscard
+      -- "efa" == "either failure a", discard everything but deadlocks
+      (Just $ \efa -> Just (if either isDeadlock (const False) efa then DiscardTrace else DiscardResultAndTrace))
+    . set lway
+      -- try 10000 executions with random scheduling
+      (randomly (mkStdGen 42) 10000)
+    $ defaultSettings
+    )
     -- the name of the test
     "Never Deadlocks"
     -- the predicate to check

doc/conf.py

@@ -48,7 +48,7 @@ master_doc = 'index'
 
 # General information about the project.
 project = u'Déjà Fu'
-copyright = u'2017, Michael Walker'
+copyright = u'2017--2018, Michael Walker'
 author = u'Michael Walker'
 
 # External link destinations

doc/contributing.rst

@@ -193,3 +193,27 @@ non-profiled build:
   Alloc rate    878,145,635 bytes per MUT second
 
   Productivity  73.4% of total user, 73.8% of total elapsed
+
+
+Heap profiling
+--------------
+
+GHC can tell you where the memory is going:
+
+.. code-block:: none
+
+  $ stack build --profile
+  $ stack exec  -- dejafu-tests +RTS -hc
+  $ hp2ps -c dejafu-tests.hp
+
+This will produce a graph of memory usage over time, as a postscript
+file, broken down by cost-centre which produced the data.  There are a
+few different views:
+
+- ``-hm`` breaks down the graph by module
+- ``-hd`` breaks down the graph by closure description
+- ``-hy`` breaks down the graph by type
+
+I typically find ``-hd`` and ``-hy`` most useful.  If you're feeling
+particularly brave, you can try ``-hr``, which is intended to help
+track down memory leaks caused by unevaluated thunks.

doc/getting_started.rst

@@ -127,11 +127,11 @@ executions, and will in general explore the state-space quickly.
 
 If your test case is just too big for complete testing, there is also
 a random scheduling mode, which is necessarily *incomplete*.  However,
-Déjà Fu will tend to produce much more schedule variety than just
-running your test case in ``IO`` the same number of times, and so bugs
-will tend to crop up sooner.  Furthermore, as you get execution traces
-out, you can be certain that a bug has been fixed by simply following
-the trace by eye.
+Déjà Fu will tend to produce much more scheduling variety than just
+running your test case in ``IO`` a bunch of times, and so bugs will
+tend to crop up sooner.  Furthermore, as you get execution traces out,
+you can be certain that a bug has been fixed by following the trace by
+eye.
 
 **If you'd like to get involved with Déjà Fu**, check out :github:`the
 "good first issue" label on the issue tracker

doc/refinement_testing.rst

@@ -103,7 +103,7 @@ functions.  These functions are:
 The signatures can have different state types, as long as the seed and
 observation types are the same.  This lets you compare different
 implementations of the same idea: for example, comparing a concurrent
-stack implemented using ``MVar`` with one implemented using ``IORef``.
+stack implemented using ``MVar`` with one implemented using ``CRef``.
 
 Properties can have parameters, given in the obvious way:
 

doc/typeclass.rst

@@ -61,8 +61,8 @@ To test ``IO``-using code, there are some rules you need to follow:
 1. Given the same set of scheduling decisions, your ``IO`` code must
    be deterministic [#]_
 
-2. As ``IO`` values can't be broken up into smaller chunks, they
-   should be kept small; otherwise dejafu may miss buggy interleavings
+2. As dejafu can't inspect ``IO`` values, they should be kept small;
+   otherwise dejafu may miss buggy interleavings
 
 3. You absolutely cannot block on the action of another thread inside
    ``IO``, or the test execution will just deadlock.