Smart Software

Reboot

It has been about a year so far since I have written anything substantive in this blog. Yet, over the year, I have actually started on writing a number of blog posts that have never materialized. I think that there are a few reasons...

(1) Although I have been treating this as a personal blog, I felt the quality of my writing had to improve, which means spending more time composing and editing.

(2) A number of posts were going to be about the technology underlying my product, and, since there was still more work for me to do, I felt it too soon.

I still get mail about NStatic. I am still developing NStatic, and will eventually release it. Due to health and fatigue, I have not been directly developing for half the year, following several years of non-stop 7-days-a-week development (on this and other products) and no vacations and little entertainment.

My quality of life is at this moment very low, probably equivalent to or less than that of a graduate student; my outlay is over $2K a month. My existence is mostly online. Though I live in the Seattle metropolitan area, I have probably visited Seattle proper at the rate of once or twice for each of the past few years. I needed to correct an imbalance in my life as it has hampering my motivation.

My hiatus began late spring after I accidentally poisoned myself by handling and absorbing thought my skin diluted household bleach, which sent me to visit the hospital, kept me bedridden for a few weeks and subsequently affected my productivity for the remainder of the year. I felt sore internally, and my focus and vision was significantly diminished. Faces and text became blurred that I began wearing glasses, but my eyesight improved over time and seems to have recovered recently after using Visine. On a related note in September, I also suffered effects of stomach ulcers from heavy use of caffiene after trying an energy pill. It wasn't a good year for my health.

I have continued to read academic papers, follow online courses, purchased books on the subject and follow development blogs. I spent some time thinking in a high-level way about my goals. I also started doing things within my limited budget that I cared about like this election, in which I voted and volunteered for Barack Obama, Chris Gregoire, Darcy Burner.

I am getting back to development. If I haven't delivered by the end of first quarter 2009, though it might reflect severe motivation as each delay is an expensive financial impact.

I'll write more posts, but they'll initially be short.

Lang.NET Presentation

I presented at both the Lang.NET Symposium and Seattle Code Camp, but it didn't proceed as I originally planned.

For several months, I have been changing the back end of my software to scale better and retain sufficient control of the performance of my product under all circumstances. I do have some hard-coded limits, but these limits and time constraints don't really work well the way my software is written. They are better for catching events that should never happen. The changes were extensive as I used functions pervasively to compress the size of my expressions and maintain the invariant that expression size stay proportional to program size. Manipulating arbitrary functions, particularly recursive functions, in a general and efficient way is really difficult.

I was using these two events as a forcing function for releasing my software. Unfortunately, I didn't make my deadline. I lost about several days of productivity due to a random apartment incident. I skipped a day and half of the conference to prepare in a valiant attempt to demo the most recent build of my software. Instead, I used an old release of my software from six months back, and messed up my demo since I forgot that I could only execute expression in the immediate window from within the context of an error.

My presentation relied heavily on slides rather than a live demo, which was not my plan. People want live code. Presentation slides also leave the audience confuse about the nature of the product as Ted Neward wrote in his Lang.NET review.

For people reading my blog, there wasn't too much extra information above and beyond what I have talked about in the past, since I could not assume that people were aware of my product. Some new points include the liveness of the environment, closed forms and some manipulations with functions.

I am wary about giving too much information, since I have leaked so much already for a considerable period of time without actually releasing the product.

I prepared the slide a month in advance, hoping that I would make changes over the course of the month, but ended up spending a full day polishing the presentation before my Code Camp talk.

Some reactions:

• Four Microsoft researchers quizzed me.
• A number of people that I have met read my blog... Most of the Microsoftees appeared to be familiar with me.
• A few people asked how they could apply for the beta. Others were hoping for a Java version. Miguel comment to me that it was a great presentation. I was surprise of my healthy applause, because I hadn't been paying attention and have never given any applause. The applause level was similar to Miguel's presentation later on, so I couldn't actually tell if the applause was enthusiastic or ordinary.
• Some questions on technical aspects:
  • did I utilize an available prover software like Z3? I wrote the software myself.
  • has my prover been benchmarked? No, and it's doesn't deal with the types of formulas use in the benchmarks.
  • how do I handle complicated cases like overflow. My overflow checking is very limited, since, in the past, I wasn't interested in cluttering my assumptions, but adding such support is trivial and now also less problematic.
  • how do I deal with invoking function variables (ie, delegates). I represent them exactly, but, for the sake of analysis, I ignore the potential effect on state if the function is unknown.

Postmortem:

• Create setup files regularly. Though I update component libraries frequently, I relied too much on .NET's XCopy support. Despite having copy DLLs to output folder, I was not able to get the build that I want working.
• Save interesting snapshot pictures of the product while in development. I reused a lot of images from my blog.
• Always try to have a working build. Include notes about the status of the software. I took a random setup build without remembering what state it was in.
• Conversations and event draw energy away from me. I usually enjoy my energy juices and bars before development, but I should actually remember to do even more so before presentations.
• Get well-rested before a presentation. This is unusually difficult for me, because I work during nights and sleep during the day.

There is still a geek dinner coming up in the next week that I may take advantage of to give a live demonstration.

Playing Chess with God

Although the title is appropriate, I wasn't actually planning on writing a post about the legendary chess grandmaster, Bobby Fischer, who died in the past few days, but I will take a few moments to pay my respects.

I was a long admirer of him, and, over the years, I identified with him ever more over the years. Here was this young natural talent who defeated several highly trained Soviet chessplayers to end Soviet domination of the chess world title. He was also very individualistic, provocative and controversial, breaking taboos and openly defying the government, by traveling to Serbia despite sanctions. In the same vein now, I do fancy myself competing against other companies and speaking freely.

Back to my intended post, I found this interesting post called "Play Chess with God" by an interesting new blogger, Russ Cox. This and his other post, SuperOptimizer, deals with computer solutions to traditional human problems mainly through brute force techniques.

Starting in the late 1970s, Ken Thompson proved by example that computers could completely analyze chess endgames, which involve only a small number of pieces. Thompson's key insight was that when there are only a few pieces on the board, there might be very many possible move sequences, but there are relatively few distinct board positions.

Given six pieces in the board, it became a simple lookup with Ken's endgame database to determine the best next move to make. Russ quotes former championship chess player Tim Krabbe describing his experiences using said database:

Playing over these moves is an eerie experience. They are not human; a grandmaster does not understand them any better than someone who has learned chess yesterday. The knights jump, the kings orbit, the sun goes down, and every move is the truth. It's like being revealed the Meaning of Life, but it's in Estonian.

While my software relies more on intelligent rules rather than brute-force techniques, the feelings and experience that I have experienced are more or less the same. My initial thought sometimes on seeing a strange result calculated by my NStatic tool is denial with the full belief that I am witnessing a software bug, only to discover after careful analysis and to my surprise that the computer's solution is in fact correct.

I don't claim this experience to be unique. This should be familiar to anyone who has ever played chess against the computer or used a declarative programming language with unpredictable control flow.

Human-like Reasoning

My goal in my static analysis work is not to solve general problems like the Four Color Theorem, but rather to simulate closely the human reasoning process to solve problems that are generated, comprehendible, and solvable by normal people. Practical and deep, rather than complete.

Humans write programs to be understood by other humans. Human understanding comes about instantaneously or with relatively little effort compared to the work performed by many analysis tools. We typically don't unroll loops and recursion, but instead "get" the meaning of programs by recognizing a few standard patterns. We look at a program and instantly see a sorting operation taking place, for instance. Programs typically consist of these recurring patterns. In many programs, the only complex data structures used are a standard few like arrays, hashtables, linked lists and stacks. My approach to reasoning adheres closely to the way humans think, even when more efficient computational approaches exist, so as to align my software with human performance; the one exception is when non-human-like approach is strictly better in every way, yet yields identical results.

Stephen Wolfram, inventor of Mathematica, wrote a post Mathematics, Mathematica and Uncertainty touching on some of these themes. Even with the more advanced symbolic capabilities of Mathematica--virtually infinite compared to more than my own software package, Wolfram encountered limits trying to use his own system to verify itself.

Sometimes we use the symbolic capabilities of Mathematica to analyze the raw code of Mathematica. But pretty quickly we tend to run right up against undecidability: there's a theoretical limit to what we can automatically verify.

Yet, I think that our approaches deviate somewhat in that Mathematica isn't geared to testing programs. Also, the Mathematica code base is not typical. Being a program for doing mathematics, it naturally consists of advanced mathematics, difficult for mortals to understand and involving non-linear arithmetic, which is theoretically undecidable.

The code was pretty clean. But it was mathematically very sophisticated. And only a very small number of experts (quite a few of whom had actually worked on the code for us) could understand it.

Another point that Wolfram makes is that, contrary to my approach, Mathematica typically avoids imitating humans but instead uses complicated, non-human-friendly procedures extending hundreds of pages in length, roughly the size of the entire analysis portion of my code base.

Think of almost any mathematical operation. Multiplying numbers. Factoring polynomials. Doing integrals. There are traditional human algorithms for doing these things.

And if the code of Mathematica just used those algorithms, it'd probably be quite easy to read. But it'd also be really slow, and fragile.

And in fact one of the things that's happened in Mathematica over the past decade or so is that almost all its internal algorithms have become very broad "polyalgorithms"---with lots of separate algorithms automatically being selected when they're needed. And routinely making use of algorithms from very different parts of the system.

So even if there's some algorithm for doing something that's written out as a page of pseudocode in a paper or a book, the chances are that the real production algorithm in Mathematica is hundreds of pages long---and makes use of perhaps hundreds of other sophisticated algorithms in other parts of the system.

But such algorithms were not constructed to be understandable---and much like things we see in physics or biology, we can see that they work efficiently, but they're really difficult for us humans to understand.

And in general, the way Mathematica works inside just isn't very "human friendly"... Like when Mathematica does an integral. It doesn't use all those little tricks people learn in calculus classes. It uses very systematic and powerful methods that involve elaborate higher mathematics.

Supercompilation

I noticed work by SuperCompilers, LLC on supercompilation that takes on the myth of the sufficiently smart compiler (which I previously wrote in my post on Humans vs Computers). Their technology seems very similar to my work with its reliance on partial evaluation.

The company deals with the same sort of criticisms about NP-completeness and undecidability in their white paper "Supercompiling Java Programs."

The problem of fully optimizing an arbitrary computer program, when mathematically formalized, turns out be an incomputable problem, we do not need to optimize arbitrary mathematically given computer programs, we only need to optimize programs written by humans. And humanly-written programs tend to have a lot of special structure too them, including both obvious and subtle redundancies that lead to inefficiencies.(this is related to algorithmic information theory; see, Chaitin, 1987 and Bennett, 1986). There is no possibility of ever creating an algorithm that can fully optimize a general computer program. Fortunately, though, the practical problem of program optimization -- though still very difficult -- is a lot easier than the general mathematical problem to which it corresponds. Because, in reality

Supercompilation does not try to solve the impossibly hard problem of fully optimizing an arbitrary computer program. Rather, it is an extremely valuable heuristic technique, which seeks to find ways of significantly optimizing a wide variety of computer programs. Most real-world computer programs are chock full of inefficiencies, which can be removed via the supercompilation process. These inefficiencies are often hard to see in the source code, but they are highly transparent when the code is translated into a more mathematical form, as is done inside the supercompiler. Some of these inefficiencies are introduced by sloppy programming; others are placed there intentionally, by programmers interested in goals besides efficiency, such as maintainability and comprehensibility of code, or speed of software development. In many cases the most efficient way to implement a given piece of code is a truly humanly infeasible way, involving literally hundreds of times more lines of code than the ways that occur naturally to humans.

Another post "Illogical Arguments in the Name of Alan Turing" in O'Reilly's website criticizes bad arguments by people, that static code analyzers are not useful at all because they are limited by the halting problem, or that logic flags can never be found because of the halting problem.

Humans are subject to the same theoretical constraints as computers, but yet they do not perform the same laborious, brute-force search. Instead, humans employ a strategy of recursive pattern matching and replacement when thinking about and checking their programs. The kinds of programs that people write are those that they can easily reason about and review later; being maintainable, these programs belong to small subset of possible programs and are inherently tractable for analysis.

One paper "Solving difficult SAT instances in the presence of symmetry" suggests that the structure of a problem can affect its performance. That, in practice, a technique such as SAT-solving which is known to be NP-complete, often doesn't break down as it theoretically should. The authors point to the presence of large number of symmetries in the problem as somewhat of a requirement for explosive behavior.

Research in algorithms for Boolean satisfiability and their implementations [23, 6] has recently outpaced benchmarking efforts. Most of the classic DIMACS benchmarks [10] can be solved in seconds on commodity PCs. More recent benchmarks take longer to solve because of their large size, but are still solved in minutes [25]. Yet, small and difficult SAT instances must exist because Boolean satisfiability is NP-complete.

A 1994 Infoworld article quoted a researcher saying that deep static analysis requires years of analysis time. Upon reading that quote, I immediately thought that the researcher's approach might be very inefficient, because it implied that, after some depth, a human could outperform a computer on the same job. Perhaps, if we mimicked actual human reasoning, we could produce more effective tools.

Specifications

My main tasks in the past couple of months have been divided between bug-fixing and improving scalability. In the latter case, testing on large projects revealed bottlenecks caused by uncontrolled expression growth, for which I came up with a general solution. I have been spending a considerable amount of time on my simplifier for recursive lambda expressions.

There was one major addition. I added syntax support and highlighting for eventual specification support. My immediate goal was to provide a clean way of adding breakpoints and assertions to the source code.

The above visual shows what the new syntax highlighting looks like. The new keywords are bolded. Two new grayed out comment delimiters were added: //@ and /*@. These comment delimiters act like white space from within NStatic with the exception that new keywords are only recognized within the comments.

Any arbitrary code, such as ghost fields, can be placed inside these comments; this serves as an alternative to using the preprocessor defines, NSTATIC and CODEANALYSIS.

The new keywords that I have included: require, ensure, assert, assume, pure, modifies, invariant, old, breakpoint, result, unreachable, and nonnull. But, for the first release, the only keywords that are actually effective are assert, assume, breakpoint, old. Assert actually verifies that the expression is true and returns a warning otherwise (or error in the case of an invalid code path). The behavior is stronger than a call to Debug.Assert. Assume does not require the expression reduce directly to a true value, but it will produce a error if there is a false path leading to it.

The specifications are modeled on both Java Modeling Language (JML) and Spec#. There are quite a number of differences between the two. For instance, JML incorporates method contracts before the method declaration whereas Spec# incorporates contracts just right before the method block. While I followed the Spec# in this case, my instinct is to prefer JML, because it is more of an industry standard, and I am less likely to encounter Microsoft IP issues.

I suspect highly that the next version of C# will incorporate some kind of design by contract.

There are a few differences from both JML and Spec#.

• Arbitrary functions are supported as expressions with specifications, including impure functions (functions containing side-effects). Side effects that occur inside the expression of a single specification are not visible to other parts of the program, including adjacent specifications.

I have never taken a course in formal methods, so I am not fully aware of the implications of my approach.

Scalability

I wrote my NStatic tool to perform quickly with the goal of scaling linearly with the size of the code base. Analysis of a single terminal function is done in a single pass and is basically linear with the size of a function. Performance is impacted more by the call depth of some of the functions than by the number of functions in the code base.  Even with deep calls, I found ways of keeping analysis tractable through lazy and cached evaluations.

The main issues I am currently grappling with are some scalability issues that I discovered while scanning Rotor (the Shared Source Common Language Implementation). I found some interesting errors in Rotors, which I'll eventually post in my blog.

I also found some gotchas as well. My tool zipped through hundreds of functions in a split second before stalling in a function, which wasn't all that complex. Some of my transformations, while seemingly simple, exhibit exponential characteristics. This occurs when a function application duplicates an argument.

f(x) => x op x

Repeated forward use of such transformations can lead to large expressions that take long to evaluate or even print.

I found a general, elegant solution that I have been implementing. Ideally, the normal form should be at least as compact as the original form [considering the fully expanded lambda expression representation of f], preferably more so. With constant and atomic arguments, this is the case. For more complex arguments, the reverse transformation is applied: The left hand side of the transform becomes the normal form. It's counterintuitive, but there's no reason why we can't continue to simplify this normal form as the two sides of the equation have the same value.

VB & Other .NET Languages

Send me mail if you are interested in beta testing experimental Visual Basic or IL+PDB support (for other .NET languages including C++/CLR--please specify language) if and when I do include it in an NStatic beta. I don't know if I'll be able to handle DLR-based languages.

There's a slight chance for support of other languages in the beta, but it will be experimental and the primary focus is C#. Any other language support will come in a minor update. I don't have much experience working with other CLR languages other than C#.

If VB support is introduced, it will likely have rich editor and intellisense, but some parts of the analysis may exhibit C# semantics except when performing the analysis indirectly through IL. All other languages will have error highlighting support.

Omniscient Debugging

Bill Lewis of Tufts University, who is a computer scientist who has worked on natural language processing, gave a fascinating Google TechTalks lecture on "Debugging Back in Time." He also has a page dedicated to this new idea of Omniscient Debugging, where the debugger knows everything.

The omniscient debugger records every state change in the entire run of the program. Bill states that omniscient debugging gives the programmer a unique view of the program that eliminates the worst aspects of breakpoints:

• No guessing where to put breakpoints
• No extra steps to debugging
• Set breapoints, start, examine, continue
• No fatal mistakes... (no, "Whoops, I went too far")
• No non-deterministic problems
• Customers can email a debugging session to developers

An omniscient debugger can be extremely effective in understanding and fixing bugs. Bill's description and walkthrough of his prototype omniscient debugger (which in his words is more already more effective than any commercial debugger) seems to offer a genuine "silver bullet" approach to debugging.

His approach to omniscient debugging logs every state change to the program. This has the obvious disadvantage of slowing down execution runs and consuming disk space. Bill claims to have a found a practical way of doing this. The disadvantages are similar to those a profiler, but even more so, because each state change is logged, not just function calls.

I noticed a long time ago that my own analysis tool, which uses a completely symbolic representation of a program's abstract state space, could in theory be able to recreate the entire run of a program with just a compact set of critical assumptions.

This could be even more effective than logging, because of the superior time and space savings of my approach. NStatic can execute a long series of nested lengthy loops in less than a millisecond; it can allocate a gigabyte-size array and fill it up with values from any algorithm, and it would still take just the few K of memory that is needed to represent the algorithm itself.

There might even be some benefit to combining my "symbolic" debugger with Mike Stall's C#/IL managed debugger sample, so that I can retroactively incorporate symbolic reasoning to an actual just-in-time debugging session. One developer actually created Deblector, which uses Reflector to decompiling and debugging IL on the fly.

I did consider at one time being able to step forward and backward through the execution history. In NStatic Directions, I did mentioned making static analysis more into a debugger than a static analysis tool.

Making C# feel more like a dynamic, interpreted, REPL language through the use of a symbolic interpreter. Code is always live and can be statically debugged. As Erik states, programming will “shake of the yoke of the dreaded (edit, compile, run, debug)* loop and replace it with a lightweight (edit=compile=run=debug) experience.”

NStatic does already feel like a debugger with ability to watch and execute code immediately, as well as the ability to apply new assumptions.

Methods, Part 1

Method handling is difficult in static analysis. I will describe in a few parts some of the issues that I have had to deal with.

I demonstrated in earlier posts my handling of recursive functions in Loops, Part 1. In this post, I will show how I elegantly handle virtual functions. Below is the code for three classes, a base class Animal and two derived classes, Cat and Dog. Animal is an abstract base class, so no implementation actually exists for one of its member function.

Each animal can make a noise and has a type.

To test the three Animal classes, a wrote the following test method below. We have three variables of type Animal, "spot," "polly," and "tabby." We know Spot is a dog through an Assert statement. We know Tabby is a cat because we just created one from scratch. However, Polly is an unknown and sounds as if it may be a parrot, a class that we actually haven't account for; or, we could be mistaken, and it could actually be a dog or cat. 

So, I run the code through NStatic and extract out all the local variables and its member variables after the scan. Here's what the resulting Locals window looks like.

Whether we assign a variable or assume it, we know through the variables of the form "isXaY" that Spot is a dog and not a cat, and Tabby is a cat and not a dog. We also know that Spot says "Bark" and Tabby saw "Meow." We can also tell each animal's type from Animal's virtual property, Type. However, the Polly variable is mysterious. Thus, the local window has to represent all information about Polly's nature and behavior through conditional expressions and possibly generated values (in the case of Animal.Say(), which has no implementation).