Reasoning about continuations with control effects
Reasoning about continuations with control effects
复制标题
关于具有控制效应的连续性的推理
DOI：
10.1145/73141.74837
复制
发表时间：
1989
期刊：
影响因子：
--
通讯作者：
D. Gifford
中科院分区：
文献类型：
--
作者：
P. Jouvelot;D. Gifford
我们为一流的连续性提供了一种新的静态分析方法，该方法使用效果系统将表达式的控制域行为进行分类。我们介绍了两个新的控制效果，即goto和comefrom，它们描述了表达式的控制流属性。据说没有Goto效应的表达方式是延续的。据说没有效果的表达方式是继续丢弃，因为它永远不会保留其续回来以供以后使用。效应系统可以掩盖不可观察的控制效果。控制效应的声音定理确保效应系统静态计算的效果是表达动态行为的保守近似。
我们描述的效应系统执行某些以前不可行的控制流分析。我们讨论了该分析如何启用各种编译器优化，包括在存在复杂控制结构的情况下并行表达调度以及连续性的堆栈分配。我们描述的效果系统已被实现为FX-87编程语言的扩展。
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.