[PRL] Spec#: type system is interesting; not so much with the soundness

[Richard Cobbe]

I've been investigating various aspects of Spec#'s type system as related
works for my dissertation and had an interesting experience with it last
week.  It's been suggested to me that my experiences might be interesting
to the lab as a whole, especially in light of Aaron's recent presentation
on Spec#.

I was specifically investigating the type system ideas presented in an
OOPSLA 2007 paper by Fähndrich & Xia, titled "Establishing Object
Invariants with Direct Types."  I won't go into much detail about their
proposed type system here; they're primarily concerned with adding enough
flexibility (back) to the Spec# type system to allow creation of (certain
kinds of) cyclical data structures that involve fields of non-null type.
The problem, essentially, is that the type system's non-null guarantees
don't hold until all of the edges in the cycle have been established, but
the type system doesn't allow them to establish the edges until the field
values aren't null.  So they need some way to indicate that certain
references have "delayed" type.  Delayed types are exempt from certain
non-null guarantees, but the type system places enough additional
restrictions (see the paper for details) on these types so that the program
can't observe these non-null types.

Well, it's not *supposed* to be able to, anyway.  The following example
demonstrates rather clearly that it can, with results that can only be
called explosive.

    using System;

    public class ExnContainer {
        public ExnItem item;

        public ExnContainer() {
            // constructors are "delayed" by default, so "this" has delayed
            // type.
            base();
            try {
                foo();
            } catch (TestException) {
                Console.WriteLine("caught");
            }
        }

        [Microsoft.Contracts.Delayed]
        public void foo() {
            // method is delayed, so "this" has delayed type.
            new ExnItem(this, "x");
        }

        static void Main() {
            ExnContainer e = new ExnContainer();
            ExnItem it = e.item;
            if (it != null) {
                // In body of this if statement, "it" has type "ExnItem!".
                // Without the test, the compiler would warn on the following
                // line that the receiver might be null.
                string! msg = it.msg;
                Console.WriteLine("about to crash!");
                Console.WriteLine(msg.Length);      // crash here
            }
        }
    }

    public class ExnItem {
        public string! msg;

        public ExnItem([Microsoft.Contracts.Delayed] ExnContainer! c,
                       string! s) {
            base();
            c.item = this;                  // not allowed by model!
            throw(new TestException());
            msg = s;
        }
    }

    public class TestException : Exception {
        public TestException() {
            base();
        }
    }

This program compiles without warnings or errors (but see the comment in
the Main method).  Executing it results in the following actions:

  1) Main instantiates ExnContainer.
  2) ExnContainer's constr calls base() to init superclass.
  3) ExnContainer's constr sets up an exception handler.
  4) Within the context of this exn handler, call foo.
  5) The foo method creates a new ExnItem, supplying "this" as an argument.
  6) ExnItem's constr calls base to init the superclass.
  7) ExnItem's constr sets the ExnContainer's item field to the
     newly-created ExnItem object.
  8) ExnItem's constr throws an exception.  Note that we haven't yet
     initialized ExnItem's msg field.
  9) ExnContainer's constr catches the exception and prints "caught."
  10) Control returns to Main, which attempts to refer to
      e.item.msg.length, the length of the string.
  11) The program crashes with an uncaught NullReferenceException,
      presumably at the indicated line in Main.  The exception message
      doesn't indicate a line number, so I can't be sure of the precise
      source of the error, but the "about to crash!" message does appear on
      stdout.

For that extra little je ne sais quoi, the exception is accompanied by a
sequence of no fewer than *six* of those lovely dialogs that say, "We're
sorry, your program has encountered an error and needs to close.  We
apologize for the inconvenience.  Do you wish to inform Microsoft of this
problem?"

No, thanks, that's OK.

Now, to be fair, Fähndrich & Xia are aware of this problem and mention it
in the paper.  (I was in fact attempting to explore the consequences of
their warning when I wrote the example above.)

They suggest that prohibiting exception *handlers* within delayed
constructors and methods would prevent this problem.  However, their model
doesn't allow the program above: exception handling aside, the model's type
system would, I believe, reject the assignment on the indicated line in
ExnItem's constructors as ill-typed.  (Basically, the model allows for a
more precise notion of delayed---delayed until time t---and enforces
certain restrictions on assignments involving two different times.  See the
paper for details.)

As a result of the model's omission, though, they cannot provide a formal
proof that restricting exception handlers suffices to fix this problem and
restore soundness.

Caveat #2: I haven't actually seen a formal statement of the soundness
theorem for Spec#, so my use of the word "soundness" here should be
considered only informal.  Indeed, it'd be pretty easy to state a soundness
theorem for Spec# that holds even in the face of the example above.  Such a
theorem would have to allow for NullReferenceExceptions from non-null
types, though, which does rather seem to defeat the purpose.

In any case, it looks to me like their implementation has gotten ahead of
their theory, with unfortunate consequences.

Richard