An invariant pattern-based approach to develop concurrent programs

In recent years, the importance of concurrent programming has increased. However, many programmers are not appropriately trained to write correct and efficient concurrent programs. The techniques that most Operating Systems (OS) textbooks teach are ad-hoc, and such ad-hoc techniques are far too error-prone for solving complex synchronization problems. The global invariant approach developed by G. Andrews is much more formal and structured, and we have been teaching this approach since 1992 at Kansas State University. One possible drawback of the invariant approach is the difficulty to identify an appropriate invariant for a given synchronization requirement. To cope with this problem, we have developed a set of useful synchronization patterns and their solution invariants. Using the patterns, we can solve a wide-variety of synchronization problems found in many advanced OS textbooks. In Fall 2001, we successfully taught our pattern-based approach in our graduate-level OS course. In this paper, we will present our methodology and report qualitative and quantitative evaluation of the methodology by students in the classroom setting.