Lambda the Ultimate

Extending the Multilisp Sponsor Model by Randy B. Osborne. 1993.

Speculative computing is a technique to improve the execution time of certain applications by starting some computations before it is known that the computations are required. A speculative computation will eventually become mandatory (i.e. required) or irrelevant (i.e. not required). In the absence of side effects irrelevant computations may be aborted. However, with side effects a computation which is irrelevant for the value it produces may still be relevant for the side effects it performs. One problem that can result is the "relevant synchronization" problem wherein one computation requires some side effect event (a "relevant synchronization") to be performed by another computation, which might be aborted, before the first computation can make progress. Another problem that can arise is the "preemptive delay" problem wherein a computation that will perform some awaited side effect event is preempted by a computation whose importance (e.g. priority) is less than that of computations waiting for the event. In this paper we show how the sponsor model developed for speculative computation in Multilisp can be extended to provide a novel solution to these two problems. The idea is for the computation awaiting some action, such as the production of a value or the release of a semaphore, to sponsor the computation or set of computations that will perform the awaited action. This sponsorship ensures that the awaited action executes, and executes with at least the waiter's level of importance. We show how to apply this technique to solve the above problems for several producer/consumer and semaphore applications. The idea extends naturally to other synchronization mechanisms.

Old news, one may say, but why the industry is continuing to ignore this knowledge (What really happened on Mars? -- Authoritative Account)?. See also the author's previous paper containing besides other information an overview of speculative computing in general: Speculative computation in Multilisp (1990).

I've been reading up on multi-stage programming recently and came accross Eta-expansion does The Trick which interests me because partial evaluation is something I think deserves higher visibility in programming in general.

I've seen η-expansion in the context of the various λ-calculi before but I can't seem to translate this to algol style languages. I must be missing something trivial or obvious. Could anyone please enlighten me?

In http://lambda-the-ultimate.org/node/1930 and http://lambda-the-ultimate.org/node/1944 i described a lambda calculus with quotation and a program logic. Ever the one to believe that theory and practice should verify each other, i have put together, here (http://svn.biosimilarity.com/src/rlambda/), a first draft implementation of the ideas in OCaml.

Currently, the system supports a very brittle command line REPL for a pretty raw syntax. The main point of interest is that the code is factored more or less along the lines of the specification, making use of recursive modules. That is, syntax and structural equivalence are functors of a module type IDENTIFIER. Then a reflective module is made by interpreting the IDENTIFER operations using terms. See the code. (Note: i wanted to have the operational semantics module also be a functor and recursively instantiate, but i couldn't get the OCaml compiler to get the three-level functor to work properly. Email me at lgreg.meredith@biosimilarity.com for further discussion.)

In an upcoming update i will add a simplistic model-checker for the logic.

System requirements

i have only tested the code on Mac OS X (tiger) using "OCamlDuce version 3.09.2pl2", but i'm pretty sure that a plain vanilla version of OCaml at or around version 3.09.x should build and run the code. The make files are written for

lgmaclt:~/work/src/projex/biosimilarity/reflection/rlambda/ocaml lgm$ `which make` --version
GNU Make 3.80
Copyright (C) 2002 Free Software Foundation, Inc.
This is free software; see the source for copying conditions.
There is NO warranty; not even for MERCHANTABILITY or FITNESS FOR A
PARTICULAR PURPOSE.
lgmaclt:~/work/src/projex/biosimilarity/reflection/rlambda/ocaml lgm$

Copyright

The source files say Copyright: Biosimilarity LLC. All rights reserved. But, everything on the site is under GPL. So, you are free to do what you want with the code -- such as it is -- as long as you respect GPL.