Stevan A

I've found the quote again: > "Almost all (96%) of the examined concurrency bugs are guaranteed to manifest if certain partial order between 2 threads is enforced." From the end...

> This error message is hard to understand, because it is expressed in terms of the internals of the library. What internals? I don't see a single concept in that...

The always combinator isn't hard to define, but look at how it's used: ```erlang prop_atomic() -> ?LET(Shrinking, parameter(shrinking, false), ?FORALL(ParCmds, parallel_commands(client), ?ALWAYS(if Shrinking -> 10; true -> 1 end, begin...

> To address the performance problem, we added a new algorithm to Knossos, based on [Lowe](http://www.cs.ox.ac.uk/people/gavin.lowe/LinearizabiltyTesting/paper.pdf), [Horn and Kroening’s](https://arxiv.org/pdf/1504.00204.pdf) refinement of [Wing & Gong’s](http://www.cs.cmu.edu/~wing/publications/WingGong93.pdf) algorithm for verifying linearizability. Following Lowe’s...

https://github.com/rystsov/fast-jepsen

_Concurrent Specifications Beyond Linearizability_: * http://drops.dagstuhl.de/opus/volltexte/2018/10088/pdf/LIPIcs-OPODIS-2018-28.pdf * http://personal.strath.ac.uk/jeremy.ledent/slides_OPODIS.pdf

I've used `pkill` in some tests, it's ugly but got the job done... In older versions of the library, `setup` and `cleanup` functions used to be part of the `StateMachine`...

> not that good, since in parallel execution the current Model is unreliable (but the environment is still reliable) Why is the model unreliable? Can we not make it: ```...

> In the parallel case executeCommands is called with the initModel as intial state. Yes, but that would be easy to change: pass in the model that's the result of...

So another option would be to require `Monoid (model r)`. Also a bit awkward...