[erlang-questions] 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: erlang-questions-bounces@REDACTED [mailto:erlang-questions-bounces@REDACTED] För Clara Benac Earle
Skickat: den 3 oktober 2017 16:09
Till: Kostis Sagonas <kostis@REDACTED>; erlang-questions@REDACTED; Lars-Åke Fredlund <lfredlund@REDACTED>
Ä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 <http://dblp2.uni-trier.de/pers/hd/a/Arts:Thomas> , Clara Benac Earle, John Derrick <http://dblp2.uni-trier.de/pers/hd/d/Derrick:John> :
Development of a verified Erlang program for resource locking. STTT 5(2-3) <http://dblp2.uni-trier.de/db/journals/sttt/sttt5.html#ArtsED04> : 205-220 (2004)

Lars-Åke Fredlund <http://dblp2.uni-trier.de/pers/hd/f/Fredlund:Lars==Aring=ke> , Clara Benac Earle: 

Model checking erlang programs: the functional approach. Erlang Workshop 2006 <http://dblp2.uni-trier.de/db/conf/erlang/erlang2006.html#FredlundE06> : 11-19

 

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://erlang.org/pipermail/erlang-questions/attachments/20171003/b44b569c/attachment.htm>