[erlang-questions] McErlang

Clara Benac Earle cbenac@REDACTED
Tue Oct 3 16:08:59 CEST 2017

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

Thomas Arts <http://dblp2.uni-trier.de/pers/hd/a/Arts:Thomas>, Clara 
Benac Earle, John Derrick 
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 

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

More information about the erlang-questions mailing list