Linearly Ordered Attribute Grammar Scheduling Using SAT-Solving. / van Binsbergen, L. Thomas.

Tools and Algorithms for the Construction and Analysis of Systems. Springer Berlin / Heidelberg, 2015. p. 289-303 (Lecture Notes in Computer Science; Vol. 9035).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Published

Standard

Linearly Ordered Attribute Grammar Scheduling Using SAT-Solving. / van Binsbergen, L. Thomas.

Tools and Algorithms for the Construction and Analysis of Systems. Springer Berlin / Heidelberg, 2015. p. 289-303 (Lecture Notes in Computer Science; Vol. 9035).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Harvard

van Binsbergen, LT 2015, Linearly Ordered Attribute Grammar Scheduling Using SAT-Solving. in Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 9035, Springer Berlin / Heidelberg, pp. 289-303, TACAS 2015, London, United Kingdom, 13/04/15. https://doi.org/10.1007/978-3-662-46681-0_24

APA

van Binsbergen, L. T. (2015). Linearly Ordered Attribute Grammar Scheduling Using SAT-Solving. In Tools and Algorithms for the Construction and Analysis of Systems (pp. 289-303). (Lecture Notes in Computer Science; Vol. 9035). Springer Berlin / Heidelberg. https://doi.org/10.1007/978-3-662-46681-0_24

Vancouver

van Binsbergen LT. Linearly Ordered Attribute Grammar Scheduling Using SAT-Solving. In Tools and Algorithms for the Construction and Analysis of Systems. Springer Berlin / Heidelberg. 2015. p. 289-303. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-662-46681-0_24

Author

van Binsbergen, L. Thomas. / Linearly Ordered Attribute Grammar Scheduling Using SAT-Solving. Tools and Algorithms for the Construction and Analysis of Systems. Springer Berlin / Heidelberg, 2015. pp. 289-303 (Lecture Notes in Computer Science).

BibTeX

@inproceedings{dd10395d101a41c580923f883719dd62,
title = "Linearly Ordered Attribute Grammar Scheduling Using SAT-Solving",
abstract = "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.",
author = "{van Binsbergen}, {L. Thomas}",
year = "2015",
month = jan,
day = "1",
doi = "10.1007/978-3-662-46681-0_24",
language = "English",
isbn = "978-3-662-46680-3",
series = "Lecture Notes in Computer Science",
publisher = "Springer Berlin / Heidelberg",
pages = "289--303",
booktitle = "Tools and Algorithms for the Construction and Analysis of Systems",
note = "TACAS 2015 ; Conference date: 13-04-2015 Through 17-04-2015",

}

RIS

TY - GEN

T1 - Linearly Ordered Attribute Grammar Scheduling Using SAT-Solving

AU - van Binsbergen, L. Thomas

PY - 2015/1/1

Y1 - 2015/1/1

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-662-46681-0_24

DO - 10.1007/978-3-662-46681-0_24

M3 - Conference contribution

SN - 978-3-662-46680-3

T3 - Lecture Notes in Computer Science

SP - 289

EP - 303

BT - Tools and Algorithms for the Construction and Analysis of Systems

PB - Springer Berlin / Heidelberg

T2 - TACAS 2015

Y2 - 13 April 2015 through 17 April 2015

ER -