%0 Conference Paper %1 1229469 %A Saraswat, Vijay A. %A Jagadeesan, Radha %A Michael, Maged %A von Praun, Christoph %B PPoPP '07: Proceedings of the 12th ACM SIGPLAN symposium on Principles and practice of parallel programming %C New York, NY, USA %D 2007 %I ACM %K Background C++ Formalism Imperative Java Mathematics Memory Model Theory %P 161--172 %R http://doi.acm.org/10.1145/1229428.1229469 %T A Theory of Memory Models %U http://www.saraswat.org/raofull.pdf %X A 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. To instantiate this framework for a specific language, the designer must choose the notion of atomic steps supported by the language (e.g. 32-bit reads and writes) and specify how a composite step may be broken into a sequence of atomic steps (the decomposition rule). This rule determines which sequence of intermediate writes (if any) are visible to concurrent reads by other threads. Different choices of the rule lead to models which permit a read to return any value if there is a concurrent write (race), or models which satisfy a "No Thin Air Read"property. The former is suitable for languages such as C++(programs with races have undefined behavior), and the latter for Java. Other intermediate models are possible, useful and interesting. %@ 978-1-59593-602-8

@inproceedings{1229469, abstract = {A 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. To instantiate this framework for a specific language, the designer must choose the notion of atomic steps supported by the language (e.g. 32-bit reads and writes) and specify how a composite step may be broken into a sequence of atomic steps (the decomposition rule). This rule determines which sequence of intermediate writes (if any) are visible to concurrent reads by other threads. Different choices of the rule lead to models which permit a read to return any value if there is a concurrent write (race), or models which satisfy a "No Thin Air Read"property. The former is suitable for languages such as C++(programs with races have undefined behavior), and the latter for Java. Other intermediate models are possible, useful and interesting.}, added-at = {2009-10-18T17:20:33.000+0200}, address = {New York, NY, USA}, author = {Saraswat, Vijay A. and Jagadeesan, Radha and Michael, Maged and von Praun, Christoph}, biburl = {https://www.bibsonomy.org/bibtex/2066d942fae10d0680c6cfec2ab07d07d/gron}, booktitle = {PPoPP '07: Proceedings of the 12th ACM SIGPLAN symposium on Principles and practice of parallel programming}, description = {A theory of memory models}, doi = {http://doi.acm.org/10.1145/1229428.1229469}, interhash = {f4feb34554dfd0a31c1ff99a07a1c3fd}, intrahash = {066d942fae10d0680c6cfec2ab07d07d}, isbn = {978-1-59593-602-8}, keywords = {Background C++ Formalism Imperative Java Mathematics Memory Model Theory}, location = {San Jose, California, USA}, pages = {161--172}, publisher = {ACM}, timestamp = {2009-10-18T17:20:33.000+0200}, title = {A Theory of Memory Models}, url = {http://www.saraswat.org/raofull.pdf}, year = 2007 }