publication . Preprint . 2016

Operational Aspects of C/C++ Concurrency

Podkopaev, Anton; Sergey, Ilya; Nanevski, Aleksandar;
Open Access English
  • Published: 04 Jun 2016
Abstract
In this work, we present a family of operational semantics that gradually approximates the realistic program behaviors in the C/C++11 memory model. Each semantics in our framework is built by elaborating and combining two simple ingredients: viewfronts and operation buffers. Viewfronts allow us to express the spatial aspect of thread interaction, i.e., which values a thread can read, while operation buffers enable manipulation with the temporal execution aspect, i.e., determining the order in which the results of certain operations can be observed by concurrently running threads. Starting from a simple abstract state machine, through a series of gradual refineme...
Read more
Subjects
free text keywords: Computer Science - Programming Languages
Download from
arXiv.org e-Print Archive
Preprint . 2016
Provider: arXiv.org e-Print Archive
48 references, page 1 of 4

[1] C/C++11 mappings to processors. Available from https://www. cl.cam.ac.uk/~pes20/cpp/cpp0xmappings.html.

[2] ISO/IEC 14882:2011. Programming language C++, 2011.

[3] ISO/IEC 9899:2011. Programming language C, 2011.

[4] J. Alglave, L. Maranget, and M. Tautschnig. Herding cats: Modelling, simulation, testing, and data mining for weak memory. ACM Trans. Program. Lang. Syst., 36(2):7:1-7:74, 2014. [OpenAIRE]

[5] M. Batty, K. Memarian, K. Nienhuis, J. Pichon-Pharabod, and P. Sewell. The problem of programming language concurrency semantics. In ESOP, volume 9032 of LNCS, pages 283-307. Springer, 2015. [OpenAIRE]

[6] M. Batty, K. Memarian, S. Owens, S. Sarkar, and P. Sewell. Clarifying and compiling C/C++ concurrency: from C++11 to POWER. In POPL, pages 509-520. ACM, 2012.

[7] M. Batty, S. Owens, S. Sarkar, P. Sewell, and T. Weber. Mathematizing C++ concurrency. In POPL, pages 55-66. ACM, 2011.

[8] H.-J. Boehm and B. Demsky. Outlawing Ghosts: Avoiding out-ofthin-air results. In MSPC, pages 7:1-7:6. ACM, 2014.

[9] R. Bornat, J. Alglave, and M. J. Parkinson. New lace and arsenic: adventures in weak memory with a program logic. CoRR, abs/1512.01416, 2015. [OpenAIRE]

[10] G. Boudol and G. Petri. Relaxed memory models: an operational approach. In POPL, pages 392-403. ACM, 2009. [OpenAIRE]

[11] G. Boudol, G. Petri, and B. P. Serpette. Relaxed operational semantics of concurrent programming languages. In EXPRESS/SOS, volume 89 of EPTCS, pages 19-33, 2012. [OpenAIRE]

[12] S. Brookes. A semantics for concurrent separation logic. Th. Comp. Sci., 375(1-3), 2007.

[13] K. Crary and M. J. Sullivan. A Calculus for Relaxed Memory. In POPL, pages 623-636. ACM, 2015. [OpenAIRE]

[14] M. Desnoyers, P. E. McKenney, A. S. Stern, M. R. Dagenais, and J. Walpole. User-level implementations of read-copy update. IEEE Transactions on Parallel and Distributed Systems, 23(2):375-382, Feb 2012.

[15] M. Doko and V. Vafeiadis. A program logic for C11 memory fences. In VMCAI, volume 9583 of LNCS, pages 413-430. Springer, 2016. [OpenAIRE]

48 references, page 1 of 4
Related research
Abstract
In this work, we present a family of operational semantics that gradually approximates the realistic program behaviors in the C/C++11 memory model. Each semantics in our framework is built by elaborating and combining two simple ingredients: viewfronts and operation buffers. Viewfronts allow us to express the spatial aspect of thread interaction, i.e., which values a thread can read, while operation buffers enable manipulation with the temporal execution aspect, i.e., determining the order in which the results of certain operations can be observed by concurrently running threads. Starting from a simple abstract state machine, through a series of gradual refineme...
Read more
Subjects
free text keywords: Computer Science - Programming Languages
Download from
arXiv.org e-Print Archive
Preprint . 2016
Provider: arXiv.org e-Print Archive
48 references, page 1 of 4

[1] C/C++11 mappings to processors. Available from https://www. cl.cam.ac.uk/~pes20/cpp/cpp0xmappings.html.

[2] ISO/IEC 14882:2011. Programming language C++, 2011.

[3] ISO/IEC 9899:2011. Programming language C, 2011.

[4] J. Alglave, L. Maranget, and M. Tautschnig. Herding cats: Modelling, simulation, testing, and data mining for weak memory. ACM Trans. Program. Lang. Syst., 36(2):7:1-7:74, 2014. [OpenAIRE]

[5] M. Batty, K. Memarian, K. Nienhuis, J. Pichon-Pharabod, and P. Sewell. The problem of programming language concurrency semantics. In ESOP, volume 9032 of LNCS, pages 283-307. Springer, 2015. [OpenAIRE]

[6] M. Batty, K. Memarian, S. Owens, S. Sarkar, and P. Sewell. Clarifying and compiling C/C++ concurrency: from C++11 to POWER. In POPL, pages 509-520. ACM, 2012.

[7] M. Batty, S. Owens, S. Sarkar, P. Sewell, and T. Weber. Mathematizing C++ concurrency. In POPL, pages 55-66. ACM, 2011.

[8] H.-J. Boehm and B. Demsky. Outlawing Ghosts: Avoiding out-ofthin-air results. In MSPC, pages 7:1-7:6. ACM, 2014.

[9] R. Bornat, J. Alglave, and M. J. Parkinson. New lace and arsenic: adventures in weak memory with a program logic. CoRR, abs/1512.01416, 2015. [OpenAIRE]

[10] G. Boudol and G. Petri. Relaxed memory models: an operational approach. In POPL, pages 392-403. ACM, 2009. [OpenAIRE]

[11] G. Boudol, G. Petri, and B. P. Serpette. Relaxed operational semantics of concurrent programming languages. In EXPRESS/SOS, volume 89 of EPTCS, pages 19-33, 2012. [OpenAIRE]

[12] S. Brookes. A semantics for concurrent separation logic. Th. Comp. Sci., 375(1-3), 2007.

[13] K. Crary and M. J. Sullivan. A Calculus for Relaxed Memory. In POPL, pages 623-636. ACM, 2015. [OpenAIRE]

[14] M. Desnoyers, P. E. McKenney, A. S. Stern, M. R. Dagenais, and J. Walpole. User-level implementations of read-copy update. IEEE Transactions on Parallel and Distributed Systems, 23(2):375-382, Feb 2012.

[15] M. Doko and V. Vafeiadis. A program logic for C11 memory fences. In VMCAI, volume 9583 of LNCS, pages 413-430. Springer, 2016. [OpenAIRE]

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