Michael Walker
aadb27ea1f
Implement sleep sets for BPOR.
...
This further improves performance in all cases, although it's still far worse
on some of the included tests, and I have yet to figure out why.
See also: "Partial-Order Methods for the Verication of Concurrent Systems"
[Godefroid 1996]
2015-07-17 15:34:52 +01:00
Michael Walker
c12cbcf707
Implement BPOR for SCT, return to listy predicates.
...
This performs better with "real" code (the Par monad) but surprisingly does far
worse with the included tests! The next thing to do is implement the orthogonal
sleep sets algorithm to cut down on available choices even further and
hopefully correct this issue.
See also: "Bounded Partial-Order Reduction" [Coons, Musuvathi, McKinley 2013]
2015-07-16 22:32:30 +01:00
Michael Walker
23c350c4b1
Fix/ignore hlint warnings
2015-07-10 18:30:34 +01:00
Michael Walker
1c8720a635
Give schedulers one-step lookahead
2015-07-10 18:27:50 +01:00
Michael Walker
89ec649d92
Don't pre-empt guaranteed blocks.
...
Pre-empting an action which is guaranteed to block is just the same
as letting it block and then inserting a regular non-pre-emptive
context switch.
2015-07-10 15:49:23 +01:00
Michael Walker
2ca7337b01
Avoid scheduling decisions which immediately block (in PB-bounded runner)
2015-07-08 20:06:15 +01:00
Michael Walker
e92d639537
Export ThreadAction' type
2015-07-08 20:05:58 +01:00
Michael Walker
6e01de2e85
Make available the full state of every CVar to SCT runners
2015-07-08 19:15:18 +01:00
Michael Walker
9ca54fea17
Include one-step lookahead in traces
2015-07-08 18:55:30 +01:00
Michael Walker
dab69aebcc
Make alwaysTrue2 result less confusing when applied to one schedule only.
2015-07-08 18:20:08 +01:00
Michael Walker
05e2d2f1e4
Fix issue with identifying only-read STM transactions as only creating new CTVars.
2015-07-08 18:18:56 +01:00
Michael Walker
426707f382
Make the stmAtomic test actually test STM atomicity
2015-07-08 18:18:18 +01:00
Michael Walker
8794276a3e
Add a Show instance for SCTTrees
2015-07-08 18:17:48 +01:00
Michael Walker
df69f4778c
Improve error reporting in alwaysTrue2 (less zealous about short-circuiting
2015-06-24 15:59:54 +01:00
Michael Walker
8944ea97a5
Use schedule bounding as the primary SCT approach.
...
This allows results to be naturally reported as lazy trees, rather
than as lists representing a tree traversal. This in turn means
that the actual bound can be moved outwards to the testing code, and
not used at all in the runner. Trees let us do nice things with
shrinking and short-circuiting, if we make the (fairly reasonable)
assumption that the children of a buggy result will exhibit the same
bug.
Storing results as trees does complicate the predicate helper
functions somewhat, but I think the clarity gained in the actual
SCT code is well worth it.
2015-06-19 16:50:51 +01:00
Michael Walker
1d085f4ea9
More transformer instances (inc. strict versions)
2015-05-30 01:45:20 +01:00
Michael Walker
d2178c2814
Add some transformer instances
2015-05-29 16:51:51 +01:00
Michael Walker
a93f8202e4
Add dejafus/dejafusIO variants to take a pre-emption bound
2015-05-26 04:14:10 +01:00
Michael Walker
192777c2c9
STMLike type synonyms to shrink type sigs
2015-05-09 19:56:54 +01:00
Michael Walker
0a4bdeee68
Add source-repository to cabal file
2015-03-13 15:01:03 +00:00
Michael Walker
096a1c0651
Switch to MIT license
2015-03-13 14:58:42 +00:00
Michael Walker
fa92d4a050
Don't pre-empt STM transactions which only allocate new variables
2015-03-10 14:18:50 +00:00
Michael Walker
f95ab4122a
Report 2 capabilities for test runners, not 4.
...
The literature sttes that many bugs are found with 2 concurrent
threads, so encouraging even more parallelism is possibly a win in
only a small number of cases, but potentially a huge cost in many.
2015-02-27 21:01:10 +00:00
Michael Walker
3d0a82d915
Lie and return 4 for getNumCapabilities in DejaFu
2015-02-27 01:32:37 +00:00
Michael Walker
6c4015c314
Avoid re-running tests in dejafus. Closes #12 .
2015-02-26 21:57:55 +00:00
Michael Walker
9aea975304
Only check runnable threads in isLocked
2015-02-23 18:39:41 +00:00
Michael Walker
14b08ff026
Un-break detection of global deadlock
2015-02-23 18:23:58 +00:00
Michael Walker
4a69fde83e
Enable detection of nonglobal deadlock when every thread is in a fully-known state. Closes #9 .
2015-02-23 17:58:12 +00:00
Michael Walker
f626e79553
Implement the new primitives in stepThread
2015-02-23 17:32:08 +00:00
Michael Walker
b8ff9a77f5
Add primitives for the new testing functions
2015-02-23 17:27:26 +00:00
Michael Walker
e72b84c613
Add an internal STM module
2015-02-23 17:24:02 +00:00
Michael Walker
2a6cbe8951
Add functions to MonadConc to record known vars
2015-02-23 17:23:26 +00:00
Michael Walker
0e3ba970bd
Make CRefs interesting
2015-02-20 18:49:19 +00:00
Michael Walker
5862d536ca
Use default writeCRef for IO
2015-02-20 16:53:38 +00:00
Michael Walker
0ea2930862
Implement CRefs in stepThread
2015-02-20 16:24:21 +00:00
Michael Walker
a4a291368d
Add primitives for CRefs
2015-02-20 16:14:50 +00:00
Michael Walker
2f61cf6557
Add mutable non-blocking atomically-modifiable references
2015-02-20 15:59:53 +00:00
Michael Walker
0dba84f9a8
Add forkOn and getNumCapabilities
2015-02-18 00:13:12 +00:00
Michael Walker
9609823dd5
Add exception checking to autocheck
2015-02-17 11:22:17 +00:00
Michael Walker
998fdeb833
Update the deadlocks* predicates to handle STMDeadlock, and add exceptions* predicates
2015-02-17 05:58:25 +00:00
Michael Walker
22a15dfe95
Resolve all name conflicts with Prelude.catch in base-4.5
2015-02-16 03:47:14 +00:00
Michael Walker
6a371e6994
Use cabal-1.22 in travis
2015-02-16 03:38:50 +00:00
Michael Walker
1063b36fbd
Resolve conflict with Prelude.catch in base-4.5 in STM
2015-02-16 03:37:16 +00:00
Michael Walker
6f253df520
Drop base dependency to 4.5
2015-02-16 03:33:37 +00:00
Michael Walker
5d0545b198
Test more GHC versions in travis
2015-02-16 03:29:40 +00:00
Michael Walker
ab6e411c38
Tidy up Deterministic.Internal
2015-02-16 03:16:55 +00:00
Michael Walker
f41a39e490
Add ImpredicativeTypes everywhere to make mask (grr, exceptions) work with GHC 7.8.4
2015-02-16 02:50:52 +00:00
Michael Walker
ad98bb6d90
Fix a => typo (why did that ever compile and run!?)
2015-02-16 02:50:20 +00:00
Michael Walker
392a8c54c6
Add some STM tests. Closes #7 .
2015-02-14 23:55:58 +00:00
Michael Walker
921d505015
Merge branch 'exceptions'
...
Closes #4 .
2015-02-14 23:45:42 +00:00
