publication . Article . Conference object . Other literature type . Preprint . 2014

Herding Cats

Michael Tautschnig; Jade Alglave; Luc Maranget;
Open Access
  • Published: 01 Jun 2014 Journal: ACM Transactions on Programming Languages and Systems, volume 36, pages 1-74 (issn: 0164-0925, eissn: 1558-4593, Copyright policy)
  • Publisher: Association for Computing Machinery (ACM)
  • Country: France
Abstract
International audience; There is a joke where a physicist and a mathematician are asked to herd cats. The physicist starts with an infinitely large pen which he reduces until it is of reasonable diameter yet contains all the cats. The mathematician builds a fence around himself and declares the outside to be the inside. Defining memory models is akin to herding cats: both the physicist's or mathematician's attitudes are tempting, but neither can go without the other. When executing shared-memory concurrent programs, modern multiprocessors (e.g. Intel x86, IBM Power or ARM) exhibit be-haviours (e.g. store buffering or load delaying) that contradict the programmin...
Subjects
free text keywords: Software, Computer Graphics and Computer-Aided Design, Weak Memory Models, Verification, [INFO.INFO-DC]Computer Science [cs]/Distributed, Parallel, and Cluster Computing [cs.DC], [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], [ INFO.INFO-DC ] Computer Science [cs]/Distributed, Parallel, and Cluster Computing [cs.DC], [ INFO.INFO-PL ] Computer Science [cs]/Programming Languages [cs.PL], Experimentation, Verification Additional Key Words and Phrases: Concurrency, Categories and Subject Descriptors: B32 [Shared Memory], C0 [Hardware/Software Interfaces] General Terms: Theory, Computer Science - Logic in Computer Science, Theoretical computer science, Architecture, Concurrency, Axiom, Model checking, Software verification, Bounded function, Sequential consistency, Herding, Programming language, computer.software_genre, computer, Computer science, Joke, Artificial intelligence, business.industry, business, Simulation testing
77 references, page 1 of 6

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Carl Leonardsson, and Ahmed Rezine. 2012. Counter-example guided fence insertion under TSO. In Proceedings of TACAS. Springer-Verlag, Berlin, Heidelberg, 204-219. [OpenAIRE]

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Carl Leonardsson, and Ahmed Rezine. 2013. Memorax, a precise and sound tool for automatic fence insertion under TSO. In Proceedings of TACAS. Springer-Verlag, Berlin, Heidelberg, 530-536. [OpenAIRE]

Allon Adir, Hagit Attiya, and Gil Shurek. 2003. Information-flow models for shared memory with an application to the PowerPC architecture. IEEE Transactions on Parallel and Distributed Systems 14, 5, 502-515. [OpenAIRE]

Sarita V. Adve and Hans-Juergen Boehm. 2010. Memory models: A case for rethinking parallel languages and hardware. Communications of the ACM 53, 8, 90-101.

Sarita V. Adve and Kourosh Gharachorloo. 1996. Shared memory consistency models: A tutorial. IEEE Computer 29, 12, 66-76.

Jade Alglave. 2010. A Shared Memory Poetics. Ph.D. Dissertation. Universite´ Paris 7.

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

Jade Alglave, Anthony C. J. Fox, Samin Ishtiaq, Magnus O. Myreen, Susmit Sarkar, Peter Sewell, and Francesco Zappa Nardelli. 2009. The semantics of power and ARM multiprocessor machine code. In Proceedings of AMP. ACM Press, New York, NY, 13-24.

Jade Alglave, Daniel Kroening, John Lugton, Vincent Nimal, and Michael Tautschnig. 2011a. Soundness of data flow analyses for weak memory models. In Proceedings of APLAS. Springer-Verlag, Berlin, Heidelberg, 272-288.

Jade Alglave, Daniel Kroening, Vincent Nimal, and Michael Tautschnig. 2013a. Software verification for weak memory via program transformation. In Proceedings of ESOP. Springer-Verlag, Berlin, Heidelberg, 512-532.

Jade Alglave, Daniel Kroening, and Michael Tautschnig. 2013b. Partial orders for efficient bounded model checking of concurrent software. In Proceedings of CAV. Springer-Verlag, Berlin, Heidelberg, 141-157.

Jade Alglave and Luc Maranget. 2011. Stability in weak memory models. In Proceedings of CAV. SpringerVerlag, Berlin, Heidelberg, 50-66.

Jade Alglave, Luc Maranget, Susmit Sarkar, and Peter Sewell. 2010. Fences in weak memory models. In Proceedings of CAV. Springer-Verlag, Berlin, Heidelberg, 258-272. [OpenAIRE]

Jade Alglave, Luc Maranget, Susmit Sarkar, and Peter Sewell. 2011b. Litmus: Running tests against hardware. In Proceedings of TACAS. Springer-Verlag, Berlin, Heidelberg, 41-44.

Jade Alglave, Luc Maranget, Susmit Sarkar, and Peter Sewell. 2012. Fences in weak memory models (extended version). Formal Methods in System Design 40, 2, 170-205.

77 references, page 1 of 6
Abstract
International audience; There is a joke where a physicist and a mathematician are asked to herd cats. The physicist starts with an infinitely large pen which he reduces until it is of reasonable diameter yet contains all the cats. The mathematician builds a fence around himself and declares the outside to be the inside. Defining memory models is akin to herding cats: both the physicist's or mathematician's attitudes are tempting, but neither can go without the other. When executing shared-memory concurrent programs, modern multiprocessors (e.g. Intel x86, IBM Power or ARM) exhibit be-haviours (e.g. store buffering or load delaying) that contradict the programmin...
Subjects
free text keywords: Software, Computer Graphics and Computer-Aided Design, Weak Memory Models, Verification, [INFO.INFO-DC]Computer Science [cs]/Distributed, Parallel, and Cluster Computing [cs.DC], [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], [ INFO.INFO-DC ] Computer Science [cs]/Distributed, Parallel, and Cluster Computing [cs.DC], [ INFO.INFO-PL ] Computer Science [cs]/Programming Languages [cs.PL], Experimentation, Verification Additional Key Words and Phrases: Concurrency, Categories and Subject Descriptors: B32 [Shared Memory], C0 [Hardware/Software Interfaces] General Terms: Theory, Computer Science - Logic in Computer Science, Theoretical computer science, Architecture, Concurrency, Axiom, Model checking, Software verification, Bounded function, Sequential consistency, Herding, Programming language, computer.software_genre, computer, Computer science, Joke, Artificial intelligence, business.industry, business, Simulation testing
77 references, page 1 of 6

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Carl Leonardsson, and Ahmed Rezine. 2012. Counter-example guided fence insertion under TSO. In Proceedings of TACAS. Springer-Verlag, Berlin, Heidelberg, 204-219. [OpenAIRE]

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Carl Leonardsson, and Ahmed Rezine. 2013. Memorax, a precise and sound tool for automatic fence insertion under TSO. In Proceedings of TACAS. Springer-Verlag, Berlin, Heidelberg, 530-536. [OpenAIRE]

Allon Adir, Hagit Attiya, and Gil Shurek. 2003. Information-flow models for shared memory with an application to the PowerPC architecture. IEEE Transactions on Parallel and Distributed Systems 14, 5, 502-515. [OpenAIRE]

Sarita V. Adve and Hans-Juergen Boehm. 2010. Memory models: A case for rethinking parallel languages and hardware. Communications of the ACM 53, 8, 90-101.

Sarita V. Adve and Kourosh Gharachorloo. 1996. Shared memory consistency models: A tutorial. IEEE Computer 29, 12, 66-76.

Jade Alglave. 2010. A Shared Memory Poetics. Ph.D. Dissertation. Universite´ Paris 7.

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

Jade Alglave, Anthony C. J. Fox, Samin Ishtiaq, Magnus O. Myreen, Susmit Sarkar, Peter Sewell, and Francesco Zappa Nardelli. 2009. The semantics of power and ARM multiprocessor machine code. In Proceedings of AMP. ACM Press, New York, NY, 13-24.

Jade Alglave, Daniel Kroening, John Lugton, Vincent Nimal, and Michael Tautschnig. 2011a. Soundness of data flow analyses for weak memory models. In Proceedings of APLAS. Springer-Verlag, Berlin, Heidelberg, 272-288.

Jade Alglave, Daniel Kroening, Vincent Nimal, and Michael Tautschnig. 2013a. Software verification for weak memory via program transformation. In Proceedings of ESOP. Springer-Verlag, Berlin, Heidelberg, 512-532.

Jade Alglave, Daniel Kroening, and Michael Tautschnig. 2013b. Partial orders for efficient bounded model checking of concurrent software. In Proceedings of CAV. Springer-Verlag, Berlin, Heidelberg, 141-157.

Jade Alglave and Luc Maranget. 2011. Stability in weak memory models. In Proceedings of CAV. SpringerVerlag, Berlin, Heidelberg, 50-66.

Jade Alglave, Luc Maranget, Susmit Sarkar, and Peter Sewell. 2010. Fences in weak memory models. In Proceedings of CAV. Springer-Verlag, Berlin, Heidelberg, 258-272. [OpenAIRE]

Jade Alglave, Luc Maranget, Susmit Sarkar, and Peter Sewell. 2011b. Litmus: Running tests against hardware. In Proceedings of TACAS. Springer-Verlag, Berlin, Heidelberg, 41-44.

Jade Alglave, Luc Maranget, Susmit Sarkar, and Peter Sewell. 2012. Fences in weak memory models (extended version). Formal Methods in System Design 40, 2, 170-205.

77 references, page 1 of 6
Any information missing or wrong?Report an Issue