CEK Abstract Machine

I stumbled upon Pycket yesterday. It grabbed my interest because I heard racket itself already has a JIT. The paper claims Pycket outperforms Racket on average. I got a reintroduction to the CEK (Control, Environment, Continuation) abstract machine.

The CEK evaluates its input lambda calculus directly. The description in the paper is only 6 lines, so I rewrote it in python. I had to describe few structures so it's lot longer than the original. The gist is in this function:

def step(expr, env, cont):
    if isinstance(expr, Var):
        return env(expr), env, cont
    if isinstance(expr, Call):
        return expr.lhs, env, Arg(expr.rhs, env, cont)
    if isinstance(expr, Lam) and isinstance(cont, Arg):
        return cont.expr, cont.env, Fun(expr, env, cont.cont)
    if isinstance(cont, Fun):
        return cont.expr.expr, Env(cont.env, cont.expr.bind, expr), cont.cont
    assert False

The expr or "control" part of CEK is the current expression or value. The program mostly acts based on that and the current continuation. Here's what happens in every condition on the above:

Variables are looked up from the environment.
Calls contain only 1 argument. The argument is shifted into continuation stack to wait until the callee is evaluated.
A matching lambda and argument in continuation stack results in an activation record being inserted and argument evaluated.
When the expression is in a normal form and there is an activation record in the stack, the value is bound to the lambda and the lambda is evaluated.
If the program ends up calling a normal form other than lambda, it crashes. It also crashes if it runs out of continuations. For demonstration purposes the latter isn't much of a problem because the program would have exited at that point anyway, and it is clear from the output why it crashed.

Despite the simple structure, it has lot in place to support complex control flow. All arguments are evaluated only after activation but before they're bound. It allows conditionals to be implemented as primitive function that prevents evaluation of one of its argument by popping one off from the continuation stack.

The lambdas are 'bare' here. The function always takes exactly one argument. That makes sense if you don't consider them as something causing an effect, but instead as something just returning a value.

At a glance it seemed more exciting than it is, though.

CEK Abstract Machine

Similar posts