Clara Benac Earle
Tue Oct 3 16:08:59 CEST 2017
> I would be interested in seeing a simple example program containing a
> _concurrency_ error that can be detected by McErlang but not by
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
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
Model checking erlang programs: the functional approach. Erlang Workshop
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the erlang-questions