Type Systems for Multithreaded Software

Developing correct multithreaded software is very challenging, due to the potential for unintended interference between threads. We present type systems for verifying two key non-interference properties in multithreaded software: race-freedom and atomicity. Verifying atomicity is particularly valuable since atomic procedures can be understood according to their sequential semantics, which significantly simplifies subsequent (formal and informal) correctness arguments. We will describe our experience applying these type systems and corresponding type inference algorithms to standard multithreaded benchmarks and other applications, and illustrate some defects revealed by this approach.

Speaker Details

Cormac Flanagan is a faculty member in the Computer Science Department at the University of California, Santa Cruz, and previously was a research scientist for Digital, Compaq, and HP. His research focuses on static and dynamic checking tools that improve program reliability and reduce development cost, with a particular focus on concurrent software systems. He is the recipient of a Sloan Foundation Fellowship, and received his Ph.D. from Rice University in 1997.

Date:
Speakers:
Cormac Flanagan
Affiliation:
University of California, Santa Cruz

    • Portrait of Jeff Running

      Jeff Running