Verification Challenges

"Analyze This" I

The apprentice challenge was presented by Moore [1] as a challenge in verification of Java programs.

The challenge is to show that the value of the counter variable of the Container class in Figure 1 increases monotonically (under all possible schedules). 

class Container {
    public int counter;
}

class Job extends Thread {
    Container objref;

    public Job incr () {
        synchronized(objref) {
            objref.counter = objref.counter + 1;
    }
        return this;
    }

    public void setref(Container o) {
        objref = o;
    }

    public void run() {
        for (;;) {
            incr();
    }
    }
}

class Apprentice {
    public static void main(String[] args) {

        Container container = new Container();

        for (;;) {
            Job job = new Job();
            job.setref(container);
            job.start();
    }
    }
}
Figure 1: Source of Apprentice Challenge Example

Solution in Solving The Apprentice Challenge with 3VMC, E. Yahav   [bib][abstract][ps][html][pdf] (original challenge by J. Moore)