International Journal of Parallel Programming, Vol. 18, No. 1, 1989 Effect Analysis in Higher-Order Languages Anne Neirynck, 1,2 Prakash Panangaden, 1'2 and Alan J. Demers 3 Received July 1987; revised June 1989 When programs are intended for parallel execution it becomes critical to determine whether the evaluations of two expressions can be carried out independently. We provide a scheme for making such determinations in a typed language with higher-order constructs and imperative features. The heart of our scheme is a mechanism for estimating the support of an expression, i.e., the set of global variables involved in its evaluation. This computation requires knowledge of all the aliases of an expression. The inference schemes are presented in a compositional fashion reminiscent of abstract interpretation. We prove the soundness of our estimates with respect to the standard semantics of the language. KEY W O R D S : Effect analysis; alias analysis; abstract interpretation; parallel evaluation. 1. INTRODUCTION In the last several years, there has been substantial interest in the develop- ment of programming languages appropriate for parallel architectures. The basic design Conflict is that languages with simple semantics tend to use storage inefficiently, whereas programs written in languages that allow the programmer to use storage efficiently tend to be difficult to analyze. Thus, it is easy to detect potential parallelism in programs written in a pure func- tional language but, as data structures are modified incrementally, the entire data structure has to be recopied since there is no mechanism for expressing in-place updates. In a typical imperative language one can use Supported by National Science Foundation Grant DCR-8602072. Computer Science Department, Cornell University. 3 Xerox Parc, Palo Alto. l 0885-7458/89/0200-0001506.00/0 9 1989 PlenumPublishingCorporation 828/18/1-1 2 Neirynck, Panangaden, and Demers assignment statements to perform in-place updating of data structures but this produces side-effects, which makes parallelism difficult to detect. We develop a compile-time estimation scheme for determining whether an expression in an imperative language either uses or updates the store. Our scheme also determines the aliasing relations that may hold between program variables. In general, we can tell whether, given two expressions, the evaluation of one of them affects the evaluation of the other. Thus, we allow programs to be written in a semantically elegant functional style but, avoid the overhead associated with replicating data unnecessarily. The present paper is an elaboration of work reported earlier. (1) The language is a simply-typed higher-order functional language with a few imperative constructs. It has the essential control features of many modern typed languages such as ML. (2) Inferring runtime properties of higher-order languages involves confronting the problems associated with interprocedural flow analysis. Thus, the analyses we present subsume the analyses previously available in the literature. Our analysis is relevant to detecting parallelism in a higher-order language that permits side-effects. We intend that our estimation scheme be used in a paralMizing compiler for a higher-order language. There are several efforts aimed at developing such paralMizing techniques for For- tran-like languages, for example the recent work of Burke and Cytron, ~3) or Allen and Kennedy. (4) Alias analysis is an essential part of these schemes and has been the subject of study by itself. (5) The support of an expression is the set of non local variables involved in the evaluation of that expression. Support sets turn out to be the key to determining whether an expression is pure, i.e., its evaluation is side- effect free, or in general, whether two expressions can be evaluated independently. The computation of support sets requires knowledge of potential aliases of some expressions. Our approach is to define functions that assign to expressions estimates of their support and alias sets. This style of presentation for static analysis is often called abstract interpretation and was pioneered by the Cousots. (6'7) It allows one to describe a static analysis scheme in a fashion that makes clear the relation between the analysis scheme and the standard semantics. The phrase "abstract interpretation," however, has come to signify a particular format for presenting the relationship between the standard semantics and the abstract semantics, due to Mycroft and Nielson. (8'9) We do not use this particular format, though we clearly have the same view about how flow analysis relates to semantics. Interference analysis is a critical aspect of compilation for parallel architectures and there has been much published on it. (1~ In the last ten years, this work has focussed on the difficult aspects of such an analysis; Effect Analysis in Higher-Order Languages 3 namely interprocedural interference analysisJ H 13) The work cited is for first-order languages only and relies on knowledge of the calling pattern of procedures. Our investigations apply to higher-order languages where one does not know the call-graph but are confined to the case where there are no pointers or arrays. A very thorough treatment of aliasing for arrays in first-order languages can be found in Ref. 3. There has also been recent work on interference in languages with dynamic data structures ~14'15) that uses a different abstraction of the standard semantics. The most important precursor of our work is a paper by Reynolds,/16) in which he defined syntactic restrictions to eliminate interference in a higher-order language with call-by-name parameter passing. The soundness of this scheme was proved by Tennent. <17) Our scheme for estimating inter- ference is more precise, though more complicated. In the conclusion, we shall discuss this and other related work (18'19~ more closely. 2. THE L A N G U A G E A N D ITS S E M A N T I C S The language is a typed, functional language with a recursive defini- tion facility. To this core we add three imperative features: static allocation performed with the new construct, an assignment statement written el ~ e2, and a dereferencing construct ei". We use the word variable to stand for an identifier that denotes a storage location. To denote the value associated with the variable we use an explicit dereferencing construct, M'. Thus to increment x by 1 we write x *-xl" + 1. An expression can evaluate to a variable rather than to the value associated with the variable as in if true then x else y, assuming that x and y are global variables. In such languages, one can easily write complex expressions that have nontrivial aliasing behavior. We are not advocating the use of our conventions in a practical programming language. This is the abstract syntax for the language: e = c l x ] if e I then e 2 else e312x: t . e l e l ( e 2 ) letrec f l = 2xl : tl. el ..... f , = 2x n : tn. e, in e new x : r e f t in e lel ~- e21 el" l el; e2 The type system is defined inductively as follows: t = i n t I booll ref int [ref booll t ~ ~ t2 We do not have pointers or "structured types" or storable functions, although the first two of these are considered in Neirynck's thesis. ~z~ Notice that our type system has only finite types, i.e., no recursively defined types. The arrow construct is used for functional types, and the ref con- 4 Neirynck, Panangaden, and Demers struct for 1-values. The type of an identifier declared by a new has to be of the form ref t. There are no constraints on the syntax except the ones required by typechecking: the two branches of a conditional should be of the same type, functions are not storable items, and only one level of reference or dereference is allowed. These restrictions were chosen to sim- plify the analysis. Furthermore, because we have lexical scoping, 1-values cannot be exported outside their scope. This property can be detected statically by the methods developed here. Parameters are passed by value. When the parameter is a variable, as in e(x), we have what is called "call- by-reference"; to get call-by-value parameter passing, we write e(x~). The way we model the store is particularly important since the crux of our analysis is the determination of which expressions actually affect the store or depend on the store. It is usual to find that the denotational defini- tion of a programming language includes a model of the store and of storage management. We are assuming that when the denotational seman- tics makes reference to the store, an implementation of the language actually does manipulate the store. In other words, we are taking the denotational semantics as giving some aspects of the operational behavior. This goes against the spirit in which denotational semantics is ofter under- stood but in fact all the denotational definitions one may see in standard textbooks (21'22~ do have such operational significance. The denotational definition of a programming language is typically given in two stages. The first stage is a translation of the programming language into a semantic meta-language, usually some minor variation of the lambda-calculus. The second stage is an interpretation of this meta- language, usually in terms of domains. This is often not done explicitly, instead reference is made to the literature on semantics of the lambda- calculus. The point of significance for us is that the semantic meta-language also comes with an operational semantics, though this is rarely made explicit. It is the operational semantics of the meta-language which we are using as the basis of our inference. Our semantic meta-language is the typed lambda-calculus with certain constants to represent the store and store-manipulation functions. We shall express the store manipulations in terms of a semantic function, written Ms, so that we can follow the com- positional style of denotational definitions. The store is modeled as a partial function with finite domain from locations to values. S t o r e = L o c --* Val We need a notation to express the restriction of that function to a subset of the locations. store I L where L ~_ L o c Effect Analysis in Higher-Order Languages 5 Given a store, A l l o c a t e returns a store and the address of the newly allowated space. The new store must coincide with the old store over all addresses except the one just allocated (Aciom Ia). We also require that the new address is not already allocated (Axiom Ib). Allocate:Store ~ Store x Loc The following two functions are used to perform reading and updating. Update: S t o r e x L o c x VaI -~ S t o r e Eval: S t o r e x L o c ~ Val Axiom I if ( newstore, a d d r e s s ) = A l l o c a t e ( s t o r e ) then (a) newstore [Loc.{ aaa~es~} = store I Lo~+d~r~} (b) Eval(store, address) = 3_ Eval( newstore, address) = e m p t y Given a store and an address, D e A l l o c a t e returns the same store, with the address deallocated. The remainder of the store in unchanged. D e A l l o c a t e : Store x L o c ~ S t o r e Axiom II if newstore = D e A l l o c a t e ( s t o r e , address) then newstore l Loc_{~aaress} = store ]roc-{~adress) Axiom III Update(store, address, value) [Loc-~aaa.... ~ = store [Loc-~adaress } Because /-values are not stored, the other usual axioms about Update and E v a l are not required. The Semantics Our denotational semantics is given in terms of domains and semantic functions from the expressions to the appropriate semantic domains. We 6 Neirynck, Panangaden, and Demers use a different domain for each type and there is a corresponding semantic function for each type as well. We will almost always omit the type labels as most clauses of the semantic functions are either the same at all types or are part of a semantic function that has a type that is clear from context. The basic semantic domains that we use in our denotational are B o o l , N a t and L o c ; these are the usual "flat" domains of truthvalues, integers and locations respectively. We also need domains to represent high-order constructs. Evaluating a function application will return a value and, in general, modify the store. We use a pair construction to package together both these effects. Tradi- tionally one writes down recursive domain equations to define a domain of functions. It is now becoming more customary to write down the semantics of a typed language in terms of a family of inductively defined domains rather than a single recursively defined domain. We adopt the latter approach. The higher types look like t--* t'. We define V a l ( t - ~') = [ ( V a l t x S t o r e ) ~ ( V a l t ' x S t o r e ) ] as the semantic domains associated with the higher types. The constructor X--* Y is the domain of continuous functions from X to Y ordered pointwise. Whenever X and Y are Scott domains (consistently-complete co-algebraic complete partial orders), so is X--, Y. Since our base domain is a Scott domain it follows that all the semantic domains are as well. We need the domain structure in order to give meaning to recursive constructs as fixed-points. The denotational semantics is defined in terms of a pair of semantic functions called Mo and Ms. [Strictly speaking, we really have a type- indexed family of pairs of semantic functions, however, the definitions are very similar at each type so we will not make this explicit and speak as if we had a single pair of semantic functions and a single semantic domain.] The first one gives the value of an expression while the second describes how the store is modified. This is just a notational variation on the ordinary semantic definitions one sees in textbooks. This notation is par- ticularly convenient for our discussion since our principal concern is how the store is affected by constructs in the language. We define environments as mappings of identifiers to elements of the appropriate domain. We use superscripts whenever we wish to make the types explicit. The arities of the semantic functions are: M e t : E x p t ~ E n v --* S t o r e ~ gal t and Ms':Exp t ~ Env ~ Store ~ Store Effect Analysis in Higher-Order Languages 7 The domain Env consists of functions from identifiers to values of the appropriate type. In order to be completely rigourous about the type of Env there needs to be a single domain of semantic values constructed by forming a disjoint sum of all the semantic domains; we shall, however, ignore this from now on. A full definition of the semantics is given in the appendix; we comment on a few clauses here to illustrate the notation and style of semantic definition. Met[new x :ref t in ~env store = Me~e~env' store' M~ [[new x: ref t in eli env store = store'" where (address, s t o r e ' ) = Allocate(store) env' = env[ x *-- address] store" = M s ~e~ env' store' s t o r e " = DeAllocate(store", address) This semantic clause shows how the store model is used to define the meaning of the new construct. Deallocation occurs when the scope of the new declaration is exited. Note that declaring a variable changes the store and not just the environment. The following clauses define the two other imperative features, assign- ment and dereferencing. Me[tel ~ e2~env store = value Ms[tel ",-- e2~env store = Update(store", address, value) where address = M e [[e11env store store' = M s [ [ e ~ e n v store value = MeEe2~env store' store" = IVls[[e2~env store' Me[[e~env store=Eval(store',address) Ms[[e~env store=store' where address = Me[[e~env store store' = M s [[e~env store 3. T H E P R O B L E M OF E S T I M A T I N G SIDE-EFFECTS In this section, we discuss the problems associated with estimating side-effects in a language with higher-order functions; 1-valued expressions, 8 Neirynck, Panangaden, and Demers and local variables. We will argue that, to solve this problem, one needs to determine support sets and aliases. In other words, a simple approach, based on using information about whether the subexpressions are side- effect free, will not work. An expression is said to be p u r e if its evaluation is independent of the values of any global variables. The notion of global variable is relative to a given expression, and a pure expression may contain impure subexpres- sions. An example of this is new x : r e f i n t in x ~ 3. Unfortunately, the reverse situation can also arise: an impure expression may be built up out of pure subexpressions. Thus a syntactic scan for occurrence of imperative constructs is not enough to make an accurate estimate of purity. A lambda-abstraction is always pure because any potential effects occur only d u r i n g application. For instance, an expression like 2 x : i n t . y ~ x is pure, but its application will cause a side-effect; if this expression is applied, even to a pure expression, the result expression is impure. The main problem with side-effect determination in a higher-order language is that we need to maintain enough information so that we can tell whether a particular application causes side-effects. To complicate matters further, this may depend on the arguments. For example in 2i: int. 2f: int ~ int. 2g: int ~ int. if odd(i) then f else g we have a function taking functional arguments and returning a functional result. The result may or may not yield impure applications depending on the functional arguments f and g. Not all applications of a function with potential side-effects actually do produce a side-effect For example, if the global variables involved in the side-effect are all captured by their enclosing declarations, the resulting expression is pure. This is the case with new x : r e f &t in let f = 2y :ref &t. y ~ 3 in f ( x ) Thus the data-flow analyses for purity which suffice for first-order languages would be inadequate to the task at hand. (3'11-13) These analyses rely on knowing the call-graph of procedures and this is of course impossible with a higher-order language. Weihl (13/ addresses the issue of functional parameters, but uses a language that is otherwise first-order. In order for our scheme to deem an expression impure only when global variables are affected, we must compute the set of global variables actually read or updated during evaluation of that expression. Consider the following two expressions: new x :ref int in x *-- 1 new x:refint in y *-- 1 Effect Analysis in Higher-Order Languages 9 Although the expressions are structurally very similar, the first one is pure whereas the second one is not. If we hope to distinguish between these two cases, we must actually know which variables are being affected by subexpressions, not just that the subexpressions do affect some variable. We call the set of global variables that are affected by or whose values affect the evaluation of an expression the support of that expression. An expression is then pure when its support set is empty, and two expressions interfere if their support sets are not disjoint. In more formal terms, we define a function to estimate the support set of an expression with respect to an environment. The support set is expressed as a set of "abstract" locations, a representation that is intended to avoid the problems associated with name conflicts in different scopes. In the case of recursive procedures, the environment is necessary to keep track of which incarnation of the procedure is intended when a variable name is used. We use the same device that is used in the standard semantics, i.e., an abstraction of the actual memory. Before calculating the support of an expression, we may need the aliasing behavior of some of its subexpressions. Consider for instance a dereferencing expression eT. The support of this expression is the support of e together with all the variables possibly aliased by e. A similar phenomenon occurs in assignment expressions. In order to simplify the presentation, we present these two estimates as if they were separate. It is essential, however, to realize that the two are being defined together. 4. AN E S T I M A T I O N S C H E M E FOR ALIASES This section describes a function A, that estimates the set of possible aliases of an expression. It is defined in a fashion similar to the semantic functions and, thus, yields a compositional inference scheme. This sort of definition is often called abstract interpretation, but our presentation does not follow the "orthodox' format of Mycroft and Nielson. Is) The next section contains a similar definition for the computation of support sets. The function A is similar to the semantic function M e restricted to the computation of 1-values. We define abstract alias domains associated with each member of the type hierarchy. Associated with each type t of we have a domain, Vale. The types Bool and Nat are associated with the two-point domain consisting of A_ and rvalue. The alias domain for the type Loc is ~(LocA), the powerset of the set of abstract locations ordered by inclusion. The set L o c A iS exactly like Loc but we view them as distinct in order to prevent one from confusing the bindings performed by A from the bindings performed by the semantic functions. Since the abstract domain is not finite 10 Neirynck, Panangaden, and Demers we need special care to ensure that A terminates on recursively defined procedures. The domain associated with t ~ t' is given by: Val~-~ r ) = [ Val~A ~ ( S t o m a ~ ( Stack A ~ Vale))] Store A is the set of abstract stores used in the computation of A. The role of StackA is to prevent repeated allocation of variables by recursively defined functions. This is explained later. The partial orders on the domains Val~ are defined as described earlier for the base types and pointwise in the higher types. Given an expression, an environment, a stack and a store, the function A maps the expression to an alias value. As with the standard semantics, the function A is really shorthand for a type-indexed family of functions. A :Exp ~ Env A ~ Store A ~ StackA ~ VaIA The alias environment is a mapping from identifiers to alias values. The store domain, StoreA, is greatly simplified compared to the standard semantic store: since the language does not allow the construction of dynamic data structures with pointers, the only function of the store required by the alias estimation is the ability to perform dynamic allocation of local variables. Thus the alias store is just a free list counter: StoreA=Int Our simplified allocation scheme allocates at most one location per instan- tiation of a variable, independently of its type. Furthermore, since variables cannot be exported outside their scope, deallocation occurs at exit of a block, and there is no need for the equivalent of M s in the definition of A. The alias stack, StackA, is used to detect whether the expression is evaluated in the context of a recursive call. If this is the case, the alias semantics will alias together all instantiations of a variable inside the recursive call. Stack A = Bool The alias stack is represented as a Boolean value; true means that the context may include a recursive call. When a function is applied, its closure will contain an abstract alias stack as well. The value of StackA is set to the disjunction of the two abstract stacks. Thus StackA will be true if the expression being evaluated may be in a recursive context. This device assures us that the evaluation of A terminates. We could have used a finite domain for LocA, in which case all fixed-point computations are guaran- teed to terminate. Unfortunately, if we did this, any recursive function that Effect Analysis in Higher-Order Languages 11 performed local allocation would saturate L o c A and the resulting informa- tion, though correct, would not be very useful. Thus A, evaluated on any given expression, essentially works on a finite domain but we cannot write down an a priori finite bound on the size of this domain that would suffice for all expressions. Since we do not know at compile-time which branch of the condi- tional will be executed, we collect alias information from the two possible executions. Our estimate therefore associates sets of possible aliases with an expression. The d o m a i n Loc of the standard semantics becomes N(LocA). The alias domains are lattices s o they have join operations defined on them. These are used in estimating the aliases of conditional expressions. The clauses for the computation of aliases are given next. The aliasing behavior of global identifiers is provided by an alias environment called ~, is the alias store and 0 is the alias stack. Constants and identifiers. A Ec ~c~ O = rvalue A E x ~ O = ~(x) We assume that there are no 1-valued or functional constants. The aliasing behavior of an identifier is determined by its binding in the alias environ- ment. Conditional and sequential evaluation. AEif el then e2 else e 3 ~ 0 = A[-e2~e~0 • A ~ e 3 ~ 0 A~el; e2~e~0 = A~e2~e~0 The least upper bound operation computes the possible alias as the union of the sets of possible aliases for each arm of the conditional. This clause introduces imprecision in the estimate. The value of el; e2 is e2, so its aliases are those of e 2. Abstraction and application. A~2x:t.e~c~O = 2u.2s.2q.A[[e~e[x *-- u]s(q or 0) A [[el (e2)]l e~0 = (A [[e1~c~0)(A [e2~~0)~0 The alias value of a lambda-term is a function of three arguments: the first one gives the alias value of the parameter, the second one is the alias store at the time of the call, the last one tells whether the expression is evaluated within a call to a recursive function. 12 Neirynck, Panangaden, and Demers Recursive functions. A ~letrec f l = e l - . . fn = en in e~ ~ 0 = A ~e~ ~'~0 where ~' =/fp(2/~. ~ [..., fi ~- A [ e i ~ true,...]) In a letrec construct, the bindings are computed first and then the body is computed in the resulting environment, which is defined as a least fixed point. Recall that allocation is performed only once when we have a recur- sive content, thus fixed-point computations converge. Imperative constructs. A Enew x: ref t in e~ ~ 0 = A We]]c~0 if 0 = true and x e dom(cQ f A~e~a[x ~ ~](~ + 1)0 otherwise AIel ~ e2~a~O = rvalue A[e~ ~a~O = rvalue In a nonrecursive context, a new variable is aliased only to its location, and the free list counter is incremented by one for the scope of the declaration. In a recursive context, a variable is allocated once, and all further instantia- tions of that variable will be aliased to that same location. The result of an assignment or of a dereferencing is a r-value, and thus their values in the alias semantics are trivial. The intuitive justification behind our scheme for estimating alias sets should be clear and the resemblance to the standard semantics is manifest. We prove a soundness theorem in a later section. 5. E S T I M A T I N G THE S U P P O R T SET In this section we define a function S that provides an estimate of the support set of an expression. This estimate uses the function A. The two functions really are defined simultaneously; we are presenting them as separate only because we wish to discuss them separately. In the next section, we work out an example of the computation of A and S in which the computations are carried out simultaneously. The definition of the support domains Valts is similar to that of ValtA. As with aliases, we have a simple hierarchy of types starting with three ground types. Unlike with aliases, an expression at any higher type can have a nontrivial support set as having a potential additional side-effect when it is applied. Thus support set values need to be pairs. Specifically, we associate a domain Valts with each type t. The domain associated with the Effect Analysis in Higher-Order Languages 13 ground type is N ( L o c A ) x ground For a type t ~ t' the associated domain is ~ ( L o c A) • [ Vales ~ Vale] where the product of domains is not strict. The arity of S at type t is S ~:Exp --* Env s --* Vat's where Envs is the appropriate type of environments mapping identifiers to support values of the appropriate type. Here, the definition of the function S is given. We use subscripts if we wish to denote only the first or second components of a pair in Val's. Note, that when we use the function A we need the environment c~; we assume that this environment results from a simultaneous computation of A for the same expression as the one for which the action of S is being defined. Thus A and S are really computed in parallel. In order to simplify the notation, we use the infix symbol ':' to stand for application of elements of Val(s'~'') to elements of Val's. Thus s:s' means (s~ u s l • (s~(s')),, (s2(s'))~) To determine the effect of an application, we collect together all the loca- tions accessed during the evaluation of the function (sl), of its argument (S'l), as well as of the additional locations that may be accessed during the application itself (s2(s')) 1. The operator ':' associates to the left. We comment only on the clauses corresponding to the imperative constructs, which differ significantly from those for the case of the alias computation. In all clauses, it is worth noticing how the computation of subexpressions contributes to the first component of the support. In all the definitions here, we suppress the type annotations. Constants and identifiers. SEc~ p = (0, ground) S~x~ p = p(x) Conditional and sequential evaluation. S~if el then e 2 else e3~ p --- ( Sl~el~ p W Sl[e2]] p W Sl [e3~ p, S2~e2~ p ~ Sz[e3]] p ) S[e~ ; e ~ p = (SI[Fel~ p u Sj ~e2~ p, $2[e2~ p ) 14 Neirynck, Panangaden, and Demers Abstraction and application. S[[2x:t.e~ p = <0, 2u.S[[e~ p [x ~ u] > S[[e1(e2)~ p = (S[[e/l p) : (S[[e2~ p) This could also be written: ($1 ~el]] p w S ll-ez~ p ~ (($2~e1~ p)(S[[e2~ P))I, ((SzEeI~ p)(S~e2~ P))2 > Recursion. S[[letree f l = e x . . "fn = en in e~ p = S[[e~ p' where p' =/fp(27. p [ ' " , f~ +- S[[ei]17...] ) Here we know that the iteration terminates because A does and the support cannot be larger than set of variables computed by A. Once again termination is assured even though the abstract domain is infinite. Imperative Clauses. If we are not in a recursive context SF[new x : r e f t in eq] p = (Sl[[e]] p [ x ~ (0, g r o u n d ) ] - ~(x), S2~e~ p [ x ~ (0, ground)] ) If we are in a recursive context then, S ~new x :ref t in eli p = S 1~e~ p [x ~ (0, ground ) ] Inside the scope of its declaration, the support of a variable is just itself, or, more precisely, the location it denotes, which is given by a. On the other hand, the support of the entire block must not include the new variable since the scope of the variable ends when the block is exited, so we explicitly remove variables from the support computed for the body of the block within which they are declared. In removing it, we use the location computed by A. Since variables are allocated afresh when a block is entered there is no aliasing to worry about in using a to remove the loca- tion of x from the support. If we are in a recursive context then we do not remove c~(x) because we cannot be sure that x refers only to itself since we do not know that a fresh allocation occurred. This is again a conservative approximation. S~el ~ e2]] p = (Sl~el~ p k.) Sl[[e2~ i9 t..)A~el~o~(O, ground) S[[e~] p = ( S 1~e~ p ~ A[[e]]c~(O, ground) Effect Analysis in Higher-Order Languages 15 The support of the explicitly imperative constructs is partly a function of the aliases of some subexpressions. In particular, the support of an assignment expression is the union of the supports of the two sides of the assignment and of all possible aliases of the left-hand side of the assignment. Similarly, the support of a dereferencing construct includes the aliases of the dereferenced expression. If one wishes to distinguish between variables read and variables updated, the definition of S can be decomposed into two functions. The definitions of these functions are straightforward. The correctness of our inference scheme is already plausible, because of the correspondence between the standard semantics and the composi- tional scheme used to estimate support sets and aliases. 6. E X A M P L E S Consider the following expression: new a :ref int in let id = 2x :ref int. x in let eval = 2x :ref int. xy in id(a); eval(a) The alias set of id(a) should be the location of a, and its support set should be empty. On the other hand, the alias set of eval(a) should be empty, since it is an r-value, but its support set should be the location of a. As mentioned previously, the computation of aliases and support sets is performed simultaneously, so that the environments are updated in a consistent fashion. Here are the combined alias and support domains: ASt: Exp ~ EnVAs ~ StoreA --* Stack A ~ ValtAs ValtAs = Val ~ x Val~ x FVal~s Val ~ = { rvaIue } + ~ ( Loc A) + { func } Val ~ = ~ ( L o c A) F V a l ~ = { ground} FVal(Ats ")= ValtAs ~ StoreA --* StackA ~ Val~s An alias&support value (AS[e~p~O) is now a triple, the first two com- ponents are the alias and support sets of the expression; func is the alias constant for all functional expressions. The third component is ground if e is a nonfunctional expression, and a function otherwise. The clause defining the alias and support value of an application is: AS ~el(e 2 )~ p'~O = ~ alias, A S 2 [el~ p'~0 w AS2 [e2~ p'~O w support, result ) 16 Neirynck, Panangaden, and Demers where (alias, support, result } = (AS 3lie ~ p'~0) (AS ~[[e2~p'~0, I~, AS 3[ee~ p'~0 } ~0 The other clauses needed for the examples are: AS[xl p~O = p(x) AS~2x : t. el p~O = (func, O, 2u. 2s. 2q. AS~[e~ p Ix ~ u] s(q or 0) } AS ~new x :ref t in el p~O = ( AS 1[[eqlp'~'0, AS2 [[el p'('0 - {~ }, AS3 Ee~ p'~'0 ) where p' = p[x ~ ( {(}, 0, ground}] AS[[el ~- e21p~O = @value, AS2[eI~ p~O u AS2~e2~ p~O w AS1 [el~ p~O, ground} AS[et~ p~0 = ( rvalue, AS2~e~ p~O u AS1 [e~ p~O, ground} AS~el ; e2~]p~O = (AS1 ~ezl p(O, ASz[[el~ p~O u AS2[[e2]] p~O, AS3[[ezl p~O ) Going back to our example, we now evaluate it in a nonrecursive content (0 =false). The initial alias and support environment is empty. After the first line is processed, the environment contains the alias and support infor- mation associated with variable a, and the store contains one allocated address for a: p ' = [a ~ ({0}, 0, ground}] ~'=(+1=1 The alias and support information for the identity function id is: AS~id~ p'~'O = (fune, 0, )~u2s2q. u } For the evaluation function eval, we have: AS~eval~ p'~'O = (func, 0, 2u2s2q. ( rvalue, ul, ground}} Let us call p' the alias and support environment updated with the values for id and evaL We are ready to compute the effect of each application: effeet( id(a) ) = (AS3~id~ p'~'0)(AS1Ea~ p'~'O, O, AS3~-a]] p'~'O } ~'0 = (2u,2s)~q.u)(( {0}, 0, ground})~'O = ({0}, 0, ground} Effect Analysis in Higher-Order Languages 17 effect(eval(a) ) = (AS 3Eeval~ p'~'O) (AS1 ~a~ p'~'0, 0, AS 3~a~ p'~'O ) ~'0 = (2u. 2s2q. ( rvalue, u 1, ground) ) ( { 0 }, 0, ground) ~'0 = (rvalue, {0}, ground) Since the support of an identifier is the empty set, we immediately obtain: ASEid(a)~ p'O = effect(id(a)) = ( {0}, 0, ground) AS Eeval(a)~ p'O = effect(eval(a) ) = ( rvaIue, { 0 }, ground) For an example illustrating allocation of local variables, consider the func- tion modapply, a modified version of apply with a local variable. It is used to define mod eval, an abstraction of the dereferencing construct. The expression in the scope of variable a causes two calls to mod_apply, with two instantiations of local variable b, since we evaluate the expression in a nonrecursive context (0 = false). new a :ref int in let mod_apply = 2g :ref int --* int. 2x : ref int. n e w b :ref int in b ~ xT; g(b) in let mod-eval = 2y :ref int. mod_apply(2z : ref int. z'r )(y) in mod_apply( mod_eval)( a ) The effect of an application of mod_apply is summarized in the third line of the equality shown here. It says that the result is an r-value, that the support had included s2, a local variable (the set difference is not simplified for illustration purposes), and now includes (u2)~, the alias of the second parameter, and the side-effect of applying the first argument to the local variable: AS ~mod-apply ~ p~ O = <fune, ~, 2u 1.2sl.,~ql. (func, 0, 2u2.2Sz.2q2. (rvalue, {s2} - {s2}u(u2)l w ((ul)3( {s2},0, ground>(s2 + 1))2, ground))) Applying mod_eval also results in an r-value, but the support includes the aliases of the argument (and had included s3, the local variable created by the call to mod_apply). AS~mod_eva~p(O= (func, 0, 2u3.2s3.2q3.(rvalue, { s 3 } w ( u 3 ) l - { s 3 } , g r o u n d ~ When evaluating the main expression, the result is an r-value, and the 828/18/1-2 18 Neirynck, Panangaden, and Demers support set consists of a, but during execution also included the two instan- tiations of b, at addresses 1 and 2: A S ~ m o d apply(mod_eval)(a)~ p(O = (rvalue, ((({0} ~ {1 } ) - {1 })w { 2 } ) - {2}, g r o u n d ) 7. S O U N D N E S S OF THE ALIAS ESTIMATE In this section we state and prove a soundness theorem for the alias estimation. Informally, we show that the set of possible locations associated, by the function A, with an expression includes the locations associated with all possible aliases of the given expression. If there were no imprecision in the estimates, A would associate a single location with each 1-valued expression; the aliases of a given expression could then be deter- mined by finding all expressions mapped to the same location by A. The heart of the proof is a joint induction on the structure of terms in the language and on their types. In the proof, the induction on the type structure is nested inside an overall structural induction. The letrec construct requires a fixed-point induction as well. The estimation scheme would not converge if we applied it to an untyped language. We need a convenient notation for expressing application of higher- order expressions in the standard semantics. Since the language is not purely functional, every application involves stores being passed around appropriately. We define a notation that handles this automatically. We focus on denotable values, i.e., values in the semantic domain that are the denotations of expressions in the language, in a given environment. We recall the definitions of the semantic domains from Section 2. D e f i n i t i o n 7.1. For each type expression of higher type t--+ t', we define the domain V a U ~ r) as Val(t~ ") = Store ~ ( Valt --* ( Valt' x Store)). These domains are the domains of values. We define D' as D ' = Store ~ ( Val t x Store) These are the domains of denotable values. A denotable value, thus, has the form ,~, store. ( v , store' ) where v is a value and store' is a store. We write M~e~ env = 2 store. ( M e ~ e ~ e n v store, Ms~e~env s t o r e ) Effect Analysis in Higher-Order Languages 19 pairing together the two semantic functions. We also need a notation for applying two denotable values; the following definition encapsulates the effects on the store of evaluating the expression in the function position and the subsequent effect of evaluating the expression in the argument position. D e f i n i t i o n 7.2. Suppose that p is an element o f D (t~'') and q is an element of D '. We define p 9 q = 2s. [ ( p ( s ) h (q((p(s))2))z](q((p(s))2))l The expression p 9 q belongs to the domain D t'. A more readable definition uses "let" notation p 9 q = 2s.let <f, s'> = p(s) in let <v, s"> = q(s') in f(s")(v) This definition allow us to conceal the details of store manipulation when we apply denotable values to other denotable values. The standard semantics of application are written as M[Fe1(e2)~env = M~el~env * M~e2~]env We say that an alias or support domain and a standard domain correspond if they are of the same type. As is fairly standard, we use the term satisfy for the correctness property. The following definition says that a value from the alias domains, henceforth called an alias value, safely estimates the possible aliases if the set of identifiers associated with any location is included in the estimate of the set of identifiers that are aliased together. D e f i n i t i o n 7.3. For any a, an alias value of ground type, a is said to be safe for value d from the corresponding domain, with respect to the pair of environments < ~, env >, if, for any store s, (a # rvalue) ~ env l(d(s)l) ~_ {i e Id[~(i) c~ a # 0 } and (a = rvalue) ~ (d(S)l r Loc). If the type of a is t ~ t', then a is said to be safe for value d of the corresponding domain, if Va~ ..... an of appropriate type such that aa~(O...an~O is of ground type and for dx ..... dn of corre- sponding domains, with each ai safe for di, we have that aal(O...a,~O is safe for d . d~ * - . . dn; where ( is an arbitrary abstract store and 0 is an abstract stack. The definition of safety given here relates alias values with the denotable semantic values; we have not mentioned the syntactic entities of 20 Neirynck, Panangaden, and Demers the programming language as yet. The soundness theorem will take the form that, for a given expression, the value computed by the function A is safe for the value it denotes in the standard semantics. In order to state the theorem, however, we need to have some correspondence between the alias environments and the standard semantics environments. The following definition is essentially the pointwise extension of the safety property. Definition 7.4. An alias environment ~ and an environment env are said to correspond if, (i) any identifier in the domain of env is also in the domain of a and (ii) ~/x~ d o m ( e n v ) 7 ( x ) is safe for 2s. (env(x), s ) . The next lemma states that the safety relation is preserved by taking least upper bounds. From this it follows at once that the relation of corresponding environments is og-inclusive. Rather than showing this for the case of least upper bounds of directed sets we shall show it for least upper bounds of chains, which is simpler and equivalent. We begin with a simple lemma that states that safety is preserved by the ordering in the lattices of alias values. In the following proofs we will often apply an alias value at a higher type to values at lower type. Each one of these applica- tions involves an abstract store and abstract stack as well. We will omit these since they clutter up the notation. Thus, we will write expressions like aal .. "an when we mean aal(O...an(O. L e m m a 7.5. If a E_ a' are alias expressions of a given type, d is a value of a corresponding type, and a is safe for d in (~, env), then a' is also safe for d in (~, envy. ProoL At the ground type, a E_ a' is just a ~ a'. For the ground type then, it is clear that if a is safe for d and a E a', then a' is also safe for d. At higher types, suppose that a E a', and that a is safe for d in (c~, env). Let al,...,a, be chosen such that aai . . . a , is of ground type (by which we also imply that the types are such that the expression is well typed). Sup- pose that dl ..... d, are also chosen so that d , dl 9 ... 9 d, is of ground type and for each i, ai is safe for d~ in (c~, envy. By the definition of safety, aa~ ... a, is safe for d , d~ 9 ... d,. Since a E a', and the order is defined pointwise in the functional types, we have ( a a l . . . an) E (a'a~..a,), which means ( a a l . . . a , ) c _ (a'al . . . a , ) . Thus a ' a ~ . . . a , is safe for d , dx * . . . * d, also, but, since the a~ were arbitrary safe alias expressions, this means that a' is safe for d as well. | The following lemma is not very profound but it is essential in order to show that fixed-point inductions are justified. The crux of the argument is that chains are finite, so if there is a failure of safety with the least upper Effect Analysis in Higher-Order Languages 21 bound of a chain then this failure must have occurred at some finite stage in the chain. L e m m a 7.6. Suppose that (c~, env) are a pair of environments. Suppose that a~,..., ai,.., is a chain of alias values and that d~ ..... d; .... is a chain of values with each ai safe for the corresponding dg in (c~, env). Let a be the least upper bound of the ag and let d be the least upper bound of the d~. Then a is safe for d in (c~, env). ProoL Throughout this proof we shall say "x is safe for y" without mentioning the pair (e, env), which is always the pair we intend to refer to. First, we note that a is safe for all the di because of the previous lemma. Second, all the alias lattices are finite so the chain of alias value reaches its least upper bound at some finite point in the chain, call this value an. Thus an is safe for all the di. Suppose that an is not safe for d. This means that for some choice of k 1,..., k m and some store s, such that d . kl * ...*kin(s) is of ground type (and denotes a location), there is some identifier, say x, bound by env to d . k l . . . * kin(s) such that c~ does not associate x with a set of possible locations that intersects abl ...bin, where the bi are alias values selected to be safe for the corresponding ki. Consider the chain { d i * k l . . . , k m ( s ) [ i~Int}. Elements in this chain can only take on one of two values, a specific location, say l, or _1_.If it always stays at _L then so does d and any alias value is safe for it. If it reaches some nonbottom value, then it does so at some finite stage in the chain, say at step j. This means that an cannot be safe for dj, a contradiction since an was supposed to be safe for all the d~. | The soundness of our abstract interpretation for aliases is stated formally in the following theorem. We qualify the statement of soundness with the proviso that the evaluation of the expression actually terminates in the standard semantics and the alias estimate does not cause the finite locations to overflow. This does not mean that the evaluation of A may not terminate; alias computations always terminate, but soundness is only guaranteed when the evaluation of the actual expression terminates as well. This is when soundness matters, because one would not be interested in parallelizing nonterminating computations. T h e o r e m 7.7. re, env, pairs of corresponding environments, and V store, ~ we have, if Me[re~env store ~ A_ 22 Neirynck, Panangaden, and Demers and the abstract store does not overflow then A[e]]c~0 safe for M~e~c~0 Proof. The proof proceeds by structural induction on e. We assume a fixed store, store, and alias store, ~. We suppress the abstract stack except in the case of the allocation of local variables since it has no effect otherwise. The reader should consult the appendix for details of the standard semantics. e~x A~e~a~O=a(x) by the definition of A, and MeEe~envstore=env(x) by definition of Mo. Since c~ and env are corresponding environments, by hypothesis, a(x) is safe for 2s. <env(x), s). e = if el then e2 else e 3 We do this case by induction on the type structure. Suppose that e, e2, e3 are all of ground type. The case when e is an r-value is trivial since there is no interesting aliasing b e h a v i o r . Thus assume that e, e2, e3 are 1-valued expressions. By the definition of A, A [ e l ] ~ 0 is AEe2~(0 u A~e3~]~(0. By the definition of the safety property, if a is safe for a value v in a pair of environments, then any superset of a is also safe for that value in the same pair of environments. This means that A l [ e ~ ( 0 is safe for MEe2~env as well as for M~e3~env in the pair of environments <~, env>. In the standard semantics, the meaning of e is either the meaning of e2 or the meaning of e3; in either case, the alias estimate is safe. Suppose now that e, e2, e 3 are of type t ~ t ' . In the rest of this paragraph, whenever we say "x safe for y" we mean "x safe for y in the pair of environments <~, env>. Now let d4,..., d, be expressions such that the application M~e~env 9 d4... * d, is Well-typed and of ground type. Let the alias expression A [ e ~ ( 0 be a, and let ai stand for alias values that are safe for the respective di. By the structural induction hypothesis, and the definition of safety at the higher types, a2a4...an is safe for MWe2~]env * d4... * d, and similarly with e 3 and a 3 in place of e2 and a 2 respectively. The definition of A, at higher types, says that a = a 2 u a 3. The definition of u says that the order is defined pointwise from the order at the ground type, which is ordinary inclusion. In other words, aa4.., an = (a2a4 --- an) u (a3a4..- an) This means, as before, that a is safe for MEe2~lenv as well as for M[[e31lenv. Thus a is safe for M[[e~env. This argument illustrates how one carries the proof of safety from the Effect Analysis in Higher-Order Languages 23 ground type to the higher type. We will not repeat it in the later cases but will just give the argument at the ground type, which is where it is interesting. e - letrec fl = e 1 ' ' " f~ = e. in e' We need to show that the estimated alias value is safe, we do this by fixed point induction. - - base case: e n v o = e n v [ .... f i ~ • and aenvo = a e n v [ . . . , f i ~ • are corresponding environments. Since any alias value is a safe estimate for -l-o. By structural induction on e', the theorem is true when applied to e', envo and aenvo. - - induction step: We do not perform allocation in the abstract semantics if the stack is true, only if it is f a l s e . Assume the latter. Assume a e n v , 1 and e n v n _ 1 are corre- sponding environments. env , = env , _ 1 [ . . . , f i ~ M e ~ e i~env , - 1 s t o r e , . . . ] a e n v , = a e n v , _ l [ . . . , f i ~- A F e i ~ a e n v , - 1 ,...] Then by structural induction on ei, a e n v , and e n v , are corresponding environments. By fixed point induction, aenv' and env' are corresponding environments, and the result follows by structural induction. Suppose the stack is true, then a e n v , and a e n v , _ 1 are the same. e n v , results from perfor- ming new allocations, it will be the case that any identifiers possibly aliased in e n v , will have been possibly aliased in e n v , _ 1 already. Since aenv~ 1 makes a safe estimate for every identifier mentioned in e n v , 1 it will make a safe estimate for every identifier in e n v , as well. Thus a e n v , will correspond to e n v , . The rest of the argument is the same as shown before. e- 2x:t.e' Here we use the definition of safety at higher types. First we need an observation. Suppose that a is of type t ~ s and that d E D t ~ s . Let a' be safe for d ' for the environment pair (~, e n v ) , and assume further that a' is of type t while d' ~ D'. Then aa' is a l w a y s safe for d * d' in the environment pair (~, e n v ) i f f a is safe for d. Now consider a pair (~, e n v ) of corre- 24 Neirynck, Panangaden, and Demers sponding environments. We must show that AE2x:t.e'~e~O is safe for M~2x:t.e'~env in the pair (c~, env). Suppose that a' is of type t and that d ' e D t and that a' is safe for d'. By the definition of A and of the standard semantics we have the following equations (A ~2x: t. e'~ a~O)a'~O = A Ee'l ct[x *-- a'] ~0 and (M[~2x:t.e'~env) , d ' = 2s.M[e'~env[x ~ (d'(s))l](d'(s))2 Since a' is safe for d' and (~, env) are corresponding environments, we know that c~[x~a'] and e n v [ x ~ (d'(s))l] are also corresponding environments. By the structural induction hypothesis, therefore, AFie'~[xw-~a']~O is safe for M~e'~env[x*--(d'(s))l](d'(s))z. Thus, we have that (A[2x:t.e'~O)a'(O is safe for (M[2x:t.e'~env),d' for any choice of ~ and with any pair a' and d' with the a' safe for d'. In view of this observation, this means that A[[e~c~0 is safe for M[e~env. e=el(e2) The proof of this case is trivial given to the previous observation. The structural induction hypothesis says that, given a pair (c4env) of corre- sponding environments, A[[ell~0 is safe for Mor(e~lenv store and A[re2~,~0 is safe for Me~ez~env store' in the pair of environments. The definition of safety, and our observation, allow us to conclude immediately that (A [Fe~~ct~0)(A [[e2~c~0 )~0 is safe for (M[Fel~env) *(M[gez~env) The first term is A[Fel(e2)~c~0 and the second is MEel(e2)]]env. e = n e w x : r e f t in e In the absence of a recursive context it is sufficient to show is safe for e n v [ x ~ address]. Since c~ and env are corresponding environ- ments, all that is left to prove is that ~(x)= {l} is safe for 2s. <address, s). Since x is not of a functional type, only the ground case need be con- Effect Analysis in Higher-Order Languages 25 sidered. Now, from the store axiom I(b), we know that env-l(address) is just {x}. In order to satisfy the safety property we need to check that ~[x ~ { / } ] ( x ) ~ {l} ~ 0 which is immediate since ~[x ~ { / } ] ( x ) = {/}. The case when we have a recursive enviroment is trivial because we are aliasing more variables together. Suppose that we have a recursive con- text then ~(x) will denote the same abstract location, say l, for all the instances of x in the standard semantics. In particular env ~(address) is included in ~-l(x). e~el ~-- e 2 In both the standard semantics and the aliasing semantics, the meaning of an assignment is that of its right-hand side. So, by the structural induction hypothesis applied to e2, the safety property remains true. e=_e'~ A 1~ e ' ~ O = rvalue Recall that the typing discipline enforces that e be an r-value. Therefore, in the standard semantics, e cannot be equal to any address. e~el;e 2 By routine structural induction. | 8. S O U N D N E S S THEOREM FOR S U P P O R T SETS In this section we state and prove a soundness theorem for our sup- port set estimate. This theorem says that the evaluation of an expression depends solely on the values of variables in its support set and, in addition, does not affect the store outside that set. As for aliases, soundness can only be guaranteed when the evaluation of the original expression terminates. The computation of S always terminates. We will need to refer to portions of the store. The notation storelL means the portion of the store restricted to L, where L is a set of locations. Since stores are functions from locations to values, we are using the usual notation for restricting functions. The notation/7, means the complement of L with respect to Loc. As for aliases, we define safety at ground types, and then extend the definition to the higher types. D e f i n i t i o n 8.1. Suppose that s is a support value of ground type that and m is a denotable value of the same type. Let (e, env) be a pair of environments and let S = e n v ( {x ~ Id[~(x)c~sl va0}) 26 Neirynck, Panangaden, and Demers We say that s is safe for m with respect to the environments (c~, env) if V store, store'.store[ s = store'[ s (i) (m(store))l = (m(store'))l (ii) (m(store))2[s= (m(store'))2[s (iii) (m(store))2[~=store[ The set S has a complicated definition; it stands for the set of actual locations that s~ estimates as being accessed by m. In order to go from the "virtual" locations represented in the abstract "semantics" to the real locations, we need the alias environment ~ to take us to a set of identifiers and the actual environment env to take us to actual locations. We extend this to higher types as follows. We use the ' : ' notation introduction in Section 5. D e f i n i t i o n 8.2. Suppose that s~ Vales~' and m is a denotable value of the same type. Let (p, a, env) be a triple of environments. Let S be defined as before. We say that s is safe for m with respect to (p, ~, env) if, s is safe for m in exactly the sense shown previously and, in addition, if for any sequence of values, Sl,...,s, from Vals such that s : s l : . . . : s , is of ground type and such that ml ..... m , are denotable values of appropriate types with each si safe for e i with respect to (p, ~, env) we have that s:s~ ...: s, is safe for m 9 ml * . . . * m , with respect to (p, ~, env ). N o w we define corresponding environments as follows. D e f i n i t i o n 8.3. A triple of environments (p, ~, env) are said to correspond if Vx ~ dom(env).p(x) is safe for fls. (env(x), s ) with respect to the given triple. The proof that the relation is ~o-inclusive follows in the same way as for aliases. T h e o r e m 8.4. Suppose that (p, ~, env) are a triple of correspond- ing environments. For any expression e, SEe~ p is safe for M[e~env, with respect to (p, ~, env) provided that M[e~env is not I . Proof. The proof of the theorem proceeds by structural induction on e. e~-x This follows immediately from the definition of corresponding environ- ments. Effect Analysis in Higher-Order Languages 27 e ~ el;e 2 Recall that M~el; ez~env = )~ (M~We2~env(M~el~env store), M,We2~env(M~el~env store)> and that S~el; e2]]p = ((S1Wel~ p) u (S1We2~p), S2[[el~p> In this case S = env({xl~(x) n (81 ~el~ p t.3 S 1~e2~ p) -~ 0 }) We define 31 = env({x I ~(x) n S, [[ex~p :~ 0} ) and $2 = env( {x[ ~(x) c~ S1H-e2~p :~ 0 } ) Let store, store' be stores that agree on S. Then, since $1 and $2 are contained in S, they certainly agree on Sx and $2. Thus the properties (i), (ii) and (iii) follow immediately by the structural induction hypothesis. Now we need to consider higher types. Let s (1).--s (k) be a sequence of support values and m (~)...m (k) a sequence of denotable values with each s (i) safe for m (i) with respect to the triple of environments. Consider the following calculation: S~el ; e2~ p: s(1): ... :s (k) = ((S1Fel]] p)t3 ($1~e2~]p) , S2[Ve2]]p>:s(1):... :s (k) = ( (Sl[-el~ p) w ($1We2~p) w s~1) w (($2~e2~ p)(s(1)))l, ((S2~e2~ p)(s(l~))2 > : s ~2) : . - - : s ~k~ = ($1Wel~ p w (S[[e2~ p : s(1): ... :s~k))l, (S~e2]] p: s(1): .-- :s(k))2 > Now we use the structural induction hypothesis to conclude that each half of the last union is safe for the corresponding denotable value. e = if e l t h e n e2 e l s e e 3 This case is also a routine structural induction, very similar to the pre- ceding case. e- letree fl = el... f . = e . in e' We have already shown, in the proof of the last theorem, that ~, defined as a least fixed-point, gives rise to a pair of corresponding environments. 28 Neirynck, Panangaden, and Demers Therefore, in this case, the c~ environment can be ignored. By fixed-point induction: - base case: - e n v o = e n v [ .... f i ~ _l_o , . . . ] and p 0 = p r .... ~.~-- / V=ts,...] are corresponding environments since e n v and p were. By the structural induction hypothesis, S ~ e ' ~ p o is safe for M ~ e ' ~ e n v with respect to <Po, envo ). - induction step: - Assume p , _ 1 and e n v y _ 1 are corresponding environments. e n v ~ = e n v y _ 1[ .... f i ~ n ~ [ e i~env , _ t s t o r e .... ] and p.=p._,[ .... f,~S~e,~p. ,,...] Then by the structural induction hypothesis applied to ei, p , and e n v , are corresponding environments. By fixed-point induction, p' and e n v ' are corresponding environments. By structural induction on e', the safety properties hold. If we are in a recursive context then the estimate is even more conservative and the soundness is immediate. e= ~x:t.e ' In this case we have an expression that is not of ground type. Informally, the effect of evaluating a lambda-expression is to build a closure, the store is not affected. Showing (i), (ii) and (iii) is trivial, since Ms[-Ax:t.e'~env s t o r e = s t o r e according to the standard semantics. To show safety at high type, we use the definition of the semantics. M e [ 2 x : t. e'~ e n v s t o r e = As. 2 v . M {e'~ e n v [ x *-- v ] For the function S we have the following equation S[[2x:t.e'-H p = <0, 2 v . S ~ e ' ~ p [ x ~ v ] } Now we note that the modified environments in which the body e' is evaluated, in the semantics and the calculation of S, are corresponding environments. Thus by the structural induction hypothesis applied to the subterm e' the safety properties hold. Effect Analysis in Higher-Order Languages 29 e=el(e2) We must show S~el(e2)~p is safe for M~el(e2)Ienv. First, we verify the three conditions in Definition 8.1. Condition (i) states that, if store and store' agree on S then, (MWel(e2)~env store)l = (MEe1(e2)Henv store')i. Using the definition of the semantics, we can write this equation as ( f h store2) = ( f ' h ' store'2) where f = M ~ e l l e n v store, h = M~Ee2~env store1, store 1 = M ~ e l ~ e n v store, store2 = M~Ee2~env store1 and the primed versions are the same with store' used instead of store. The set S in this case is S = e n v ( {x[c~(x) c~ (Sa~el~p w S l ~ e 2 ~ p w (S2~el~PS~e2~P)1) ~13 } Let 31 env( {x [ a(x) ~ $1F-el~ p r 13} ~- $2 = env({x I c4x) ~ S~ [~e2~p r 13) and S 3 = env({x I ~(x) n ((S2~e~]] p)(S~-e2~ P))I 4: 0} From the structural induction hypothesis, and from the fact that S~, $2, $3 --- S we have f = f ' , h = h' and store2 Is = store'zrs. Thus condi- tion (i) is verified. Similar arguments apply to show that conditions (ii) and (iii) are met. To show safety at higher types we use the definitions of 9 and :. Suppose that we have a sequence of safety values s(1)...s (kl and of denotable values m (1). ..m (k) with each s (i) safe for rn (i). Then we need to check that (S~el(e2)~ p): s (1) ... s (k) is safe for the corresponding expression expressed in terms of the m values. The above expression is equal to (S~-ell] p) : (S~e2~ p): s(1): ... :s (k) Now we use the structural induction hypothesis to infer that (SEel~ p) and (S[[e2~p) are safe for MWel~env and M~e2-~env. From the definition of safety at higher types, this means that (S~el~ p): (S~e2~ p): s(1): ... :s (k) is safe for (M~el~env) * rn ~1) * . . . * m (~) 30 Neirynck, Panangaden, and Demers Finally, we note that this is the same as (M~el(e2)~env) * m ~1) * . . . * m ~k) e = new x : ref t in e1 We first show that the effects of the declaration on the environments result in corresponding environments. Let env', c( and p' be the new environ- ments. By definition, env' = env [ x ~ address] p' = p [ x ~ (0, g r o u n d ) ] ~'=~[x~a] Since env, ~ and p are corresponding environments, and x is not of functional type, it is sufficient to show that (~, ground) is safe for 2s. (address, s ) . This however, is trivially true. Then condition (i) follows from the fact that 2s. (address, s ) returns address in any store and (ii) and (iii) follow from the fact that ,~s. (address, s ) is the identity on any store. Now the structural induction hypothesis gives us the fact that all the conditions are satisfied for the evaluation of the body. We only need to check that the exit from the block does not invalidate this. Suppose that S is the set of actual locations that may have been affected during the evalua- tion of el. On entry to the block, address gets allocated and, on exit, it is removed; no other location is added or removed from the store. Thus the set S of possibly accessed locations is not affected. In the estimate com- puted by S, the symbolic location a is removed on exit from the block. We know that address is the only actual address that could have been referred to by a so the removal of a will not affect the rest of the support estimate. For the case where the expression isbeing evaluated in the context of a recursive call we do not perform the deallocation on exit so the proof of soundness does not even require the argument of the last paragraph. e ~ e l +--- e 2 Since we do not have storable functions we only need consider the ground type. We establish the three safety properties (i), (ii) and (iii) from Definition 8.1. (i) According to the standard semantics, the value of this expression is the value of e2, so by the structural induction hypothesis applied to ez we see that condition (i) holds. (ii) Using the structural induction hypothesis on el, we see that M e ~ e ~ e n v store and Me[Fe~env store' are equal; let us call this value address. The effect on the store in either ease is that Effect Analysis in Higher-Order Languages 31 address gets updated by the same value, by part (i). Thus condi- tion (ii) is met. (iii) We note that by the structural induction hypothesis and from env( {x ]~(x) c~ ($1 [[el~ p) :# 0}) _ S we have M,~el~env store] s = store] ~. Similarly, from env( {X ]~(x) n ($1 [Ve2]]p) # 0 } ) _ S we conclude that Ms~e21env s t o r e l ] s = s t o r e l ] s = s t o r e ] s where store~ = Ms[[e~env store. By axiom III, the update opera- tion only affects the given address. The soundness theorem for aliases says that all possible values of this address are included in Al~el~x~0 which contributes to the definition of S. Thus outside S the store is not affected; i.e., condition (iii) holds. This completes the three conditions needed for the proof of this case. e=ely MeEel T~env store = Eval(storel, address) by the standard semantics, where store~ is the store resulting from the evaluation of el. Since we so not have storable functions we need only consider the ground type. If two stores agree on S, by structural induction, el will evaluated to the same value address in both. According to the definition of S, we have $1 ~e~ p = (S 1rel~ p) ~ (A 1[e,~a(0) By the soundness theorem on aliases, address ~ S. By the structural induc- tion hypothesis, applied to el, (ii) holds since the effect of el is the same as the effect of elT. Now, to show that (i) holds, we need to check that the equation Eval(storel, address) = Eval(store'l, address) holds, where store'~ is the store resulting from the evaluation of e~ in the store store,. This equation follows immediately from (ii) applied to ed~. Finally, we note that dereferencing does not modify the store, so, by the structural induction hypothesis applied to el, we immediately have (iii). This completes all the cases we have to consider. | 32 Neirynck, Panangaden, and Demers 9. C O N C L U S I O N In this paper we have produced a method for determining (approximately) whether the evaluations of two expressions are inde- pendent of each other. The presentation of our method uses the technique of abstract interpretation. We feel that using abstract interpretation allows one to present static analysis schemes in a compositional fashion. Further- more, the static analysis scheme which we describe brings an interesting and pragmatically relevant new problem within the scope of abstract inter- pretation techniques. The problem of determining side-effects has been studied for a fairly long time by workers developing flow analysis techniques. In particular, Banning, ~11) Barth, (12) and Weihl, (13) have studied interprocedural inter- ference analysis. The work of Barth addresses the problem of interference analysis in the presence of recursive procedures and aliasing but he does not consider higher-order functions or pointer variables. Banning also considers only first-order block-structured languages and does not allow 1-valued expressions. Weihl considers parameters of functional type, but his language is otherwise first-order. All three papers just cited use various flow-analysis algorithms rather than a compositional scheme. These techni- ques are based on doing flow analysis on the call-graph of the program. Thus they would not extend to higher-order languages where one cannot determine the call-graph in advance. Also, the correctness of their schemes is hidden in algorithmic details. The paper by Reynolds (~6) cited in the introduction is the starting point for our work and the work of Gifford and Lucassen (is) mentioned. In his paper, Reynolds defines a symmetric, decidable binary relation # between program phrases such that when P # Q, P and Q can be executed in parallel without interference. The elegance and simplicity of his scheme derive from the fact that with call-by-name semantics one can determine interference by examining whether the sets of free identifiers are disjoint. However, this can also lead to imprecision if the argument to a procedure is not used. Suppose that we have the following procedures: procedure use-n(p); procedure p; begin n := 0 end; and procedure use-m begin m := 0 end; Now it is easy to see that in Reynolds' scheme he would say that use-n Effect Analysis in Higher-Order Languages 33 (use-m) and m := 0 interfere whereas our scheme would realize that these two phrases were interference-free. We are able to do this by representing the support sets and alias sets for higher-order expressions as pairs with the second component of the pair storing information that keeps track of the possible aliases or interference that may result when the function is applied. This complicates the theory but is essential if one needs to do interference analysis for languages with call-by-value semantics. Furthermore, it is not clear how one could relax the restrictions in Reynolds' paper to handle pointers. Recently, Gifford and Lucassen (18'19~ related effect checking (as they call it) to polymorphic type checking. Their scheme incorporates the rele- vant information into the type system and their effect inference mechanism becomes part of the type inference mechanism. The programmer is expec- ted to divide the store into regions. The type inference mechanism checks that expressions manipulate disjoint regions and thus ensures interference freedom. The precision of the inference mechanism is now under the control of the programmer, which is an attractive feature. Their scheme, however, needs programmer supplied annotations in order to obtain useful interference analysis. The fundamental difference is that they have a mechanism for the user to express interference constraints via the type system whereas we have an automatic scheme which could be one phase of a paralMizing compiler. We are currently working on the questions left open in this paper. (2~ We removed the restrictions on pointers, recursive data types and dynamic allocation. The two semantic functions then require an abstract store and the cost of their computation increases accordingly. We are also developing heuristics to compute fixed points, with which we reduce the more than exponential cost of the current algorithms for fixed-point computations. ACKNOWLEDGMENTS We would like to thank Ken Birman for proofreading the manuscript. We have benefited from helpful remarks made by Carl Gunter, Paul Hudak, Dieter Maurer and especially Robert Tennent. A STANDARD SEMANTICS To keep the definitions simple, we do not explicitely give the cases dealing with nontermination. The reader should assume that the semantic functions are strict. 828/18/1-3 34 Neirynck, Panangaden, and Demers M~F(x3env store = env(x) M s ~x~ env store = store ~M~[[e2~env store' if val = true M~Iif el then e2 else e3q]env store = ~ M ~ e 3 ~ e n v store' if v a l = false = ~Ms~e2~env store' if val = true MJifel then e2 else e3~env store ~ Ms[[e3~env store' if v a l = false where v a I = M~Eel~env store store' = Ms~ea~env store M~[( 2 x : t.e~env store = 2s.;w. ( Me~ e~env[ x ~ v ] s, MsE e~env ] x ~ v ]s ) M s ~2 x : t. e~ env store = store M~Eel(ez)~env store = ( f store 2 h)l Ms[rel(e2)~env store = ( f store2 h)2 where f = Mo~el~env store h = Me~e2~env store1 store1 = Ms[[e l ]]env store store2 = Ms~e2~env store1 Me~letree f l = 2x~ : tl .e, ..... f n . . . . in e~env store = M~e]]env' store MsEletree f l = 2 x l : tl .e~ ..... f , . . . . in e~env store = Ms~e~env' store where env' = lfp(F) F: Ev --* Env = 2p .env[ .... f i ~ M~[[ )oxi:ti.ei~ P store,...] Me[Fnew x: t in e l e n v store = M~[[e']env' store' MsEnew x : t in e~env store = store'" where ( loc, store' ) = Allocate(store) env' = e n v [ x ~ loci store" = Ms~e~env' store' store"' = DeAllocate(store", loc) Mo[[e~ ~ e2]]env store = value MsEel ~- e2~env store = Update(store", loc, value) Effect Analysis in Higher-Order Languages 35 where loc = M e [ e l ~ e n v store value = Me~e2~env store' store' = Ms~el~env store store" = M s Ee2~ env store' M~EelT~env store = Eval(store', M ~ e l ~ e n v store) M s ~el ~ env store = store' where store' = Ms~el~env store Me~el ; e2~env store = Me~e2~env store' Ms[Fel ; e2~env store = Ms~e2~env store' where s t o r e ' = M ~ e l ~ e n v store REFERENCES 1. A. Neirynck, P. Panangaden, and A. J. Demers, Computation of Aliases and Support Sets, In Proc. of the Fourteenth Annual ACM Symp. on Principle of Programming Languages, pp. 274-283 (1987). 2. M. J. Gordon, A. J. R. Milner, and C. P. Wadsworth, Edinburgh LCF, LNCS 78. Springer-Verlag (1979). 3. M. Burke and R. Cytron, Interprocedural Dependence Analysis and Parallelization, ACM Sigplan Notices, 21(7):162-175 (1986). 4. K. Kennedy, J. R. Allen, and D. Callahan, An Implementation of Inter-procedural Analysis in a Vectorizing Fortran Compiler, Technical Report TR86-38, Rice University (1986). 5. K. Cooper, Analyzing Aliases of Reference Formal Parameters, In Conf. Record of the Twelfth Annual A C M Symp. on Principles of Programming Languages, ACM, pp. 281-290 (1985). 6. P. Cousot and R. Cousot, Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints, In Conf. Record of the 4th A C M Symp. on Principles of Programming Languages (1977). 7. P. Cousot and R. Cousot, Static Determination of Dynamic Properties of Programs, In Proc. of the 2nd Int'l Syrup. on Programming (1976). 8. A. Mycroft and F. Nielson, Strong Abstract Interpretation Using Power Domains, In Proc. ICALP 1983, Lecture Notes in Computer Science, 154:536-5447. Springer-Verlag (1983). 9. G. L. Burn, C. L. Hankin, and S. Abramsky, The Theory and Practice of Strictness Analysis for Higher Order Functions, Proc. of Programs as Data Objects, Springer Lecture Notes in Computer Science, Vol. 217 (1986). 10. A. J. Bernstein, Analysis of Programs for Parallel Processing, IEEE Transactions on Electronic Computers, EC-15(5):757-763 (October 1966). 36 Neirynck, Panangaden, and Demers 11. J. P. Banning, An Efficient Way to Find the Side-effects of Procedure Calls and the Aliases of Variables, In Proc. of the Sixth Annual A C M Syrup. on Principles of Program- ming Languages, pp. 29-41 (1979). 12. J. Barth, A Practical Interprocedural Data Flow Analysis Algorithm, CACM, 21:724-736 (1978). 13. W. Weihl, Interprocedural Data Flow Analysis in the Presence of Pointers, Procedure Variables, and Label Variables, In Proc. of the Seventh Annual ACM Syrup. on Principles of Programming Languages, pp. 83-94 (1980). 14. J. R. Larus and P. N. Hilfinger, Detecting Conflicts Between Structure Accesses, In Proc. of the SIGPLAN 88 Conf. on Programming Language Design and Implementation, pp. 21-34 (1988). 15. L. J. Hendren and A. Nicolau, Parallelizing Programs with Recursive Data Structures, In Proc. of the Third A CM Int'l Conf. on Supercomputing, pp. 205-214 (1989). 16. J. C. Reynolds, Syntactic Control of Interference, In Proc. of the Fifth Annual A C M Symp. on Principles of Programming Languages, pp. 39-46 (1978). 17. R. D. Tennent, Semantics of Interference Control, Theoretical Computer Science, 27:297-310 (1983). 18. D. K. Gifford and J. M. Lucassen, Integrating Functional and Imperative Programming, In Proc. of ACM Conference on Lisp and Functional Programming, pp. 28-38 (1986). 19. J. M. Lucassen, Types and Effects, PhD thesis, Massachusetts Institute of Technology (1987). 20. A. Neirynck, Static Analysis of Aliases and Side-Effects in Higher-Order Languages, PhD thesis, Cornell University (January 1988). 21. R. D. Tennent, Principles of Programming Languages, Prentice-Hall (1981). 22. M. J. C. Gordon, The Denotational Description of Programming Languages, Springer- Verlag (1979).
US