Central Themes from the Ynot Papers

The Ynot project is the fancy name for Hoare Type Theory, which is a body of work developed by Greg Morrisett at Harvard. Hoare Type Theory is a dependent type theory for stateful programs, which is based on Hoare Logic. The Hoare type {P} T {Q} denotes a computation that expects a world described by P, leaves the world in a state described by Q, and yields T.

This work is intimately related to my own work on linearizability types, and my work will probably share a great deal with Hoare Type Theory. The work's major ideas include the following:

1) Type-checking is split into two parts. The first is an ML-style, decidable, terminating type checking phase. This phase also generates a multitude of proof obligations. The second phase discharges these obligations in one of many possible ways, such as a) ignoring them, b) relying on proof annotations in the code itself, c) checking by hand, d) using an interactive prover, or e) using an automated prover. This sets up a nice, pay-as-you-go system that allows for rapid development as well as more formal processes.

2) The Hoare types incorporate separation logic, which allows for minimal specifications. P and Q in {P} T {Q} only describe those portions of various heaps which the term in question actually uses. This allows for much smaller, and reusable specifications.

3) The separation logic can also express ownership of various locations. This can be used to describe a garbage collector or memory allocator, for instance.

4) Abstract predicates can describe state and effects without actually revealing details about internal representations. For instance, a naïve typing of an increment function on a counter object might be inc : c : counter,n : int.{ c ↦ n } c → n { c ↦ n + 1 }, however, this reveals too much about the structure of the object. A better way is to include in the object's description a proposition over counters and integers, like yields : counter × int → Prop (I'll write this in infix notation). Then, the type of the counter ends up being inc : c : counter,n : int.{ c yields n } c → n { c yields (n + 1) }. This tells me nothing about the internal structure of c. C could be anything for all I care, so long as the abstract predicate yields tells me what I'll get from each call to inc.

Hoare Type Theory itself has predicative (ML-style) polymorphism with existential types (data hiding). They have proven that impredicative polymorphism could feasibly exist, but it doesn't appear that they've actually added it. The have attempted to add support for transactions, but this is copy-catting the Haskell STM with invariants monad, not what I'm trying to do. At the present, they have no subtyping.

Analyzing GC Traces

For the chaos research, I'm building a simulator framework for analyzing garbage collection traces. What I've had in mind up to this point is a simulator for a simple language, which generates traces, an analyzer which runs on traces to simulate collection events. I recently had the idea of using an ILP solver to compute the optimal collection strategy, and compare the results against any online (read: usable) approaches we came up with.

However, I realized yesterday that the branch and bound algorithm for solving ILP problems potentially yields alot of very useful information regarding garbage collection. The algorithm provides a way to analyze the impact of choosing whether or not to collect at a given point, and the shape of the search tree should give some indication as to which points are the most important. This in itself is potentially very useful information. Moreover, it could become a profiling technique in its own right. If a certain point is a useful point for garbage collection in most of the runs of a program, then it could be statically marked as a preferential point for collection.