Reasoning about continuations with control effects

We present a new static analysis method for first-class continuations that uses an effect system to classify the control domain behavior of expressions in a typed polymorphic language. We introduce two new control effects, goto and comefrom, that describe the control flow properties of expressions....

Full description

Saved in:
Bibliographic Details
Main Authors: Jouvelot, P., Gifford, D. K.
Format: Conference Proceeding
Language:English
Subjects:
Computing methodologies > Concurrent computing methodologies > Concurrent programming languages
Software and its engineering > Software notations and tools > Compilers
Software and its engineering > Software notations and tools > Formal language definitions
Software and its engineering > Software notations and tools > General programming languages > Language features > Control structures
Software and its engineering > Software notations and tools > General programming languages > Language types > Concurrent programming languages
Theory of computation > Formal languages and automata theory
Citations: Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:We present a new static analysis method for first-class continuations that uses an effect system to classify the control domain behavior of expressions in a typed polymorphic language. We introduce two new control effects, goto and comefrom, that describe the control flow properties of expressions. An expression that does not have a goto effect is said to be continuation following because it will always call its passed return continuation. An expression that does not have a comefrom effect is said to be continuation discarding because it will never preserve its return continuation for later use. Unobservable control effects can be masked by the effect system. Control effect soundness theorems guarantee that the effects computed statically by the effect system are a conservative approximation of the dynamic behavior of an expression. The effect system that we describe performs certain kinds of control flow analysis that were not previously feasible. We discuss how this analysis can enable a variety of compiler optimizations, including parallel expression scheduling in the presence of complex control structures, and stack allocation of continuations. The effect system we describe has been implemented as an extension to the FX-87 programming language.
ISSN:0362-1340
DOI:10.1145/73141.74837