Linearly Ordered Attribute Grammar Scheduling Using SAT-Solving

详细信息    查看全文

• 作者：Jeroen Bransen (15)
  L. Thomas van Binsbergen (15) (16)
  Koen Claessen (17)
  Atze Dijkstra (15)
  
  15. Utrecht University ; Utrecht ; The Netherlands
  16. Royal Holloway ; University of London ; Egham ; UK
  17. Chalmers University of Technology ; Gothenburg ; Sweden
  
• 关键词：Attribute Grammars ; static analysis ; SAT ; solving
• 刊名：Lecture Notes in Computer Science
• 出版年：2015
• 出版时间：2015
• 年：2015
• 卷：9035
• 期：1
• 页码：289-303
• 全文大小：240 KB
• 参考文献：1. Binsbergen, L.T., Bransen, J., Dijkstra, A. (2015) Linearly ordered attribute grammars: With automatic augmenting dependency selection. Proceedings of the 2015 Workshop on Partial Evaluation and Program Manipulation, PEPM 2015. ACM, New York, pp. 49-60 CrossRef
  2. Bird, R.S. (1984) Using circular programs to eliminate multiple traversals of data. Acta Informatica 21: pp. 239-250 CrossRef
  3. Bransen, J., Middelkoop, A., Dijkstra, A., Swierstra, S.D. The Kennedy-Warren algorithm revisited: Ordering attribute grammars. In: Russo, C., Zhou, N.-F. eds. (2012) Practical Aspects of Declarative Languages. Springer, Heidelberg, pp. 183-197 CrossRef
  4. Bryant, R.E., Velev, M.N. (2002) Boolean satisfiability with transitivity constraints. ACM Trans. Comput. Logic 3: pp. 604-627 CrossRef
  5. Claessen, K., Een, N., Sheeran, M., S枚rensson, N., Voronov, A., 脜kesson, K. (2009) Sat-solving in practice. Discrete Event Dynamic Systems 19: pp. 495-524 CrossRef
  6. Codish, M., Zazon-Ivry, M. Pairwise cardinality networks. In: Clarke, E.M., Voronkov, A. eds. (2010) Logic for Programming, Artificial Intelligence, and Reasoning. Springer, Heidelberg, pp. 154-172 CrossRef
  7. Cook, S.A. (1971) The complexity of theorem-proving procedures. Proceedings of the Third Annual ACM Symposium on Theory of Computing, STOC 1971. ACM, New York, pp. 151-158 CrossRef
  8. Dijkstra, A., Fokker, J., Swierstra, S.D. (2009) The architecture of the Utrecht Haskell Compiler. Proceedings of the 2nd ACM SIGPLAN Symposium on Haskell, Haskell 2009. ACM, New York, pp. 93-104
  9. Dirac, G.A. (1961) On rigid circuit graphs. Abh. Math. Sem. Univ. Hamburg 25: pp. 71-76 CrossRef
  10. E茅n, N., S枚rensson, N. An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. eds. (2004) Theory and Applications of Satisfiability Testing. Springer, Heidelberg, pp. 502-518 CrossRef
  11. Ekman, T., Hedin, G. (2007) The JastAdd extensible Java compiler. Proceedings of the 22nd Annual ACM SIGPLAN Conference on Object-Oriented Programming Systems and Applications, OOPSLA 2007. ACM, New York, pp. 1-18 CrossRef
  12. Engelfriet, J., Fil猫, G. (1982) Simple multi-visit attribute grammars. Journal of Computer and System Sciences 24: pp. 283-314 CrossRef
  13. Heeren, B., Leijen, D., IJzendoorn, A. (2003) Helium, for learning haskell. Proceedings of the 2003 ACM SIGPLAN Workshop on Haskell, Haskell 2003. ACM, New York, pp. 62-71
  14. Kastens, U. (1980) Ordered attributed grammars. Acta Informatica 13: pp. 229-256 CrossRef
  15. Kennedy, K., Warren, S.K. (1976) Automatic generation of efficient evaluators for attribute grammars. Proceedings of the 3rd ACM SIGACT-SIGPLAN Symposium on Principles on Programming Languages, POPL 1976. ACM, New York, pp. 32-49
  16. Knuth, D.E. (1968) Semantics of context-free languages. Mathematical Systems Theory 2: pp. 127-145 CrossRef
  17. Middelkoop, A., Elyasov, A.B., Prasetya, W. Functional instrumentation of actionscript programs with asil. In: Gill, A., Hage, J. eds. (2012) Implementation and Application of Functional Languages. Springer, Heidelberg, pp. 1-16 CrossRef
  18. Saraiva, J.: Purely Functional Implementation of Attribute Grammars: Zuiver Functionele Implementatie Van Attributengrammatica鈥檚. IPA dissertation series. IPA (1999)
  19. Swierstra, S.D., Alcocer, P.R.A. Designing and implementing combinator languages. In: Swierstra, S.D., Oliveira, J.N. eds. (1999) Advanced Functional Programming. Springer, Heidelberg, pp. 150-206 CrossRef
  
• 作者单位：Tools and Algorithms for the Construction and Analysis of Systems
• 丛书名：978-3-662-46680-3
• 刊物类别：Computer Science
• 刊物主题：Artificial Intelligence and Robotics
  Computer Communication Networks
  Software Engineering
  Data Encryption
  Database Management
  Computation by Abstract Devices
  Algorithm Analysis and Problem Complexity
  
• 出版者：Springer Berlin / Heidelberg
• ISSN：1611-3349

文摘

Many computations over trees can be specified using attribute grammars. Compilers for attribute grammars need to find an evaluation order (or schedule) in order to generate efficient code. For the class of linearly ordered attribute grammars such a schedule can be found statically, but this problem is known to be NP-hard. In this paper, we show how to encode linearly ordered attribute grammar scheduling as a SAT-problem. For such grammars it is necessary to ensure that the dependency graph is cycle free, which we approach in a novel way by transforming the dependency graph to a chordal graph allowing the cycle freeness to be efficiently expressed and computed using SAT solvers. There are two main advantages to using a SAT-solver for scheduling: (1) the scheduling algorithm runs faster than existing scheduling algorithms on real-world examples, and (2) by adding extra constraints we obtain fine-grained control over the resulting schedule, thereby enabling new scheduling optimisations.