Commit Graph

705 Commits

Author SHA1 Message Date
Michael Walker
6788274f7f async-dejafu now requires dejafu-0.4 2016-07-21 19:33:49 +01:00
Michael Walker
2f0f51ceb6 Split concurrency modules into a separate package.
The new 'concurrency' package is starting at version 1.0.0.0 because the
API is already very mature (copied from base).

This breaks the dejafu-0.2 compatibility of async-dejafu.

Closes #51.
2016-07-21 19:33:49 +01:00
Michael Walker
f3c546f591 Add a non-monadic peekTicket'
Also removes the APeekTicket/PeekTicket/WillPeekTicket constructors.
2016-07-21 19:33:49 +01:00
Michael Walker
b47e95735c Drop TH boilerplate functions and lineNum.
The TH boilerplate was really fragile, and by dropping lineNum as well
the entire template-haskell dependency can be dropped. This is a small
sacrifice, as the name needed to be passed in explicitly anyway, and
there are probably more meaningful names than just the line number.
2016-07-21 19:33:49 +01:00
Michael Walker
fe251512f5 Make autocheck' functions take the schedule bounds
Closes #47.
2016-07-21 19:33:49 +01:00
Michael Walker
43b2dd3913 Make runTestIO monad-polymorphic
This + 7652ad5, 77aec63, 9375a61 closes #44.
2016-07-21 19:33:49 +01:00
Michael Walker
2aa2b8f447 Unify IO and ST instances
Closes #44
2016-07-21 19:33:49 +01:00
Michael Walker
c742da2bfd Drop _concKnows stuff and fix litmus tests.
Removing the stuff broke some of the litmus tests, which is bad. It
probably means that those actions were being put into sleep sets, and so
hiding actually interesting interleavings from the POR implementation. I
need to improve the lookahead behaviour to ignore these invisible
actions.

Closes #46.
2016-07-21 19:33:49 +01:00
Michael Walker
25718a6162 Move common internal stuff to Test.DejaFu.Common 2016-07-21 19:33:49 +01:00
Michael Walker
b42077c0ec Use 'ref-fd' for MonadRef. 2016-07-21 19:33:49 +01:00
Michael Walker
066ce937e6 Drop the penultimate Lift.
The final write-to-a-reference is now in the Stop action. This is a
fairly large change as it was easiest to do this by also removing the
Ref and Fixed types, and going for a typeclass for monadic references.

Fixes #43.
2016-07-21 19:33:49 +01:00
Michael Walker
70bcad4615 Bump versions for 0.4.0.0 release 2016-07-21 19:33:46 +01:00
Michael Walker
b160cfd793 Bump to dejafu-0.3.2.1 2016-07-21 18:55:18 +01:00
Michael Walker
8b35ec9ef7 Propagate read TVars in orElse.
Fixes #55.
2016-07-21 18:53:26 +01:00
Michael Walker
1483056d1b Use the BacktrackFunc synonym in SCT. 2016-06-06 20:31:34 +01:00
Michael Walker
f3b0eaf4ba Merge branch 'dejafu-0.3.2' 2016-06-06 20:22:57 +01:00
Michael Walker
d8e2e52cdc Merge branch 'dpor-0.2' 2016-06-06 20:04:03 +01:00
Michael Walker
305f473ed5 Don't allow nightly build failures 2016-06-06 09:04:36 +01:00
Michael Walker
5b99fc47fa Add module headers. 2016-06-06 00:09:09 +01:00
Michael Walker
83a0d4e229 Test building dejafu against dpor-0.1 2016-06-06 00:09:05 +01:00
Michael Walker
b978476c8b Add a test case for #40. 2016-06-05 23:40:03 +01:00
Michael Walker
0a72a561a7 Add a dependency for daemon threads when dpor<0.2
This is a HUGE performance penalty, as it effectively treats the intiial
thread stopping as throwing an exception to every thread.
2016-06-05 23:40:03 +01:00
Michael Walker
3ed51908a3 Improve STM dependency function.
Only consider STM transactions dependent if there is overlap in the
TVars they reference. Lookahead is the same worst-case behaviour as
before, as that information isn't available then.
2016-06-05 23:40:03 +01:00
Michael Walker
d78c1fefc8 Tidy dependent' 2016-06-05 23:40:03 +01:00
Michael Walker
028a7a5003 Improve POR for exceptions.
Keep track of thread masking states and only consider a 'throwTo' as
dependent if the action being thrown at can be interrupted. This halves
the execution time of the testsuite on my linode (~190s to ~90s).

Requires dpor-0.2, as thread IDs must be known when stepping the state.

Closes #32, although I feel like there might be yet more gains possible.

-- unconfirmed hunch follows --

I feel like there might be a bug lurking here, but I haven't been able
to exhibit one.

My intuition is that because throwing an exception which can't interrupt
WILL block and so enable other threads, this might have issues in
combination with preemption bounding, although the testsuite still
passes.
2016-06-05 23:40:03 +01:00
Michael Walker
798a4397cc Bump versions for dejafu-0.3.2.0 2016-06-05 23:40:03 +01:00
Michael Walker
8554ce9968 Drop use of killsEarly for daemon threads.
See comment in #52.
2016-06-05 23:38:14 +01:00
Michael Walker
a056f54b72 Treat daemon threads specially.
dporSched now schedules all daemon threads if any of the initial
decisions willl terminate the computation. Closes #40.
2016-06-05 23:38:14 +01:00
Michael Walker
c7aee7646f Pass thread ID to state step function.
Closes #54.
2016-06-05 23:38:14 +01:00
Michael Walker
95129fd587 Allow optional schedule bounds for 'pureRandom' 2016-06-05 23:38:14 +01:00
Michael Walker
b667930529 Implement pure random testing.
Closes #50.
2016-06-05 23:38:14 +01:00
Michael Walker
a16a06542b Implement random, execution-limited, DPOR.
Closes #48.
2016-06-05 23:38:14 +01:00
Michael Walker
b5c90df845 Add module headers 2016-06-05 23:38:14 +01:00
Michael Walker
fc2bdf0b42 Bump version numbers for dpor-0.2 / dejafu-0.3.1.2 2016-06-05 23:38:14 +01:00
Michael Walker
7030e0c3b9 Don't try building dejafu-0.2 against GHC 8 2016-06-05 23:36:25 +01:00
Michael Walker
232e7e5f40 Bump version numbers 2016-05-26 14:02:07 +01:00
Michael Walker
d4cb712b50 Make everything build with GHC 8 2016-05-26 13:54:13 +01:00
Michael Walker
c306deb1f9 Support Stackage lts-3, lts-4, and lts-6 2016-05-26 13:08:24 +01:00
Michael Walker
dd5042e78f Build all branches with travis 2016-05-12 14:37:13 +01:00
Michael Walker
246f680248 Add Travis tests 2016-05-03 20:05:02 +01:00
Michael Walker
832559c4a7 Better README 2016-05-03 00:12:08 +01:00
Michael Walker
88da371bf6 Bump versions for dejafu-0.3.1.0 2016-05-02 23:44:00 +01:00
Michael Walker
452cc07553 Merge branch 'commit-preemptions' 2016-05-02 23:38:49 +01:00
Michael Walker
cea4d59b3c Correctly count preemptions with commit threads.
Conceptually, commits are happening truly in parallel
nondeterministically, and the commit threads are introduced to unify
this source of nondeterminism with the scheduling decisions. Commit
threads are not real threads, and switching to one is not a real context
switch, it therefore doesn't count as a preemption.

For example, this execution clearly has no preemptions in:

    S1---C-S1---

It would be absurd to say it has 1 preemption. But what about this?

    S1---C-S2---

This clearly DOES have a preemption. S1 was preempted by C (but we don't
count that), and then S2 started to execute! Control should have been
returned to S1.

Prior to now, this case was not considered specially. So every commit
effectively gives rise to a free preemption! This is bad for two
reasons:

- More schedules get executed, so testing takes longer.
- This is actually, in a sense, unsound! Results are potentially being
  reported which could NEVER arise under ANY real-world execution
  subject to those bounds!

It is because of this latter point that some of the expected results in
test litmusWP27 have been removed. They require more than the standard
two preemptions to observe.

Closes #39.
2016-05-02 23:35:08 +01:00
Michael Walker
e931a1a2c5 Code tidying 2016-05-02 23:16:10 +01:00
Michael Walker
396a743327 Code tidying 2016-05-02 22:35:33 +01:00
Michael Walker
ebcf7686c4 Bump versions for async-dejafu-0.1.2.1 2016-05-01 21:56:27 +01:00
Michael Walker
8b4785f51b Fix async-dejafu tests 2016-05-01 21:56:17 +01:00
Michael Walker
50a5e0c63b Bump versions for {hunit,tasty}-dejafu-0.3 2016-04-28 23:22:12 +01:00
Michael Walker
a1ef5a8813 Merge branch 'test-concurrently' 2016-04-28 23:20:19 +01:00