Conference

Workshop

Local

Fun

Pig Data @ UW CSA

Our paper, The Barnyard of Pig Data Research: A View from UW CSA, was presented at PoCSci 2013.

Abstract

A new interdisciplinary program in Computer Science and Agriculture at the University of Washington is breaking down fences between diverse computational, scientific, and agricultural fields to cultivate research on disruptive Barnyard Computing technologies that will radically grow the impacts of emerging Pig Data applications. In this paper we plot the UW CSA view of Barnyard Computing and Pig Data, outlining high-priority research efforts within our immersive Pig Data agenda, our educational efforts to produce a new Pig Data workforce, and our innovations to leverage organic growth in this sector via a novel research funding model. These are exciting times at UW CSA!

Read our white paper (local draft for now, publicly available soon), peruse the slides, or (eventually) watch the talk video:

Concurrency Exceptions

The goal of this project is to provide (and exploit) support for exceptions delivered on concurrency errors. Our initial focus is on data-race exceptions, which can help simplify memory models to provide stronger semantics to programmers and can also aid in higher-level debugging or dynamic analysis. Many ideas from our work on low-level data-race detection and exceptions generalize to other types of concurrency errors. We have developed a hybrid hardware-software dynamic data-race detector (RADISH, ISCA 2012) that is sound and complete and has performance good enough for many deployment situations. We have also outlined potential unorthodox uses of low-level data-race exceptions (MSPC 2011). Currently, we are exploring the implications of data-race exceptions throughout the system stack.

Cloud Types for EC

In summer 2011, I interned in the RiSE group at Microsoft Research with Sebastian Burckhardt, Daan Leijen, and Manuel Fahndrich. We adapted the Concurrent Revisions model to provide language support for eventually consistent storage in simple distributed systems such as smartphone applications sharing data through the cloud. The resulting paper will appear at ECOOP 2012.

Greedy Coherence

Greedy Coherence is a simple mechanism for best-effort avoidance of sequential consistency violations and small-scale atomicity violations. It works by delaying responses to coherence requests for recently used or in-flight memory addrseses.

Recon

Our paper Isolating and Understanding Concurrency Errors Using Reconstructed Execution Fragments was accepted to PLDI 2011.

Multicore Memory Models for the Masses

There is an attempt afoot to establish a new world order (NWO) in computing. This paper discusses why you should join us to rise up against this new world order and reclaim multicore memory models for the masses. We demonstrate how current memory models not only fail to meet the needs of programmers but, worse yet, actively subjugate them. We outline a number of proposals for new and friendlier memory models, citing examples from the real world.

Paper forthcoming.

OSHA (Organized Sharing)

The goal of the OSHA project is to make inter-thread communication through shared memory explicit by specifying and checking which pieces of code communicate between threads by writing and reading shared memory. We have built a modular specification language and checker for inter-thread communication in Java programs (OOPSLA 2010) and an earlier communication understanding and visualization tool for C and C++ programs.

Hominy Grits: Specification and Inference of Synchronization Disciplines for Concurrent Programs

Most previous work on race condition detection and inference of synchronization disciplines (methods of synchronizing access to shared data in concurrent programs) has focused on the lockset model, using both static and dynamic analyses. However, the lockset model is restrictive and is not sufficiently expressive to capture synchronization disciplines other than mutual exclusion locks. We present the Grits synchronization discipline specification language, an expressive model for ensuring race-freedom in concurrent programs. We also present Hominy, an accompanying synchronization discipline specification inference tool for the Grits specification language. Our experience shows that Grits and Hominy are sufficiently expressive to capture nearly all synchronization disciplines.

Errata

The example ChangeLocks program presented in Figure 5.1 (page 60) can fail to terminate due to missed updates in non-atomic decrements of the volatile barrier field. Nonetheless, the specification inferred by Hominy is correct.