[erlang-questions] PropEr and determinism of statem scenario execution

[Clara Benac Earle]

Hi Paul,

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 
> Proper/Quickcheck?
>
> 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
> +48602112091
>
>
> _______________________________________________
> erlang-questions mailing list
> erlang-questions@REDACTED
> http://erlang.org/mailman/listinfo/erlang-questions

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://erlang.org/pipermail/erlang-questions/attachments/20121128/c9589904/attachment.htm>