Type Systems for Multithreaded Software

 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.