Commit Graph

85 Commits

Author SHA1 Message Date
Michael Walker
5ce63d0d50 Use MonadThrow/MonadCatch for MonadConc exceptions 2015-02-13 00:46:14 +00:00
Michael Walker
ef580d66e8 Use MonadThrow/MonadCatch for MonadSTM exceptions 2015-02-13 00:46:13 +00:00
Michael Walker
a305354b65 Add STM exceptions 2015-02-13 00:46:11 +00:00
Michael Walker
78ee2b2f75 Add MonadSTM constraint to MonadConc 2015-02-10 01:19:45 +00:00
Michael Walker
9b5e010d90 Implement a STM runner. 2015-02-09 22:04:28 +00:00
Michael Walker
f79f7fd245 Add a MonadSTM
- Each MonadConc has an associated MonadSTM, transactions of which
   it can run atomically.
 - The MonadSTM for IO is STM.
 - Conc and ConcIO do not yet have a MonadSTM.
2015-02-09 15:30:54 +00:00
Michael Walker
7aceb6a6f9 Implement an atomic-for-testing-purposes function.
This adds a new `MonadConc` primitive, `_concNoTest`, which is (for
all non-test implementations) the identity function. For test
implementations, it is understood as "this action is completely safe
under all schedules, so just execute it all at once and don't consider
any internal interleavings." It is not required to be deterministic,
merely to never fail.

Actions annotated with `_concNoTest` will show up as one step in the
trace, and new `Failure` and `ThreadAction` values have been added.
2015-02-06 16:18:25 +00:00
Michael Walker
00ad122b65 Refactor code and update docs to make more not-me friendly 2015-02-01 01:21:42 +00:00
Michael Walker
fbc262c361 Rename and remodularise 2015-01-31 15:50:54 +00:00
Michael Walker
304df27a35 Add a simple autocheck function, to look for deadlocks and multiple results 2015-01-30 16:09:32 +00:00
Michael Walker
8b28633f20 Implement shrinking, and shrink test output.
Shrinking attempts to find a "maximally simple" trace which
exhibits the same bug as the original. Typically, this means that
the results are equal. Shrinking is implemented in terms of
recursively trying to find the simplest variant of the original
trace, where simplest in particular means:

1. A trace with fewer pre-emptions is simpler.
2. A trace with fewer non-pre-emptive context switches is simpler.
3. A trace lexicographically smaller is simpler.

These three criteria are applied in that order in order to determine
which the simplest trace out of a collection is.

For test output, there is a final set of simplification done at the end.
Shrinking attempts to reduce individual traces to their simplest variant,
which can result in multiple test failures having the same shrunk trace.
Thus, the test runner then filters out duplicate failures by only keeping
the simplest trace for a given result.
2015-01-30 15:31:40 +00:00
Michael Walker
765f8d0bd5 Move CVars into Control.Concurrent 2015-01-28 17:59:17 +00:00
Michael Walker
531b9fd05b Add a module for strict CVars 2015-01-28 17:46:04 +00:00
Michael Walker
21a248bfa2 Drop MultiParamTypeClasses and FunDeps for TypeFamilies 2015-01-28 17:25:15 +00:00
Michael Walker
69fdd561d9 Factor out the utility list functions to a separate module 2015-01-27 13:54:46 +00:00
Michael Walker
d7e30e87ba Improve output of test cases 2015-01-27 12:52:43 +00:00
Michael Walker
bb8b85d9f3 Implement delay bounding 2015-01-27 11:45:59 +00:00
Michael Walker
cc40353001 Tidy up code a bit, also drop monad-st 2015-01-27 11:45:47 +00:00
Michael Walker
03a61057b5 Pull in monad-loops for unfoldrM 2015-01-24 10:57:05 +00:00
Michael Walker
dca91cc988 Drop the Test type 2015-01-23 17:12:34 +00:00
Michael Walker
f733a1ed43 Add a helper function for running a collection of tests 2015-01-23 17:06:14 +00:00
Michael Walker
2332c93cd7 Include the failed results and traces in a Result 2015-01-23 16:48:38 +00:00
Michael Walker
cf8a10c9f2 Correctly handle termination in the PB runner 2015-01-23 15:08:25 +00:00
Michael Walker
1a12ba0c5e Fix a couple of issues with generating schedules and early termination in PB runner 2015-01-23 13:14:43 +00:00
Michael Walker
a13df17156 Add Show, Read, and Eq instances for Results 2015-01-23 12:27:32 +00:00
Michael Walker
69bcc1878c Fix the half-reversed SCT traces 2015-01-23 12:27:20 +00:00
Michael Walker
19ff7c51e7 Restrict language extensions a bit 2015-01-21 15:31:10 +00:00
Michael Walker
8aa15b5496 Fix docs, and add a defaultSpawn function for ConcCVar monads 2015-01-21 11:26:27 +00:00
Michael Walker
aa921a0423 Add NFData instances for things, and fix a few space leaks in SCT 2015-01-19 11:50:43 +00:00
Michael Walker
ff3f8a48a4 Be strict in the Fixed result 2015-01-19 11:06:40 +00:00
Michael Walker
2b95ab7e46 Add somewhereTrue and somewhereTrue2 testing methods 2015-01-15 02:16:31 +00:00
Michael Walker
914d298f55 Drop bool param of alwaysTrue2 2015-01-12 19:12:20 +00:00
Michael Walker
a889b23b5d Add alwaysTrue and alwaysTrue2 functions for SCT tests 2015-01-12 19:08:09 +00:00
Michael Walker
78fbf5e5c6 Interpret a pre-emption bound < 0 as no bound 2015-01-12 17:52:30 +00:00
Michael Walker
886da7195e Provide utilities for writing SCT test cases 2015-01-12 17:27:41 +00:00
Michael Walker
fb44f15865 Use NonEmpty in Lazy to get rid of a pattern match warning 2015-01-12 16:28:16 +00:00
Michael Walker
b062d1e14c Structure runSCT' and runSCTIO' explicitly as unfolds, to make clearer how the state evolves 2015-01-12 16:28:04 +00:00
Michael Walker
6aefd27e9a Tuple up scheduler & runner sct states, as partial application doesn't really make sense 2015-01-12 16:04:23 +00:00
Michael Walker
ff015054f4 Use a non-empty list type for scheduler threads 2015-01-12 15:58:53 +00:00
Michael Walker
bf91775629 Remove Ord instances 2015-01-12 14:25:06 +00:00
Michael Walker
0f1675070b Update documentation 2015-01-12 14:24:12 +00:00
Michael Walker
8d23ad1fbe Wrap up PB scheduler state in a record 2015-01-12 13:26:04 +00:00
Michael Walker
4efd3b5a25 Consider pre-emptions around liftIOs in PB runner 2015-01-12 00:13:49 +00:00
Michael Walker
9aee30ac57 Deconflate lifting and creating new CVars in Fixed 2015-01-12 00:08:53 +00:00
Michael Walker
9745357817 Fix comment 2015-01-09 02:38:53 +00:00
Michael Walker
981169c25f Vastly improve PB runner 2015-01-09 02:35:28 +00:00
Michael Walker
c0ac24773e Fix comment 2015-01-09 02:29:21 +00:00
Michael Walker
6272abe7fd Fix the pre-emption runner (wasn't generating suffixes correctly) 2015-01-05 15:05:29 +00:00
Michael Walker
242babbc05 Fix a fromJust issue in Fixed 2015-01-05 12:01:06 +00:00
Michael Walker
1aa8765f4e Significantly faster PB runner, and enable 100 philosophers test 2015-01-05 06:42:41 +00:00