[concurrency-interest] On A Formal Definition of 'Data-Race'

oleksandr otenko oleksandr.otenko at oracle.com
Tue Apr 16 10:02:09 EDT 2013

Java PathFinder and SMV implement NP-complete validation of concurrent 
code. But like I mentioned before, the state space explodes, so it is 
not useful with more than N threads.

(Someone posted a blog jeering at "how many contenders do you need to 
prove the code is not thread-safe?" As I found out, it depends! If I 
have just 4 contenders, some conditions never happen - because there'd 
be not more than 4 distinct states at any given time)

The problem with SMV also is in mapping the specification into 
implementation. (even if you have a correct SMV model, what will it look 
like in Java?)

So NP-complete validation exists - computer science hasn't failed you 
there - but it is not what you want.


On 16/04/2013 13:01, thurstonn wrote:
> Yes, concurrency is hard.
> So is database concurrency control. But there is a formal methodology for
> analyzing it (even if it is NP-complete)
> It seems to me that the lack of something similar for analyzing
> multi-threaded code on SMP systems is a real failure of computer science.  I
> mean we have a MM.
> Even if you accept the "leave it to the experts" prescription, the point is
> that "experts" make mistakes as well (there's a great academic paper (that I
> can't find the link to at the moment) that describes some putatively
> thread-safe program that ran continuously for 2+ years before it failed)
> The "how do you know this program is thread-safe"?
> Pause.
> "I thought *really* hard about it"
> I can't be the only one who finds that deeply unsatisfying

More information about the Concurrency-interest mailing list