Class Initialization

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

Short Description

Develop a specification and verification technique for lazy class initialization.

Code

Specification

Long Description

Modern programs often rely on large library components. Reducing the time to load and initialize these libraries is important to improve the responsiveness of the programs. A solution employed by both the Java Virtual Machine and the .NET Common Language Runtime is to support lazy class initialization. This means that a class is not loaded and initialized until its first use. While this feature can improve responsiveness, it complicates reasoning about programs.
Consider the following program snippet:

   int x = A.a;
   int y = B.b;
   int z = A.a;
   assert x == z;

where A.a and B.b are static fields in two classes, A and B. If one expects the reading of static fields to have no side effects, then one would conclude that the assertion will hold. However, given the following class declarations:

   class A {
      public static int a;
      static { a = 0; }
   }
   class B {
      public static int b;
      static { b = 0; A.a = 5; }
   }

it is possible, in the presence of lazy class initialization, to arrive at the assertion with local variables x and z having the values 0 and 5, respectively. This would happen if class B has not yet been loaded at the time B.b is read; the reading of B.b will then first invoke class B’s static initializer, which sets A.a to 5^4.
We certainly need to allow static initializers to mutate state, but it would be horribly non-modular to have to reason about the possibility of such mutations happening any time something from another class is referenced. What we would like is a specification and verification technique that confines the side effects of class initializers in such a way that one can ignore the specific time at which they actually occur.

Supplementary Materials

The paper by Gary T. Leavens and K. Rustan M. Leino and Peter Müller from which this challenge is taken contains some additional information including references to relevant papers related to this challenge. Some more specification and verification challenges which are also included on this site can also be found there.

Submitted by

Timo Eifler verifythis@cost-ic0701.org