Edinburgh Research Archive logo

Edinburgh Research Archive

University of Edinburgh homecrest
View Item 
  •   ERA Home
  • Informatics, School of
  • Informatics thesis and dissertation collection
  • View Item
  •   ERA Home
  • Informatics, School of
  • Informatics thesis and dissertation collection
  • View Item
  • Login
JavaScript is disabled for your browser. Some features of this site may not work without it.

Program Transformations in Weak Memory Models

View/Open
Sevcik J PhD thesis 08.pdf (1.027Mb)
Date
2009
Author
Sevcik, Jaroslav
Metadata
Show full item record
Abstract
We analyse the validity of common optimisations on multi-threaded programs in two memory models—the DRF guarantee and the Java Memory Model. Unlike in the single-threaded world, even simple program transformations, such as common subexpression elimination, can introduce new behaviours in shared-memory multi-threading with an interleaved semantics. To validate such optimisations, most current programming languages define weaker semantics, called memory models, that aim to allow such transformations while providing reasonable guarantees. In this thesis, we consider common program transformations and analyse their safety in the two most widely used language memory models: (i) the DRF guarantee, which promises sequentially consistent behaviours for data race free programs, and (ii) the Java Memory Model, which is the semantics of multithreaded Java. The DRF guarantee is the semantics of Ada and it has been proposed as the semantics of the upcoming revision of C++. Our key results are: (i) we prove that a large class of elimination and reordering transformations satisfies the DRF guarantee; (ii) we find that the Java language is more restrictive—despite the claims in the specification, the Java Memory Model does not allow some important program transformations, such as common subexpression elimination. To establish the safety results, we develop a trace semantic framework and describe important program optimisations as relations on sets of traces. We prove that all our elimination and reordering transformations satisfy the DRF guarantee, i.e., the semantic transformations cannot introduce new behaviours for data race free programs. Moreover, we prove that all the transformations preserve data race freedom. This ensures safety of transformations composed from eliminations and reorderings. In addition to the DRF guarantee, we prove that for arbitrary programs, our transformations prevent values appearing “outof- thin-air”—if a program does not contain constant c and does not perform any operation that could create c, then no transformation of the program can output c. We give an application of the semantic framework to a concrete language and prove safety of several simple syntactic transformations. We employ similar semantic techniques to prove validity of several classes of transformations, such as the elimination of an overwritten write or reordering of independent memory accesses, in the Java Memory Model. To establish the iii negative results for the Java Memory Model, we provide counterexamples showing that several common optimisations can introduce new behaviours and thus are not safe.
URI
http://hdl.handle.net/1842/3132
Collections
  • Informatics thesis and dissertation collection

Library & University Collections HomeUniversity of Edinburgh Information Services Home
Privacy & Cookies | Takedown Policy | Accessibility | Contact
Privacy & Cookies
Takedown Policy
Accessibility
Contact
feed RSS Feeds

RSS Feed not available for this page

 

 

All of ERACommunities & CollectionsBy Issue DateAuthorsTitlesSubjectsPublication TypeSponsorSupervisorsThis CollectionBy Issue DateAuthorsTitlesSubjectsPublication TypeSponsorSupervisors
LoginRegister

Library & University Collections HomeUniversity of Edinburgh Information Services Home
Privacy & Cookies | Takedown Policy | Accessibility | Contact
Privacy & Cookies
Takedown Policy
Accessibility
Contact
feed RSS Feeds

RSS Feed not available for this page