<html xmlns:v="urn:schemas-microsoft-com:vml" xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40"><head><meta http-equiv=Content-Type content="text/html; charset=utf-8"><meta name=Generator content="Microsoft Word 15 (filtered medium)"><style><!--
/* Font Definitions */
@font-face
{font-family:"Cambria Math";
panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
{font-family:Calibri;
panose-1:2 15 5 2 2 2 4 3 2 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0cm;
margin-bottom:.0001pt;
font-size:11.0pt;
font-family:"Calibri",sans-serif;
color:black;}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:blue;
text-decoration:underline;}
a:visited, span.MsoHyperlinkFollowed
{mso-style-priority:99;
color:purple;
text-decoration:underline;}
p.msonormal0, li.msonormal0, div.msonormal0
{mso-style-name:msonormal;
mso-margin-top-alt:auto;
margin-right:0cm;
mso-margin-bottom-alt:auto;
margin-left:0cm;
font-size:11.0pt;
font-family:"Calibri",sans-serif;
color:black;}
span.this-person
{mso-style-name:this-person;}
span.title
{mso-style-name:title;}
span.E-postmall20
{mso-style-type:personal;
font-family:"Calibri",sans-serif;
color:windowtext;}
span.E-postmall21
{mso-style-type:personal-compose;
font-family:"Calibri",sans-serif;
color:windowtext;}
.MsoChpDefault
{mso-style-type:export-only;
font-size:10.0pt;}
@page WordSection1
{size:612.0pt 792.0pt;
margin:70.85pt 70.85pt 70.85pt 70.85pt;}
div.WordSection1
{page:WordSection1;}
--></style><!--[if gte mso 9]><xml>
<o:shapedefaults v:ext="edit" spidmax="1026" />
</xml><![endif]--><!--[if gte mso 9]><xml>
<o:shapelayout v:ext="edit">
<o:idmap v:ext="edit" data="1" />
</o:shapelayout></xml><![endif]--></head><body bgcolor=white lang=SV link=blue vlink=purple><div class=WordSection1><p class=MsoNormal><span lang=EN-GB style='color:windowtext;mso-fareast-language:EN-US'>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.<o:p></o:p></span></p><p class=MsoNormal><span lang=EN-GB style='color:windowtext;mso-fareast-language:EN-US'><o:p> </o:p></span></p><p class=MsoNormal><span lang=EN-GB style='color:windowtext;mso-fareast-language:EN-US'>John<o:p></o:p></span></p><p class=MsoNormal><span lang=EN-GB style='color:windowtext;mso-fareast-language:EN-US'><o:p> </o:p></span></p><div><div style='border:none;border-top:solid #E1E1E1 1.0pt;padding:3.0pt 0cm 0cm 0cm'><p class=MsoNormal><b><span style='color:windowtext'>Från:</span></b><span style='color:windowtext'> erlang-questions-bounces@erlang.org [mailto:erlang-questions-bounces@erlang.org] <b>För </b>Clara Benac Earle<br><b>Skickat:</b> den 3 oktober 2017 16:09<br><b>Till:</b> Kostis Sagonas <kostis@cs.ntua.gr>; erlang-questions@erlang.org; Lars-Åke Fredlund <lfredlund@fi.upm.es><br><b>Ämne:</b> Re: [erlang-questions] McErlang<o:p></o:p></span></p></div></div><p class=MsoNormal><o:p> </o:p></p><div><p class=MsoNormal style='margin-bottom:12.0pt'>Dear Kostis,<o:p></o:p></p></div><blockquote style='margin-top:5.0pt;margin-bottom:5.0pt'><p class=MsoNormal>I would be interested in seeing a simple example program containing a _concurrency_ error that can be detected by McErlang but not by Concuerror. <o:p></o:p></p></blockquote><p class=MsoNormal><br>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. <br><br>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.<br><br>Best regards<br>Clara <br><br><a href="http://dblp2.uni-trier.de/pers/hd/a/Arts:Thomas">Thomas Arts</a>, <span class=this-person>Clara Benac Earle</span>, <a href="http://dblp2.uni-trier.de/pers/hd/d/Derrick:John">John Derrick</a>:<br><span class=title>Development of a verified Erlang program for resource locking.</span> <a href="http://dblp2.uni-trier.de/db/journals/sttt/sttt5.html#ArtsED04">STTT 5(2-3)</a>: 205-220 (2004)<br><br><a href="http://dblp2.uni-trier.de/pers/hd/f/Fredlund:Lars==Aring=ke">Lars-Åke Fredlund</a>, <span class=this-person>Clara Benac Earle</span>: <o:p></o:p></p><div><p class=MsoNormal><span class=title>Model checking erlang programs: the functional approach.</span> <a href="http://dblp2.uni-trier.de/db/conf/erlang/erlang2006.html#FredlundE06">Erlang Workshop 2006</a>: 11-19<o:p></o:p></p></div><p class=MsoNormal><o:p> </o:p></p></div></body></html>