[concurrency-interest] Ensuring the correctness of concurrent code

Nathan Reynolds nathan.reynolds at oracle.com
Wed Sep 3 20:34:13 EDT 2014


I used a tool called Java Pathfinder (JPF), 
http://en.wikipedia.org/wiki/Java_Pathfinder.  It runs a Java program 
and will find all data races and deadlocks if given enough time.

It does this by simulating all thread interleavings.  By this I mean, 
when a bytecode executes, JPF saves the state and picks a thread to 
continue the execution.  Later JPF will backtrack to that state and pick 
a different thread.  It continues to execute and backtrack until all 
threads have executed from that given state.

This would be terribly slow except that a lot of bytecodes don't do 
anything that can be seen by multiple threads.  Hence, these bytecodes 
don't cause backtracking.

It is terribly slow if you run more than 2 threads or have a very 
complicated program.  The best thing to do is create a very small toy 
program which models what you want to test.  This cuts down on the 
shared state and hence the thread interleavings.

I haven't used it in a while.  When I last used it, it didn't support 
JMM.  So, you can't test volatile very well.  You also can't test 
whether instruction reordering is going to cause a problem.

-Nathan

On 9/3/2014 4:16 PM, Szabolcs Ferenczi wrote:
> Hi, I have used CSP before and I liked it. It is very powerful but it 
> needs a special thinking when you try to map the procedural language 
> notation such as Java into the CSP notation. It is better to generate 
> the mapping if possible. Even better to model first and generate the 
> code from the model. In the book Concurrency: State Models & Java 
> Programs the authors show a way how to do the mapping by hand. You 
> need to deal with the memory model at the lowest level though. The 
> advantage of the CSP notation is that you can model your program at 
> different abstraction levels and check that the refinement still holds 
> between the levels.
> --
> Szabolcs
>
>
> On 3 September 2014 22:49, Chris Vest <mr.chrisvest at gmail.com 
> <mailto:mr.chrisvest at gmail.com>> wrote:
>
>     Hi,
>
>     I occasionally have to write code that does shared mutable memory
>     concurrency, have high performance requirements, and needs a high
>     degree of confidence in the correctness of the implementation.
>
>     So far I have tackled this by thinking hard and working hard. I’ve
>     written hundreds of tests for tiny APIs, targeted and randomised
>     alike, I’ve drawn up diagrams summarising all the state
>     transitions, I’ve gone through the code to check every against
>     said diagram, I’ve written documentation to specify all observable
>     behaviours, and then written more tests for things I discovered
>     while writing said documentation, sleep on it, wake up and write
>     even more tests for new scenarios I’ve literally dreamt up. And so on…
>
>     This has worked well so far, though it takes a lot of effort and
>     discipline. However, as the problems I try to solve get harder,
>     and the optimisations I want to pull off gets more cunning, I feel
>     like I’m approaching the limits of this “technique.”
>
>     So, how to other people approach this? How is the correctness of
>     the j.u.c. implementations ensured, for instance?
>
>     I have begun studying TLA+ in the hope that the formal
>     specifications might be helpful, but I’m not sure if that’s the
>     right path. I haven’t studied proof techniques before. One worry I
>     have with TLA+ is how to accurately represent the given memory
>     model I’m working with, which has thus far been the JMM.
>
>     Cheers,
>     Chris
>
>
>     _______________________________________________
>     Concurrency-interest mailing list
>     Concurrency-interest at cs.oswego.edu
>     <mailto:Concurrency-interest at cs.oswego.edu>
>     http://cs.oswego.edu/mailman/listinfo/concurrency-interest
>
>
>
>
> _______________________________________________
> 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/20140903/784e6952/attachment.html>


More information about the Concurrency-interest mailing list