The charter of SRC is to advance both the state of knowledge and the state of the art in computer systems. From our establishment in 1984 by Digital Equipment Corporation (now Compaq), we have performed basic and applied research to support the company's business objectives. Our interests span scaleable systems (including hardware, networks, distributed systems, and programming languages and technology), the Internet (including the web, and internet appliances), and human/computer interaction. Our strategy is to test the technical and practical value of our ideas by building hardware and software prototypes and using them as daily tools. Interesting systems are too complex to be evaluated solely in the abstract; extended use allows us to investigate their properties in depth. This experience is useful in the short term in refining our designs, and invaluable in the long term in advancing our knowledge. Most of the major advances in information systems have come through this strategy, including personal computing, distributed systems, and the Internet. We also perform complementary work of a more mathematical flavor. Some of it is in established fields of theoretical computer science, such as the analysis of algorithms, computational geometry, and logics of programming. Other work explores new ground motivated by problems that arise in our systems research. We have a strong commitment to communicating our results; exposing and testing our ideas in the research and development communities leads to improved understanding. Our research report series supplements publication in professional journals and conferences while our technical note series complements research reports and journal/conference publication by allowing timely dissemination of recent research findings. We seek users for our prototype systems among those with whom we have common interests, and we encourage collaboration with university researchers. David L. Detlefs, K. Rustan M. Leino, Greg Nelson, and James B. Saxe December 18, 1998 Author Affiliations David L. Detlefs is a staff engineer at Sun Microsystems Laboratories. He can be reached at david.detlefs@sun.com. This work was completed by him and the other authors before he left SRC in 1996. This work may not be copied or reproduced in whole or in part for any commercial purpose. Permission to copy in whole or in part without payment of fee is granted for nonprofit educational and research purposes provided that all such whole or partial copies include the following: a notice that such copying is by permission of the Systems Research Center of Compaq Computer Corporation in Palo Alto, California; an acknowledgment of the authors and individual contributors to the work; and all applicable portions of the copyright notice. Copying, reproducing, or republishing for any other purpose shall require a license with payment of fee to the Systems Research Center. All rights reserved. The paper describes a mechanical checker for software that catches many common programming errors, in particular array index bounds errors, nil dereference errors, and synchronization errors in multi-threaded programs. The checking is performed at compile-time. The checker uses an automatic theorem-prover to reason about the semantics of conditional statements, loops, procedure and method calls, and exceptions. The checker has been implemented for Modula-3. It has been applied to thousands of lines of code, including mature systems code as well as fresh untested code, and it has found a number of errors. The authors of this paper were still children when the leading lights of computing declared that the world faced a "software crisis". While hardware improved every year, software was mired in complexity, and programming was expensive, error-prone, and grueling. But these gloomy observations didn't stop the software industry, which proceeded to grow its revenues and profits dramatically, and which has sustained that growth with continuous innovation. Was the software crisis a false alarm? Not really. Although profitable, writing software is still expensive, error-prone, and grueling. Innovation in the software industry has mostly been confined to finding new things to do with software, and has not found many new ways to produce software. It is still common to see software disasters in which millions of dollars are spent writing a program that is abandoned before release, because the implementors simply can't get it to work. The tragic failure to establish software as a reliable engineering discipline is painfully clear from studies such as Leveson and Turner's Investigation of the Therac-25 accidents [31] . Although revenues and profits have grown, figures from economic consulting firm DRI/McGraw-Hill indicate that during a recent period of generally rising productivity, productivity in the software industry has actually fallen [10] . These computations may not be entirely accurate-since it is difficult to correct for inflationbut it seems safe to say that software productivity has not kept pace with productivity in other areas of the computing industry such as hardware. In fact, we would claim that the growth of the software industry has defied the stagnation of programming technology only because of the tailwind created by the million-fold improvement in price/performance of CPUs over the last thirty years. As the information revolution moves out of its infancy, and we in the engineering community assume the responsibility of delivering on its vast promises, from robots to knowbots, it is insufficiently considered that our progress would be enormously accelerated if programming technology advanced on anything like the same curve as microprocessors. Many silver bullets have been heralded as the solution to the software crisis. If you have a software problem, Structured Programming with PL/I is the answer! The Object-Oriented Revolution will bring mass production methods to software and make program fragments into inexpensive reusable reliable commodities! Program verification will eliminate all errors! Programming in natural language will eliminate the need for arcane languages; end users will express their requirements directly to the computer, and programming as a profession will wither away! None of the dreams behind these slogans has been fulfilled. We believe that programming and its difficulties are here to stay. race conditions in multi-threaded programs. The tool is useful because the cost of an error is greatly reduced if it is detected early in the development process. The tool is intended to be like a type-checker or like the C tool lint [23] : its warnings are intended to be interpreted by the author of the program being checked. The checker is implemented using the technology of program verification. The program is annotated with specifications; the annotated program is presented to a "verification condition generator", which produces logical formulas that are provable if and only if the program is free of the particular class of errors under consideration, and these formulas are presented to an automatic theorem-prover. This sounds like program verification, but it is not: firstly because we don't try to prove that a program does what it is supposed to do, only to check for certain specific types of errors; secondly because we are interested in failed proofs only, not in successful ones. A crucial point is that failed proofs are more useful than successful ones, since they warn the programmer of possible errors. In addition to being more useful, ESC is more feasible than full-scale program verification. For example, an unsound full-scale program verifier is an oxymoron, but the amount of unsoundness to tolerate in a static checker is a matter of engineering judgment: nobody expects a type-checker or a lint tool to find all errors; its utility is determined by the number of errors it finds weighed against the cost of running the tool. Similarly, since we are not promising that ESC will find all errors, we are free to declare that some kinds of errors are out of the tool's range. This idea of extended static checking is not new. The first Ph.D. thesis that we know of that addressed the idea was by Dick Sites a quarter of a century ago [44] , and the problem has held its own as a Ph.D. thesis topic ever since. But the research prototype checkers that have been implemented over the decades have made too many simplifying assumptions. They may not handle dynamically allocated data or object-oriented programming; they may not handle concurrency; they may require the source for the entire program in order to check any part of it; they may require the user to guide the theorem-prover or to provide complicated loop invariants. Such simplifying assumptions are a way of separating concerns, which can help to focus on particular aspects of the problem, thus gaining depth of insight. Indeed, our work builds on the deep insights produced by many earlier researchers, but our ESC project has followed a complementary mode of research, in which every 2 effort is made to produce and test a realistic artifact. This complementary mode of research can often reveal surprises. Most previous checking tools were tested only on small programs written by the tool implementors themselves. In contrast, our plan was to run our checker on significant pieces of the Modula-3 runtime system. By tackling realistic programs written by others (or in some cases, by ESC project members before the ESC project was launched), we hoped to learn the answers to the following questions: • Could we generate verification conditions for such "systems programs"? • Would we be able to turn failed verifications into specific error messages? • How much of a burden would it be to write the necessary annotations? • To what extent could we automate the theorem-proving task? In summary, we were determined to stress-test an idea that had long been in gestation. Our checker handles multi-threaded multi-module object-oriented programs. Our checker works on Modula-3 programs [40] , but the techniques would work for any language in which address arithmetic is restricted, including Java, Ada, Oberon, and FORTRAN. Indeed, as this paper goes to press, a follow-on project has replicated the technology in a tool for Java. Our checker performs modular checking: you can use it to check selected modules of a program without checking the entire program. Since modern programming is inconceivable without libraries, we consider modular checking to be essential. The checker also allows you to check for selected classes of errors; for example, it is often useful to check for deadlocks and race conditions without checking for array index bounds errors. When the checker produces spurious warnings, there are a variety of ways to suppress them, that is, to get the checker to ignore the spurious warnings and continue to report real errors. A Although our checker is a research prototype, with plenty of rough edges, we feel that it demonstrates the promise of the technology more clearly than previous checkers: ESC catches errors that no type-checker could possibly catch, yet it feels to the programmer more like a type-checker than a program verifier. The specifications required are statements of straightforward facts like inequalities, the error messages are specific and accurate with respect to source position and error type, and the theorem-proving is carried out behind the scenes automatically. Our main goal for this paper is to convey to the reader what it feels like to use a checker that operates in this intermediate level between type-checking and verification. Therefore, the paper consists largely of two examples. After the examples, we describe at a rather general level some of the novel aspects of our checker, but we have relegated many details to other papers. In this section, we lay the groundwork for the examples that form the heart of the paper by briefly introducing ESC's specification language. The design of the specification language reflects the structure of well-designed programs. One pillar of program structure is procedural abstraction, in which a compound operation is named and parameterized and used by the rest of the program as though it were an elementary operation. Procedural abstraction makes static analysis difficult, so difficult that many static analysis methods described in the literature apply only to programs without procedures, and many practical compilers perform no inter-procedural analysis at all, even if they perform extensive intra-procedural analysis. The reason for this is that the authors of compilers and other tools have not wanted to rely on specifications, but inter-procedural analysis fundamentally requires dealing with specifications, whether supplied by the programmer or inferred by the tool. To perform inter-procedural analysis, ESC relies on programmer-supplied specifications of the form illustrated in Figure 0 . Pre-and postconditions are formulas in a first-order theory that includes the Modula-3 built-in operators. A procedure specification is a contract between the implementer and the client: the client contracts to call the procedure in a state where the precondition is true, and the implementer contracts (a) to modify no variable except those in the MODI-FIES list, and (b) to return only in a state satisfying the postcondition. Thus when checking the body of the procedure, ESC assumes that the precondition is true initially, and checks that when the procedure returns the postcondition is true and only those variables in the MODIFIES clause have been modified. Conversely, when checking a client, ESC checks that the precondition is true at the point of call, and assumes that the call respects both the postcondition and the MODIFIES clause. For example, here are a Modula-3 declaration and ESC specification of a simple random number generator: MODIFIES seed REQUIRES 0 < n AND seed # 0 ENSURES 0 <= RES AND RES < n AND seed' # 0 *> The example also illustrates several other points. First, for a variable listed in the MODIFIES clause (such as seed), occurrences in the postcondition can be unprimed or primed (seed'). A primed occurrence denotes the value of the variable in the post-state, while an unprimed occurrence denotes the value of the variable in the pre-state. Second, the reserved name RES is used to denote the result of the procedure, if any. Third, Modula-3 pragma brackets, <* *>, surround the ESC annotations to distinguish them from ordinary Modula-3. Fourth, x # y is Modula-3 syntax to assert that the values of x and y are different. Another pillar of program structure is data abstraction, in which a collection of program variables (or concrete variables) are considered conceptually to represent a single abstract variable. The abstract variable is used by clients for reasoning about the semantic effect of operations on the abstraction, and the concrete variables are used by the implementation to operate efficiently on the state. For example, the abstract value of a complex number z could be represented concretely in terms of two floating point Cartesian coordinates z.x and z.y; alternatively the same abstraction might be represented in terms of the polar coordinates z.r and z.theta. Generally, the module structure of a program is arranged so that the concrete representation of an abstraction is invisible (that is, out of scope) within the modules that use the abstraction (its clients) [42] . Figure 1 shows the ESC syntax for declaring an abstract variable and specifying its representation (also known as its abstraction function). For example, 5 <* SPEC VAR a: INTEGER *> VAR c: INTEGER; <* SPEC REP a = c*c *> declares an abstract integer variable a, a concrete integer variable c, and specifies that the square of c represents a. We haven't described the whole specification language, but we have described enough to give the first example. Both of the two extended examples in this paper use Modula-3's standard I/O library, which is designed around the key abstraction of a monitored object-oriented buffered stream. In particular, a reader is an input stream and a writer is an output stream. Each stream object contains a buffer and methods for managing the buffer. Different stream subclasses override the methods in different ways, so that, for example, a file reader refills the buffer from the disk and a network reader refills the buffer from the network. Class-independent code can be common to all subclasses; for example, Wr.PutInt writes the ASCII representation of an integer into a writer's buffer. The Modula-3 design is described in Chapter 6 of Nelson's Modula-3 book [40] , the original design is described by Stoy and Strachey [46] . We describe various aspects of the relevant interfaces as we need them for our examples. For each type of stream, the Modula-3 I/O library provides two interfaces, a basic interface for simple clients, and an advanced interface that offers additional functionality (in particular, access to the buffer structure) at the price of additional complexity. The basic writer interface. Our first example uses only the basic writer interface Wr, which is presented in Figure 2 . Here is a translation of Figure 2 from Modula-3 into English. The writer class is given the global name Wr.T, where Wr is the name of the interface and T is by convention the principal type declared in the interface. The class is declared as an opaque object type, publicly known only to be a subtype of the built-in class ROOT. (In Modula-3, classes correspond to object types.) The actual declaration of the representation type is hidden in the advanced interface, and is invisible to clients of the basic interface. The procedures PutChar, PutText, and Close have the given signatures and specifications (TEXT is Modula-3's predeclared string type). .) A U-valued field f declared in a class T corresponds semantically to a map from T to U. Thus the declarations of valid and state can be thought of as BOOLEAN-valued and ANY-valued fields of writers. Although Modula-3 uses the syntax x.f to denote the f field of an object x, the annotation language uses the syntax f[x] when f is abstract. The specifications for the writer interface fall into a common pattern that we call the state/validity paradigm. In this paradigm, there are two abstract variables, valid and state. The idea is that valid[wr] represents the condition that wr is a properly-initialized valid writer, and state[wr] represents all other state of wr (for example, its contents and position). If we were doing full-scale program verification, there would be pages of specifications about state; but since we are doing extended static checking only, there is almost nothing to say about state, except to specify that some procedures may modify it. (Not even the type of state is relevant, so we use the special ESC type ANY.) In the state/validity paradigm, specifications become very stylized. A typical procedure or method operating on a writer wr (like PutChar) has the specification Because valid does not appear in the MODIFIES list, this specification implies the preservation of validity. Often a few procedures will have some additional annotations-for example, PutText requires that its text argument be non-NIL-but for simple interfaces the stylized specifications of the state/validity paradigm are the lion's share of what has to be written for an ESC verification. The text writer interface. Figure 3 illustrates the text writer interface, a particular writer subclass that occurs in our example. A text writer is a writer that doesn't do any output; it just stores everything that has been written in an internal buffer and provides a procedure GetText that returns the contents of the buffer as a TEXT. Because TextWr.T is a subclass of Wr.T, the specification variables valid and state apply to text writers, and are used in the specification of the text writer interface. The method init initializes a text writer (establishes valid'[twt]) and returns it (establishes RES=twt). The specification is entirely typical for initialization methods in the state/validity paradigm. Similarly, the specification of GetText is typical of the state/validity paradigm, with one additional postcondition conjunct RES # NIL. Example. Our first example program is the kind of elementary programming exercise that might be assigned to students first learning to program with output streams, and we have seeded our program with elementary errors. The problem is to program a procedure that takes an array of texts as an argument and returns a single text containing the concatenation of all the texts in the array. This could be done rather straightforwardly by repeatedly calling the Modula-3 binary concatenation operation Text.Cat, but doing so leads to a performance trap, since with most implementations of text concatenation, the total cost in time of this simple approach can be proportional to the square of the length of the final result. A good way to avoid this quadratic cost is to use a text writer, which leads us to the procedure ArrayCat shown in Figure 4 . The procedure allocates a text writer, writes the elements of the array to the writer in order, and finally retrieves and returns a text containing everything that was written. (This approach avoids the quadratic cost if text writers are well-implemented.) Running ESC on the ArrayCat procedure of Figure 4 produces a warning about an array index bounds error: array index bounds error, line 4: (The exact format of an ESC error message is identical to that of a compiler error message; in this paper, we use italics and underlining to convey the same information.) The error message also includes a so-called "error context" which is a long list of atomic formulas that characterize the situation in which the error can occur. Because it is long, we won't show the error context here, but we remark that a study of the context reveals that it implies the formula i=NUMBER(a), which is in fact the condition in which the array bounds error can occur: in Modula-3, open arrays are indexed from 0, but the FOR loop was written as though they were indexed from 1. Correcting the error in one natural way produces the following A study of the error context reveals that it implies the formula NOT valid [twr]. That is, ESC has detected and warned about the failure to initialize twr (the program allocated the text writer, but failed to initialize it). To correct this error, we add a call to the init method, which requires inserting the seven characters ".init()": This correction eliminates both of the previous warnings, but ESC gives one more warning: precondition failed, line 4: A study of the error context shows that the TEXT argument to PutText is equal to NIL, which is forbidden by the precondition of PutText but not ensured by ArrayCat, which blindly passes a[i], whether or not it is NIL. This error forces a rethinking of the design for ArrayCat: what should we do about NIL entries in the TEXT array? Two designs come immediately to mind: to ignore NILs or to forbid NILs. Either design is easy to get through ESC. In the design where NILs are ignored, the procedure is recoded as follows: and of course ESC, which understands IF statements, is perfectly happy with this version. In the design where NILs are forbidden, the specification for ArrayCat is strengthened with a quantified precondition: ESC is perfectly happy with this design, too: the stronger precondition suppresses the error message. Furthermore, ESC will enforce the stronger precondition wherever ArrayCat is called. We would like to make several comments about this example. First, although careful specifications were required for the writer and text writer interfaces, the beginning programmer was able to make use of ESC without writing any specifications for his program at all. No preconditions or loop invariants were required in ArrayCat. We think that this is as it should be: anybody qualified to design the interfaces of a stream library understands preconditions and postconditions and abstractions at some level, and will find an explicit notation for their design decisions to be a useful tool rather than a burden. On the other hand, many simple errors in programs can and should be identified by reading the unannotated erroneous program; to require a loop invariant in order to check ArrayCat seems pedagogical and heavy-handed. Second, the reader should be aware that, although we have concentrated in this example on the checking of a client of the I/O system, we have in fact also used ESC to check the implementation of text writers. In the implementation, a representation declaration is made to give the concrete meaning of valid [twr] in terms of the concrete fields of twr. And this representation is used by ESC when checking the body of procedures like PutText and GetText, that require validity as a precondition and whose implementations depend on the concrete meaning of validity. A third remark that this example allows us to make is that it is up to the user to choose a point on the continuum between full functional-correctness verification 12 and minimal extended static checking. For example, it is in fact true that initializing a text writer leaves its contents empty, but our specifications did not reflect this truth. If we wanted to, we could reflect this by strengthening the postcondition of init along the following lines: . Also, the notation "" is not actually correct for the empty character sequence.) It would be easy to concoct an artificial example in which this stronger specification would be essential for some ESC verification. For example, the absence of array bounds errors in some client might depend on the fact that a newly initialized text writer is empty. But this is a slippery slope. If init's effect on the state is specified fully, why not PutChar's as well? Without discipline, you can quickly slide into the black hole of full correctness verification. Luckily, our experience has been that many ESC verifications can be successfully completed with almost no specifications at all about the contents and meanings of abstract types, other than the specification of validity. You can go a long way just relying on the state/validity paradigm: that is, the specifications for each procedure record accurately how the procedure affects and requires validity, but all other side effects are swept under the ample rug of MODIFIES state [wr]. We believe this is a key reason why ESC verifications can be more cost effective than full correctness verifications. In this section, we will describe the use of ESC on a more sophisticated program, WhiteSpace.Skip. The example is also a short client program of the Modula-3 I/O system, but differs in several ways from the example in the previous section. A rather minor difference is that this program is a client of input streams rather than output streams. A more important difference is that in this example, we will pay attention to the synchronization protocol that is designed into both readers and writers. In the previous example, we omitted synchronization in order to simplify the exposition. Another important difference is that in this section we will see a program that uses the advanced interface to deal with the buffer structure of the stream, instead of exclusively using the procedures in the basic interface. PROTECT v BY mu shared variable v is not to be accessed without holding the lock mu PROTECT f BY SELF for every object t, shared field t.f is not to be accessed without holding the lock t LL set of locks held by the current thread sup supremum (maximum) in the programmerdeclared locking order Figure 5 : Locking-level syntax. The second form of PROTECT can be used only when f is a field declared in a subclass of MUTEX. How ESC checks for synchronization errors. Our experience has been that many synchronization errors are failures to acquire locks (causing race conditions) or acquiring locks out of order (causing deadlocks). Therefore, we have designed the ESC annotation language to catch these simple errors; Figure 5 shows the syntax. The programmer declares which locks protect which shared variables and which locks can or must be held on entry to various procedures. The programmer also declares a partial order in which threads are allowed to acquire locks. ESC checks that shared variables are never accessed without holding the lock that protects them, and also checks that threads acquire locks in strictly increasing order (Modula-3 features non-reentrant locks). This doesn't prove correctness-more expensive techniques like monitor invariants would be required for that-but it does catch many common errors. The locking order on mutexes is denoted by "<", and the programmer specifies it using a general facility for adding axioms to an ESC verification: SPEC AXIOM. For example, the Modula-3 window system is based on an object called a VBT. VBTs are arranged in trees, and can be locked only from a leaf of the tree toward the root, not vice versa. This rule is declared in the VBT interface as follows: Axioms about the locking order arise only in subtle situations. In particular, the example we are about to present acquires only one reader lock at a time, so we don't need to declare axioms about the locking order. The basic reader interface. Figure 6 shows the basic Modula-3 interface Rd, including its ESC specifications. The only new features of Figure 6 relate to concurrency. The synchronization protocol designed into readers is highly stylized, we call it the monitored-object paradigm: An object is treated like a monitor in that mutual exclusion is provided for threads operating on the object via procedure 15 calls and method calls. The mutual exclusion is achieved by locking the object itself, whose type is a subtype of MUTEX, Modula-3's predeclared mutual exclusion semaphore type. Acquiring the lock is equivalent to entering the monitor. The text of the interface in Figure 6 reflects the monitored-object paradigm in two ways. First, Rd.T is declared to be an opaque subtype not of ROOT but of MU-TEX. Second, the monitor entry procedures have the extra precondition sup(LL) < rd, which reflects the requirement that they be called from a state in which it is legal to acquire the lock rd. The advanced reader interface. The basic Rd interface is the one used by most simple clients, but it is insufficient for more sophisticated clients. For example, since it hides the buffer and the method for refilling the buffer, it is insufficient for clients that implement new classes of readers. Figure 7 shows the RdrRep interface, which provides the specifications needed for more sophisticated clients. With the RdrRep interface we get beyond the boiler-plate ESC specification paradigms, and start to put the specification language through its paces. The interface begins by revealing the representation of the type Rd.T, which is opaque in the basic interface. The representation is an object type containing a buff field, which is a reference to an array of characters. The Modula-3 keyword BRANDED substitutes name equivalence for Modula-3's default structural equivalence for types. In addition to the buff field, Rd.T also contains several integer and boolean fields. The integer fields determine the active portion of the buffer, according to a convention illustrated in Figure 8 . The boolean fields are irrelevant for this example. The full interface contains several methods, but we show only the seek method, since the others are irrelevant for our example. The SPEC PROTECT annotation specifies that the fields of a reader are protected by the reader itself; that is, a thread is not allowed to read or write any of the reader's fields unless it has acquired the reader lock. This annotation is typical of the monitored-object paradigm. Next we come to the specification of seek. This method is responsible for performing the class-specific computation involved in repositioning the buffer: the call rd.seek(n) repositions the buffer so that byte number n of the source of the reader is present in the buffer. In particular, rd.seek(rd.hi) will advance to the next buffer of data (since rd.hi is the index of the first byte that is beyond the current buffer of data). The method returns SeekResult.Ready if the repositioning is successful; if n is beyond the end of the reader, it returns SeekResult.Eof. (If dontBlock is set and the seek method can't do its job without risking blocking, it is allowed to return SeekResult.WouldBlock.
An interesting example of such a tool is ESC/Java REF .
Extended static checking
PROCOMET
Computer Science