|
|
Instruction Set Completness Detection for Retargetable C Compiler Generation
Nagy, Michal ; Dolíhal, Luděk (referee) ; Hruška, Tomáš (advisor)
This thesis concerns the issue of completness detection of instruction set description for the LLVM compiler, or the ability of a compiler to generate target program for every valid source program in the appropriate high-level programming language. On the basis of regular tree grammar theory and several scietific theses that also concern this issue, formal tool for inclusion checking of two grammars. Furthermore a method for automatic extraction of the two grammars from the instruction set description has been devised, as a result of which the tool can be used for checking completeness of instruction selection. In combination with checking completeness of the legalization process of the LLVM compiler, which preceeds the instruction selection, it should be feaseable to check completeness of most compiler parts dependent on the target architecture.
|
|
|
Classification of (in)finitary logics
Lávička, Tomáš ; Noguera, Carles (advisor) ; Botur, Michal (referee)
In this master thesis we investigate completeness theorems in the framework of abstract algebraic logic. Our main interest lies in the completeness with respect to the so called relatively (finitely) subdirectly irreducible models. Notable part of the presented theory concerns the difference between finitary and infinitary logical systems. We focus on the well-known fact that the completeness theorem with respect to relatively (finitely) subdirectly irreducible models can be proven in general for all finitary logics and we discuss the possible of generalizing this theorem even to infinitary logics. We show that there are two interesting inter- mediate properties between this completeness and finitarity, namely (completely) intersection-prime extension properties. Based on these notions we define five classes of logics and propose a new hierarchy of finitary and infinitary logics. As a main contribution of this dissertation we present an example of a logic separat- ing some of these classes. Keywords: Abstract algebraic logic, completeness, relatively (finitely) sub- directly irreducible models, RSI-completeness, RFSI-completeness, (completely) intersection-prime extension property, IPEP, CIPEP.
|
|
|
Instruction Set Completness Detection for Retargetable C Compiler Generation
Nagy, Michal ; Dolíhal, Luděk (referee) ; Hruška, Tomáš (advisor)
This thesis concerns the issue of completness detection of instruction set description for the LLVM compiler, or the ability of a compiler to generate target program for every valid source program in the appropriate high-level programming language. On the basis of regular tree grammar theory and several scietific theses that also concern this issue, formal tool for inclusion checking of two grammars. Furthermore a method for automatic extraction of the two grammars from the instruction set description has been devised, as a result of which the tool can be used for checking completeness of instruction selection. In combination with checking completeness of the legalization process of the LLVM compiler, which preceeds the instruction selection, it should be feaseable to check completeness of most compiler parts dependent on the target architecture.
|
guest ::
