[erlang-questions] McErlang

[Kostis Sagonas]

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