Maintaining Dynamic State: Deep, Shallow, and Parallel

Christopher T. Haynes
Indiana University

1 Richard M. Salter
Oberlin College

2

Abstract

In the presence of first-class continuations, shallow maintenance of dynamic bindings requires more than the traditional stack-based techniques. This paper provides correctness criteria for such dynamic environments, along with contrasting implementations. A store semantics provides the framework for our correctness criteria and presentation of deep- and shallow-binding implementations. The latter implementation is a new state-space algorithm, which is proved correct. A variation of the algorithm implements Scheme's dynamic-wind operation. Finally, a technique for maintaining dynamic state called semi-shallow binding is presented. This compromise between deep- and shallow-binding appears suitable for parallel systems. Applications include fluid binding of lexical variables and logic programming with first-class continuations.

1 Introduction

Dynamic state-management is required in many situations. Usually dynamic contexts are associated with control contexts, as with dynamic variables, fluid" assignment to lexical variables [3], and the dynamic-wind operation [2]. Logic variable binding is an example of dynamic state-maintenance that is not strictly associated with control (return with success does not undo bindings).

In this paper we address the problem of maintaining multiple dynamic contexts when their extent is not limited by a first-in-last-out discipline. Examples include OR-parallel logic programming systems and systems with first-class continuations that capture their dynamic context. The latter is implied by the combination of the call-with-current-continuation and dynamic-wind operations in Scheme. To be specific, we focus on the problem of maintaining dynamic variable bindings in the presence of first-class continuations, though our analysis applies with minor modification to a variety of other dynamic state-management problems.

We first present a store-semantics that provides a framework for dynamic-binding correctness criteria. A simple deep-binding implementation is presented in this context. Shallow binding yields more efficient lookup, but in the presence of first-class continuations, stack-based techniques cannot be used. State-spaces have traditionally been used to maintain shallow bindings when control is abruptly transferred to prior contexts by the invocation of first-class continuations [1, 4]. A statespace algorithm, simpler than those previously reported, is presented and proved correct in our formal context. A generalization of the state-space algorithm that implements the dynamic-wind operation of Scheme is also provided. Finally, we propose a semi-shallow binding technique that represents a cross between the deep- and shallow-binding with promise for use in parallel systems.

Figure 1 presents a state semantics for a simple language with constants, variable references, functions that dynamically bind their arguments, applications, and a call-with-current-continuation 1Computer Science Department, Lindley Hall, Bloomington IN 47401. e-mail: [email protected]. 2Computer Science Program, Oberlin OH 44074. e-mail: [email protected]. Research supported by NSF Grant CCR-9002132.