author: Niels ten Dijke
title: Comparison of Verification Methods for Weak Memory Models
keywords: Weak memory models, Program verification, Comparison Overview
topics: Logics and semantics
committee: Jaco van de Pol
started: September 2013
end: January 2014

Abstract

Modern multi-core systems allow for reordering of memory instructions for performance reasons. This reordering of instructions can be a source of bugs, especially in algorithms which do not use locks for synchronization. Verification of concurrent code on relaxed memory models is a computationally hard problem and many approaches to verify software under these models have been proposed,however no overview or comparison of current methods exists. In this project we give an overview of three recent veri fication methods for relaxed memory models. These methods are mainly chosen because, next to being cited, they have tools which can be used to verify concurrentcode. Furthermore, these methods are recent and shouldgive a good picture of the current state of the art. We compare these methods on veri fication of real world software, i.e. algorithms which have been proposed in research or are used in industry, under commonly used weak memory models. This is done by running the tools against a benchmark of concurrent C programs.

References

  1. S. V. Adve and K. Gharachorloo. Shared memory consistency models: A tutorial. computer, 29(12):66-76, 1996
  2. J. Alglave, D. Kroening, V. Nimal, and M. Tautschnig. Software verification for weak memory via program transformation. In Programming Languages and Systems, pages 512{532. Springer, 2013.

Additional Resources

  1. The paper