Home

Analyzing the Environment Structure ofHigher-Order Languages using Frame Strings

Analyzing the Environment Structure of Higher-Order Languages using Frame Strings, Matthew Might and Olin Shivers. 2007.

Reasoning about program behaviour in programming languages based on the lambda-calculus requires reasoning in a unified way about control, data and environment structure. Previous analysis work has done an inadequate job on the environment component of this task. We develop a new analytic framework, Delta-CFA, which is based on a new abstraction: frame strings, an enriched variant of procedure strings that can be used to model both control flow and environment allocation. This abstraction enables new environment-sensitive analyses and transformations that have not been previously attainable. We state the critical theorems needed to establish correctness of the entire technology suite, with their proofs.

Even if you're not interested in flow analysis of functional languages, the preface to this paper is very enjoyable reading. (If you are interested in flow analysis, the whole thing is enjoyable reading. I want a couple of weeks to go through this paper in detail.)

By neelk at 2007-08-16 16:23 | Functional | Lambda Calculus | Semantics | other blogs | 9255 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Link to PDF is here

Right now the link points back to the LtU home page. The paper in question can be found here:

http://matt.might.net/papers/might2007dcfa.pdf

By mzraly at Thu, 2007-08-16 16:41 | login or register to post comments

I added the link. Thanks.

I added the link. Thanks.

By Ehud Lamm at Thu, 2007-08-16 17:43 | login or register to post comments

like the focus on bindings

This paper looks really interesting. I always found bindings more central than anything else, so it's nice to see tools for environment analysis. At a glance, this looks like it could help practice by regularizing how we talk about it. (It would be even better if it changed how I think about it.)

By Rys McCusker at Thu, 2007-08-16 17:19 | login or register to post comments

I knew it :-)

I don't think I ever told you, Rys, that you were the one who really got me thinking about the pragmatics of "functional programming" by pointing out that even functional programs have state in the form of bindings. That provided a very important and persistent backdrop to some explorations that came much later for me, e.g. understanding how that insight is manifested in monads and the formulation that "state isn't the problem; unconstrained mutation is the problem." It gave me the impetus to appreciate the Alan Kay quote from "The Early History of Smalltalk" that I posted elsewhere, and to be able to see how programming approaches that I hadn't associated with minimizing the negative impact of unconstrained mutation, such as object-oriented programming, can, in fact, be seen in that same light. So, thanks!

By Paul Snively at Thu, 2007-08-16 17:42 | login or register to post comments

the incredible lightness of bindings

I'll touch 3 things: 1. modesty, 2. paper reaction, 3. bindings associations.

You're welcome and thanks for pleasantries! But I did nothing hard to note functional runtimes mutate state to capture bindings not present before. I'm glad you derived insights — I just don't feel that clever about it.

I went over the paper again (as best I could with two sons talking very loudly a dozen feet away) and still found the frame strings material very engaging, but decided it might only be an algebraic representation of things I visualize spatially when I think about such mechanisms in systems. I gather the paper's motivation is inline substitutions, and analysis to guarantee safety based on equivalence in resulting evironment frames (so bindings are not altered by substition). I probably won't do any such inlining optimizations in my own work, so the analysis is less critical for me to dredge more fully.

The notation to express frame effects was fun. :-) I guess I never thought much about how I've never had notation to express what I see when I simulate changes in spatial systems mentally. (Spatial visualization is my normal thought mode taking least effort; algebra and linear text is hard to get very enthused about.)

I've been mostly interested in knowledge representation the last 30 years, so that's why I gravitated to bindings in languages and other sorts of runtimes. All my fun jobs (like my current day job) have involved creation, maintenance, and optimization of bindings for knowledge apps or servers must have. This is one aspect in which all my non-language reasoning has often looked like reasoning for programming languages. I've often wondered whether a programming language would be more suitable for some things I do.

For example most of my day job lately involves bindings in a server, and how they get created, maintained, and destroyed in a distributed network environment. Hard issues involve avoiding unconstrained mutation in a highly multi-threaded shared memory context, actually involving issues like propagation delay of bindings: when and where they have force, and for how long. The server is "compiling" all the time, and bindings decay radioactively. Optimization primarily focuses on speed in using bindings despite size and stochastic unpredictability. There's probably some sort of programming language that can express what happens, but it's like I implement effects with a naked runtime beneath such a language. Maybe someone will read this and dream up a good language for it.

By Rys McCusker at Fri, 2007-08-17 08:21 | login or register to post comments

constrained state

If anyone's looking for a nice overview of constraining state mutation, implicit state, etc. CTM has a nice treatment of it in chapter 6.

By Oliver Mooney at Fri, 2007-08-17 09:51 | login or register to post comments

Further reading

To the LtU community: Thanks for noticing the paper!

As an author, I'll add that I believe the real value of this paper is not in the analysis, but in the concrete theory of environments it provides. Most of my first two years in grad school was spent meditating on concrete environment structure and change.

In the two years since then, I've found much better ways of doing environment analysis itself---via abstract counting (augmented with abstract garbage collection) in particular. But, the concrete frame-string semantics still yields the deepest insight on the nature of environments themselves.

Shamefully, I'm still fussing over the typesetting for a public version of my dissertation, but if anyone wants the latest and most complete treatment of environment analysis, the latest public draft of my diss is here:

http://matt.might.net/tmp/diss-draft.pdf

The Delta-CFA article appears (reworked and expanded) as Chapter 8. Armed with an unlimited page budget, I also included 44 worked examples with discussion, in the hopes that it might help people trying to learn from it.

(Also, the applications chapter shows that environment analysis is good for a lot more than just the inlining that is the focus of the article.)

By might at Fri, 2007-08-17 22:37 | login or register to post comments