propcheck icon indicating copy to clipboard operation
propcheck copied to clipboard

Concurency testing improvments

Open x4lldux opened this issue 4 years ago • 7 comments

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

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

x4lldux avatar Jan 21 '20 12:01 x4lldux

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

x4lldux avatar Jan 21 '20 12:01 x4lldux

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:

  • [ ] Scheduling algorithms
  • [ ] Instrumentation
  • [ ] Test suite (examples, and tests for internal behaviours)
  • [ ] Good error reporting, possibly generating of trace diagrams as by PulSe and Concuerror
  • [ ] Documentation
  • [ ] Instrumentation of existing libraries - if required

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

alfert avatar Jan 22 '20 07:01 alfert

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.

x4lldux avatar Jan 22 '20 08:01 x4lldux

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.

alfert avatar Jan 22 '20 17:01 alfert

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?

x4lldux avatar Jan 22 '20 21:01 x4lldux

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.

alfert avatar Jan 23 '20 18:01 alfert

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)

x4lldux avatar Jan 23 '20 18:01 x4lldux