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

[Erik Søe Sørensen]

Don't know if it's usable with Proper, but Quviq has a tool called "PULSE"
for that kind of test. Afaik it does something like the token thing, except
that it's for each message sent.
It's somewhat ungoogleable, but Basho uses it.
Den 23/11/2012 12.32 skrev "Paul Peregud" <paulperegud@REDACTED>:

> 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/20121123/2e2263cc/attachment.htm>