Operational Aspects of C/C++ Concurrency

Preprint English OPEN
Podkopaev, Anton; Sergey, Ilya; Nanevski, Aleksandar;
(2016)
  • Subject: Computer Science - Programming Languages
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 buf... View more
  • References (48)
    48 references, page 1 of 5

    [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.

    [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.

    [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.

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

  • Similar Research Results (3)
  • Metrics
Share - Bookmark