Finalizers

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

Short Description

Develop a verification technique for finalizers.

A solution to this challenge is necessary to guarantee that verification is not unsound for programs containing finalizers.

Code

import java.io.*;

public class TempStorage {
   private /*@ nullable @*/ FileReader tempFile;
   private /*@ nullable @*/ FileWriter logFile;
  
   //@ private invariant tempFile != null && logFile != null;

   public TempStorage() throws IOException {
      tempFile = new FileReader("/tmp/dummy");
      logFile = new FileWriter("/tmp/log");
   }

   protected void finalize() throws Throwable {
      super.finalize();
      logFile.write("Bye bye");
      logFile.close();
      tempFile.close();
   }
}

The finalize method closes the files used by the receiver object.

Specification

Long Description

Finalizers are special methods that are invoked by the runtime system before an unreachable object is de-allocated. Their purpose is mainly to free system resources. For instance, the finalize method in the example above closes the files used by its receiver object.
Since the runtime environment of languages like Java and C# may invoke the garbage collector in any execution state, programs have no control over the execution of finalizers. This leads to two problems for verification.
First, a finalizer might be invoked in a state in which certain object invariants do not hold. In our example, the constructor of TempStorage throws an exception if opening the files fails. In this case, the object is never fully initialized and thus its invariant does not hold. However, the finalizer of TempStorage relies on the object invariant and, therefore, will abort with a null-pointer exception when a partly-initialized object is destroyed. A verification technique can prevent an application program from calling a method on a partly-initialized object, for instance, by making explicit which object invariant may be assumed to hold. However, finalizers are called by the runtime system and, therefore, cannot be controlled.
Second, like any other method, a finalizer potentially modifies the heap. Since finalizers might be called in any execution state, a verification technique has to deal with spontaneous heap changes, which is even worse than the heap changes caused by static initializers.

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

Comment

It should be noted that finalization involves very subtle JMM issues. Most uses of finalizers are apparently wrong. See the presentation by Hans Boehm Finalization, Threads, and the Java Technology-Based Memory Model.
(Vladimir Klebanov)