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