Re: [Javapathfinder-user] BUG: Too rigorously POR on array operations (Test model included)

[Viet Y. N. <v.y...@al...>]

Peter Mehlitz schreef:

Thanks for your fast reply!

I have investigated this thoroughly this weekend, and the POR 
optimisation is allowed under certain conditions and assumptions.

The example I sent contains a race, thus it is incorrectly synchronised 
(as defined by the Java Memory Model). That is why arr[0] += 1; cannot 
be seen atomicly.

The POR optimisation is however allowed if you state/assume that JPF 
only verifies a program correctly iff it is correctly synchronised, and 
also state/assume that you only can synchronise statement blocks (thus 
not at the granularity of a JVM bytecode). This ensures sequentially 
consistent semantics of the statements, and thus also the atomicity 
statement arr[0] += 1;

Yet, such Java Memory Model issues are delicate to deal with. It is 
better to bet safe, and assume that an array operation is scheduling 
irrelevant if the array in question is thread-local. Otherwise, the 
array operation should be considered scheduling relevant.

With regards,

Viet Yen



> Thanks - you are right. I guess the comment in 
> ArrayInstruction.isNewPorBoundary(..) was just wishful thinking. If you 
> restore the commented out check, JPF finds the assertion. So it has to 
> go in again, but I want to give it some more thoughts about performance
> 
> -- Peter
> 
> P.S. nice to finally see a JPF counterpart for .NET
> 
> On Dec 3, 2007, at 1:34 AM, Viet Yen Nguyen wrote:
> 
>> Hi,
>>
>> While testing our own model checker 
>> (http://www.cs.utwente.nl/~ruys/mmc/), I discovered, what I believe, 
>> is a bug in yours. The attached model has assertion violations, but 
>> JPF does not find them.
>>
>> It is a POR bug in JPF, as JPF considers array operations as 
>> scheduling irrelevant on the assumption that an array operation is 
>> always preceded by a getfield/getstatic, which is scheduling relevant. 
>> This is not true.
>>
>> Below is a trace to the undetected assertion violation.
>>
>> Could you please verify this bug?
>>
>> With regards,
>>
>> Viet Yen
>>
>>
>>
>> Trace to assertion violation:
>>
>> t1: getfield arr     (gets reference to arr)
>> t2: getfield arr    (gets reference to arr)   
>> t1: iaload          (loads 0 from arr)
>> t1: iadd        (adds 1, result is 1 on t1's stack)       
>> t2: iaload        (loads 0 from arr)
>> t2: iadd        (adds 1, result is 1 on t2's stack)       
>> t1: iastore        (stores 1 to arr)
>> t2: iastore        (stores 1 to arr)
>> t0: check assertion
>> public class TestMArr implements Runnable {
>>
>>     public static int[] arr = new int[1];
>>            
>>     public static void main(String[] args) {
>>         arr[0] = 0;
>>
>>         Thread t1 = new Thread(new TestMArr());
>>         t1.start();
>>
>>         Thread t2 = new Thread(new TestMArr());
>>         t2.start();
>>            
>>         try {
>>             t1.join();
>>             t2.join();
>>         } catch (Exception e) {
>>         }
>>
>>         System.out.println(arr[0]);   
>>         assert(arr[0] == 2);
>>
>>     }
>>     
>>     public void run() {
>>         arr[0] += 1;
>>     }
>> }
>> -------------------------------------------------------------------------
>> SF.Net email is sponsored by: The Future of Linux Business White Paper
>> from Novell.  From the desktop to the data center, Linux is going
>> mainstream.  Let it simplify your IT future.
>> http://altfarm.mediaplex.com/ad/ck/8857-50307-18918-4_______________________________________________ 
>>
>> Javapathfinder-user mailing list
>> Jav...@li...
>> https://lists.sourceforge.net/lists/listinfo/javapathfinder-user
> 
> ---------------------------------------------------------------------
> Peter C. Mehlitz                    Robust Software Engineering Group
> PSGS/NASA Ames Research Center               Pet...@na...
> M/S 269-3                       http://ti.arc.nasa.gov/people/mehlitz
> Moffett Field, CA 94035                                (650) 604-1682
> 
> 
> 
>