Abstract
The C/C++ memory model provides a range of mechanisms that programmers of concurrent code can use to control accesses to shared variables. The C standard describes the memory model in terms of cross-thread relationships between events, making thread-local, compositional reasoning difficult. In this paper we define the C memory model as a relationship between instructions, straightforwardly based on fundamental properties of data dependencies or artificially injected ordering constraints. Reasoning comprises program transformation with respect to potential instruction reorderings. In the best case one can then reuse an existing result from standard imperative techniques, or failing that employ standard techniques to the transformed program. Other formalisations typically involve complex semantic models, requiring the development of specialised inference systems and assertion languages. A key aspect of our work is that the memory model definition is kept separate to other considerations of a rich programming language such as C. The formal framework is especially suitable for concise code targeting x86, Arm, and RISC-V architectures.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Batty, M., Dodds, M., Gotsman, A.: Library abstraction for C/C++ concurrency. In: POPL 2013, pp. 235–248. ACM (2013)
Batty, M., Owens, S., Sarkar, S., Sewell, P., Weber, T.: Mathematizing C++ concurrency. In: POPL 2011, pp. 55–66. ACM (2011)
Boehm, H.-J., Adve, S.V.: Foundations of the C++ concurrency memory model. In: PLDI 2008, pp. 68–78. ACM (2008)
Chakraborty, S., Vafeiadis, V.: Grounding thin-air reads with event structures. Proc. ACM Program. Lang. 3(POPL), 1–28 (2019)
Colvin, R.J.: Parallelized sequential composition and hardware weak memory models. In: Calinescu, R., Păsăreanu, C.S. (eds.) SEFM 2021. LNCS, vol. 13085, pp. 201–221. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-92124-8_12
Colvin, R.J.: Parallelized sequential composition, pipelines, and hardware weak memory models. CoRR, abs/2105.02444 (2021)
Colvin, R.J.: Separation of concerning things: a simpler basis for defining and programming with the C/C++ memory model (extended version) (2022). https://arxiv.org/abs/2204.03189
Colvin, R.J., Smith, G.: A wide-spectrum language for verification of programs on weak memory models. In: Havelund, K., Peleska, J., Roscoe, B., de Vink, E. (eds.) FM 2018. LNCS, vol. 10951, pp. 240–257. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-95582-7_14
Colvin, R.J., Winter, K.: An abstract semantics of speculative execution for reasoning about security vulnerabilities. In: Sekerinski, E., et al. (eds.) FM 2019. LNCS, vol. 12233, pp. 323–341. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-54997-8_21
Coughlin, N., Winter, K., Smith, G.: Rely/guarantee reasoning for multicopy atomic weak memory models. In: Huisman, M., Păsăreanu, C., Zhan, N. (eds.) FM 2021. LNCS, vol. 13047, pp. 292–310. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-90870-6_16
Gharachorloo, K., Lenoski, D., Laudon, J., Gibbons, P., Gupta, A., Hennessy, J.: Memory consistency and event ordering in scalable shared-memory multiprocessors. In: ISCA 1990, pp. 15–26. ACM (1990)
Herlihy, M.P., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. TOPLAS 12(3), 463–492 (1990)
Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969)
Jeffrey, A., Riely, J., Batty, M., Cooksey, S., Kaysin, I., Podkopaev, A.: The leaky semicolon: compositional semantic dependencies for relaxed-memory concurrency. Proc. ACM Program. Lang. 6(POPL), 1–30 (2022)
Jones, C.B.: Specification and design of (parallel) programs. In: IFIP Congress, pp. 321–332 (1983)
Kang, J., Hur, C.-K., Lahav, O., Vafeiadis, V., Dreyer, D.: A promising semantics for relaxed-memory concurrency. In: POPL 2017, pp. 175–189. ACM (2017)
Lahav, O., Giannarakis, N., Vafeiadis, V.: Taming release-acquire consistency. In: POPL 2016, pp. 649–662. Association for Computing Machinery (2016)
Lahav, O., Vafeiadis, V.: Owicki-Gries reasoning for weak memory models. In: Halldórsson, M.M., Iwama, K., Kobayashi, N., Speckmann, B. (eds.) ICALP 2015. LNCS, vol. 9135, pp. 311–323. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-47666-6_25
Lahav, O., Vafeiadis, V., Kang, J., Hur, C.-K., Dreyer, D.: Repairing sequential consistency in C/C++11. In: Programming Language Design and Implementation (PLDI 2017), pp. 618–632. ACM (2017)
Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Comput. C–28(9), 690–691 (1979)
Lau, S., Gomes, V.B.F., Memarian, K., Pichon-Pharabod, J., Sewell, P.: Cerberus-BMC: a principled reference semantics and exploration tool for concurrent and sequential C. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 387–397. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-25540-4_22
Lee, S.-H., et al.: Promising 2.0: global optimizations in relaxed memory concurrency. In: PLDI 2020, pp. 362–376. ACM (2020)
Memarian, K., et al.: Into the depths of C: elaborating the de facto standards. SIGPLAN Not. 51(6), 1–15 (2016)
Morgan, C.: Of wp and CSP. In: Feijen, W.H.J., van Gasteren, A.J.M., Gries, D., Misra, J. (eds.) Beauty Is Our Business: A Birthday Salute to Edsger W. Dijkstra. Texts and Monographs in Computer Science, pp. 319–326. Springer, New York (1990). https://doi.org/10.1007/978-1-4612-4476-9_37
Nienhuis, K., Memarian, K., Sewell, P.: An operational semantics for C/C++11 concurrency. In: OOPSLA 2016, pp. 111–128. ACM (2016)
Ou, P., Demsky, B.: Towards understanding the costs of avoiding out-of-thin-air results. Proc. ACM Program. Lang. 2(OOPSLA), 1–29 (2018)
Owicki, S., Gries, D.: An axiomatic proof technique for parallel programs I. Acta Inf. 6(4), 319–340 (1976)
Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE J. Sel. Areas Commun. 21(1), 5–19 (2003)
Sarkar, S., Sewell, P., Alglave, J., Maranget, L., Williams, D.: Understanding POWER multiprocessors. In: Programming Language Design and Implementation (PLDI 2011), pp. 175–186. ACM (2011)
Smith, G., Coughlin, N., Murray, T.: Value-dependent information-flow security on weak memory models. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) FM 2019. LNCS, vol. 11800, pp. 539–555. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-30942-8_32
Vafeiadis, V., Balabonski, T., Chakraborty, S., Morisset, R., Nardelli, F.: Common compiler optimisations are invalid in the C11 memory model and what we can do about it. In: POPL 2015, pp. 209–220. ACM (2015)
Wehrheim, H., Travkin, O.: TSO to SC via symbolic execution. In: Piterman, N. (ed.) HVC 2015. LNCS, vol. 9434, pp. 104–119. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-26287-1_7
Winter, K., Coughlin, N., Smith, G.: Backwards-directed information flow analysis for concurrent programs. In: 2021 IEEE 34th Computer Security Foundations Symposium (CSF), pp. 1–16 (2021)
Wright, D., Batty, M., Dongol, B.: Owicki-Gries reasoning for C11 programs with relaxed dependencies. In: Huisman, M., Păsăreanu, C., Zhan, N. (eds.) FM 2021. LNCS, vol. 13047, pp. 237–254. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-90870-6_13
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
A Syntax and Semantics Definitions
A Syntax and Semantics Definitions
Functions over the Syntax. Write and read variables can be extracted from instructions (11) as follows.
We set . The fences of an instruction \(\alpha \), \(|\!\alpha \!|\), underpinning relation \({{ \textsc {fnc}}} \), are given by , , and . Memory order constraints from instructions and expressions, underpinning relation \({{ \textsc {ocs}}} \), are extracted as follows.
Any of the functions (\(\textsf{fn}(.)\)) defined above can be straightforwardly lifted to commands in the following generic pattern.
Operational Semantics. The main rules of the operational semantics for the language in (6) are below [5]. An action \(\alpha \) executes as a single step and terminates, i.e., . The composite commands execute as follows, where \(\tau \) is a silent (unobservable) step and \(c^{n}_{{{ \textsc {m}}}}\) is n-fold iteration of \(c\) wrt. \({{ \textsc {m}}} \).
These rules are standard, except for the rule for that allows an action \(\beta \) of \(c_2\) to proceed before \(c_1\) provided \(\beta \) can be reordered with \(c_1\) according to \({{ \textsc {m}}} \).
Rights and permissions
Copyright information
© 2022 Springer Nature Switzerland AG
About this paper
Cite this paper
Colvin, R.J. (2022). Separation of Concerning Things: A Simpler Basis for Defining and Programming with the C/C++ Memory Model. In: Riesco, A., Zhang, M. (eds) Formal Methods and Software Engineering. ICFEM 2022. Lecture Notes in Computer Science, vol 13478. Springer, Cham. https://doi.org/10.1007/978-3-031-17244-1_5
Download citation
DOI: https://doi.org/10.1007/978-3-031-17244-1_5
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-17243-4
Online ISBN: 978-3-031-17244-1
eBook Packages: Computer ScienceComputer Science (R0)