[erlang-questions] PropEr and determinism of statem scenario execution
Clara Benac Earle
Wed Nov 28 20:10:34 CET 2012
McErlang does give you control over schedulers thus it might help you to
solve your problem. If you want to give McErlang a try we are more than
happy to help you with it.
Please contact us either on the mcerlang-questions mailing list or just
send me an email.
Looking forward to hearing from you,
Clara (co-creator of McErlang)
On 11/23/2012 12:32 PM, Paul Peregud wrote:
> Hi everyone!
> This is a PropEr-related question. I am developing a distributed
> algorithm for broadcasting messages, with very specific requirements
> (which are not really relevant to the problem, but prohibits use of
> e.g. Paxos in my case).
> Situation is following: I want to test a distributed algorithm. It's
> goal - synchronization of state consisting of sequence of broadcasted
> messages. Configuration is following - there are N actors, each actor
> implements publish/2 that adds new entry to cache and broadcasts.
> Actors are communicating, trying to achieve consistent state of cache
> among all of them. Actors are unreliable - they can be added and they
> may crash.
> My test case is a sequence of commands from following set: [actor_up,
> actor_down, publish]. My "system under test" is a process that starts
> actors, shuts them down and publishes new messages. It also collects
> reports that actors provide and provides that reports as a material
> for postcondition that checks cache consistency.
> The problem - I don't have a control over schedulers. That leads to
> scenarios that MAY OR MAY NOT fail. And that causes problems with
> shrinking. As a result after a night of crunching scenarios on a fast
> machine I get a test case of 70 steps that is impossible to debug,
> because it is too large. When I repeat this test case using
> proper:check/2, it fails very seldom.
> I've tried to tackle the problem in following way.
> I have introduced an execution token. An actor is waiting in selective
> receive for the token, when it gets it, it takes one message from it's
> queue and processes it. After that token is returned to proper tester
> process and can be passed to another actor.
> This approach is not good enough, because every generated scenario
> passes. I can think of one reason only - if actors A and B perform and
> they both send 2 messages (upon receiving the execution token) to
> actor C then actors C queue may look only like that: [A1, A2, B1, B2].
> In real life scenario queue [A1, B1, A2, B2] is also possible.
> I understand that I can modify actors even more and introduce more
> fine-grained control over their actions - execution token will be
> returned after one single message sent. But this approach feels like
> an ugly hack. Is there a more general way to deal with this problem?
> Is it possible to achieve fine-grained concurrent simulation using
> Any ideas are welcome!
> As far as I understand McErlang solves this problem in a more low
> level way, but I have never heard it used for practical problems. Did
> anyone used it to test non-academic systems? Any success stories here?
> How hard is it to use?
> Best regards,
> Paul Peregud
> erlang-questions mailing list
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the erlang-questions