[concurrency-interest] Concurrent algorithms verification

Martin Buchholz martinrb at google.com
Mon Nov 6 07:53:31 EST 2017


Nikita,
Are you aware of the work in "violat" project?
https://github.com/michael-emmi/violat/blob/master/README.md
https://arxiv.org/pdf/1706.09305.pdf
This has prompted work here on improving linearizability in
ConcurrentLinkedDeque.

On Fri, Nov 3, 2017 at 2:47 PM, Nikita Koval via Concurrency-interest <
concurrency-interest at cs.oswego.edu> wrote:

> Hi All,
>
> I think it would be interesting for you. I have developed a special tool,
> *Lin-Check,* for testing concurrent data structures for correctness. The
> approach is based on linearization definition and the tool tries to find
> non-linearizable execution with specified operations, using a specially
> crafted test to produce lots of different executions. The execution is
> represented as a list of actors for every test thread, where the actor is
> the operation (e.g. *put(key, value)* and *get(key)* in *java.util.Map*)
> with already counted parameters.
>
> For more details see the project on GitHub: https://github.com/Devexperts/
> lin-check.
> I will be also glad to provide you all necessary information in case you
> have any questions.
> Best regards,
> Nikita Koval
>
> _______________________________________________
> Concurrency-interest mailing list
> Concurrency-interest at cs.oswego.edu
> http://cs.oswego.edu/mailman/listinfo/concurrency-interest
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://cs.oswego.edu/pipermail/concurrency-interest/attachments/20171106/29118145/attachment.html>


More information about the Concurrency-interest mailing list