Return to search

A calculus of loop invariants for dense linear algebra optimization

Loop invariants have traditionally been used in proofs of correctness (e.g. program verification) and program derivation. Given that a loop invariant is all that is required to derive a provably correct program, the loop invariant can be thought of as being the essence of a loop. Being the essence of a loop, we ask the question “What other information is embedded within a loop invariant?” This dissertation provides evidence that in the domain of dense linear algebra, loop invariants can be used to determine the behavior of the loops. This dissertation demonstrates that by understanding how the loop invariant describes the behavior of the loop, a goal-oriented approach can be used to derive loops that are not only provably correct, but also have the desired performance behavior. / text

Identiferoai:union.ndltd.org:UTEXAS/oai:repositories.lib.utexas.edu:2152/22974
Date29 January 2014
CreatorsLow, Tze Meng
Source SetsUniversity of Texas
Languageen_US
Detected LanguageEnglish
Formatapplication/pdf

Page generated in 0.0019 seconds