Physical Sciences and Mathematics Commons^™

Operational Verification Of A Relativistic Program, Robert T. Bauer

Computer Science Faculty Publications and Presentations

Engineering eorts to achieve scalable multiprocessor perfor- mance for concurrent reader-writer programs have resulted in a family of algorithms that are non-blocking and that tolerate interprocessor in- terference. Because these algorithms accept a unique frame of reference for each processor's accesses to memory, they typify a concurrent pro- gramming technique for shared memory multicore architectures called relativistic programmming.

Rigorous verification of these algorithms is not possible with existing semantic based approaches because the semantics under approximates multiprocessor behavior and the algorithms rely on abstruse interactions with the operating system that aren't reconciled with language seman- tics.

The Read-Copy Update (RCU) …

The Design And Implementation Of A Safe, Lightweight Haskell Compiler, Timothy Jan Chevalier

Computer Science Faculty Publications and Presentations

Typed programming languages offer safety guarantees that help programmers write correct code, but typical language implementations offer no proof that source-level guarantees extend to executable code. Moreover, typical implementations link programs with unsafe runtime system (RTS) code. I present a compiler for the functional language Haskell that preserves some of the properties of Haskell’s type system. The soundness proof for the combination of the compiler and a verified RTS requires a proof that the compiler emits code that cooperates correctly with the RTS. In particular, the latter proof must address the boundary between the user program and the garbage collector. …

Is Parallel Programming Hard, And If So, Why?, Paul E. Mckenney, Maged M. Michael, Manish Gupta, Philip William Howard, Josh Triplett, Jonathan Walpole

Computer Science Faculty Publications and Presentations

Of the 200+ parallel-programming languages and environments created in the 1990s, almost all are now defunct. Given that parallel systems are now well within the budget of the typical hobbyist or graduate student, it is not unreasonable to expect a new cohort in excess of several thousand parallel languages and environments to appear in the 2010s. If this expected new cohort is to have more practical impact than did its 1990s counterpart, a robust and widely applicable framework will be required that encompasses exactly what, if anything, is hard about parallel programming. This paper revisits the fundamental precepts of concurrent …

Finding Irc-Like Meshes Sans Layer 7 Payloads, Akshay Dua, Jim Binkley, Suresh Singh

Computer Science Faculty Publications and Presentations

We present an algorithm for detecting IRC-like chat networks that does not rely on Layer 7 payload information. The goal is to extract only those meshes from conventional flows where long-term periodic data is being exchanged between an external server and multiple internal clients. Flow data is passed through a series of filters that reduce the memory requirements needed for final candidate mesh sorting. Final outputs consist of two sorted lists including the fanout list, sorted by the number of client hosts in the mesh, and a secondary list called the evil sort. The latter consists of meshes with any …

Evaluating Similarity-Based Trace Reduction Techniques For Scalable Performance Analysis, Kathryn Marie Mohror, Karen L. Karavanic

Computer Science Faculty Publications and Presentations

Event traces are required to correctly diagnose a number of performance problems that arise on today’s highly parallel systems. Unfortunately, the collection of event traces can produce a large volume of data that is difficult, or even impossible, to store and analyze. One approach for compressing a trace is to identify repeating trace patterns and retain only one representative of each pattern. However, determining the similarity of sections of traces, i.e., identifying patterns, is not straightforward. In this paper, we investigate pattern-based methods for reducing traces that will be used for performance analysis. We evaluate the different methods against several …

Squeak By Example, Andrew P. Black, Stéphane Ducasse, Oscar Nierstrasz, Damien Pollet, Damien Cassou, Marcus Denker

Computer Science Faculty Publications and Presentations

Squeak is a modern open-source development environment for the classic Smalltalk-80 programming language. This book, intended for both students and developers, will guide you gently through the language and tools by means of a series of examples and exercises.

Additional material is available from the book's web page at SqueakByExample.org.