(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.su...@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_______________________________________________
mlvm-dev mailing list
mlvm-dev@openjdk.java.net
http://mail.openjdk.java.net/mailman/listinfo/mlvm-dev
