Beverly A. Sanders
ABSTRACT
We describe the ideas behind a method to use assertional reasoning to statically show that all sequentially consistent executions of a concurrent program are free from data races.
- Jeremy Manson, William Pugh, and Sarita V. Adve. The java memory model. In POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 378--391, New York, NY, USA, 2005. ACM Press. Google Scholar
Digital Library
- Susan Owicki and David Gries. Verifying Properties of Parallel Programs: an Axiomatic Approach. Commun. ACM, 19(5):279--285, 1976. Google ScholarDigital Library
- Vijay A. Saraswat, Radha Jagadeesan, Maged Michael, and Christoph von Praun. A Theory of Memory Models. In PPoPP '07: Proceedings of the 12th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, pages 161--172, New York, NY, USA, 2007. ACM Press. Google ScholarDigital Library
- Beverly A. Sanders and KyungHee Kim. Assertional Reasoning about Data Races in Relaxed Memory Models. Technical report, Department of Computer and Information Science and Engineering, University of Florida, 2007.Google Scholar
Index Terms
- Assertional reasoning about data races in relaxed memory models
Recommendations
Foundations of the C++ concurrency memory model
PLDI '08Currently multi-threaded C or C++ programs combine a single-threaded programming language with a separate threads library. This is not entirely sound [7].
We describe an effort, currently nearing completion, to address these issues by explicitly ...
Foundations of the C++ concurrency memory model
PLDI '08: Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and ImplementationCurrently multi-threaded C or C++ programs combine a single-threaded programming language with a separate threads library. This is not entirely sound [7].
We describe an effort, currently nearing completion, to address these issues by explicitly ...
A theory of memory models
PPoPP '07: Proceedings of the 12th ACM SIGPLAN symposium on Principles and practice of parallel programmingA memory model for a concurrent imperative programming language specifies which writes to shared variables may be seen by reads performed by other threads. We present a simple mathematical framework for relaxed memory models for programming languages. ...
Comments