Analyses of Java programs over weak memory
AffiliationComputing and Information Systems
Document TypePhD thesis
Access StatusOpen Access
© 2018 Dr. David Anthony Winscom Clarke
Between 1980 and 2000, the clock speeds of CPU chips showed an exponential increase from about 1MHz to 1-2GHz. Since then the clock speed of these chips has stagnated. However, contemporary chips offer multiple cores and hardware support for multi-threading. To exploit their power the programmer must use concurrent processing. This is difficult and errorprone. The Java language has always provided direct high-level support for multi-threading. We provide experimental evidence that these features incur significant overheads. The acquire/release paradigm provided by the synchronized construct relies on the developer to conform to the implicit access protocol. Data race errors occur where this protocol is violated. Programs that try to avoid the costs of the synchronized construct become exposed to the lack of sequential consistency in weak memory models. Inserting memory fences into the instruction stream restores sequential consistency. Some CPU architectures require few fences, while others require many fences because they have a weaker memory model. In some cases, a memory fence can be replaced by other instruction patterns that may incur fewer overheads than the fence. In our work, we have investigated the direct placement of fences, the default placement of fences triggered by the use of volatile variables, and the elimination of unnecessary fences. In this thesis we offer four major innovations: • An analysis that detects data race errors caused by misimplementation of the acquire/release paradigm. This analysis provides a valuable trade-off between a significant improvement in processing time and a decreased completeness; • A Java-based extension of the Abstract Event Graph analysis for the optimal selection and placement of memory fences that ensures the sequential consistency of novel synchronisation patterns or lock-free algorithms; • An improved implementation of memory fences that can reduce the overhead incurred on architectures with relaxed memory models. • An innovative design for a thread-safe shared data-store class with minimal use of memory fences. We provide experimental evidence that the prototype implementation successfully prevents harmful data races and that its performance is superior to functionally equivalent code that uses conventional synchronisation. While working on these innovations we noted some related problems: • The event abstraction that we employ cannot usefully handle references to the elements of arrays or Collections • Our algorithms have pre-requisite conditions that are not easily satisfied in a static analysis; We have provided solutions to these problems: • Java streams encapsulate the handling of Collections. We offer a proof that the actions of Java streams can be summarised within an Abstract Event Graph (AEG) and that the resultant Summarised Abstract Event Graph (SAEG) is no less sound and complete with respect to the detection of data races than the AEG of the program that includes the stream; • We have developed designs and proof-of-concept that show how elements of our static analysis prototypes may be incorporated within the Java Virtual Machine. These innovations significantly advance the correctness and efficiency of multi-threaded Java programs and, consequentially, facilitate the full exploitation of contemporary CPU hardware.
KeywordsJava; data race; weak memory; static analysis; avoiding data races
- Click on "Export Reference in RIS Format" and choose "open with... Endnote".
- Click on "Export Reference in RIS Format". Login to Refworks, go to References => Import References