Hi,
Does MTRAT support volatile as correct way of synchronization?
It looks like it does not:
% cat VolatileTest.java
public class VolatileTest {
public static volatile boolean volatile_var;
public static void main (String[] args) {
volatile_var = false;
(new Thread() { public void run() { volatile_var = true; }; }).start();
(new Thread() { public void run() { while (!volatile_var); }; }).start();
}
}
% javac VolatileTest.java && java VolatileTest && mtrat VolatileTest
Data Race 1 : 49 : VolatileTest : volatile_var
Thread "Thread-1" : Tid 11 : Rid 0 : WRITE
Lock Set : [ ]
Vector Clock : 2
VolatileTest$1 : run : 5
Thread "Thread-2" : Tid 12 : Rid 0 : READ
Lock Set : [ ]
Vector Clock : 2
VolatileTest$2 : run : 6
Thanks!
