thinking about proper implementation of tail calls

[John Rose]

(Moving the tail call conversation forward a notch since last August.)

A belated thanks to Rene Sugar for forwarding this link on tail calls and stack-based permission checking.

On Feb 14, 2013, at 11:44 AM, Rene Sugar <rene.sugar at gmail.com> wrote:
> 
> Regarding: http://mail.openjdk.java.net/pipermail/mlvm-dev/2012-August/004944.html
> 
> 
> A Tail-Recursive Machine with Stack Inspection
> [John Clements and Matthias Felleisen, 2004]
> http://www.ccs.neu.edu/racket/pubs/cf-toplas04.pdf
> 
> 
> "Security folklore holds that a security mechanism based on stack inspection is incompatible with a global tail call optimization policy; that an implementation of such a language must allocate memory for a source-code tail call, and a program that uses only tail calls (and no other memory allocating construct) may nevertheless exhaust the available memory. In this article, we prove this widely held belief wrong. We exhibit an abstract machine for a language with security stack inspection whose space consumption function is equivalent to that of the canonical tail call optimizing abstract machine. Our machine is surprisingly simple and suggests that tail calls are as easy to implement in a security setting as they are in a conventional one."
> 
> 
> "Our work fills the gap between Fournet and Gordon’s [2002] formal model and Wallach’s alternative implementation of stack inspection. Specifically, our security model exploits a novel mechanism for lightweight stack inspection [Flatt 1995–2002]. We demonstrate the equivalence between our model and Fournet and Gordon’s, and prove our claims of TCO. More precisely, our abstract implementation can transform all tail calls in the source program into instructions that do not consume any stack (or store) space. Moreover, our abstract implementation represents a relatively minor change to the models used by current implementations, suggesting that these implementations might accommodate TCO with minimal effort."

The paper is dense with formality.  Here is my take on it.

As the Clements/Felleisen paper points out, since the protection domain information in an AccessControlContext is order-independent (up to access controller boundaries), it can be easily summarized apart from the concrete sequence of active stack frames.  The paper also points out the good trick of hoisting the summarization out of the tail-call loop and into the continuation frame shared by a linear sequence of tail calls.  It provides a proof that this approach would correctly preserve the equivalent notion to PD sets in a formal calculus lambda_sec, which is not too different from the JVM.

The paper uses a flexible notion of "continuation mark" which I find interesting.  The original reference on continuation marks is Clements and Flatt, 2001, "Modeling an Algebraic Stepper" http://dl.acm.org/citation.cfm?id=651947.  That latter paper takes the idea of a findable "magic mark frame" and works it out in detail, with a nice API and use cases, and in the context of guaranteed ("hard") tail calls.

This paper is also referenced in Arnold Schwaighofer's thesis which describes the mlvm prototype for tail calls; see http://ssw.jku.at/Research/Papers/Schwaighofer09Master/ .

Arnold's comments on Clements and Felleisen show the reason for investigating lazy stack compression:
> Clements and Felleisen [12] describe an abstract machine that can optimize all tail calls while still maintaining correct security information in the presence of stack inspection.  The proposed machine stores a table of permissions with each frame. When a tail call is performed the table of the caller’s caller is updated to include the permissions of the caller. When the stack is inspected these tables are taken into account. Hence the permissions of the removed caller frame are not lost. Using such a scheme within the Java HotSpot VM incurs an overhead for every tail call that involves differing protection domains even if the stack does not overflow. Hence we decided to lazily compress the stack.


— John
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://mail.openjdk.java.net/pipermail/mlvm-dev/attachments/20130718/3a7b0933/attachment.html