publication . Preprint . 2017

Weak Memory Models with Matching Axiomatic and Operational Definitions

Zhang, Sizhuo; Vijayaraghavan, Muralidaran; Lustig, Dan; Arvind;
Open Access English
  • Published: 11 Oct 2017
Abstract
Memory consistency models are notorious for being difficult to define precisely, to reason about, and to verify. More than a decade of effort has gone into nailing down the definitions of the ARM and IBM Power memory models, and yet there still remain aspects of those models which (perhaps surprisingly) remain unresolved to this day. In response to these complexities, there has been somewhat of a recent trend in the (general-purpose) architecture community to limit new memory models to being (multicopy) atomic: where store values can be read by the issuing processor before being advertised to other processors. TSO is the most notable example, used in the past by...
Subjects
free text keywords: Computer Science - Programming Languages
Download from
56 references, page 1 of 4

[1] The risc-v instruction set. https://riscv.org/.

[2] Alpha Architecture Handbook, Version 4. Compaq Computer Corporation, 1998.

[3] Sarita V Adve and Kourosh Gharachorloo. Shared memory consistency models: A tutorial. computer, 29(12):66-76, 1996.

[4] Jade Alglave. A formal hierarchy of weak memory models. Formal Methods in System Design, 41(2):178- 210, 2012.

[5] Jade Alglave, Anthony Fox, Samin Ishtiaq, Magnus O Myreen, Susmit Sarkar, Peter Sewell, and Francesco Zappa Nardelli. The semantics of power and arm multiprocessor machine code. In Proceedings of the 4th workshop on Declarative aspects of multicore programming, pages 13-24. ACM, 2009.

[6] Jade Alglave, Daniel Kroening, Vincent Nimal, and Michael Tautschnig. Software verification for weak memory via program transformation. In Programming Languages and Systems, pages 512-532. Springer, 2013.

[7] Jade Alglave and Luc Maranget. Computer Aided Verification: 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, chapter Stability in Weak Memory Models, pages 50-66. Springer Berlin Heidelberg, Berlin, Heidelberg, 2011.

[8] Jade Alglave, Luc Maranget, and Michael Tautschnig. Herding cats: Modelling, simulation, testing, and data mining for weak memory. ACM Transactions on Programming Languages and Systems (TOPLAS), 36(2):7, 2014.

[9] ARM. Cortex-A9 MPCoreTM, programmer advice notice, read-after-read hazards. Technical report, 2011. URL: http://infocenter.arm.com/help/topic/com.arm.doc.uan0004a/UAN0004A_a9_read_read.pdf.

[10] ARM. ARM Architecture Reference Manual: ARMv8, for ARMv8-A architecture profile. 2017.

[11] Arvind and Jan-Willem Maessen. Memory model = instruction reordering + store atomicity. In ACM SIGARCH Computer Architecture News, volume 34, pages 29-40. IEEE Computer Society, 2006.

[12] Mark Batty, Alastair F. Donaldson, and John Wickerson. Overhauling sc atomics in c11 and opencl. SIGPLAN Not., 51(1):634-648, January 2016.

[13] Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, and Tjark Weber. Mathematizing c++ concurrency. In ACM SIGPLAN Notices, volume 46, pages 55-66. ACM, 2011.

[14] Colin Blundell, Milo MK Martin, and Thomas F Wenisch. Invisifence: performance-transparent memory ordering in conventional multiprocessors. In ACM SIGARCH Computer Architecture News, volume 37, pages 233-244. ACM, 2009.

[15] Hans-J Boehm and Sarita V Adve. Foundations of the c++ concurrency memory model. In ACM SIGPLAN Notices, volume 43, pages 68-78. ACM, 2008.

56 references, page 1 of 4
Powered by OpenAIRE Open Research Graph
Any information missing or wrong?Report an Issue