This paper introduces the approach, now known as the Boogie method, which form the basis of Spec#. The basic idea is a modular approach to verifying object invariants (and pre- and post-conditions) by maintaining a notion of object validity and packing and unpacking that validity in the course of checking invariants. The main motivation was to tidy up problems with DbC where objects could run into problems when calling their own public methods while their invariants didn’t hold. The modularity is a big win as well as the fact that a lot of useful things can be statically verified rather than deferring all checking until runtime (as is common in DbC). I can only hope that some of these ideas eventually see the light of day in a stack other than the one encumbered by the evil empire.

Source: PDF CiteSeerX

It mainly describes a technique to preserve some sanity in inferred finite-state behavioral models of software systems. While the idea seems like a good one, in terms of its effects on the inferred model, I’m not so sure how these inferred models are useful. Shrug.

Source: PDF ACM

I already reviewed the other Thorn paper, Thorn—Robust, Concurrent, Extensible Scripting on the JVM. This one just goes into more detail on the type system, and how like-types interact with dynamic and static types. I like the idea of minimizing the impact of converting part of your code to being type checked, as a step toward making your whole program statically typed.

Source: PDF ACM

Another crazy use of type systems. Here the idea is to completely ignore the declared types of variables and instead just run a type inference algorithm (Milner’s Algorithm W) on the program and see what types you get. Instead of using primitive operations (like addition) to constrain variables to representation types (like int), you just constrain variables to the same type. Naturally, assignment and function calls cause type unification as well. You end up with a bunch of abstract types assigned to variables that reflect whether they are “related”. The idea is that this helps you to understand where values flow through your program and what might be impacted when making changes. It sounds like an interesting idea; I have no idea if it would be useful in practice.

Source: PDF ACM

This is a follow-up to Milner’s introduction of the type inference algorithm known as Hindley-Milner or Algorithm W. Here they provide a sketch of a proof that it infers “principal” types which are the most general possible types. (This proof was given by Hindley over a decade earlier, but apparently Milner nor the any of the reviewers knew about it.) It’s the sort of paper that wastes no ink on pesky prose explanations of the nice compact formulas, which is great for the trees, but really annoying when any of those formulas contain typos. If you’re not already familiar with the subject matter, you might spend an awful lot of time trying to figure out whether they really meant theta-sub-one when they wrote theta-sub-two.

Source: PDF ACM

More fun with type systems! Here they use type annotations to distinguish between pointers under user control and pointers under kernel control, and type inference to allow them to only add annotations on system calls and on functions where passing a user pointer is safe and where it’s not. The type inference fills in everything in between, or rather specifically identifies places where user pointers are used unsafely. They then run this on all 1.4 million lines of the Linux kernel. That’s a pretty impressive case study.

One of the cool things about this paper is that they mostly focus on how they improved an existing analysis tool to eliminate false positives (as well as characterizing the false positives they were unable to avoid), which provides object lessons in why you care about things like context sensitivity, flow sensitivity, field sensitivity, and so forth.

Source: PS ACM

Describes a library for .NET that introduces constructs for lightweight parallel programming, mainly Parallel.For and Parallel.Aggregate. These are parallel for-loops and fork/join (also popularly known as map/reduce). Unlike DPJ, these guys don’t provide a type system or any guarantees that you’re not shooting yourself in the foot. They claim those are “orthogonal concerns” which is a bit of a cop-out, but not totally. For parallel for-loop kind of stuff, you probably are doing something mostly safe. For fork/join and their more flexible basic futures, you’re free to use those in all sorts of naive ways and not realize that you have race conditions coming out of your proverbial orifices. In any case, they describe their implementation, which is cool.

Source: PDF ACM

Describes a points-to analysis expressed entirely as a Datalog program. (Datalog is awesome!) They focus on the optimizations done to the Datalog program to allow the analysis to be faster and more scalable than the state-of-the-art (the paper being from OOPSLA 2009). The existing techniques have moved toward using BDDs to improve scalability and these guys are keen to prove that to be a bad idea.

Source: PDF ACM

Extends the work described in Points-to Analysis in Almost Linear Time, which didn’t handle structs or unions (all this is for C). Unfortunately, C’s “type system” makes this work very messy because they need to account for all the nasty things you can do with structs (like overwrite two adjacent int fields by assigning through a long pointer). Sausage making indeed.

Source: PDF ACM

Describes a cool technique for turning a points-to analysis into a type inference problem—one that can be done in almost linear time, hence the title. As type checking is flow-insensitive, so is the analysis, and since it infers monomorphic types, the analysis is also context-sensitive, but there’s nothing stopping you from doing a polymorphic inference and getting a context sensitive analysis (which I think Steensgaard later did).

Source: PDF ACM

My introduction to predicate abstraction (not the first work to make use of it), another interesting technique. Basic idea is: you have some complicated state in your program that is causing your model checker to blow up (i.e. consider too many states), replace it with a predicate over that state that captures whatever it is that your program cares about. Maybe you have two timer variables that could in theory each take on any 64-bit value, but all you care about is whether one is greater than the other. You can reduce 2^128 possible states to 2. Big win. In this case, they used it to apply model checking directly to the source code of a real-time OS kernel.

Source: PDF ACM

This paper was part of my introduction to model checking. It introduces an idea that has gotten a lot of mileage in the program analysis and model checking community. To wit: start with a rough (but soundly over-approximating) abstraction, if said abstraction demonstrates a violation figure out whether the violation is real (you’re done) or spurious, in the latter case use the spurious example to refine your abstraction as little as possible. Repeat until your abstraction is sufficiently refined to find a real violation or no violations.

Source: PDF CiteSeerX

I’m falling way behind with my paper reviews. I think a more scalable approach henceforth will be full reviews of papers that particularly catch my interest, and brief, no-summary blurbs about all the ones in between. Here comes a deluge of the latter.

Summary
Describes a language, Deterministic Parallel Java, which extends Java with parallel constructs (cobegin and foreach) and a type and effect system that guarantees deterministic semantics for said constructs. Describes region-based type and effect system including: named regions, region parameters, disjointness constraints, method effect summaries (for modular checking), region path lists (for describing nested regions), partially specified regions (for describing recursive algorithms), index-parametrized arrays, and sub-arrays. Manual commutativity annotations can be added to communicate invariants inexpressible in the type system.

Comments
Providing light-weight parallelized primitives is clearly an important step toward more wide-spread use of parallelism in every day programs. If you have problems amenable to parallel divide-and-conquer solutions, then cobegin and foreach are going to be your friends, and index-parametrized arrays and sub-arrays will allow you to express your algorithm in a way that DPJ can prove has no data races.

When things get messier and you have a mishmash of computations where some are parallelizable and some are just concurrently executable (maybe they block on disk or network I/O) and you want to weave these all together with a type system to point out any “sharing accidents”, I’m not sure how useful something like DPJ is going to be. That’s not to say that there’s obviously a better approach that does reconcile a more ad hoc workload, and maybe DPJ is a step toward such a thing. It may be that something like Kilim is a more appropriate abstraction for general-purpose computing. Or perhaps these approaches are orthogonal.

Source: PDF ACM