CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Linearly ordered attribute grammar scheduling using SAT-solving

J. Bransen ; L.T. Van Binsbergen ; Koen Claessen (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; A.H. Dijkstra
Lecture Notes in Computer Science: 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015; London; United Kingdom; 11 April 2015 through 18 April 201 (0302-9743). Vol. 9035 (2015), p. 289-303.
[Konferensbidrag, refereegranskat]

© Springer-Verlag Berlin Heidelberg 2015. 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.

Nyckelord: Attribute Grammars , SAT-solving , Static analysis

Denna post skapades 2015-05-12. Senast ändrad 2016-06-29.
CPL Pubid: 217045


Läs direkt!

Länk till annan sajt (kan kräva inloggning)