Re: [Javapathfinder-user] Volatile variables & Double Checked Locking

[Peter C. M. <Pet...@na...>]

> Java PathFinder can do any kind of check over volatile variables?

JPF doesn't specifically handle volatile - all fields are treated as  
potentially shared, and there is no compilation (JPF is a strict  
interpreter), hence no added caching. The only effect you will see in  
your program is that javac (or whatever bytecode compiler you use)  
will reload the field instead of keeping it on the operand stack or  
locals. There is no difference between one- or two-slot values (long/ 
double), since we treat all writes atomically. If there is a  
potential race, the RaceDetectors will get it anyways.

>   Is there a way to check a Double Checked locking pattern without  
> excluding the fields from lock protection?

not yet. I could see several ways to do that, all based on

(1) the preserved volatile modifier of the field

(2) the associated bytecode pattern, which looks like

   getfield
   if..
   monitorenter
   ..
   getfield
   if..
   ..
   putfield
   monitorexit

This could be done by either providing your own  
+vm.por.fieldlockinfo.class, or - probably more simple - by using a  
BytecodeFactory that overrides the GETFIELD/PUTFIELD insns.

I can't look into this right now, but if you want to work on it I  
would be interested in the result.

-- Peter