research-article

Open access

Herding Cats: Modelling, Simulation, Testing, and Data Mining for Weak Memory

Authors:

Michael TautschnigAuthors Info & Claims

ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 36, Issue 2

Article No.: 7, Pages 1 - 74

https://doi.org/10.1145/2627752

Published: 01 July 2014 Publication History

Abstract

We propose an axiomatic generic framework for modelling weak memory. We show how to instantiate this framework for Sequential Consistency (SC), Total Store Order (TSO), C++ restricted to release-acquire atomics, and Power. For Power, we compare our model to a preceding operational model in which we found a flaw. To do so, we define an operational model that we show equivalent to our axiomatic model.

We also propose a model for ARM. Our testing on this architecture revealed a behaviour later acknowledged as a bug by ARM, and more recently, 31 additional anomalies.

We offer a new simulation tool, called herd, which allows the user to specify the model of his choice in a concise way. Given a specification of a model, the tool becomes a simulator for that model. The tool relies on an axiomatic description; this choice allows us to outperform all previous simulation tools. Additionally, we confirm that verification time is vastly improved, in the case of bounded model checking.

Finally, we put our models in perspective, in the light of empirical data obtained by analysing the C and C++ code of a Debian Linux distribution. We present our new analysis tool, called mole, which explores a piece of code to find the weak memory idioms that it uses.

References

[1]

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.

Digital Library

[2]

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.

Digital Library

[3]

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.

Digital Library

[4]

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.

Digital Library

[5]

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

Digital Library

[6]

Jade Alglave. 2010. A Shared Memory Poetics. Ph.D. Dissertation. Université Paris 7.

[7]

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

Digital Library

[8]

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.

Digital Library

[9]

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.

Digital Library

[10]

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.

Digital Library

[11]

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.

[12]

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

Digital Library

[13]

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.

Digital Library

[14]

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.

Digital Library

[15]

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.

Digital Library

[16]

ARM Ltd. 2010. ARM Architecture Reference Manual: ARMv7-A and ARMv7-R Edition. ARM Ltd.

[17]

ARM Ltd. 2011. Cortex-A9 MPCore, Programmer Advice Notice, Read-after-Read Hazards. ARM Ltd.

[18]

Arvind and Jan-Willem Maessen. 2006. Memory Model = Instruction Reordering + Store Atomicity. In Proceedings of ISCA. IEEE Computer Society, Washington, DC, 29--40.

Digital Library

[19]

Mohamed Faouzi Atig, Ahmed Bouajjani, Sebastian Burckhardt, and Madanlal Musuvathi. 2010. On the verification problem for weak memory models. In Proceedings of POPL. ACM Press, New York, NY, 7--18.

Digital Library

[20]

Mohamed Faouzi Atig, Ahmed Bouajjani, Sebastian Burckhardt, and Madanlal Musuvathi. 2012. What’s decidable about weak memory models&quest; In Proceedings of ESOP. Springer-Verlag, Berlin, Heidelberg, 26--46.

Digital Library

[21]

Mohamed Faouzi Atig, Ahmed Bouajjani, and Gennaro Parlato. 2011. Getting rid of store-buffers in TSO analysis. In Proceedings of CAV. Springer-Verlag, Berlin, Heidelberg, 99--115.

Digital Library

[22]

Mark Batty, Mike Dodds, and Alexey Gotsman. 2013. Library abstraction for C/C++ concurrency. In Proceedings of POPL. ACM Press, New York, NY, 235--248.

Digital Library

[23]

Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, and Tjark Weber. 2011. Mathematizing C++ concurrency. In Proceedings of POPL. ACM Press, New York, NY, 55--66.

Digital Library

[24]

Yves Bertot and Pierre Casteran. 2004. Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions. Springer-Verlag.

Digital Library

[25]

Hans-Juergen Boehm and Sarita V. Adve. 2008. Foundations of the C++ concurrency memory model. In Proceedings of PLDI. ACM Press, New York, NY, 68--78.

Digital Library

[26]

Hans-Juergen Boehm and Sarita V. Adve. 2012. You don’t know jack about shared variables or memory models. Communications of the ACM 55, 2, 48--54.

Digital Library

[27]

Ahmed Bouajjani, Egor Derevenetc, and Roland Meyer. 2013. Checking and enforcing robustness against TSO. In Proceedings of ESOP. Springer-Verlag, Berlin, Heidelberg, 533--553.

Digital Library

[28]

Ahmed Bouajjani, Roland Meyer, and Eike Möhlmann. 2011. Deciding robustness against total store ordering. In Proceedings of ICALP (2). Springer-Verlag, Berlin, Heidelberg, 428--440.

Digital Library

[29]

Gérard Boudol and Gustavo Petri. 2009. Relaxed memory models: An operational approach. In Proceedings of POPL. ACM Press, New York, NY, 392--403.

Digital Library

[30]

Gérard Boudol, Gustavo Petri, and Bernard P. Serpette. 2012. Relaxed operational semantics of concurrent programming languages. In Proceedings of EXPRESS/SOS. 19--33.

[31]

Sebastian Burckhardt, Rajeev Alur, and Milo M. K. Martin. 2007. CheckFence: Checking consistency of concurrent data types on relaxed memory models. In Proceedings of PLDI. ACM, New York, NY, 12--21.

Digital Library

[32]

Sebastian Burckhardt, Alexey Gotsman, and Hongseok Yang. 2013. Understanding eventual consistency. Technical Report TR-2013-39. Microsoft Research.

[33]

Sebastian Burckhardt, Alexey Gotsman, Hongseok Yang, and Marek Zawirski. 2014. Replicated data types: Specification, verification, optimality. In Proceedings of POPL. ACM Press, New York, NY, 271--284.

Digital Library

[34]

Sebastian Burckhardt and Madan Musuvathi. 2008. Memory Model Safety of Programs. In Proceedings of the Workshop on Exploiting Concurrency Efficiently and Correctly (EC)².

[35]

Pietro Cenciarelli, Alexander Knapp, and Eleonora Sibilio. 2007. The Java memory model: Operationally, denotationally, axiomatically. In Proceedings of ESOP. Springer-Verlag, Berlin, Heidelberg, 331--346.

Digital Library

[36]

Nathan Chong and Samin Ishtiaq. 2008. Reasoning about the ARM weakly consistent memory model. In Proceedings of MSPC. ACM Press, New York, NY, 16--19.

Digital Library

[37]

Edmund M. Clarke, Daniel Kroening, and Flavio Lerda. 2004. A tool for checking ANSI-C programs. In Proceedings of TACAS. Springer-Verlag, Berlin, Heidelberg, 168--176.

[38]

William Collier. 1992. Reasoning About Parallel Architectures. Prentice Hall.

Digital Library

[39]

Compaq Computer Corp. 2002. Alpha Architecture Reference Manual. Compaq Computer Corp.

[40]

Kourosh Gharachorloo, Daniel Lenoski, James Laudon, Phillip B. Gibbons, Anoop Gupta, and John L. Hennessy. 1990. Memory consistency and event ordering in scalable shared-memory multiprocessors. In Proceedings of ISCA. ACM Press, New York, NY, 15--26.

Digital Library

[41]

Jacob Goodman. 1989. Cache consistency and sequential consistency. Technical Report. IEEE Scalable Coherent Interface Group.

[42]

Ganesh Gopalakrishnan, Yue Yang, and Hemanthkumar Sivaraj. 2004. QB or not QB: An efficient execution verification tool for memory orderings. In Proceedings of CAV. Springer-Verlag, Berlin, Heidelberg, 401--413.

[43]

Michael J. C. Gordon. 2002. Relating event and trace semantics of hardware description languages. Computer Journal 45, 1, 27--36.

[44]

Richard Grisenthwaite. 2009. ARM Barrier Litmus Tests and Cookbook. ARM Ltd.

[45]

Sudheendra Hangal, Durgam Vahia, Chaiyasit Manovit, Juin-Yeu Joseph Lu, and Sridhar Narayanan. 2004. TSOtool: A program for verifying memory systems using the memory consistency model. In Proceedings of ISCA. IEEE Computer Society, Washington, DC, 114--123.

Digital Library

[46]

C. A. R. Hoare and Peter E. Lauer. 1974. Consistent and complementary formal theories of the semantics of programming languages. Acta Informatica 3, 135--153.

Digital Library

[47]

David Howells and Paul E. MacKenney. 2013. Linux Kernel Memory Barriers, 2013 version. Retrieved May 29, 2014, from https://www.kernel.org/doc/Documentation/memory-barriers.txt.

[48]

IBM Corp. 2009. Power ISA Version 2.06. IBM Corp.

[49]

Intel Corp. 2002. A Formal Specification of Intel Itanium Processor Family Memory Ordering. Intel Corp.

[50]

Intel Corp. 2009. Intel 64 and IA-32 Architectures Software Developer’s Manual. Intel Corp.

[51]

ISO. 2011. ISO/IEC 9899:2011 Information technology — Programming languages — C. International Organization for Standardization.

[52]

Daniel Jackson. 2002. Alloy: A lightweight object modelling notation. ACM Transactions on Software Engineering and Methodology 11, 2, 256--290.

Digital Library

[53]

Vineet Kahlon, Yu Yang, Sriram Sankaranarayanan, and Aarti Gupta. 2007. Fast and accurate static data-race detection for concurrent programs. In Proceedings of CAV. Springer-Verlag, Berlin, Heidelberg, 226--239.

Digital Library

[54]

Michael Kuperstein, Martin T. Vechev, and Eran Yahav. 2010. Automatic inference of memory fences. In Proceedings of FMCAD. IEEE Computer Society, Washington, DC, 111--119.

Digital Library

[55]

Michael Kuperstein, Martin T. Vechev, and Eran Yahav. 2011. Partial-coherence abstractions for relaxed memory models. In Proceedings of PLDI. ACM Press, New York, NY, 187--198.

Digital Library

[56]

Leslie Lamport. 1979. How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Transactions on Computer Systems 28, 9, 690--691.

Digital Library

[57]

Richard J. Lipton and Jonathan S. Sandberg. 1988. PRAM: A scalable shared memory. Technical Report CS-TR-180-88. Princeton University.

[58]

Feng Liu, Nayden Nedev, Nedyalko Prisadnikov, Martin T. Vechev, and Eran Yahav. 2012. Dynamic synthesis for relaxed memory models. In Proceedings of PLDI. ACM Press, New York, NY, 429--440.

Digital Library

[59]

Sela Mador-Haim, Rajeev Alur, and Milo M. K. Martin. 2010. Generating litmus tests for contrasting memory consistency models. In Proceedings of CAV. Springer-Verlag, Berlin, Heidelberg, 273--287.

Digital Library

[60]

Sela Mador-Haim, Luc Maranget, Susmit Sarkar, Kayvan Memarian, Jade Alglave, Scott Owens, Rajeev Alur, Milo M. K. Martin, Peter Sewell, and Derek Williams. 2012. An axiomatic memory model for POWER multiprocessors. In Proceedings of CAV. Springer-Verlag, Berlin, Heidelberg, 495--512.

Digital Library

[61]

Jeremy Manson, William Pugh, and Sarita V. Adve. 2005. The Java memory model. In Proceedings of POPL. ACM Press, New York, NY, 378--391.

Digital Library

[62]

Paul E. McKenney and Jonathan Walpole. 2007. What is RCU, fundamentally&quest; Retrieved May 29, 2014, from http://lwn.net/Articles/262464/.

[63]

Gil Neiger. 2000. A taxonomy of multiprocessor memory-ordering models. In Tutorial and Workshop on Formal Specification and Verification Methods for Shared Memory Systems.

[64]

Scott Owens, Peter Böhm, Francesco Zappa Nardelli, and Peter Sewell. 2011. Lem: A lightweight tool for heavyweight semantics. In Proceedings of ITP. Springer-Verlag, Berlin, Heidelberg, 363--369.

Digital Library

[65]

Scott Owens, Susmit Sarkar, and Peter Sewell. 2009. A better x86 memory model: x86-TSO. In Proceedings of TPHOLs. Springer-Verlag, Berlin, Heidelberg, 391--407.

Digital Library

[66]

Susmit Sarkar, Kayvan Memarian, Scott Owens, Mark Batty, Peter Sewell, Luc Maranget, Jade Alglave, and Derek Williams. 2012. Synchronising C/C++ and POWER. In Proceedings of PLDI. ACM Press, New York, NY, 311--322.

Digital Library

[67]

Susmit Sarkar, Peter Sewell, Jade Alglave, Luc Maranget, and Derek Williams. 2011. Understanding power multiprocessors. In Proceedings of PLDI. ACM Press, New York, NY, 175--186.

Digital Library

[68]

Susmit Sarkar, Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Tom Ridge, Thomas Braibant, Magnus O. Myreen, and Jade Alglave. 2009. The semantics of x86-CC multiprocessor machine code. In Proceedings of POPL. ACM Press, New York, NY, 379--391.

Digital Library

[69]

Dennis Shasha and Marc Snir. 1988. Efficient and correct execution of parallel programs that share memory. ACM Transactions on Programming and Language Systems 10, 2, 282--312.

Digital Library

[70]

SPARC International Inc. 1992. The SPARC Architecture Manual Version 8. SPARC International Inc.

Digital Library

[71]

SPARC International Inc. 1994. The SPARC Architecture Manual Version 9. SPARC International Inc.

Digital Library

[72]

Robert C. Steinke and Gary J. Nutt. 2004. A unified theory of shared memory consistency. Journal of the ACM 51, 5, 800--849.

Digital Library

[73]

Robert Tarjan. 1973. Enumeration of the elementary circuits of a directed graph. SIAM Journal of Computing 2, 3, 211--216.

Digital Library

[74]

Joel M. Tendler, J. Steve Dodson, J. S. Fields Jr., Hung Le, and Balaram Sinharoy. 2002. POWER4 system microarchitecture. IBM Journal of Research and Development 46, 1, 5--26.

Digital Library

[75]

Emina Torlak, Mandana Vaziri, and Julian Dolby. 2010. MemSAT: Checking axiomatic specifications of memory models. In Proceedings of PLDI. ACM Press, New York, NY, 341--350.

Digital Library

[76]

Yue Yang, Ganesh Gopalakrishnan, Gary Lindstrom, and Konrad Slind. 2004. Nemos: A framework for axiomatic and executable specifications of memory consistency models. In Proceedings of IPDPS. IEEE Computer Society, Washington, DC, 31b.

[77]

Francesco Zappa Nardelli, Peter Sewell, Jaroslav Sevcik, Susmit Sarkar, Scott Owens, Luc Maranget, Mark Batty, and Jade Alglave. 2009. Relaxed memory models must be rigorous. In Proceedings of the Workshop on Exploiting Concurrency Efficiently and Correctly (EC)².

Cited By

Bargmann LWehrheim H(2025)View-based axiomatic reasoning for the weak memory models PSO and SRAScience of Computer Programming10.1016/j.scico.2024.103225240(103225)Online publication date: Feb-2025
https://doi.org/10.1016/j.scico.2024.103225
Bender JNaik MPereira FTitzer B(2024)Correct Compilation of Concurrent C CodeProceedings of the Workshop Dedicated to Jens Palsberg on the Occasion of His 60th Birthday10.1145/3694848.3694856(39-42)Online publication date: 22-Oct-2024
https://dl.acm.org/doi/10.1145/3694848.3694856
Ambal GDongol BEran HKlimis VLahav ORaad A(2024)Semantics of Remote Direct Memory Access: Operational and Declarative Models of RDMA on TSO ArchitecturesProceedings of the ACM on Programming Languages10.1145/36897818:OOPSLA2(1982-2009)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689781
Show More Cited By

Index Terms

Herding Cats: Modelling, Simulation, Testing, and Data Mining for Weak Memory
1. Computer systems organization
2. Hardware
  1. Integrated circuits
    1. Semiconductor memory

Recommendations

Partial-coherence abstractions for relaxed memory models
PLDI '11

We present an approach for automatic verification and fence inference in concurrent programs running under relaxed memory models. Verification under relaxed memory models is a hard problem. Given a finite state program and a safety specification, ...
Partial-coherence abstractions for relaxed memory models
PLDI '11: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation

We present an approach for automatic verification and fence inference in concurrent programs running under relaxed memory models. Verification under relaxed memory models is a hard problem. Given a finite state program and a safety specification, ...
Optimal Reads-From Consistency Checking for C11-Style Memory Models

Over the years, several memory models have been proposed to capture the subtle concurrency semantics of C/C++. One of the most fundamental problems associated with a memory model M is consistency checking: given an execution X, is X consistent with M? ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Programming Languages and Systems

ACM Transactions on Programming Languages and Systems Volume 36, Issue 2

July 2014

171 pages

ISSN:0164-0925

EISSN:1558-4593

DOI:10.1145/2633904

Issue’s Table of Contents

Copyright © 2014 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 July 2014

Accepted: 01 February 2014

Revised: 01 December 2013

Received: 01 August 2013

Published in TOPLAS Volume 36, Issue 2

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

243
Total Citations
View Citations
2,113
Total Downloads

Downloads (Last 12 months)555
Downloads (Last 6 weeks)81

Reflects downloads up to 17 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Bargmann LWehrheim H(2025)View-based axiomatic reasoning for the weak memory models PSO and SRAScience of Computer Programming10.1016/j.scico.2024.103225240(103225)Online publication date: Feb-2025
https://doi.org/10.1016/j.scico.2024.103225
Bender JNaik MPereira FTitzer B(2024)Correct Compilation of Concurrent C CodeProceedings of the Workshop Dedicated to Jens Palsberg on the Occasion of His 60th Birthday10.1145/3694848.3694856(39-42)Online publication date: 22-Oct-2024
https://dl.acm.org/doi/10.1145/3694848.3694856
Ambal GDongol BEran HKlimis VLahav ORaad A(2024)Semantics of Remote Direct Memory Access: Operational and Declarative Models of RDMA on TSO ArchitecturesProceedings of the ACM on Programming Languages10.1145/36897818:OOPSLA2(1982-2009)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689781
de Vilhena PLahav OVafeiadis VRaad A(2024)Extending the C/C++ Memory Model with Inline AssemblyProceedings of the ACM on Programming Languages10.1145/36897498:OOPSLA2(1081-1107)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689749
Kokologiannakis MMarmanis IVafeiadis V(2024)SPORE: Combining Symmetry and Partial Order ReductionProceedings of the ACM on Programming Languages10.1145/36564498:PLDI(1781-1803)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656449
Svyatlovskiy MMermelstein SLahav O(2024)Compositional Semantics for Shared-Variable ConcurrencyProceedings of the ACM on Programming Languages10.1145/36563998:PLDI(543-566)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656399
Geng CBlanas SBond MWang Y(2024)IsoPredict: Dynamic Predictive Analysis for Detecting Unserializable Behaviors in Weakly Isolated Data Store ApplicationsProceedings of the ACM on Programming Languages10.1145/36563918:PLDI(343-367)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656391
Bailleu MStavrakakis DRocha RChakraborty SGarg DBhatotia P(2024)Toast: A Heterogeneous Memory Management SystemProceedings of the 2024 International Conference on Parallel Architectures and Compilation Techniques10.1145/3656019.3676944(53-65)Online publication date: 14-Oct-2024
https://dl.acm.org/doi/10.1145/3656019.3676944
Zhang AGoens AOswald NGrosser TSorin DNagarajan V(2024)PipeGen: Automated Transformation of a Single-Core Pipeline into a Multicore Pipeline for a Given Memory Consistency ModelProceedings of the 2024 International Conference on Parallel Architectures and Compilation Techniques10.1145/3656019.3676889(1-13)Online publication date: 14-Oct-2024
https://dl.acm.org/doi/10.1145/3656019.3676889
Margalit RChristakis MPradel M(2024)Robustness against the C/C++11 Memory ModelProceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3650212.3685549(1881-1885)Online publication date: 11-Sep-2024
https://dl.acm.org/doi/10.1145/3650212.3685549
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents