Home

Analyzing Logic Programs with Dynamic Scheduling

image

Contents

1. Herne It has auxiliary functions lookup Atom gt p Var gt Den gt Env gt p Env wmset AnnMSet gt yg Var gt Den gt Env gt p Env watom AnnAtom gt g Var gt Den gt Env gt gEnv and parametric functions Awake Atom AEgqns gt AEqns Adelay Atom gt AEqns AEqns Acomb AEgqns gt AEqns gt AEqns Arestrict Vars gt AEqns gt AEqns Aadd Eqns gt AEqns gt AEqns Awoken AnnMSet Eqns gt AEqns gt AnnMSet Adelayed AnnMSet gt Eqns gt AEqns gt AnnMSet The semantic and auxiliary functions are defined by P P Ae A A vars e lfp Q P e Q P dAe let V varsein _ B B V u vars A B d e A amp B defnp A V B nil W de e B L B Wde JB B W de e L L Wde L L if L Atom then A L else E L A A W d r D if Awake A 7 LAEqns then 7 A def U D else if Adelay A 7 LAEqns then lookup A W d 7 D else Adelay A 7 A pos U D U lookup A W d Awake A 7 D E 6 W d 7 D let7 Aadd 9 7 in if r LAEqns then else wmset Awoken D 0 7 W d z Adelayed D 6 7 lookup A W d r D let V vars A U vars D in let E d A Arestrict V r D in Acomb 7 7 D n D rename E V W wmset 0 W de e wmset A UD W de _ wmset D W de e watom A W de watom A def W d r D lookup A W d
2. canonical atom 8 Example Analysis We now present an example of the analysis algorithm s use In our example analysis we use simple modes to describe the equality constraints We will use this Table after 1st Iteration permute X Y Y X 0 0 Table after 2nd Iteration permute X Y Y X 6 0 delete U Y Z Y U Z 0 0 Table after 3rd and Final Iteration permute X Y Y X 6 0 delete U Y Z Y U Z 0 0 gt gt X 9 0 0 X 0 0 0 gt U Z 0 0 0 Analysis of permute X Y Y X 9 nil Table after 1st Iteration permute X Y X Y 0 0 Table after 2nd Iteration permute X Y X Y 6 0 delete U Y Z U Z Y 0 0 Table after 3rd and Final Iteration permute X Y X Y 6 0 delete U Y Z U Z Y 0 0 gt Ne Y 0 0 0 e is Analysis of permute X Y X Y 0 nil Figure 3 Example Analyses mode descriptions to analyze the state corresponding to query Q1 from Section 2 The domain used is similar to that of 28 and has been used for analyzing traditional Prolog A mode description for equality constraint 8 has the form Vena s Viree Waep where Vena is the set of variables that definitely grounds V ree is the set of variables that 0 leaves defi nitely free that is not instantiated to a no
3. r D watom A pos W d r D x D U lookup A W d Awake A z D Figure 2 Denotational Semantics Arestrict restricts an equality constraint description to a set of variables and should approximate the func tion restrict defined by restrict W 0 dw The definition also makes use of the function call rename E V W which returns a variant of the en vironments E which is disjoint from the variables W but which leaves the variables in V unchanged More exactly it returns p E where p is a renaming such that for all v V p v v and vars p E N W V 9 Equations are handled by the semantic function E The function call E 6 W d r D first adds the equality constraint to m and tests for satisfiabil ity If this succeeds it then wakes up the atoms in D and processes these The definition is paramet ric in the functions Aadd Awoken and Adelayed The function Aadd adds an equality constraint to an equality constraint description and must approximate the function add defined previously Awoken returns the multiset of atoms that will be possibly and definitely woken by adding an equality constraint to an equality constraint description and Adelayed returns the mul tiset of atoms that will possibly and definitely remain delayed Awoken must approximate diffwoken and Adelayed must approximate diffdelay where these are defined by diffwoken D 6 6 woken D woken D 6 8 diffdelay D 0 6 D wok
4. If L Atom there are two cases If delay L 0 holds it is reduced to G L D Otherwise it is reduced to B G 6 D for some L B defnp L vars S Note that denotes concatenation of sequences A derivation of state S for program P is a sequence of states Sg gt S gt gt Sn where So is S and there is a reduction from each S to Sj41 The above definition makes use of two parametric functions which are dependent on the systems or lan guage being modeled These are delay A 0 which holds iff a call to atom A delays with the equations 9 and woken D which is the subsequence of atoms in the sequence of delayed calls D that are woken by equations Note that the order of the calls returned by woken is system dependent We will assume that these functions satisfy the fol lowing four conditions The first ensures that there is a congruence between the conditions for delaying a call and waking it 1 A woken D 0 amp A DA delay A 6 The remaining conditions ensure that delay behaves reasonably It should not take variable names into ac count 2 Let p Ren delay A 0 amp delay p A p 0 It should only be concerned with the effect of on the variables in A 3 delay A 6 amp delay A ee ayo Finally if an atom is not delayed adding more con straints should never cause it to delay 4 If lt 6 and delay A then delay A 6 Although these conditions ca
5. International Con 2 3 4 5 6 7 8 9 10 11 12 13 14 15 ference on Logic Programming pages 40 58 University of Melbourne MIT Press May 1987 M Carlsson Sicstus Prolog User s Manual Po Box 1263 S 16313 Spanga Sweden February 1988 M Codish A Provably Correct Algorithm for Sharing and Freeness Inference In 1992 Workshop on Static Analysis WSA 92 September 1992 M Codish M Falaschi and K Marriott Suspension Analysis for Concurrent Logic Programs In K Fu rukawa editor Proc Eighth Int l Conf on Logic Pro gramming pages 331 345 The MIT Press Cambridge Mass 1991 M Codish M Falaschi K Marriott and W Winsbor ough Efficient analysis of concurrent constraint logic programs Proc of Twentieth Int Coll Automata Languages and Programming A Lingus and R Karls son and S Carlsson Ed LNCS Springer Verlag pages 633 644 C Codognet P Codognet and M Corsini Abstract Interpretation for Concurrent Logic Languages In S Debray and M Hermenegildo editors Proc North American Conf on Logic Programming 90 pages 215 232 The MIT Press Cambridge Mass 1990 P Cousot and R Cousot Abstract Interpretation a Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints Proc of the Fourth ACM Symposium on Principles of Pro gramming Languages 238 252 1977 P Cousot and R Cousot
6. Section 2 qsort the classical quick sort program using append app3 which concatenates three lists by performing two consecutive calls to append nrev which naively reverses a list and neg an implementation of safe negation us ing suspension on the groundness of the negated goal a simple test of membership in a list All benchmarks have been implemented in a reversible way so that they can be used forwards and backwards through the use of suspension declarations In the first test the optimizations to eliminate un necessary delaying were performed in two steps The first step was to eliminate and or relax suspension dec larations as indicated by the analysis The second step was to reorder the clause bodies provided the analysis indicated that it reduced suspension It is important to note that although the obtained orderings are already implicit in the results of the first analysis in order to eliminate suspension conditions that are redundant after the reordering a second pass of the analysis is sometimes needed The tests where performed with Sic stus Prolog 2 1 which is an efficient implementation of Prolog with a rich set of suspension primitives Due to lack of space we cannot include the code for the benchmarks and their resulting specialized ver sions However in order to give an idea of the accuracy of the analyzer and to help in understanding the effi ciency results we point out that in all cases but for permute
7. ZA delete X Y1 2Z1 Note that uppercase letters denote variables Clearly the relation declaratively given by permute is symmetric Unfortunately the behavior of the program with traditional Prolog is not Given the query Q1 permute X a b nil Prolog will correctly backtrack through the answers X a b nil and X b a nil However for the query Q2 permute a b nil X Prolog will first return the answer X a b nil and on subsequent backtracking will go into an infinite derivation without returning any more answers For languages with delay the program permute does behave symmetrically For instance if the above program is given to the NU Prolog compiler a pre processor will generate the following when declara tions permute X Y whenXorY delete X Y Z U whenZorU These may be read as saying that the call permute X Y should delay until X or Y is not a variable and that the call delete X Y Z U should delay until Z or U is not a variable Of course program mers can also annotate their programs with when dec larations Given these declarations both of the above queries will behave in a symmetric fashion backtrack ing through the possible permutations and then failing What happens is that with Q1 execution proceeds as in standard Prolog because no atoms are delayed With Q2 however calls to delete are delayed and only woken after the recursive calls to permute The
8. dataflow analysis algorithm We sketch an example instantiation of the generic analysis which gives information about groundness and freeness of variables in the delayed and actual calls Information from the example analysis can be used to optimize tar get code in many different ways In particular it can be used to reduce the overhead of dynamic scheduling by removing unnecessary tests for delaying and awak ening and by reordering goals so that atoms are not delayed It can also be used to perform optimizations used in the compilation of traditional Prolog such as recognizing determinate code and so allowing unneces sary backtrack points to be deleted improving the code generated for unification recognizing calls which are independent and so allow the program to be run in parallel etc Preliminary test results given here show that the analysis and associated optimizations used to reduce the overhead of dynamic scheduling give signif icant improvements in the performance of these lan guages Abstract interpretation of standard Prolog was suggested by Mellish 26 as a way to formalize mode analysis Since then it has been an active research area and many frameworks and applications have been given for example see 9 The approach to program analy sis taken here is based on the denotational approach of Marriott et al 25 A common implementation of abstract interpretation based analyses of Prolog is in terms of mem
9. dataflow analysis developed in this paper can be used to analyze this program with these queries In the case of Q1 it will determine that the overhead of delaying is not needed as no call ever delays if the second argument is ground Furthermore it will also determine that in all calls to permute the first argument will be a variable and the second argument will be ground and in all calls to delete the first and third arguments will be variables and the second will be ground This can be used to optimize the code for unification In the case of Q2 it will determine that all calls to delete from the second clause delay Furthermore that in all calls to permute the first argument will be ground and in all calls to delete when unification is performed the first and third arguments will be ground and the second will be a variable The reader is encouraged to check that this is indeed true Again this information can be used to optimize the code for unification parallelism or other purposes The benefits obtained from the optimizations made possible with such information are illustrated by the performance results presented in Section 9 We note that if a traditional mode analysis is per formed with the query Q2 it will ignore delaying and incorrectly generate the information that the third ar gument of delete is free which it would be in the non terminating execution that the analyzer would be ap proximating rather than ground 3 Ope
10. Analyzing Logic Programs with Dynamic Scheduling Kim Marriott Dept of Computer Science Monash University Clayton Vic 3168 Australia marriott cs monash edu au Abstract Traditional logic programming languages such as Prolog use a fixed left to right atom schedul ing rule Recent logic programming languages however usually provide more flexible schedul ing in which computation generally proceeds left to right but in which some calls are dynamically delayed until their arguments are sufficiently in stantiated to allow the call to run efficiently Such dynamic scheduling has a significant cost We give a framework for the global analysis of logic pro gramming languages with dynamic scheduling and show that program analysis based on this frame work supports optimizations which remove much of the overhead of dynamic scheduling 1 Introduction The first logic programming languages such as DEC 10 Prolog used a fixed scheduling rule in which all atoms in the goal were processed left to right Unfor tunately this meant that programs written in a clean declarative style were often very inefficient only ter minated when certain inputs were fully instantiated or ground and if negation was used produced wrong results For this reason there has been widespread interest in a class of second generation logic pro gramming languages such as IC Prolog NU Prolog Prolog II Sicstus Prolog Prolog III CHIP Pro
11. Comparing the Galois Con nection and Widening Narrowing Approaches to Ab stract Interpretation Technical report LIX Ecole Polytechnique France 1991 P Cousot and R Cousot Abstract Interpretation and Application to Logic Programs Journal of Logic Pro gramming 13 2 and 3 103 179 July 1992 S Debray Static Analysis of Parallel Logic Programs In Fifth Int l Conference and Symposium on Logic Programming Seattle Wasinghton August 1988 MIT Press S K Debray Static Inference of Modes and Data De pendencies in Logic Programs ACM Transactions on Programming Languages and Systems 11 3 418 450 1989 S K Debray QD Janus A Sequential Implementation of Janus in Prolog Technical Report University of Ari zona 1993 S K Debray and D S Warren Functional Computa tions in Logic Programs ACM Transactions on Pro gramming Languages and Systems 11 3 451 481 1989 M Falaschi M Gabbrielli K Marriott and C Palamidessi Compositional analysis for concurrent constraint programming IEEE Symposium on Logic in Computer Science Montreal June 1993 M Garcia de la Banda and M Hermenegildo A Prac tical Application of Sharing and Freeness Inference In 1992 Workshop on Static Analysis WSA 92 pages 118 125 Bourdeaux France September 1992 16 17 18 19 20 21 22 23 24 25 26 27 28 29 D Gudeman K De Bosschere and S K Debray jc An Effic
12. MSet D A def A in D and AnnMSet is ordered by Dj lt D3 iff all Dj C all D2 A def D3 C def Dj It follows that the annotated multiset D approximates the sequence D iff all atoms in D are in all D and every atom in def D is in D We will also be interested in describing equality constraints The analysis given in the next section is generic in the choice of description We require that the description chosen AEqns argns Eqns say satis fies Q A Eqns 0 LAEqns lt Q false where LAEqns is the least element in AEqns One example of an equality constraint description is the standard equality constraint description Eqns A8 0 Eqns in which constraints describe themselves More pre cisely the description domain is Eqns which is the set of constraint equalities with a new top element T Eqns is a complete lattice ordered by lt 6 36 false or 0 0 or 0 T The abstraction function is the identity function as the best description of a constraint is just itself 5 Denotational Semantics In this section we give a generic denotational semantics for programs with dynamic scheduling Correctness of the denotational semantics depends on the following re sults about the operational semantics The first propo sition means that we can find the qualified answers of a state in terms of its constituent atoms the second means that we can consider states modulo variable re naming the third that we can res
13. but that is beyond the scope of this paper A significant reduction in computation time is obtained from parallelism at least for the forward query This is illustrated in Table 2 which shows results from running the forward query with the optimized program under amp Prolog 19 a parallel version of Sicstus Prolog running on a commercial multiprocessor Times are in seconds 10 Conclusion We have given a framework for global dataflow anal ysis of logic languages with dynamic scheduling The framework extends memoization based analyses for tra ditional logic programming languages with a fixed left to right scheduling Information from analyses based on the framework can be used to perform optimizations which remove the overhead of dynamic scheduling and also to perform optimizations used in the compilation of traditional Prolog A potential application of the framework is for the analysis of constraint logic programming languages which handle difficult constraints by delaying them un til they become simpler Information from an analysis based on our framework could be used to avoid testing constraints for difficulty at run time or to move difficult constraints to points in the program in which they are simpler thus avoiding suspensions An analysis specif ically for this purpose has also recently been suggested by Hanus 18 References 1 M Carlsson Freeze Indexing and Other Implementa tion Issues in the Wam In Fourth
14. d to indicate if they are possibly delayed or if they are definitely delayed The use of multisets instead of sequences greatly simplifies the semantics with we be lieve little loss of precision This is because in most real programs delayed atoms which wake at the same time are independent while delayed atoms which are dependent will be woken at different times Second we give a generic global dataflow analysis algorithm which is based on the denotational semantics Correctness is formalized in terms of abstract interpre tation 7 The analysis gives information about call arguments and the delayed calls as well as implicit in formation about possible call schedulings at runtime The analysis is generic in the sense that it has a para metric domain and various parametric functions The parametric domain is the descriptions chosen to approx imate sets of term equations Different choices of de scriptions and associated parametric functions provide different information and give different accuracy The parametric functions also allow the analysis to be tai lored to particular system or language dependent crite ria for delaying and waking calls Implementation of the analysis is by means of a memoization table in which information about the calls and their answers en countered in the derivations from a particular goal are iteratively computed Finally we demonstrate the utility and practical importance of the
15. e analy sis with respect to the standard interpretation is ar gued by providing an approximation relation which holds whenever an element in a non standard domain describes an element in the corresponding standard do main We define the approximation relation in terms of an abstraction function which maps an element in permute X Y 61 nil where is X a nil Vv X U X1 delete U Y Z permute X1 Z 61 nil v delete U Y Z permute X1 Z 42 nil v where 4 is 6 AX U X1 permute X1 Z 62 delete U Y Z yY X1 nil Z nil 62 delete U Y Z N Z nil 63 delete U Y Z v delete U Y Z 84 nil v Y U Z 64 nil vw nil 5 nil where 3 is 62 A X1 nil where 8 is 63 A Z nil where 5 is 64 AY U Z Figure 1 Example Derivation the standard domain to its best or most precise de scription A description D a consists of a description domain D which must be a complete lattice a data domain E and an abstraction functiona gt D We say that d a approximates e written d Xe e iff e lt d The approximation relation is lifted to func tions Cartesian products and sets as follows e Let D1 a1 1 and D2 a2 2 be descriptions and F Di gt Dz and F gt amp be functions Then F x F iff Vd Di Ve E d Xa gt E d a F e e Let D1 a1 1 and D2 2 E2 be d
16. e analysis will termi nate iff there are a finite number of calls in the mem oization table and each call has a finite number of an swers This is true if the following two requirements are met The first is that for each finite set of variables W there are only a finite number of descriptions which de scribe some equality constraints Jy This is the usual requirement for the termination of memoization based analysis of standard Prolog The second requirement is that there is a bound on the size of the annotated multi sets in both the calls and the answers In this section we sketch two modifications to the analysis which ensure that only multisets of a bounded size need be consid ered albeit at some loss of accuracy In some sense this is a form of widening 8 however correctness does not depend on the semantics of the description domain but rather on properties of the program semantics The first modification allows us to only consider calls with annotated multisets of a bounded size Cor rectness depends on the following property of the oper ational semantics Proposition 7 1 Let P Prog and G D State If D D U D qansp G 0 D qansp G D 0 D m This means in the analysis that lookup can be modified to 1 remove annotated atoms D from the multiset of delayed atoms if it is to large 2 proceed as before and then 3 process D using a variant of B which handles annotated atoms The second
17. en D 6 A 6 Note that Adelayed may change the annotation of a delayed atom from def to pos and that Awoken returns a multiset of woken atoms which are also anno tated The woken atoms are handled by the auxiliary functions wmset and watom almost exactly as if they were a clause body the only difference is to handle the pos annotated atoms The standard denotational semantics Psta is ob tained by from the denotational semantics by instantiat ing AEqns to the standard equality constraint descrip tions and instantiating the parametric functions to the function they are required to approximate for instance Aadd and Acomb are both instantiated to add Using the four propositions given at the start of this section it is possible to show that the denotational semantics is correct Theorem 5 5 Let D Atom 0 Eqns A Atom and P Prog Then Psta P A 0 D qansp A nil 0 D where D G annMSet D E Using results from abstract interpretation theory it follows that analyses based on the semantics are correct Theorem 5 6 Let e Env A Atom P Prog Ife x 8 D P P A e x qansp A nil D m Actually the denotational semantics does not ex actly give the information a compiler requires for the generation of efficient code This is because we are pri marily interested in removing unnecessary tests for de laying and improving the code for unification There fore we must obtain inf
18. er allo cation optimizations can be performed for delayed goals finally space needs to be allocated for delayed goals until they are woken 1 Furthermore global dataflow analyses used in the compilation of traditional Prologs such as mode analysis are not correct with dynamic scheduling This means that compilers for languages with dynamic scheduling are currently unable to per form optimizations which improve execution speed of traditional Prologs by an order of magnitude 19 21 31 32 33 However it is not simple to extend anal yses for traditional Prologs to languages with dynamic scheduling as in existing analyses the fixed scheduling is crucial to ensure correctness and termination Here we develop a framework for global dataflow analysis of logic languages with dynamic scheduling This provides the basis for optimizations which remove the overhead of dynamic scheduling and promises to make the performance of logic languages with dynamic scheduling competitive with traditional Prolog First we give a denotational semantics for lan guages with dynamic scheduling This provides the se mantic basis for our generic analysis The main differ ence with denotational definitions for traditional Prolog is that sequences of delayed atoms must also be ab stracted and are included in calls and answers A key feature of the semantics is to approximate sequences of delayed atoms by multisets of atoms which are anno tate
19. eration in the analysis for this state description The result of the analysis is X Y 0 That is if calls to permute have their first argument ground and sec ond argument free the answers will ground the second argument Termination is achieved by restricting calls in the memoization table so that they have an empty annotated multiset Thus when the call permute X1 Z X1 U Y Z 6 delete U Y Z def is encountered when processing the second clause of permute first the call permute X1 Z X1 Z 0 0 is looked up in the table and then as this grounds Z the call delete U Y Z U Z Y 0 0 is looked up If the analysis is extended to give infor mation about call patterns it gives the results promised in Section 2 9 Performance Results We conclude with an empirical evaluation of the accu racy and usefulness of an implementation in Prolog of the analyzer presented Our first results show that in formation from the analysis can be used to eliminate redundant delay declarations leading to a large perfor mance improvement The last test illustrates how the analysis can be used to guide optimizations which are performed for traditional Prolog In this case we show how implicit independent and parallelism as detected by the analyzer can be used to parallelize the bench mark The benchmarks used for the evaluation were permute the permute program presented in
20. escriptions and dj d2 D x Dz and e1 e2 E1 x E2 Then di dz x e1 e2 iff di Xa 1 A d2 Xos 2 e Let D a E be a description and D C D and C E Then D x E if Ye 3d E D daxge When clear from the context we say that d approxi mates e and write d x e and let D denote both the description and the description domain In the analysis we will need to describe sequences of delayed atoms and sequences of woken atoms Because of the inherent imprecision in analyzing programs with a dynamic computation rule we cannot always be definite that a particular atom is in the sequence but may only know that it is possibly in the sequence Further it is difficult to keep track of all possible sequence orderings Hence we will describe atom sequences by a multiset of annotated atoms in which each atom is annotated with def if it definitely appears in the sequence and pos if it possibly appears in the sequence For example the multiset p X pos q Y def describes only the sequences p X q Y nil q Y p X nil and q Y nil More formally Ann def pos AnnAtom Atom x Ann AnnMSet gAnnAtom Let D AnnMSet Define def D to be the multiset of atoms in D that are annotated with def and all D to be the multiset of all atoms in D that is the atoms annotated with either pos or def The atom sequence description is AnnMSet aannmset Atom where AnnMSet is defined by Ann
21. eturns a description of those equality constraints which are de scribed by a and for which A will delay More exactly Awake and Adelay should satisfy Awake A 7 7 6A 7 7 delay A 6 Adelay A 7 x 0 7 A delay A Note that Awake A 7 argns implies m x 6 gt delay A 0 and Adelay A z LAEqns implies m x6 gt n delay A 6 The auxiliary function lookup is used to find the denotation of an atom which possibly does not delay The call lookup A W d 7 D returns the deno tation according to d of A with environment 7 D However there are complications because d only handles canonical calls Hence lookup must 1 restrict m to the variables in the call 2 rename the variables intro duced in the delayed atoms in the answers so that they do not interfere with the variables in W and 3 com bine the equality constraint description with that of the original call so as to undo the result of the restriction Lookup is defined in terms of the parametric functions Acomb and Arestrict Acomb combines two equal ity constraint descriptions and should approximate the function add defined by add 0 0 O0A0 The denotational semantics has semantic functions Prog gt Den Prog Den gt Den Lit p Var Den gt Env gt p Env Lit gt p Var gt Den gt Env gt p Env Atom gt p Var gt Den gt Env gt p Env Eqns gt p Var gt Den gt Env gt p Env
22. guage In programming languages which do not support a call by need semantics implementation is somewhat harder To avoid redundant computations the result of invoking atom A in the context of environment e should be recorded Such memoing can be implemented using function graphs The function graph for a function f is the set of pairs e gt f e e dom f where dom f denotes the domain for f Computation of a function graph is done in a demand driven fashion so that we only compute as much of it as is necessary in order to answer a given query This corresponds to the minimal function graph semantics used by Jones and Mycroft 23 However matters are complicated by the fact that we are performing a fixpoint computation and we must iteratively compute the result by means of the function s Kleene sequence This idea leads to a generic algorithm for the memoization based analysis of programs with dynamic scheduling The algorithm extends memoization based analysis for traditional Prolog The analysis starts from a call and incrementally builds a memoization ta ble This contains tuples of calls and their answers which are encountered in derivations from the initial call Calls are tuples of the form A m D where A is an atom D is a multiset of annotated atoms describ ing the sequence of delayed atoms and is an equality constraint description restricted to the variables in A and D An answer to a ca
23. ient and Portable Sequential Implementation of Janus In Proc of 1992 Joint International Confer ence and Symposium on Logic Programming 399 413 MIT Press November 1992 M Hanus On the Completeness of Residuation In Proc of 1992 Joint International Conference and Sym posium on Logic Programming 192 206 MIT Press November 1992 M Hanus Analysis of Nonlinear Constraints in CLP R In Proc of 1993 International Conference on Logic Programming 83 99 MIT Press June 1993 M Hermenegildo and K Greene amp Prolog and its Per formance Exploiting Independent And Parallelism In 1990 International Conference on Logic Programming pages 253 268 MIT Press June 1990 M Hermenegildo R Warren and S Debray Global Flow Analysis as a Practical Compilation Tool Jour nal of Logic Programming 3 4 349 367 August 1992 T Hickey and S Mudambi Global Compilation of Pro log Journal of Logic Programming 7 193 230 1989 J Jaffar and J L Lassez Constraint Logic Program ming In Proc Fourteenth Ann ACM Symp Principles of Programming Languages pages 111 119 1987 N D Jones and A Mycroft Dataflow analysis of ap plicative programs using minimal function graphs In Proc Thirteenth Ann ACM Symp Principles of Pro gramming Languages pages 296 306 St Petersburg Florida 1986 K Marriott H S ndergaard and P Dart A charac terization of non floundering logic programs In S K Debray and M Her
24. ll A x D is of the form x D where D is a multiset of annotated atoms describing the sequence of delayed atoms and 7 is an equality constraint description restricted to the vari ables in A and D Our actual implementation has two improvements which reduce the size of the memo ization table The first improvement is when adding an an swer to the answers of call to remove redundant answers and merge similar answers together Answers m D and m2 D3 are merged into the single answer m U m2 Di whenever D3 lt Dj The second improvement is to only consider calls modulo variable renaming Entries in the memoization table are canonical and really represent equivalence classes of calls and answers Another possible improvement which has not been implemented yet is based on the observation that de layed atoms which are independent of the calling atom can never be woken when the call is executed Such atoms need not be considered in the call as they will occur in each answer The exact definition of inde pendence is somewhat difficult as it really means inde pendence from any delayed atom which could be woken in the call 7 Termination Correctness of the denotational semantics Theorem 5 6 is not quite enough as it only guarantees partial correct ness of an analysis and of course we would also like the analysis to terminate Given that all calls to the parametric functions terminate th
25. log M and SEPIA etc that provide more flexible scheduling in which computation generally proceeds left to right but in which some calls are dynamically delayed un til their arguments are sufficiently instantiated to al low the call to run efficiently Such dynamic schedul Maria Jos Garcia de la Banda Manuel Hermenegildo Facultad de Informatica UPM 28660 Boadilla del Monte Madrid Spain maria herme fi upm es ing overcomes the problems associated with traditional Prologs and their fixed scheduling First it allows the same program to have many different and efficient oper ational semantics as the operational behaviour depends on which arguments are supplied in the query Thus programs really behave efficiently as relations rather than as functions Second the treatment of negation is sound as negative calls are delayed until all argu ments are ground Third it allows intelligent search in combinatorial constraint problems Finally dynamic scheduling allows a new style of programming in which Prolog procedures are viewed as processes which com municate asynchronously through shared variables Unfortunately dynamic scheduling has a signifi cant cost goals if affected by a delay declaration must be checked to see whether they should delay or not upon variable binding possibly delayed calls must be woken or put in a pending list so that they are woken before the next goal is executed also few regist
26. ly Hanus 17 gives an analysis for improving the residuation mecha nism in functional logic programming languages This analysis handles the delay and waking of equality con straints but does not easily extend to handle atoms as these may spawn subcomputations which in turn have delayed atoms In the next section we give a simple example to il lustrate the usefulness of dynamic scheduling and the type of information our analysis can provide In Section 3 we give the operational semantics of logic languages with dynamic scheduling In Section 4 we review ab stract interpretation and introduce various descriptions used in the analysis In Section 5 we give the deno tational semantics In Section 6 we give the generic analysis and in Section 7 we give modifications which ensure termination In Section 8 we give an example analysis Section 9 presents some performance results and in Section 10 we conclude 2 Example The following program adapted from Naish 30 illus trates the power of allowing calls to delay and the infor mation our analysis can provide The program permute is a simple definition of the relationship that the first argument is a permutation of the second argument It makes use of the procedure delete X Y Z which holds if Z is the list obtained by removing X from the list Y permute X Y X nil Y nil permute X Y X U X1 delete U Y Z permute X1 Z delete X Y Z Y X Z delete X Y Z Y U Y1 Z U
27. menegildo editors Logie Program ming Proc North American Conf 1990 pages 661 680 MIT Press 1990 K Marriott H S ndergaard and N D Jones Deno tational abstract interpretation of logic programs To appear in ACM Trans Programming Languages and Systems C S Mellish The automatic generation of mode declarations for Prolog programs Technical Report 163 Dept of Artificial Intelligence University of Ed inburgh Scotland 1981 K Muthukumar and M Hermenegildo The CDG UDG and MEL Methods for Automatic Compile time Parallelization of Logic Programs for Independent And parallelism In 1990 International Conference on Logic Programming pages 221 237 MIT Press June 1990 K Muthukumar and M Hermenegildo Combined De termination of Sharing and Freeness of Program Vari ables Through Abstract Interpretation In 1991 In ternational Conference on Logic Programming pages 49 63 MIT Press June 1991 K Muthukumar and M Hermenegildo Compile time Derivation of Variable Dependency Using Abstract In terpretation Journal of Logic Programming 13 2 and 3 315 347 July 1992 30 31 32 33 34 L Naish Negation and Control in Prolog LNCS 238 Springer Verlag 1985 A Taylor LIPS on a MIPS Results from a Prolog Compiler for a RISC Proc of the 7th International Conference on Logic Programming 174 185 1990 P Van Roy and A M Despain The Benefits of Global Dataflow Analysis for an O
28. mns R execution time for the program optimized by reordering the clause bodies as dictated by the analysis information and R S ratio between R and S columns In the P column In stands for non termination and Er stands for a wrong result or an execution error the fact that these cases appear shows the superiority of the version of the program with sus pension declarations Two sets of data corresponding to two lines in the table are given for each program the first one corresponding to forwards execution of the program the second to the backwards execution Note that in some cases the number of elements given as queries for forward execution are different from those used for the backward execution of the same pro gram The reason is the amount of time required by each query due to the different behaviour when run ning forwards one solution and backwards multiple solutions The results are rather appealing as they show that the optimizations based on relaxing and eliminating sus pension declarations using the information provided by the analyzer allows use of the more general version of the program written with suspension declarations with Name _Quey PT S SO sso R FR permute 8 In 272 240 Ii por 389 8 20 206 20 0s 20 103 Table 1 Analysis and optimization with delay Reversible quick sort 5000 elements Standard Prolog Suspension declarations after analysis and reorde
29. modification allows us to only consider answers with annotated multisets of a bounded size Now a delayed atom A can if it is woken only add constraints affecting variables in A and variables which are local to its subcomputation Thus in the analysis when we encounter an answer n D in which the mul tiset D is too large we can replace it by the answer x T pos where 7 approximates 0 A Ivars p T 9 A 6 Eqns and T pos is a special annotated atom which sig nifies that there are possibly delayed atoms of indeter minate name Note that T pos can never be woken With these two modifications the analysis will ter minate whenever the usual termination requirements for memoization based analysis of standard Prolog are met We can also use the idea behind the second modi fication to analyse modules The problem is that when analyzing a module in isolation from the context in which it will be used we have no idea of the delayed atoms associated with calls to the module However the delayed atoms can only affect variables in the ini tial call Thus by taking the downward closure of the initial call we are assured to obtain correct informa tion about the calling patterns regardless of the atoms delayed in the actual call Another approach to ensure termination would be to approximate the delayed multiset of atoms by a star abstraction 4 in which variants of the same atom are collapsed on to a single
30. n be relaxed they sim plify the analysis presentation and are met in existing systems and languages The declarative semantics of a program is in terms of its qualified answers Consider a derivation from state S and program P with last state G 0 D where G nil It is successful if D nil and it flounders otherwise We say the tuple 6 D is a qualified an swer to S It is understood as representing the logical implication Avars s D A 0 S For this reason we regard qualified answers 6 D and 0 D to S as equivalent if X DAI o gt D A 6 vars 8 vars S In particular qualified answers y and y are regarded as the same if there is a renaming p such that p Y y and p S S As there is a non deterministic choice of the clause in an atom s definition there may be a num ber of qualified answers generated from the initial state We denote the set of qualified answers for a state S and program P by qansp S In the case of no calls delay ing this semantics is the same as the usual operational semantics of Prolog with left to right scheduling As an example consider the initial state permute X Y X a nil nil and the program from Section 2 These have the single successful derivation shown in Figure 1 4 Abstract Interpretation In abstract interpretation 7 an analysis is formalized as a non standard interpretation of the data types and functions over those types Correctness of th
31. n variable term and Waep the set of sets of variables which 6 makes possibly dependent For example the equality constraint X aAY ZAW f V is most precisely described by X Y Z Y Z W V A more complete description of this description domain and abstract operations over it can be found in 28 Of course for accuracy more complex domains could be used in the analysis The first state description to be analyzed is permute X Y Y X 0 nil Figure 3 shows the memoization table at each iteration in the analysis for this state description The result of the analysis is X Y 0 0 0 That is if calls to permute have their second argument ground and first argument free the answers will ground the first argument As no calls were delayed in this example the analysis was virtually the same as given by a tradi tional left to right mode analysis of the program If the analysis is extended to give information about call pat terns it shows as promised in Section 2 that for calls to permute in which the second argument is ground and the first free no atom ever delays Further it shows that in all calls to permute the first argument will be free and the second argument will be ground and in all calls to delete the first and third arguments will be free and the second will be ground Now consider the state description permute X Y X Y 0 nil Figure 3 shows the memoization table at each it
32. oization tables 11 13 which our analy sis generalizes To our knowledge this is the first paper to consider the global dataflow analysis of logic pro gramming languages with delay Related work includes Marriott et al 24 which gives a dataflow analysis for a logic programming language in which negated calls are delayed until their arguments are fully ground However the analysis does not generalize to the case considered here as correctness relies on calls only being woken when all of their arguments are ground Other related work is the global analysis of concurrent constraint program ming languages 4 5 6 14 These languages differ from the languages considered here as they do not have a de fault left to right scheduling but instead the compiler or interpreter is free to choose any scheduling Thus pro gram analysis must be correct for all schedulings In our setting knowledge of the default scheduling allows much more precise analysis Related work also includes Gudeman et al 16 and Debray 12 which investigate local analyses and optimization for the compilation of Janus a concurrent constraint programming language The optimizations include reordering and removal of redundant suspension conditions Debray 10 studies global analysis for compile time fixed scheduling rules other than left to right However this approach does not work for dynamic scheduling nor for analyses to determine freeness information Final
33. ormation about the call pat terns That is for each atom A appearing in the pro gram we want to know whether the calls to the atom initially delay and when each call to A is eventually reduced perhaps after being delayed the value of the current equation restricted to the variables in A It is straightforward to modify the denotational semantics to collect this information for atoms which are not de layed For the case of atoms which are delayed it is more difficult as although treating the delayed atoms as a multiset does not affect the qualified answers if more than one atom is woken it may affect the calls made in the evaluation Because of space limitations we will ignore this extra complication but note that it has been done in the analyzer used to obtain the results presented in Section 9 6 Implementation The denotational equations given in the previous sec tion can be considered as a definition of a class of pro gram analyses Read naively the equations specify a highly redundant way of computing certain mathemat ical objects On the other hand the denotational def initions can be given a call by need reading which guarantees that the same partial result is not repeat edly recomputed and only computed if it is needed for the final result With such a call by need reading the definition of P is modulo syntactic rewriting a working implementation of a generic dataflow analyzer written in a functional programming lan
34. ptimizing Prolog Compiler Proc of the 1990 North American Conference on Logic Programming 501 515 1990 R Warren M Hermenegildo and S K Debray On the Practicality of Global Flow Analysis of Logic Pro grams Proc of the 5th International Conference and Symposium on Logic Programming 684 699 1988 K Yelick and J Zachary Moded type systems for logic programming In Proc Sixteenth Annual ACM Symp on Principles of Programming Languages pages 116 124 ACM 1989
35. rational Semantics In this section we give some preliminary notation and an operational semantics for logic programs with dynamic scheduling A logic program or program is a finite set of clauses A clause is of the form H B where H the head is an atom and B the body is a finite sequence of literals A literal is either an atom or an equation be tween terms An atom has the form p x1 Xn where p is a predicate symbol and the x are distinct variables An equality constraint is essentially a conjunction of equations between terms For technical convenience equality constraints are treated modulo logical equiv alence and are assumed to be closed under existen tial quantification and conjunction Thus equality con straints are ordered by logical implication that is 8 lt 0 iff gt 6 The least inconsistent equality constraint is denoted by false We let Jy 0 denote the equality constraint 3 V1 3 V 2 a Va where variable set W Vi Vn We let 4y 6 be constraint 0 restricted to the variables W That is J w is Jvars 9 w 9 where function vars takes a syntactic object and returns the set of free variables occurring in it Note that al though we concentrate on equality constraints the anal ysis generalizes to handle other constraints such as arithmetic or Boolean in the more general context of constraint logic programs 22 Var is the set of variables Atom the set of atoms Eqns the set of equalit
36. ring Above program parallelized 1 processor Above program parallelized 2 processors Above program parallelized 4 processors Above program parallelized 6 processors Table 2 Analysis and optimization of quick sort out a performance penalty when executing the program in the mode that runs in Prolog Furthermore the anal ysis and resultant optimization also improves execution speed even if some suspensions still need to be used during execution The optimizations based on reorder ing give even more impressive results This is mainly explained by the fact mentioned above that for all pro grams the reordering has achieved the elimination of all suspension declarations Finally in the last test we show how information from the analysis can be used to perform optimizations used in the compilation of traditional Prolog As an ex ample we consider automatic parallelization based on the independent and parallelism model The only pro gram in which this kind of parallelism exists for the given queries is qsort In this case the parallelism can be automatically exploited using existing tools given the information obtained from the analysis This is be cause the analysis determines that there is no goal sus pension in the reordered program and so the tools and techniques described in 20 27 are applicable These techniques can also be extended to deal with cases in which goals are delayed by extending the notion of de pendence
37. the information provided by the analyzer was optimal In the case of permute one condition can be relaxed beyond those inferred by the analyzer In par ticular for all the examples in their forward execu tion mode the analyzer accurately infers that no goal suspends and therefore all suspension declarations can be eliminated With respect to the backwards execu tion in all cases but neg the suspension conditions are either relaxed or eliminated This does not occur for neg since the analyzer accurately infers that the exist ing groundness suspension condition is still needed for correctness Finally with respect to the optimizations where reordering is allowed all backward executions are reordered in such a way that no suspension conditions are needed Thus we can conclude that the accuracy results for the analyzer are encouraging Table 1 lists execution times expressed in seconds for the original benchmarks and the optimized versions Each column has the following meaning Name pro gram name Query number of elements in the list given as query P execution time for the program written in standard Prolog i e with no suspension dec larations S execution time for the program written with suspension declarations SO execution time for program written with suspension declarations and opti mized by removing suspension declarations as dictated by the analysis information S SO ratio between the last two colu
38. trict the equality con straint to the variables in the delayed atoms and the goal Proposition 5 1 Let P Prog A Atom and A G 0 D State Then qansp A G 6 D is aansp G 6 D D qansp A D m Proposition 5 2 Let P Prog p Ren and S State Q qansp S p Q E qansp pS E Proposition 5 3 Let P Prog and G 0 D State qansp G 0 D Le A 0 D 6 D qansp S where S is G Feces G U vars py D a Taken together these propositions mean that we can find the qualified answers to a state as long as we know the qualified answers to the canonical calls en countered when processing the state where a canonical call is a call that represents all of its variants and in which the constraint is restricted to the variables of the call atom and the delayed atoms This is the basic idea behind the denotational semantics as the denotation of a program is simply a mapping from calls to answers The last proposition means that the meaning of a goal is independent of the order that the atoms are scheduled Thus we can ignore the sequencing infor mation associated with delayed atoms and treat them as multisets It is variant of Theorem 4 in Yelick and Zachary 34 Proposition 5 4 Let P be a program and G 8 D be a state If G is a rearrangement of G then qansp G D qansp G 0 D m In the denotational semantics atoms bodies cla
39. uses and programs are formalized as environment transformers where an environment consists of the cur rent equality constraint description and an annotated multiset of delayed atoms In a sense an environment is the current answer Thus an environment has type Env AEgqns x AnnMSet and the denotation of a program has type Den Atom gt Env gt gEnv as it maps a call to its set of answers The complete denotational definition is shown in Figure 2 The semantics is generic as it is paramet ric in AEqns the equality constraint descriptions and various parametric functions The semantic functions associated with programs P clause bodies B and liter als L need little explanation The only point to note is that the variable set W is passed around so as to ensure that there are no variable re naming conflicts The function A gives the meaning of an atom for the current denotation Consider the call A A W d z D There are three cases to consider the first is when A is delayed for all equality constraints approximated by 7 the second is when A is not delayed for any equality constraints approximated by 7 and the third is when A is delayed for some equality constraints approximated by m but not all A is defined in terms of the parametric functions Awake and Adelay The call Awake A 7 returns a description of those equal ity constraints which are described by 7 and for which A will not delay Conversely Adelay A r
40. y constraints Lit the set of lit erals and Prog the set of programs A renaming is a bijective mapping from Var to Var We let Ren be the set of renamings and naturally extend renamings to mappings between atoms clauses and constraints Syntactic objects s and s are said to be variants if there is a p Ren such that p s s The definition of an atom A in program P with respect to variables W defnp A W is the set of variants of clauses in P such that each variant has A as a head and has variables disjoint from W vars A The operational semantics of a program is in terms of its derivations which are sequences of reductions between states where a state G 8 D consists of the current literal sequence or goal G the current equal ity constraints 0 and the current sequence of delayed atoms D Literals in the goals are processed left to right If the literal is an equality constraint and it is consistent with the current equality constraints it is added to these Delayed atoms woken by the addition are processed If the literal is an atom it is tested to see if it is delayed If so it is placed in the delayed atom se quence otherwise it is replaced by the body of a clause in its definition More formally State Lit x Eqns x Atom A state L G D can be reduced as follows 1 If L Eqns and A L is satisfiable it is reduced to D G AL D D where D woken D 6 A L 2

Download Pdf Manuals

image

Related Search

Related Contents

取扱説明書 ~ うすまき全自動種機  Descarga el manual  Digital pressure gauge model CPG500 GB - K  Chapter 4: The C programming environment for the 8051  I GB F D E P NL GR  LCS III - BYK Additives & Instruments  取扱説明書を必ずご参照ください 1/4 ZTL1398 作成: 2014 年 1 月 22  

Copyright © All rights reserved.
Failed to retrieve file