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
Michael Walker
f4bcf51709
Add IsTest and IsOption instances to tasty-dejafu
2016-04-28 23:18:17 +01:00
Michael Walker
bdf289d84d
Add Assertable and Testable instancs to hunit-dejafu
2016-04-28 23:16:51 +01:00
Michael Walker
710529df39
Bump versions for async-dejafu-0.1.2
2016-04-28 23:05:28 +01:00
Michael Walker
6757a2a857
Merge branch '0.2-compat'
2016-04-28 23:02:49 +01:00
Michael Walker
3334928acf
Make tasty-dejafu work with 0.2 and 0.3
2016-04-28 17:09:46 +01:00
Michael Walker
636886c6fc
Relax hunit-dejafu constraint to work with 0.2 and 0.3
2016-04-28 17:07:05 +01:00
Michael Walker
4e08f66302
Make async-dejafu work with 0.2 and 0.3
2016-04-28 17:05:41 +01:00
Michael Walker
6fef2be497
Bump version numbers for hackage release.
...
async-dejafu, hunit-dejafu, and tasty-dejafu only get a minor bump
because the API didn't change, only the dependencies. I'm not entirely
sure how to fit that properly into the PVP.
2016-04-03 14:40:51 +01:00
Michael Walker
93c9ff9aa8
Document deviations from standard functionality
2016-04-03 06:56:26 +01:00
Michael Walker
aefba4b7d3
Add an Ord constraint on ThreadId.
2016-04-03 06:45:22 +01:00
Michael Walker
4afca62119
Drop the lock and unlock MVar functions
2016-04-03 06:45:11 +01:00
Michael Walker
073f3c69fb
Add a README and source repository for dpor
2016-04-03 06:07:37 +01:00
Michael Walker
539be21df5
Make tasty-dejafu work with new Trace type
2016-04-03 05:48:53 +01:00
Michael Walker
355a54cde6
Merge branch 'dpor-as-a-library'
2016-04-03 05:41:46 +01:00
Michael Walker
8ad7548faa
Add a simpler DPOR function variant
2016-04-03 05:36:43 +01:00
Michael Walker
39658767df
Improve dpor docs
2016-04-03 05:36:38 +01:00
Michael Walker
7d02708f92
Move Schedule module from DejaFu to DPOR.
2016-04-03 05:36:34 +01:00
Michael Walker
58643b9374
Reorganise Test.DPOR exports.
2016-04-03 05:36:28 +01:00
Michael Walker
5a599db0ca
More consistent type variable naming
2016-04-03 05:36:23 +01:00
Michael Walker
c8139ace2b
Tidy up Test.DPOR a bit
2016-04-03 05:36:16 +01:00
Michael Walker
7733c762c1
Merge the SCT modules
2016-04-03 05:34:01 +01:00
Michael Walker
552894d0bb
Split DPOR packages into separate library
2016-04-03 05:34:01 +01:00
Michael Walker
05741e1cd8
hlint fixes
2016-04-03 05:34:01 +01:00
Michael Walker
20a18ae598
Drop the unknown CRState.
2016-04-03 05:34:01 +01:00
Michael Walker
29150d03a3
Drop dependency (3) and compute state in dporSched
...
This massively reduces the number of schedules tried for the litmus
tests, as expected, which is great! Interestingly, it does result in
more unique results being discovered for intelWP27 and intelWP28. This
is surprising DPOR is supposed to be complete. Perhaps this indicates
some unsoundness in the way I have integrated schedule bounding with
relaxed memory.
2016-04-03 05:31:06 +01:00
Michael Walker
6df702f818
Document dpor function.
2016-04-03 05:09:51 +01:00
Michael Walker
f89b4d81e8
Move the rest of the generic SCT stuff to DPOR
2016-04-03 05:07:34 +01:00
Michael Walker
db8df120b9
Generalise and move todo to DPOR module.
2016-04-03 05:04:29 +01:00
Michael Walker
f3457b23a0
Generalise and move grow to DPOR module.
...
For some reason, this causes significantly more schedules to be explored
in some of the litmus tests, in particular intelWP27 and intelWP28. I've
not dug too deeply, but it's probably something which should be
addresed.
2016-04-03 05:02:44 +01:00
Michael Walker
bc205f428e
Generalise and move BacktrackStep and findBacktrack to DPOR module.
2016-04-03 04:08:25 +01:00
Michael Walker
6f3bcb4190
Generalise and move next to DPOR module.
2016-04-03 04:07:50 +01:00
Michael Walker
3e6a463014
Generalise and move BPOR type to DPOR module
2016-04-03 04:07:05 +01:00
Michael Walker
8ae1bbe14b
Start moving generic DPOR to separate module
2016-04-03 04:06:14 +01:00
Michael Walker
802d823351
Avoid repeated O(n) list traversals in todo.
...
Store the prior tid, rather than compute every time.
2016-04-03 04:05:22 +01:00
Michael Walker
87ffa1aa52
Remove the Commit decision
2016-04-03 04:04:31 +01:00
Michael Walker
894a521c7c
Pass the dependency function to findBacktrack and grow
2016-04-03 04:03:30 +01:00
Michael Walker
a551893ccf
Fix implementation of PSO.
...
There should be one buffer for each (thread, ref) pair, not simply for
each ref. The former is too strict as it enforces a total order on the
commits to the same ref, yielding some bizarro memory model which is
both stricter and more relaxed than TSO.
This does add extra schedules when testing PSO. But that is to be
expected, as this makes PSO executions less deterministic. Unfortunately
this additional nondeterminism is required by the memory model.
2016-04-01 17:57:17 +01:00
Michael Walker
ee7580dfe7
Add an independency between writes and commits.
...
An unsynchronised write and a commit to the same CRef are independent if
the buffer is nonempty, because the commit will take from the front of
the buffer and the write will append to the end.
See [RMMVerification], lemma 5.25. It doesn't translate directly because
of the different models, but it's the same optimisation in spirit.
2016-04-01 17:57:15 +01:00
Michael Walker
5e166e9df5
Tidy up README and add bibliography
2016-04-01 17:57:13 +01:00
Michael Walker
65e4ddc6c8
Add an isCommit predicate and refactor synchronises.
2016-04-01 17:56:47 +01:00
Michael Walker
6c29594675
Add a function to compare the different memory models
2016-03-31 18:43:10 +01:00
Michael Walker
a1122405fe
Less restrictive module exports in tests
2016-03-31 18:16:09 +01:00
Michael Walker
b98a03e22c
Add more litmus tests
2016-03-31 18:14:11 +01:00
Michael Walker
4c89ecf1d8
Fix TSO/PSO write buffers being the wrong way around.
2016-03-31 17:07:03 +01:00
Michael Walker
3ee0b3dc75
Add the Search Party failing test example
2016-03-31 15:08:37 +01:00
