[concurrency-interest] On A Formal Definition of 'Data-Race'
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"?
> "I thought *really* hard about it"
> I can't be the only one who finds that deeply unsatisfying
More information about the Concurrency-interest