Paul Graunke, Robert Bruec Findler,
Shriram Krishnamurthi, Matthias Felleisen (Northeastern, Rice,
Brown, Northeastern)
Proc. ASE 2001
|
Summary by AF |
One-line summary:
Automatically convert imperative programs to "inverted" control
flow programs (similar to continuation-passing) so they can be recast as
CGI-based programs where each step consists of collecting input and then
continuing the computation. The techniques here are simpler than
continuation-passing, since CP requires a server-side scripting language that
supports this feature (or a server-side runtime that does).
Overview/Main Points
- Concept 1: argument currying L(x,y).x+y takes x and y and
retursn the sum.
Lx.(Ly.x+y) takes x, and returns a function which given y will
return x+y.
- Concept 2: lambda lifting, to eliminate the need for the language
to support closures.
Suppose you have a function (L args body). Because the
function may contain free variables, for correct execution it must
be executed within the lexical scope in which it was defined.
This would require the language to support closures, which is tricky
to do (though Perl happens to do it). So each such function is
transformed into ((L free-vars (L args body) free-vars),
which is closed and can be executed correctly in global (outermost)
lexical scope.
- Concept 3: defunctionalization.
How to apply them. In the original program, distinguish
computation-only steps from steps that require user input (ie require
the server-side program to suspend itself, send the user a web form,
then collect the values in the form and resume itself.) Displaying
output can be folded into the step of collecting input. Think of the
original program as a series of steps:
(define temp1 (read-values-from-form form1)) ;;temp1 could be a vector of several values, or whateve
(define temp2 (read-values-from-form form2))
(display-output (local-compute-1 temp1 temp2))
First, invert the control flow of the program to convert it to
continuation-passing style. Anyplace a "suspending"
procedure is called (in this example, read-values-from-form), we have to
replace it with a continuation. Define a new function read-values-from-form-CPS
that looks like this:
(define (read-values-from-form-CPS form cont-function)
(apply cont-function (read-values-from-form form)))
So we can write
(read-values-from-form-CPS
form1
(lambda (temp1)
(read-values-from-form-CPS form2 (lambda (temp2) (local-compute-1 temp1 temp2)))))
First, convert each of the local-compute calls into a closure, to
eliminate free variables.
(define closure-1 (lambda () (lambda (temp1)
(read-values-from-form-CPS (closure-2 temp1)))))
(define closure-2 (lambda (temp1)
(lambda (temp2) (local-compute-1 temp1 temp2))
temp1))
Note that closure-1 and closure-2 are closed functions, i.e. the
function bodies do not contain any free variables. The new CGI
invocation is then:
(read-values-from-form-CPS form1 (closure-1))
The only remaining issue is the implementation of
read-values-from-form, since it has to generate and deliver an HTML form
that embodies the continuation closure-1. The idea is that
when the form is submitted, the submission values include the value of
closure-1 in addition to whichever variables the form was supposed to
collect. This means that closure-1 has to be represented in a way
that allows it to be passed back and forth over HTTP. The basic
approach in this paper is as follows:
- Do the transformations above; you are left with N closures, where
each closure represents the continuation-passing argument of each
form interaction.
- Put these closures into a linear array that is stored on the
server.
- Along with each HTML form, include a variable that indexes the
number of the continuation to be invoked when this form is
submitted. Standard tricks like signing a hash can be used to
make sure the submitted form is tamper-evident.
- The server-side code for handling a CGI then boils down to: (a)
identify which "application" generated this form; (b)
extract the values of the user-variables collected by the form; (c)
extract the index of the closure representing the continuation; (d)
apply the closure to the extracted variables.
The paper talks about problems involving server-side state
maintenance, but well-known solutions can address these. In
principle, if the server side state is kept "forever", a
"stale" form can be submitted arbitrarily far in the future
and will still work.
Another alternative is to marshal the entire closure and pass it back
and forth (cryptographically sealed, etc.). This avoids having
server-side state at the expense of making each client interaction more
expensive. Note that since a closure is closed (duh), its execution
doesn't depend on anything except the body of the closure itself (and
possibly global variables associated with the server-side state but not
with any particular user or application, etc).
The paper talks about future work involving a formal proof using
"observational equivalence" to prove the correctness of the
transformation. I'd like to ask Shriram about this when he visits
on Fri.
|