Staff View
Practical formal techniques and tools for developing LLVM’s peephole optimizations

Descriptive

TitleInfo
Title
Practical formal techniques and tools for developing LLVM’s peephole optimizations
Name (type = personal)
NamePart (type = family)
Menendez
NamePart (type = given)
David
NamePart (type = date)
1977-
DisplayForm
David Menendez
Role
RoleTerm (authority = RULIB)
author
Name (type = personal)
NamePart (type = family)
Nagarakatte
NamePart (type = given)
Santosh
DisplayForm
Santosh Nagarakatte
Affiliation
Advisory Committee
Role
RoleTerm (authority = RULIB)
chair
Name (type = personal)
NamePart (type = family)
Kremer
NamePart (type = given)
Ulrich
DisplayForm
Ulrich Kremer
Affiliation
Advisory Committee
Role
RoleTerm (authority = RULIB)
internal member
Name (type = personal)
NamePart (type = family)
Nguyen
NamePart (type = given)
Thu D.
DisplayForm
Thu D. Nguyen
Affiliation
Advisory Committee
Role
RoleTerm (authority = RULIB)
internal member
Name (type = personal)
NamePart (type = family)
Alur
NamePart (type = given)
Rajeev
DisplayForm
Rajeev Alur
Affiliation
Advisory Committee
Role
RoleTerm (authority = RULIB)
outside member
Name (type = corporate)
NamePart
Rutgers University
Role
RoleTerm (authority = RULIB)
degree grantor
Name (type = corporate)
NamePart
School of Graduate Studies
Role
RoleTerm (authority = RULIB)
school
TypeOfResource
Text
Genre (authority = marcgt)
theses
OriginInfo
DateCreated (qualifier = exact)
2018
DateOther (qualifier = exact); (type = degree)
2018-01
CopyrightDate (encoding = w3cdtf); (qualifier = exact)
2018
Place
PlaceTerm (type = code)
xx
Language
LanguageTerm (authority = ISO639-2b); (type = code)
eng
Abstract (type = abstract)
Modern compilers perform extensive transformation of code in order to optimize run- ning time and binary code size. These occur in multiple passes, including translations between representations at different levels of abstraction and transformations which re- structure code within a particular representation. Of particular interest are optimiza- tions that operate on a compiler’s intermediate representation (IR), as these can be shared across programming languages and hardware architectures. One such optimiza- tion pass is LLVM’s peephole optimizer, which is a suite of hundreds of small algebraic transformations which simplify code and perform canonicalization. Performing these transformations not only results in faster software, but simplifies other optimization passes by reducing the number of equivalent forms they must consider. It is essential that these optimizations preserve the semantics of input programs. Even a small transformation which changes the value computed by a code fragment or introduces undefined behavior can result in executable programs with incorrect or unpredictable behavior. Optimizations, and analysis of optimizations, must be partic- ularly careful when treating undefined behavior, as modern compilers increasingly use the knowledge that certain operations are undefined in order to streamline or eliminate ii code—occasionally in ways that are surprising to compiler users. Unfortunately, com- piler developers can also overlook undefined behavior or fail to consider rare edge cases, resulting in incorrect transformations. In particular, LLVM’s peephole optimizer has historically been one of the buggier parts of LLVM. To aid the development of correct peephole transformations in LLVM, we introduce Alive, a domain-specific language for specifying such transformations. Selecting a small yet expressive subset of LLVM IR allows for automated verification of Alive transforma- tions, and the Alive toolkit can generate an implementation of a correct transformation suitable for inclusion in LLVM. The correctness checks for Alive consider the various forms of undefined behavior defined by LLVM and ensure that transformations do not change the meaning of a program. Alive specifications can include a mixture of inte- ger and floating-point operations, and transformations can be generalized over different types. Some transformations require a precondition in order to be correct. These precon- ditions may be simple, but occasionally it is challenging to find a precondition that is sufficiently strong while remaining widely applicable. To assist in this process, the Alive toolkit includes Alive-Infer, a data-driven method for synthesizing preconditions. Depending on the complexity of the transformation, the weakest precondition sufficient to make a transformation correct may not be desirable, so Alive-Infer can provide a choice of concise but stronger preconditions. The Alive-Infer method automatically finds positive and negative examples to guide inference and finds useful predicates through enumeration. Finally, specifying transformations in Alive enables analyses of multiple transfor- mations and their interaction. It is possible to have transformations or sequences of transformations which can be applied indefinitely to a finite input. This dissertation presents a method for testing whether such a sequence can be applied indefinitely to some input. Alive demonstrates that a properly chosen abstraction can provide the benefits of formal code verification without the need for manually written proofs, and can enable new techniques and analyses to assist development.
Subject (authority = RUETD)
Topic
Computer Science
RelatedItem (type = host)
TitleInfo
Title
Rutgers University Electronic Theses and Dissertations
Identifier (type = RULIB)
ETD
Identifier
ETD_8600
PhysicalDescription
Form (authority = gmd)
electronic resource
InternetMediaType
application/pdf
InternetMediaType
text/xml
Extent
1 online resource (xv, 188 p. : ill.)
Note (type = degree)
Ph.D.
Note (type = bibliography)
Includes bibliographical references
Subject (authority = ETD-LCSH)
Topic
Compilers (Computer programs)
Note (type = statement of responsibility)
by David Menendez
RelatedItem (type = host)
TitleInfo
Title
School of Graduate Studies Electronic Theses and Dissertations
Identifier (type = local)
rucore10001600001
Location
PhysicalLocation (authority = marcorg); (displayLabel = Rutgers, The State University of New Jersey)
NjNbRU
Identifier (type = doi)
doi:10.7282/T3FF3WK4
Genre (authority = ExL-Esploro)
ETD doctoral
Back to the top

Rights

RightsDeclaration (ID = rulibRdec0006)
The author owns the copyright to this work.
RightsHolder (type = personal)
Name
FamilyName
Menendez
GivenName
David
Role
Copyright Holder
RightsEvent
Type
Permission or license
DateTime (encoding = w3cdtf); (qualifier = exact); (point = start)
2017-12-27 22:36:43
AssociatedEntity
Name
David Menendez
Role
Copyright holder
Affiliation
Rutgers University. School of Graduate Studies
AssociatedObject
Type
License
Name
Author Agreement License
Detail
I hereby grant to the Rutgers University Libraries and to my school the non-exclusive right to archive, reproduce and distribute my thesis or dissertation, in whole or in part, and/or my abstract, in whole or in part, in and from an electronic format, subject to the release date subsequently stipulated in this submittal form and approved by my school. I represent and stipulate that the thesis or dissertation and its abstract are my original work, that they do not infringe or violate any rights of others, and that I make these grants as the sole owner of the rights to my thesis or dissertation and its abstract. I represent that I have obtained written permissions, when necessary, from the owner(s) of each third party copyrighted matter to be included in my thesis or dissertation and will supply copies of such upon request by my school. I acknowledge that RU ETD and my school will not distribute my thesis or dissertation or its abstract if, in their reasonable judgment, they believe all such rights have not been secured. I acknowledge that I retain ownership rights to the copyright of my work. I also retain the right to use all or part of this thesis or dissertation in future works, such as articles or books.
Copyright
Status
Copyright protected
Availability
Status
Open
Reason
Permission or license
Back to the top

Technical

RULTechMD (ID = TECHNICAL1)
ContentModel
ETD
OperatingSystem (VERSION = 5.1)
windows xp
CreatingApplication
Version
1.5
ApplicationName
pdfTeX-1.40.16
DateCreated (point = end); (encoding = w3cdtf); (qualifier = exact)
2017-12-27T22:24:54
DateCreated (point = end); (encoding = w3cdtf); (qualifier = exact)
2017-12-27T22:24:54
Back to the top
Version 8.4.8
Rutgers University Libraries - Copyright ©2022