Concurrent algorithms verification

classic Classic list List threaded Threaded
5 messages Options
Reply | Threaded
Open this post in threaded view
|

Concurrent algorithms verification

JSR166 Concurrency mailing list
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
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest
Reply | Threaded
Open this post in threaded view
|

Re: Concurrent algorithms verification

JSR166 Concurrency mailing list
Hi Nikita,
Thanks for your sharing.

2017-11-04 5:47 GMT+08:00 Nikita Koval via Concurrency-interest
<[hidden email]>:
> 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

AFAIK, being a correct concurrent data structure does not imply
linearization consistency.

Yubin
_______________________________________________
Concurrency-interest mailing list
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest
Reply | Threaded
Open this post in threaded view
|

Re: Concurrent algorithms verification

JSR166 Concurrency mailing list
It is a very good remark, thanks. There are some modifications of the linearizability (such as k-linearizability, local linearizability, etc) in order to describe relaxed contracts. And we are going to support some of them in Lin-Check tool a bit later.

Best regards, 
Nikita Koval

05:12, November 4, 2017, Yubin Ruan <[hidden email]>:

Hi Nikita,
Thanks for your sharing.

2017-11-04 5:47 GMT+08:00 Nikita Koval via Concurrency-interest
<[hidden email]>:

 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


AFAIK, being a correct concurrent data structure does not imply
linearization consistency.

Yubin


_______________________________________________
Concurrency-interest mailing list
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest
Reply | Threaded
Open this post in threaded view
|

Re: Concurrent algorithms verification

JSR166 Concurrency mailing list
In reply to this post by JSR166 Concurrency mailing list
Nikita,
Are you aware of the work in "violat" project?
This has prompted work here on improving linearizability in ConcurrentLinkedDeque.

On Fri, Nov 3, 2017 at 2:47 PM, Nikita Koval via Concurrency-interest <[hidden email]> 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
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest



_______________________________________________
Concurrency-interest mailing list
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest
Reply | Threaded
Open this post in threaded view
|

Re: Concurrent algorithms verification

JSR166 Concurrency mailing list
Thanks for the links, Martin. Yes, I have heard about this project. However, I started developing Lin-Check tool before I found out "violat" project and these projects have different solutions. While "violat" uses JCStress to run tests and checks for linearizability only, under Lin-Check tool we are working on different more complex execution strategies and more complex (relaxed) correctness contracts verification. In addition, Lin-Check is more convenient for unit testing.
 
BR,
Nikita
 
 
06.11.2017, 15:53, "Martin Buchholz" <[hidden email]>:
Nikita,
Are you aware of the work in "violat" project?
This has prompted work here on improving linearizability in ConcurrentLinkedDeque.
 
On Fri, Nov 3, 2017 at 2:47 PM, Nikita Koval via Concurrency-interest <[hidden email]> 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
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest
 

_______________________________________________
Concurrency-interest mailing list
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest