Dissertation Talk: Lightweight Specifications for Parallel Correctness

Seminar: Departmental | December 5 | 11 a.m.-12 p.m. | 373 Soda Hall

Speaker/Performer: Jacob Burnim, UC Berkeley EECS

Sponsor: Electrical Engineering and Computer Sciences (EECS)

The spread of multicore processors and the end of rapidly growing single-core performance is increasing the need for programmers to write parallel software. Yet writing correct parallel programs with explicit multithreading remains a difficult undertaking. Though many tools exist to help test, debug, and verify parallel programs, such tools are often hindered by a lack of any specification from the
programmer as to the intended, correct parallel behavior of his or her software. In this talk, I will give an overview of our work on lightweight specifications for the parallelism correctness of multithreaded software. By focusing on just the correctness of a program's use of parallelism, we have developed several novel, lightweight specifications for parallel software: semantic determinism, semantic atomicity, and nondeterministic sequential specifications for parallelism correctness. These specifications are not only simple for programmers to write -- they enable us to much more effectively test, debug, and verify parallel software, independent of the software's complex and sequential functional correctness.

Target audiences: Faculty, Students - Graduate

Open to audience: All Audiences

Event Contact: jburnim@cs.berkeley.edu, 415-971-8004