McErlang

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
12 messages Options
Reply | Threaded
Open this post in threaded view
|

McErlang

Richard A. O'Keefe-2
I just downloaded McErlang today.
I note that
  - the last entry in NEWS is from 2011
  - the last change in GitHub is 2 years ago
  - I had to change the type :: record() to :: any() to
    get it to compile, and there are numerous warnings
    from the compiler, including an ambiguous call, and
    of course lots of erlang:now() complaints.
  - it was produced as part of an EU project which
    appears to have come to an end, so there may not be
    money to keep it up to date.

I have got it to the point where it compiles, but given
the date, I haven't dared to see what it does with maps.

Now this looked like a very useful tool, but before I
spend any time getting a clean compilation,
  - is anyone else (still) using McErlang?
  - has McErlang been replaced by something better that
    I can afford?
  - or should I just forget all about it?

_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions
Reply | Threaded
Open this post in threaded view
|

Re: McErlang

zxq9-2
On 2017年10月03日 火曜日 18:02:32 Richard A. O'Keefe wrote:

> I just downloaded McErlang today.
> I note that
>   - the last entry in NEWS is from 2011
>   - the last change in GitHub is 2 years ago
>   - I had to change the type :: record() to :: any() to
>     get it to compile, and there are numerous warnings
>     from the compiler, including an ambiguous call, and
>     of course lots of erlang:now() complaints.
>   - it was produced as part of an EU project which
>     appears to have come to an end, so there may not be
>     money to keep it up to date.
>
> I have got it to the point where it compiles, but given
> the date, I haven't dared to see what it does with maps.
>
> Now this looked like a very useful tool, but before I
> spend any time getting a clean compilation,
>   - is anyone else (still) using McErlang?
>   - has McErlang been replaced by something better that
>     I can afford?
>   - or should I just forget all about it?

I think this is *great*, at least in concept, if not in execution.
I had never heard of this before. It looks pretty dead, though.

Depending on the condition of the code I would be interested in patching
it to bring the thing up to date with changes in Dialyzer and Erlang,
but I don't have much time to contribute to that sort of thing for at
least a few more months.

Concurrent model testing in Erlang is a rather large gap we have that
tends to get covered by actual runs and post-mortem analysis. Which is
actually fine for the majority of cases (clearly; we've gotten this far)
but having a tool that can do for concurrent sequence testing what tools
like PropER can do for functional testing would be quite useful.

Definitely putting it on my list of things to sort...

-Craig
_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions
Reply | Threaded
Open this post in threaded view
|

Re: McErlang

Kostis Sagonas-2
On 10/03/2017 07:13 AM, zxq9 wrote:

>> Now this looked like a very useful tool, but before I
>> spend any time getting a clean compilation,
>>    - is anyone else (still) using McErlang?
>>    - has McErlang been replaced by something better that
>>      I can afford?
>>    - or should I just forget all about it?
> ... <SNIP> ...
>
> Concurrent model testing in Erlang is a rather large gap we have that
> tends to get covered by actual runs and post-mortem analysis. Which is
> actually fine for the majority of cases (clearly; we've gotten this far)
> but having a tool that can do for concurrent sequence testing what tools
> like PropER can do for functional testing would be quite useful.

I think that you should really take a look at Concuerror.

        http://concuerror.com/

Besides various tutorials, which are quite comprehensive, it also comes
with (not always easy to read) papers that explain its technology and
its differences from McErlang.

I am of course very partial, since I'm heavily involved in its design
and development, but it's in many ways a superior tool.

Hope that others find it useful; some already have.


Kostis
_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions
Reply | Threaded
Open this post in threaded view
|

Re: McErlang

Scott Lystig Fritchie
In reply to this post by Richard A. O'Keefe-2
Hi, Richard. It is too late in the middle of the US for a great answer (zzzzz...), but since it isn’t such a crazy hour for you (probably), a terrible answer might be helpful?

The Concuerror tool at http://concuerror.com/ is under active development today by Stavros Aronis. Its DPOR techniques are likely far more efficient than McErlang’s search strategies, even if McErlang were cleaned up for a newer Erlang release.  I’ve used it on a couple of verification projects with good results. 

-Scott 


_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions
Reply | Threaded
Open this post in threaded view
|

Re: McErlang

zxq9-2
In reply to this post by Kostis Sagonas-2
On 2017年10月03日 火曜日 08:27:06 Kostis Sagonas wrote:

> On 10/03/2017 07:13 AM, zxq9 wrote:
> >> Now this looked like a very useful tool, but before I
> >> spend any time getting a clean compilation,
> >>    - is anyone else (still) using McErlang?
> >>    - has McErlang been replaced by something better that
> >>      I can afford?
> >>    - or should I just forget all about it?
> > ... <SNIP> ...
> >
> > Concurrent model testing in Erlang is a rather large gap we have that
> > tends to get covered by actual runs and post-mortem analysis. Which is
> > actually fine for the majority of cases (clearly; we've gotten this far)
> > but having a tool that can do for concurrent sequence testing what tools
> > like PropER can do for functional testing would be quite useful.
>
> I think that you should really take a look at Concuerror.
>
> http://concuerror.com/
>
> Besides various tutorials, which are quite comprehensive, it also comes
> with (not always easy to read) papers that explain its technology and
> its differences from McErlang.
>
> I am of course very partial, since I'm heavily involved in its design
> and development, but it's in many ways a superior tool.
>
> Hope that others find it useful; some already have.

Wow, awesome!

This is an area I haven't had a chance to get on board with yet (limited
time) but I'm very glad that ROK's email wound up pointing me toward both
McErlang and inadvertently led me to Concuerror.

Thank you guys for the link!

-Craig
_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions
Reply | Threaded
Open this post in threaded view
|

Re: McErlang

Lars-Åke Fredlund-2
Hello all,

as you have noticed we haven't really been working on McErlang for some
time. There is no support for some modern features of Erlang, and
frankly I doubt we will have time to fix things in the short term.

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. Clearly applying Concuerror
to a program is easier than applying McErlang, and so I would definitely
try using Concuerror first.

Another tool  worth trying is QuickCheck with the pulse random
scheduler; it can be surprisingly good at detecting concurrency bugs
with a very moderate effort.

Lars-Ake



On 03/10/17 09:40, zxq9 wrote:

> On 2017年10月03日 火曜日 08:27:06 Kostis Sagonas wrote:
>> On 10/03/2017 07:13 AM, zxq9 wrote:
>>>> Now this looked like a very useful tool, but before I
>>>> spend any time getting a clean compilation,
>>>>     - is anyone else (still) using McErlang?
>>>>     - has McErlang been replaced by something better that
>>>>       I can afford?
>>>>     - or should I just forget all about it?
>>> ... <SNIP> ...
>>>
>>> Concurrent model testing in Erlang is a rather large gap we have that
>>> tends to get covered by actual runs and post-mortem analysis. Which is
>>> actually fine for the majority of cases (clearly; we've gotten this far)
>>> but having a tool that can do for concurrent sequence testing what tools
>>> like PropER can do for functional testing would be quite useful.
>> I think that you should really take a look at Concuerror.
>>
>> http://concuerror.com/
>>
>> Besides various tutorials, which are quite comprehensive, it also comes
>> with (not always easy to read) papers that explain its technology and
>> its differences from McErlang.
>>
>> I am of course very partial, since I'm heavily involved in its design
>> and development, but it's in many ways a superior tool.
>>
>> Hope that others find it useful; some already have.
> Wow, awesome!
>
> This is an area I haven't had a chance to get on board with yet (limited
> time) but I'm very glad that ROK's email wound up pointing me toward both
> McErlang and inadvertently led me to Concuerror.
>
> Thank you guys for the link!
>
> -Craig
> _______________________________________________
> erlang-questions mailing list
> [hidden email]
> http://erlang.org/mailman/listinfo/erlang-questions

_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions
Reply | Threaded
Open this post in threaded view
|

Re: McErlang

Kostis Sagonas-2
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
_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions
Reply | Threaded
Open this post in threaded view
|

Re: McErlang

Lars-Åke Fredlund-2
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

_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions
Reply | Threaded
Open this post in threaded view
|

Re: McErlang

Stavros Aronis
Concuerror is indeed an actively maintained tool that is a suitable replacement for McErlang. I spent the morning updating some of the pages on http://concuerror.com. :-)

/Stavros

_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions
Reply | Threaded
Open this post in threaded view
|

Re: McErlang

Clara Benac Earle
In reply to this post by Kostis Sagonas-2
Dear Kostis,

I would be interested in seeing a simple example program containing a _concurrency_ error that can be detected by McErlang but not by Concuerror.

Please have a look at the locker case-study presented in several of our papers (see below). This case-study contains a server that grants exclusive/shared access to resources. It is vaguely inspired on some code in the AXD301.

Starvation of a client requesting shared access to one resource occurs when there are two clients requesting exclusive access to the same resource, since exclusive access has priority over shared access. We were able to find this already in 2004, and later on with McErlang. Concuerror has been running now for more than 20 minutes and still no answer so I cannot tell you whether it can find the starvation problem or not.

Best regards
Clara

, , :
Development of a verified Erlang program for resource locking. STTT 5(2-3): 205-220 ()
, :
Model checking erlang programs: the functional approach. Erlang Workshop : 11-19


_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions
Reply | Threaded
Open this post in threaded view
|

Re: McErlang

john.hughes

Concuerror will guarantee to find bugs… with relatively short runs, relatively few processes, and a small number of preemptions. It’s searching very thoroughly in a small part of the space of possible executions—and it’s very good at it, but there is still an exponential blowup that will strike eventually. Random sampling, such as QuickCheck and PULSE do, can sample from a much larger part of the space… and if that’s where the bugs are, then that’s where you have to look for them! So Concuerror/McErlang and random tools are really complementary—either one may find bugs faster, depending on the kind of bug. There is plenty of evidence that sampling larger random tests, and shrinking them, can be a much faster way to find faults than enumerating smaller tests.

 

John

 

Från: [hidden email] [mailto:[hidden email]] För Clara Benac Earle
Skickat: den 3 oktober 2017 16:09
Till: Kostis Sagonas <[hidden email]>; [hidden email]; Lars-Åke Fredlund <[hidden email]>
Ämne: Re: [erlang-questions] McErlang

 

Dear Kostis,

I would be interested in seeing a simple example program containing a _concurrency_ error that can be detected by McErlang but not by Concuerror.


Please have a look at the locker case-study presented in several of our papers (see below). This case-study contains a server that grants exclusive/shared access to resources. It is vaguely inspired on some code in the AXD301.

Starvation of a client requesting shared access to one resource occurs when there are two clients requesting exclusive access to the same resource, since exclusive access has priority over shared access. We were able to find this already in 2004, and later on with McErlang. Concuerror has been running now for more than 20 minutes and still no answer so I cannot tell you whether it can find the starvation problem or not.

Best regards
Clara

Thomas Arts, Clara Benac Earle, John Derrick:
Development of a verified Erlang program for resource locking. STTT 5(2-3): 205-220 (2004)

Lars-Åke Fredlund, Clara Benac Earle:

Model checking erlang programs: the functional approach. Erlang Workshop 2006: 11-19

 


_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions
Reply | Threaded
Open this post in threaded view
|

Re: McErlang

Kostis Sagonas-2
On 10/03/2017 07:08 PM, John Hughes wrote:

> Concuerror will guarantee to find bugs… with relatively short runs,
> relatively few processes, and a small number of preemptions. It’s
> searching very thoroughly in a small part of the space of possible
> executions—and it’s very good at it, but there is still an exponential
> blowup that will strike eventually. Random sampling, such as QuickCheck
> and PULSE do, can sample from a much larger part of the space… and if
> that’s where the bugs are, then that’s where you have to look for them!
> So Concuerror/McErlang and random tools are really complementary—either
> one may find bugs faster, depending on the kind of bug. There is plenty
> of evidence that sampling larger random tests, and shrinking them, can
> be a much faster way to find faults than enumerating smaller tests.

I very much agree that systematic and random-based tools are really
complementary: both have their pros and cons and, for that reason, their
proper place in a programmer's tool suite.  Also, for testing purposes,
there is a lot to be said for finding bugs sooner rather than later and
perhaps one can detect bugs faster with random sampling if the bug
occurs sufficiently frequently.

Still, some of my recent experiences [1] [2] are different: a
sufficiently powerful stateless model checking tool, such as Concuerror
(or a similar such tool for C), can find concurrency bugs pretty fast,
_provided_ that one pays attention to the careful *modeling* of the
system.  This is where one of the difficulties of using systematic
concurrency testing tools lies: how to "minimize the model"(*) in order
to fight the combinatorial explosion.  Once this is done properly,
finding concurrency bugs is easy, because most such bugs require very
few preemptions/context switches to manifest themselves.

(*) In many cases the part that needs to be minimized consists of the
components of the system that are not tested; in some others it's the
complete program under test.

Unfortunately, this manual minimization process that tools which test
very thoroughly require (e,g., in a program with N reader processes and
M writer processes, all concurrent, one does not need to use large
values of N and M to find a data race; using just one of each kind will
suffice for read/write races and two writers for write/write races or
immutability violations) goes very much against the idea of "you need to
stress-test to increase your likelihood of finding concurrency errors"
that many programmers have been brainwashed to use, which may or may not
be related to why random sampling often works well.

But if one is interested just in "finding bugs", bounding techniques can
often do wonders.  [1] reports by that by using bounding, Concuerror
finds a bug in some particular method/program (Method 1 in that paper)
in less than a minute, while without bounding the tool needs 144 hours
to detect the bug.  (Later, the same paper shows that, even without
bounding, the bugs in that method are detected very fast if one pays
attention to the model [1, Table 2].)


An interesting (to me at least) question is what should happen after all
"shallow" bugs have been fixed and a particular tool does NOT detect a
bug anymore.  What sort of guarantees are provided by the tool?  Isn't
it time to use a systematic instead of a random-based tool?  This is
exactly what I was referring to in my previous mail where I wrote:

   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).

As both [1] and [2] report, it's possible to get actual guarantees about
the absence of certain classes of (concurrency) errors using a stateless
model checking tool, even in code bases of significant size such as
portions of the Linux kernel.  This guarantee exists _because of_ the
systematic exploration and the fact that the tools are sound (i.e., can
in principle detect all errors).


Kostis


[1] Testing and Verifying Chain Repair Methods for Corfu Using Stateless
Model Checking (http://concuerror.com/assets/pdf/iFM2017.pdf)

[2] Stateless model checking of the Linux kernel's hierarchical
read-copy-update (Tree RCU) - https://dl.acm.org/citation.cfm?id=3092287
_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions