Typestate and SSA

2010/07/19 · by · in Comp*, Ideas

Since Rust was announced, I looked into the underlying idea of Typestate[1]. The most striking aspect about this paper is its age. The authors consider an extension to ordinary type checking to also verify that the state of a variable is valid for the operation being performed. The most immediate benefit is that it helps to identify operations being performed on uninitialized variables. Of course, in today’s most popular OO languages, such checks are usually buried into the semantics of the language itself.

In reading the paper, one example made me immediately think of SSA:

Another mechanism which can be used to enhance program reliability is one based on static scope rules in block-structured languages of the Algol family. Static scope rules enable a compiler to detect references to variables which are made outside the lifetime of these variables. For example, in this program segment

declare
  A: integer;
begin
  A := 3;
  Print(2*A);
end;
Y := A

the final statement will be detected by the compiler as an illegal reference to variable A, thereby avoiding a potential reference to deallocated storage.

The insight follows from SSA’s separation of value from variable. Here we should immediately identify that the typestate of a variable is actually an attribute of its SSA value. So all the research that has gone into SSA should find immediate applicability here (esp. linear construction).

The idea of checking for a variables state as well as it’s type seems pretty valuable. For example, it would be nice if I could annotate function signatures that they expect initialized types to be passed in, so that I can receive a compiler error. It’s not really much more work for me to annotate than it is to assert( arg != null );. But I’d rather have the error occur much earlier, at compile-time rather than test/run-time.

The typestate idea also naturally fits with the OO-paradigm, when you think of each class being a state machine and methods providing transitions between states. Experimental languages with this feature already exist[2] and make the expression of object state much more explicit. A suitably extend type checker can handle the additional complexity, and typestate-aware SSA can handle any specialized optimizations that can be performed with the increased knowledge.

[1] Robert E Strom and Shaula Yemini. Typestate: A Programming Language Concept for Enhancing Software Reliability. IEEE Transactions on Software Engineering 12(1):157-171, 1986.

[2] Jonathan Aldrich, Joshua Sunshine, Darpan Saini, and Zachary Sparks. Typestate-Oriented Programming. In Proceedings of Onward!, 2009.