Lambda the Ultimate

SICP gets many nods when it comes to introductory texts to programming and the study of PLs. I've been slowly working my way through SICP in a number of different PLs, most notably Oz and Alice ML. In that process, I've come across Eli Bendersky's methodical solutions to the SICP Exercises in a series of blog posts. His review of SICP is instructive of the role of the exercises:

A word about exercises in SICP. They are numerous, some of them are hard, but the exercises are the best way to really understand what the book tries to teach. In a manner, they’re as integral part of the book as the text itself. The exercises are very well prepared and lead the reader through the examples coded by the authors into greater understanding of the topics taught. At times, it feels like the exercises are specifically designed to force you to think about the essence of the topics, and not just grasp them superficially.

Highly recommended reading for anyone that is working their way through SICP. Unlike my own work, which concentrates solely on code, his explanations are quite good. He uses mostly Common Lisp for the solutions, though resorting to Scheme when it makes for more concise solutions.

Local Rely-Guarantee Reasoning, Xinyu Feng. Accepted for publication at POPL 2009.

Rely-Guarantee reasoning is a well-known method for verification of shared-variable concurrent programs. However, it is difficult for users to define rely/guarantee conditions, which specify threads' behaviors over the whole program state. Recent efforts to combine Separation Logic with Rely-Guarantee reasoning have made it possible to hide thread-local resources, but the shared resources still need to be globally known and specified. This greatly limits the reuse of verified program modules.

In this paper, we propose LRG, a new Rely-Guarantee-based logic that brings local reasoning and information hiding to concurrency verification. Our logic, for the first time, supports a frame rule over rely/guarantee conditions so that specifications of program modules only need to talk about the resources used locally, and the certified modules can be reused in different threads without redoing the proof. Moreover, we introduce a new hiding rule to hide the resources shared by a subset of threads from the rest in the system. The support of information hiding not only improves the modularity of Rely-Guarantee reasoning, but also enables the sharing of dynamically allocated resources, which requires adjustment of rely/guarantee conditions.

In the beginning there was Hoare logic, which taught us how to reason about sequential, imperative programs. Then, Owicki and Gries extended Hoare logic with some additional rules that enabled reasoning about some concurrent imperative programs. This was good, but there were a lot of "obviously correct" concurrent programs that it couldn't handle. So Owicki-Gries logic begat two children.

The elder child was Jones's introduction of the rely-guarantee method. The intuition here is that if you have two subprograms M1 and M2, and M1 will work in an environment with a working M2, and M2 will work in an environment with a working M1, then when you put the two together you have a working M1 and M2. This is a really powerful reasoning method, but unfortunately it's not terribly modular.

The younger child of Owicki-Gries was concurrent separation logic. The intuition behind it is that if you can divide the heap into disjoint (logical) pieces, and only let one process access each chunk at a time, then you can't have any race conditions. This is a very simple principle, and permits modular, compositional reasoning about concurrent programs -- even pointer programs. But there are programs that can't be proven in this style.

So the obvious thing to want is the ability to combine these two styles of reasoning. Unfortunately, this is hard -- there have been several logics proposed to do this, each of which does a bit better than the last. Feng's is the latest, and the best I've seen so far. (Though concurrency is not really my area.)

An interesting point is that these kinds of reasoning principles, while invented for the concurrent world, are also interesting for reasoning about modular sequential programs. This is because when you create imperative abstractions, it's helpful to be able to give up knowledge about exactly when state changes can happen. So you need the same sorts of techniques to handle this kind of conceptual nondeterminism that you need for the actual nondeterminism of parallel hardware.

www.lisperati.com/fringedc.html

FringeDC is a group for people interested in fringe and functional programming languages (Lisp, Haskell, Erlang, Prolog, etc) in the DC area.

This Saturday Andrew Harris will discuss the geeky internals of his EmbeddedML project, which aims to bring functional programming to the world of microcontrollers. It's a lightweight system that generates generic C code, allowing it to support many low resource devices.

This meeting will be presented in conjunction with HacDC, the one-and-only workshop for microcontroller geekery in DC. After the presentation, we'll go out for some beer to discuss all the latest programming topics of the day. Everyone is welcome to join us!

Date: Oct 11th 6PM
Address: HacDC headquarters- 1525 Newton St NW, Washington DC 20010 USA
(Near corner of 16th and Newton NW)
The closest MetroRail station is Columbia Heights (Green Line). You can check online to see the next train arriving there. The S1-2-4, H1, and H2-3-4 buses go right by our location.
Approach on the 16th St side of the building. Look for the red doors. We are on the third floor. Follow the signs to our space after signing in with the guard.

http://maps.google.com/maps/ms?ie=UTF8&hl=en&msa=0&msid=112368426664365520724.00044a72684e313eb7ebd&ll=38.932307,-77.03521&spn=0.008813,0.007253&z=17&iwloc=00044a727d23d707d87b9

-Conrad Barski, M.D.

In the interest of discovering some further reading material,
I have created a quick survey open to all LtU'ers..

Please name:

1) One of your favourite papers of all time
2) A recent paper you consider ground-breaking in some way
3) A lesser-known paper that you feel ought to be more widely read

Any PL topics welcome!