Analyzing Concurrent Algorithms under Weak Memory Orderings

• Speaker : Bengt Jonsson
• Time : Thu, Nov 6th, 2008 at 13.30
• Room : 1113

Abstract

Several concurrent implementations of familiar data abstractions such as queues, sets, or maps typically do not follow locking disciplines, and often use lock-free synchronization to gain performance.

Since such algorithms are exposed to a weak memory model (weaker than the traditional sequential consistency or interleaving model), they are harder to get correct.

We outline a technique for analyzing correctness of concurrent algorithms under weak memory models, in which a model checker is used to search for correctness violations. The algorithm to be analyzed is transformed into a form where statements may be reordered according to a particular weak memory ordering. The transformed algorithm can then be analyzed by a model-checking tool, e.g., by enumerative state exploration. We illustrate the approach on a small example, for a particular memory model.

The seminar will also provide some introduction to different memory models, and how they can be taken into account during different forms of analysis.