SLAM and BLAST are automated static checkers that took the programming language world by storm. Recently I have spent a bit of time trying to understand the way these tools work and quite honestly, I think it is their ability to formalize their ideas that have made them such successes over as opposed to the ingenuity which we ideally want to promote as good samaritans.
State Space Explosion is what limits checker from being built at run time. So what do you do? Build some abstractions over some things in your program and keep asserting these at all points. For eg: My mutex C program should never call unlock or lock twice continuously– clearly a cause for deadlock. This is a predicate that is invariant over the lifetime of a program (Did I just say lifetime? Rich Hickey influence I guess). Now, how does one make these abstractions? Remove all lines of code in your program that are not associated to the assertion(s) you are making and retain just those that are.
Fintd the state space and you are practically done. This may not have been a simple task in terms of the programming work involved with building the tool. But there are several gaps between what I would expect a tool to do and what SLAM and BLAST accomplish.
Many of the thoughts and conclusions I have expressed on BLAST may be premature since they are predictive more than experiential. In the interest of analyzing how BLAST would do “on the field”, I was forced to take the (bold) predictive approach. BLAST (like SLAM) is designed to check if software conforms to the recommended behavioral properties of interfaces that are used — much like unit-tests that seem like BLAST’s design-driving runtime counterparts. Like UT, BLAST has the overhead of needing a specification from a programmer. Since it requires this meta-data (meta-code actually), I tend to feel that it is most beneficial in cases where the test is to be run on several pieces of software that need to conform to a common specification — Eg: Windows Drivers need to conform to interfaces provided by the OS’ API. In such cases the return on investment on the meta-code will clearly be high.
It is also interesting to think of what it would take to rewrite BLAST for other (some dynamic) languages. Several difficulties that may have (possibly) been encountered with regard to providing memory safety and pointer aliasing intelligence tend to get trivialized with languages like Java that provide well-managed memory. There is a necessity to abstract a piece of code into a boolean program to control the state space explosion that is a run-time consequence of having a “rich” type-system like C does. Drawing from that, rewriting BLAST for a duck-typed language like Ruby can pose challenges in other domains too. Contrary to what may seem, the state space explosion problem will only be more acute in duck-typed languages. Hence it may be necessary for BLAST to bring in a pseudo-type system into itself in order for any meaningful predicate/propositional assertions to be made before a Ruby program runs —- a bit of an irony. In either of these language-types, I find that the specifications (meta-code) can often communicate intent better than the code itself (much like unit-tests).
Another interesting aspect of the implementation is how the atomicity of operations has been handled. When a statement long pval=0 is encountered in a program, the ART constructed assumes that Predicate(pval == 0) holds true after that statement. It is clear from this that BLAST will not handle multi threaded software. The assumption of all assignments being atomic can cause havoc in most languages (C included). Although this may be more related to the non functional way the code is written and the static nature of the mechanism, it is still fair to expect that a tool understands atomicity of operations in a language and constructs its ART considering other threads running (in the same process). This may bring us back to the state explosion problem once again on account of the numerous orders of execution threads may assume. Intuitively, languages like Clojure that support immutable data structures may tend to benefit/tolerate the static nature of the atomicity that blast proposes. I am thinking of building an equivalent tool for a language with immutable data structures for a final project.