barrucadu/dejafu
1
1
Fork 0
mirror of https://github.com/barrucadu/dejafu.git synced 2024-12-19 11:32:01 +03:00
Code Issues Projects Releases Wiki Activity
608 Commits 2 Branches 194 Tags 3.4 MiB
5f9ad29b1b
Commit Graph

608 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
Michael Walker
b3b275cdb1 Add a 'noBounds' binding for convenience. 2015-12-02 14:40:05 +00:00
Michael Walker
a18a7d2fa5 Support unbounded DPOR (closes #34) 
If no bounds are enabled, just backtrack to the point identified.
 2015-12-02 14:35:22 +00:00
Michael Walker
c64ecbee94 Factor out common backtracking code 2015-12-02 04:43:19 +00:00
Michael Walker
cae5704ac9 Enable building tests with GHC <7.10 2015-12-01 05:13:47 +00:00
Michael Walker
37a5886c83 Make a separate package for the test suite. Closes #31. 2015-12-01 05:07:56 +00:00
Michael Walker
bd340e6eb3 Fix for pre-FTP GHC 2015-12-01 04:29:46 +00:00
Michael Walker
0ff053eaae Add a Dining Philosophers example 2015-12-01 04:27:58 +00:00
Michael Walker
cdcaebb26c Add aborting predicates 2015-12-01 04:27:47 +00:00
Michael Walker
1e0eb2a172 Add typeclass laws test/example 2015-12-01 04:12:02 +00:00
Michael Walker
e75c1ee24a Change test suite to use test-framework 2015-12-01 04:11:44 +00:00
Michael Walker
cb146a7769 Correctly count pre-emptions in a schedule 2015-12-01 04:10:23 +00:00
Michael Walker
acf2150788 Add a variant of 'toDot' which prunes aborted subtrees 2015-12-01 03:18:30 +00:00
Michael Walker
cb77ae234a Correctly identify CVar read/write dependencies 2015-12-01 03:18:05 +00:00
Michael Walker
917c8a3954 Add missing symmetric cases to dependentActions 2015-11-30 22:08:44 +00:00
Michael Walker
efa65859b1 Add setNumCapabilities. Closes #23. 2015-11-30 22:08:44 +00:00
Michael Walker
42f0132ff4 Add some more typeclass instances 2015-11-30 22:08:44 +00:00
Michael Walker
b84614b46f Add a function to convert a 'BPOR' into a GraphViz graph 2015-11-30 22:08:44 +00:00
Michael Walker
e50152874b Properly implement sleep sets. 
- Don't make decisions in bporSched which are in the sleep set.
 - Don't consider backtracking points from executions which terminated
   due to every decision being in the sleep set.
 2015-11-30 22:08:42 +00:00
Michael Walker
a47d8c00e7 Move willRelease to Deterministic.Internal.Common 2015-11-30 22:06:44 +00:00
Michael Walker
96d0964ea4 Return the most recent state when aborting. 2015-11-30 22:06:44 +00:00
Michael Walker
b13650b892 Don't pre-empt thread termination with exceptions. 
If a thread is about to terminate gracefully, there's no point in
pre-empting the `Stop` action to throw an exception to it.
 2015-11-30 22:06:43 +00:00
Michael Walker
5371e74ff0 Make PFL bounding the default 2015-11-30 22:06:43 +00:00
Michael Walker
3327358520 Introduce a dependency between the final action and everything. 
Introducing length bounding failed to find a deadlock in the Dining
Philosophers! I believe that the typical DPOR algorithm assumes that
every thread terminates before the entire process terminates, which
simply isn't the case in Haskell.

To combat this, a dependency was introduced between the final action
in a trace and everything. Just introducing a dependency for (0, Stop)
isn't enough, as execution can be aborted due to the length bound on
any action.
 2015-11-30 22:06:40 +00:00
Michael Walker
258d8dfc17 Add length bounding 2015-11-18 12:31:06 +00:00
Michael Walker
49a903c6e3 Add newtype for preemption bounds and fair bounds 2015-11-17 19:29:35 +00:00
Michael Walker
b6ceaede99 Abort SCT execution early if there are no decisions in bound. Closes #28. 2015-11-17 19:16:19 +00:00
Michael Walker
68ef26727b Give schedulers the trace so far 2015-11-17 19:16:13 +00:00
Michael Walker
d1643bb360 Enable building with Stackage lts-2 2015-11-17 19:15:56 +00:00
Michael Walker
f3be1d12ab Replace type synonyms with newtypes. Closes #29. 2015-11-17 19:15:52 +00:00
Michael Walker
c6a702f725 Use ThreadId in definition of Conc, not Int 2015-11-17 18:03:03 +00:00
Michael Walker
3d3119ffd6 Expand test suite 2015-11-16 02:48:54 +00:00
Michael Walker
bc04990dbd Fix off-by-one in adding backtracking points 2015-11-16 02:46:22 +00:00
Michael Walker
17ddc217c4 Unsynchronised reads and writes ARE dependent 2015-11-16 02:45:53 +00:00
Michael Walker
4081a6d7d7 Fix error with stepCommit argument order 2015-11-16 01:49:35 +00:00
Michael Walker
74dce99d71 Make stepModRefCas strict in the new value 2015-11-15 16:53:10 +00:00
Michael Walker
64057590db Merge branch 'primops-simp'. Closes #20. 
This only implements the atomic-primops operations which deal with CRefs,
as handling relaxed memory in the presence of MutVar#s is really hard.
 2015-11-15 15:45:12 +00:00
Michael Walker
343e097f83 Implement casCRef and modifyCRefCAS 2015-11-15 15:42:45 +00:00
Michael Walker
12f0a118ef Store threads in an IntMap 2015-11-15 15:42:45 +00:00
Michael Walker
af1985747d Implement readForCAS 2015-11-15 15:42:45 +00:00
Michael Walker
8d3be1cd19 Add modifyCRefCAS_ 2015-11-15 15:42:45 +00:00
Michael Walker
5d3e84ac76 Move lookahead to Deterministic.Internal.Common 2015-11-15 15:42:45 +00:00
Michael Walker
b20f254c29 Add a primitive for peekTicket 2015-11-15 15:42:45 +00:00
Michael Walker
62c2b38867 Add primitives for readForCAS, casCRef, and modifyCRefCAS 2015-11-15 15:42:45 +00:00
Michael Walker
e8bbb191ed Add compare-and-swap primitives to MonadConc 2015-11-15 15:42:45 +00:00
Michael Walker
385d67a842 Remvoe Par comparison from MonadConc description 2015-11-15 15:42:37 +00:00
Michael Walker
b1ee473068 Clarify default memory model 2015-11-15 15:39:07 +00:00
Michael Walker
39b0ae8a45 Fix comment on memory behaviour of CRefs 2015-11-14 01:15:09 +00:00
Michael Walker
24faa57f29 Only show representative failures in autocheck 2015-11-12 14:56:32 +00:00
Michael Walker
41b1368f0b Remove explicit nubby functions 2015-11-12 14:53:37 +00:00
Michael Walker
e9b417684a Improve nubbyness 2015-11-12 14:52:58 +00:00