Analyzing Concurrent Algorithms under Weak Memory Orderings
- Speaker : Bengt Jonsson
- Time : Thu, Nov 6th, 2008 at 13.30
- Room : 1113
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.