[erlang-questions] McErlang

[Lars-Åke Fredlund]

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.


/Lars-Ake









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 
> Concuerror.
>
> 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).
>
> Best,
> Kostis