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
Michael Walker
18cb1c86c9
Organise tests a little
2016-03-31 14:45:55 +01:00
Michael Walker
9e68038e2b
Add AutoUpdate example to tests
2016-03-31 14:37:02 +01:00
Michael Walker
2952b75526
Drop the CVState stuff.
2016-03-27 21:39:47 +01:00
Michael Walker
ad33fb729b
Drop import/export shortcut for better haddocks
2016-03-26 06:50:47 +00:00
Michael Walker
ab1212ad07
Merge branch 'rename-remodularise'.
...
Closes #36 . Closes #37 .
2016-03-26 06:45:10 +00:00
Michael Walker
3ed2e1e25b
Remove strict Chan and MVar modules
...
If people want strict concurrency types, they can just use $!!
themselves.
2016-03-26 06:43:25 +00:00
Michael Walker
f7d0059b7e
Add CRef module
2016-03-26 06:42:57 +00:00
Michael Walker
5b4911032e
Rename modifyCRef to atomicModifyCRef
2016-03-26 06:37:27 +00:00
Michael Walker
41af1cdaa6
hlint/style fixes
2016-03-26 06:26:28 +00:00
Michael Walker
dd50876d1b
Add strict and normal MVar chans
2016-03-26 06:23:33 +00:00
Michael Walker
d87ae811ca
Add QSem and QSemN
2016-03-26 02:57:40 +00:00
Michael Walker
6a913c96ca
Reduce boilerplate in Conc/STM instance decls
2016-03-24 07:52:10 +00:00
Michael Walker
ad753d1f33
Move Control.Concurrent.STM.Classy -> Control.Concurrent.Classy.STM
2016-03-23 04:38:34 +00:00
Michael Walker
bb291c8128
Add a classy STM TArray
2016-03-23 04:33:20 +00:00
Michael Walker
5d2425e8c2
Add a classy STM TBQueue
2016-03-23 04:28:42 +00:00
Michael Walker
ef133a5d06
Add classy STM TQueue
2016-03-23 04:20:26 +00:00
Michael Walker
1150f2814a
Add a classy STM TChan
2016-03-23 04:13:49 +00:00
