[erlang-questions] McErlang

[Clara Benac Earle]

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/d4b4302c/attachment.htm>