Interested in a verification tool that automatically answers such a
question? We have one available (called DefectFindere) at
http://www.cs.utah.edu/~yyang/research.html.
Our method is described in our recent paper "Rigorous Concurrency Analysis
of Multithreaded Programs", in which we provided a formal definition of
what a data-race means according to the new JMM proposal. We also take
essential language constructs (such as branch conditions and the
usage of local variables) into consideration to enable an automatic and rigorous analysis.
Our tool is a proof-of-concept prototype written in Prolog which exploits
the built-in constraint solver from Prolog. Using a SAT solver, more
advanced tool can be developed with any programming language.
Our prototype currently does not explicitly handle loops. We believe that
for the purpose of memory model specification alone, the way we define
conditional instructions is sufficient for loops. This is because the
task of a memory model specification can be regarded as simply answering
if a concrete execution (where loops are already resolved with a finite
number of iterations) is legal. I think that in order to support a fully
automatic analysis, loops should also be taken into account. For now, I
just simulate this example with the following code, which captures the
essential scenario that the reads of w in T2 only occurs when v is read
back as true.
T1 T2
w = true; lock m1;
lock m1; r1 = v;
v = true; unlock m1;
unlock m1; if(r1)
r2 = w;
With our tool, it answers that this code is race-free after an exhaustive
coverage.
Cheers!
- Jason
On Fri, 20 Feb 2004, Adam Welc wrote:
> Hello,
> I am trying to get a better understanding of what it means for a program
> to be correctly synchronized (as defined in the JSR-133). The JSR states
> that:
>
> "A data race occurs in an execution of a program if there are conflicting
> actions in that execution that are not ordered by synchronization (ie, by
> a happnes-before relationship). A program is correctly synchronized iff
> all sequentially consistent executions are free of data races"
>
> Is the following program correctly synchronized?
>
>
> public static boolean w = false;
> public static boolean v = false;
>
> T1 T2
> w=true; while(true) {
> synchronized(M) { synchronized(M) {
> v =true; if (v) break;
> } }
> }
> boolean tmp=w;
>
>
> In any legal execution of that program the following sequence of actions
> will occur: T1 writes to w, T1 releases M, T2 acquires M, T2 reads w. This
> is enforced by the fact that the read of w can only happen after T1 exits
> the loop, which in turn can only happen after T2 modifies v.
>
> For example (arrow describes a happens-before edge):
>
> T1 T2
> ACQ(M)
> READ(v) // v still false; cannot exit loop
> REL(M)
> WRITE(w)
> ACQ(M)
> WRITE(v)
> REL(M) ------->
> ACQ(M)
> READ(v) // exits the loop
> REL(M)
> READ(W)
>
>
> Acording to the definition above, there is a happens-before relationship
> (by transitivity) between the write to w and the read from w in any
> execution of the program. But is it correctly synchronized?
>
> Best regards
>
> Adam Welc
>
>
> --
> Adam Welc
> Computer Science Building, room 274
> West Lafayette, IN 47906
> Telephone number (work): (765) 4947836
>
> http://www.cs.purdue.edu/homes/welc
>
> -------------------------------
> JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
>
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:58 EDT