Abstract:

Multithreaded programs often exhibit erroneous behavior because of unintended interactions between threads. In these talks, we will explore lightweight analyses for preventing such errors. We will focus on several key non-interference properties including the absence of simultaneous-access race conditions and the stronger notion of atomicity. A method is atomic if its execution is not affected by and does not interfere with concurrently-executing threads. Atomic methods can be understood according to their sequential semantics, which significantly simplifies formal and informal correctness arguments and subsequent validation activities such as code inspection and testing.

These non-interference properties will be examined in the context of type systems because they often provide the best balance between ease-of-use, scalability, and expressiveness. Specific topics include the theoretical foundations and implementation issues surrounding these systems, as well as type inference algorithms for them. We will also discuss our experiences with prototype checkers and alternative approaches based model-checking, dynamic analysis, and theorem proving.