2026-09-20T06:23:02Z https://www.ideals.illinois.edu/oai-pmh

oai:www.ideals.illinois.edu:2142/18416 2023-07-10 col_2142_5131 col_2142_10761 com_2142_5130 com_2142_10755 com_2142_234

effect checking programming languages determinism nondeterminism regions effects effect systems Adve, Vikram S. Adve, Vikram S. Padua, David A. Roşu, Grigore Snir, Marc Chamberlain, Bradford L. Grossman, Dan Bocchino, Robert L., Jr. 2011-01-14T22:50:09Z 2011-01-14T22:50:09Z 2011-01-14T22:50:09Z This thesis presents a new, Java-based object-oriented parallel language called Deterministic Parallel Java (DPJ). DPJ uses a novel effect system to guarantee determinism by default. That means that parallel programs are guaranteed to execute deterministically unless nondeterminism is explicitly requested. This is in contrast to the shared-memory models in widespread use today, such as threads and locks (including threads in ordinary Java). Those models are inherently nondeterministic, do not provide any way to check or enforce that a computation is deterministic, and can even have unintended data races, which can lead to strange and unexpected behaviors. Because deterministic programs are much easier to reason about than arbitrary parallel code, determinism by default simplifies parallel programming. This thesis makes several broad contributions to the state of the art in programming languages and effect systems. First, it presents a comprehensive research agenda for achieving determinism by default in parallel languages with reference aliasing and shared mutable state. It argues that an object-oriented effect system is a good approach to managing shared memory conflicts. It also raises several technical challenges, many of which are taken up in the rest of the thesis. Second, this thesis presents an effect system and language for deterministic parallel programming using a fork-join model of parallel control. With simple modular checking, and with no runtime checking overhead, the effect system guarantees at compile time that there are no conflicting memory accesses between any pairs of parallel tasks. The effect system supports several important patterns of deterministic parallelism that previous systems cannot express. We describe the effect system and language both formally and informally, and prove soundness for the formal language. We also describe our evaluation showing that the language can express a range of parallel programming patterns with good performance. Third, this thesis extends the effect system and language for determinism to support a controlled form of nondeterminism. Conflicting accesses are allowed only for an explicitly identified nondeterministic parallel construct, so the language is deterministic by default. A transactional runtime provides isolation for atomic statements, while the extended effect system provides stronger compile-time safety guarantees than any system we know of. In addition to determinism by default, the language guarantees race freedom; strong isolation for atomic statements even if the runtime guarantees only weak isolation; and an elegant way of composing deterministic and nondeterministic operations that preserves local reasoning about deterministic operations. Again we give an informal treatment, a formal treatment, and soundness proofs. We describe an evaluation showing that the extended language can express realistic nondeterministic algorithms in a natural way, with reasonable performance given the transactional runtime we used. Further, by eliminating unnecessary synchronization, the effect system enables a significant reduction in the software runtime overhead. Fourth, this thesis describes programming techniques and further extensions to the effect system for supporting object-oriented parallel frameworks. Frameworks represent an important tool for parallel programming in their own right. They can also express some operations that the language and effect system alone cannot, for example pipeline parallelism. We show how to write a framework API using the DPJ effect system so that the framework writer can guarantee correctness properties to the user, assuming the user's code passes the DPJ type checker. We also show how to extend the DPJ effect system to add generic types and effects, making the frameworks more general and useful. Finally, we state the requirements for a correct framework implementation. These requirements may be checked with a combination of DPJ's effect system and external reasoning. Again we give an informal treatment, a formal treatment, and soundness proofs. We also describe the results of an evaluation showing that the techniques described can express realistic frameworks and parallel algorithms. Item withdrawn by Mark Zulauf (zulauf@illinois.edu) on 2010-11-18T22:56:18Z Item was in collections: University of Illinois Theses & Dissertations (ID: 1) No. of bitstreams: 3 Bocchino_Robert.pdf: 1176049 bytes, checksum: b73eab398a32b382409a9b7bbe78666c (MD5) Bocchino_Robert.tar.gz: 1057673 bytes, checksum: 56c282b3415d59faef7dc0af5e20c25e (MD5) Bocchino_Robert.pdf: 1176059 bytes, checksum: 6913f07bf1763c1e89837123863c6185 (MD5) Made available in DSpace on 2011-01-14T22:50:09Z (GMT). No. of bitstreams: 3 Bocchino_Robert.pdf: 1176050 bytes, checksum: 7ef11fdde7114f6ec37d6342d31215e6 (MD5) license.txt: 4065 bytes, checksum: e552fa02235e1e50e2019b398f3d2e25 (MD5) Bocchino_Robert.tar.gz: 1057673 bytes, checksum: dd121cbe0aaefbbd6f7511b10a52cdba (MD5) http://hdl.handle.net/2142/18416 en © 2010 Robert L. Bocchino Jr. Chapters 3 and 5 are derived from work published in ACM conference proceedings (OOPSLA 2009 and POPL 2011). As to that work only, the following notice applies: Copyright © 2009, 2011 by the Association for Computing achinery, Inc. Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, to republish, to post on servers, or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from Publications Dept., ACM, Inc., fax +1 (212) 869-0481, or permissions@acm.org. parallel parallelism fork-join strong isolation atomicity transactional memory atomic sections data race freedom frameworks An effect system and language for deterministic-by-default parallel programming 2010-12 Computer Science 1434 Computer Science 0112 University of Illinois at Urbana-Champaign Dissertation Ph.D. PHD:Computer Science -UIUC 10KS0112PHD