Tue Oct 3 12:16:04 CEST 2017
I am very impressed that Concuerror is able to find all concurrency
errors, for an arbitrary complex program, given a finite amount of time,
and a finite amount of memory... :-)
McErlang can find all errors too, of course, but in practice for many
(complex) programs it will fail to do so given the practical limitations
(memory, time). Concurerror has a different search strategy, and in
many/most cases will suffer less than McErlang from the inherent complex
behaviour of the program under analysis, but it will suffer too.
On 03/10/17 11:57, Kostis Sagonas wrote:
> On 10/03/2017 11:05 AM, Lars-Åke Fredlund wrote:
>> McErlang was a cool project though. Is McErlang better or worse than
>> Concuerror? Well, it is always better to use a maintained tool than a
>> tool that nobody has time to fix. The tools are based on different
>> internal ideas, with different search strategies, which at least in
>> theory can cause some errors to be detected by one tool to fail to be
>> detected by the other tool, and vice versa.
> I would be interested in seeing a simple example program containing a
> _concurrency_ error that can be detected by McErlang but not by
> AFAIK, Concuerror finds *all* concurrency errors (for a particular way
> of using/running a program), where the set of concurrency errors
> contains program crashes, assertion violations and global deadlocks
> that happen in some (and not necessarily in all) process schedulings
> of an Erlang program.
> Thus Concuerror, in principle at least (i.e., modulo bugs in its
> code), actually *verifies*, using stateless model checking, that a
> particular (part of a) program is free of concurrency errors, in
> contrast to e.g. QuickCheck/PULSE which fundamentally cannot provide
> any correctness guarantees (other than probabilistic ones).
More information about the erlang-questions