Java Memory Model (Fixes in J2SE 5.0)

[This is inspired from Erik Poll's talk in the 4th KeY symposium.]

Immutable Objects are of interest for software verification because they are easy to argument about in presence of concurrency. Verification of concurrent programs is much harder than sequential ones because threads can effect shared variables in subtle ways. However, if an object is immutable, we don't need to think that different threads will see inconsistent values.

An example of an immutable class is Integer: you can't modify the value of Integer once it has been created. Other examples where immutability makes sense are classes for representing URL's, Date, Property Files, etc.

Suppose you are writing an immutable class MyInteger as follows:

public class MyInteger {
   private final int i;
   public MyInteger (int value) {
      i = value;
   }
   public int getValue () {
      return i;
   }
}

This class is immutable because all the members are private (as well as final) and there is no setValue() method in the class. The client code can give the instantiating value but can't modify it later. Assume a client uses the class as follows:

x = new MyInteger (5);

If another thread tries to access the shared variable x, we would expect x.getValue() to give 5 (or throw a null pointer exception, but not 0 in any case). However, the Java Language Specification didn't ensure that! The default initialization value of an integer is 0 and it's later changed to 5! Following the old spec, it's possible that running on a particular JVM, a thread would get 0 and later 5 for x.getValue().

With JSR 133, which has been officially implemented in J2SE 1.5 aka 5.0, this has been fixed by giving formal mathematical semantics to Java Memory Model as well as doing some formal proof for some desirable properties.


This has very profound conclusions:

Firstly, software is complex. How can you explain to your customer that the code that worked perfectly in thousands of test runs failed right during the demo?

Secondly, it means that as a software developer, you should restrict yourself to only a single set of tools as it's impossible to be master of all. Moreover, you need to keep yourself abreast of the activity going on related to that tool. Read JSRs, participate in online discussions, etc.

Thirdly, and most importantly, it proves once again that one should have a formal Mathematical semantics of programming languages as well as some formal proofs of correctness - at least of something as significant as Java itself. Moreover, we need more and more peer review to write better software. This indirectly supports the Open Source Initiative.

This article at java.net is a must read if you can spare some time.