alfert / propcheck

Property based Testing for Elixir (based upon PropEr)
GNU General Public License v3.0
376 stars 42 forks source link

Concurency testing improvments #148

Open x4lldux opened 4 years ago

x4lldux commented 4 years ago

@alfert please fill this in with your proposal mentioned in #147

I just wanted to share things I've gather about this topic.

x4lldux commented 4 years ago

Mailing list discussion about McErlang, Concuerror and PULSE https://groups.google.com/forum/#!topic/erlang-programming/G6Zxs_LrkVc

PULSE

Original paper - http://publications.lib.chalmers.se/records/fulltext/125252/local_125252.pdf

Quviq's PULSE docs - http://quviq.com/documentation/pulse/ PULSE tutorial - http://www.erlang-factory.com/upload/presentations/191/EUC2009-PULSE.pdf

Video presentation - https://vimeo.com/6638041

Opensourced version - https://github.com/prowessproject/pulse-time https://github.com/Quviq/pulse_otp

Concuerror

Original paper - https://mariachris.github.io/Pubs/ERLANG-2011.pdf

Apparently Concuerror can't be used with *.exs files, but some work has begun (but stalled) - parapluu/Concuerror#300

alfert commented 4 years ago

Beneath state machine models I am most stunned by QuickCheck's Pulse subsystem to use property based testing for analysing concurrent algorithms and systems. Alas, it is available only in the commercial version. The approach for parallel testing implemented in PropEr is very limited, but the research group behind PropEr developed concuerror, which applies model checking techniques for running all important schedules of concurrent system. I tried this a couple of years ago, but it wasn't a too positive experience.

So, with new features in PropEr (targeted PBT), a new property-based testing framework for Elixir by the Elixir Core Team, new DSLs and features in PropCheck I thought the time has come for realising my dream of having an open source equivalent of Pulse called Tracer.

Scientific papers are available, also the open source implementation of the scheduler and the instrumentation (thanks to @x4lldux for providing the pointer!). I started with implementing the instrumentation via macros and some infrastructures based upon the scientific paper descriptions and will publish my branch soon.

There are lots of tasks to be done, here is a first incomplete list:

For managing this stuff, I started an experimental project in this GitHub repo, perhaps it helps.

x4lldux commented 4 years ago

I'd suggest we walk before running, and improve PropCheck's/PropEr's builtin support for concurrent testing (albeit limited as it is). Improve documentation, add some examples (we have none at this moment) and add support for it in Reporter. It would be nice if Reporter could draw some ASCII art for it and then for Tracer.

alfert commented 4 years ago

Interesting idea for the Reporter!

My gut feeling is that we need to exploit the Erlang trace API to get information about running processes and their messages. Putting these traces into a directed graph (I like the libgraph more than Erlang's digraph) and we should be able to render the graph via dot (i.e. GraphViz).

We can pretty sure re-use this infrastructure also for Tracer later.

x4lldux commented 4 years ago

My gut feeling is that we need to exploit the Erlang trace API to get information about running processes and their messages.

You mean for Tracer/PULSE?

alfert commented 4 years ago

With Tracer, we would have explicit access to all messages send etc since we intercept them (similar to what Pulse does). No, I thought of using the tracing capabilities for cool reporting in PropErs parallel testing, which - if I remember right - simply executes the state models in an concurrent fashion after some sequential prefix of events.

x4lldux commented 4 years ago

Oh. Than I wasn't thinking about that. I'm not sure that tracing messages in that case would give us anything useful to show. What I was thinking is more in the spirit of just showing a tree of parallel commands:

      ,-> cache(6,0) -> flush()
  0 --+
      '-> cache(0,-1)