JMM: Safe one-time publication

June 22, 2010 – 6 years, 10 months ago, by vladimir

Short Description

The Java Memory Model recognizes two kinds of synchronization links: based on locking and based on volatile reads/writes. The verification systems available today (as far as they deal with the JMM at all) are incomplete as they only consider locking-based synchronization. The benchmark is to verify a program that is safe due to the use of volatile-based synchronization links. An example of such a program is given below.

Code

The following example, called "safe one-time publication" is from this IBM article.

public class BackgroundFloobleLoader {
    public volatile Flooble theFlooble;

    public void initInBackground() {
        // do lots of stuff
        theFlooble = new Flooble();  // this is the only write to theFlooble
    }
}

public class SomeOtherClass {
    public void doWork() {
        while (true) { 
            // do some stuff...
            // use the Flooble, but only if it is ready
            if (floobleLoader.theFlooble != null) 
                doSomething(floobleLoader.theFlooble);
        }
    }
}

Specification

The above program is JMM-safe. If SomeOtherClass sees a non-null reference to floobleLoader.theFlooble, then it will also see the whole object completely constructed.

Long Description

Supplementary Materials

Submitted by

Vladimir Klebanov (vladimir@cost-ic07101.org)