Abstract
Developers of concurrent code for multicore architectures must navigate weak memory models (wmms) – either directly at the hardware/assembly level or at a somewhat generalised software level – making the verification of concurrent code an even more difficult task. Semantic models based on a system-wide partial-ordering on events have been developed to define the behaviour of code executing under wmms, but typically require specialised assertion languages and inference techniques to reason about, and often apply to only rudimentary programming constructs. In this paper we present a generic but versatile abstract imperative language “IMP+ptr ” which includes pointers and arrays, from which can be built high-level imperative programming constructs for verifying abstract algorithmic logic, or low-level microassembly for, e.g., investigating hardware security vulnerabilities. The base language carefully controls the syntax of atomic instructions to allow program-level, algebraic reasoning about the additional nondeterminism inherent in programs executing under wmms. We show how arrays of pointers, aliasing, and linked lists may be affected by wmms, establishing a base from where we apply pre-existing verification results and techniques for sequential programs with nested parallelism.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
Although \({\varphi }^\succeq \) is infinite it reduces, for the purposes of calculating reordering, to a pointwise-check wrt. \({\textsc {g}} \), i.e., \( {\varphi _1}^\succeq \int {\varphi _2}^\succeq = \emptyset \iff \lnot (\varphi _1 \succeq \varphi _2 \vee \varphi _2 \succeq \varphi _1) \). For \(x,y \in \textsf{Var}\) it collapses to \(x \ne y\).
References
Adve, S.V., Gharachorloo, K.: Shared memory consistency models: a tutorial. Computer 29(12), 66–76 (1996)
Alglave, J.: A formal hierarchy of weak memory models. Formal Methods in System Design 41(2), 178–210 (2012)
Alglave, J., Cousot, P.: Ogre and Pythia: an invariance proof method for weak consistency models. In: POPL 2017, pp. 3–18. ACM, New York (2017)
Alglave, J., Deacon, W., Grisenthwaite, R., Hacquard, A., Maranget, L.: Armed cats: formal concurrency modelling at Arm. ACM Trans. Program. Lang. Syst. 43(2), 1–54 (2021)
Alglave, J., Maranget, L., Tautschnig, M.: Herding cats: modelling, simulation, testing, and data mining for weak memory. ACM Trans. Program. Lang. Syst. 36(2), 7:1–7:74 (2014)
Amani, S., Andronick, J., Bortin, M., Lewis, C., Rizkallah, C., Tuong, J.: COMPLX: a verification framework for concurrent imperative programs. In: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, pp. 138–150. Association for Computing Machinery, New York (2017)
Bergstra, J.A., Klop, J.W.: Process algebra for synchronous communication. Inf. Control 60(1–3), 109–137 (1984)
Boehm, H.-J., Adve, S.V.: Foundations of the C++ concurrency memory model. In: PLDI 2008, pp. 68–78. ACM (2008)
Brookes, S.: A semantics for concurrent separation logic. Theoret. Comput. Sci. 375(1–3), 227–270 (2007)
Colvin, R., Doherty, S., Groves, L.: Verifying concurrent data structures by simulation. Electron. Notes Theor. Comput. Sci. 137, 93–110 (2005). Proceedings of the REFINE 2005 Workshop (REFINE 2005)
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.: 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.: Separation of concerning things: a simpler basis for defining and programming with the C/C++ memory model. In: Riesco, A., Zhang, M. (eds.) ICFEM 2022. LNCS, vol. 1347, pp. 71–89. Springer, Cham (2022). https://doi.org/10.1007/978-3-031-17244-1_5
Colvin, R.J., Hayes, I.J., Meinicke, L.A.: Designing a semantic model for a wide-spectrum language with concurrency. Formal Aspects Comput. 29(5), 853–875 (2017)
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
Dinsdale-Young, T., Birkedal, L., Gardner, P., Parkinson, M., Yang, H.: Views: compositional reasoning for concurrent programs. SIGPLAN Not. 48(1), 287–300 (2013)
Doherty, S., Dalvandi, S., Dongol, B., Wehrheim, H.: Unifying operational weak memory verification: an axiomatic approach. ACM Trans. Comput. Logic 23(4), 1–39 (2022)
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)
Hayes, I.J., Colvin, R.J., Meinicke, L.A., Winter, K., Velykis, A.: An algebra of synchronous atomic steps. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 352–369. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-48989-6_22
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)
Hoare, C.A.R.: Towards a theory of parallel programming. In: Operating System Techniques, pp. 61–71. Academic Press (1972). Proceedings of Seminar at Queen’s University, Belfast, Northern Ireland, August-September 1971
Hoare, C.A.R.T., Möller, B., Struth, G., Wehrman, I.: Concurrent Kleene algebra. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol. 5710, pp. 399–414. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-04081-8_27
Ishtiaq, S.S., O’Hearn, P.W.: BI as an assertion language for mutable data structures. In: Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pp. 14–26. ACM Press (2001)
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)
Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst. 5, 596–619 (1983)
Kang, J., Hur, C.-K., Lahav, O., Vafeiadis, V., Dreyer, D.: A promising semantics for relaxed-memory concurrency. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, pp. 175–189. ACM, New York (2017)
Klein, G., et al.: SeL4: formal verification of an OS kernel. In: Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles, SOSP 2009, pp. 207–220. Association for Computing Machinery, New York (2009)
Kocher, P., et al.: Spectre attacks: exploiting speculative execution. In: Security and Privacy, pp. 1–19. IEEE (2019)
Kocher, P.C.: Timing attacks on implementations of Diffie-Hellman, RSA, DSS, and other systems. In: Koblitz, N. (ed.) CRYPTO 1996. LNCS, vol. 1109, pp. 104–113. Springer, Heidelberg (1996). https://doi.org/10.1007/3-540-68697-5_9
Kozen, D.: Kleene algebra with tests. ACM Trans. Program. Lang. Syst. 19(3), 427–443 (1997)
Kozen, D.: On Hoare logic and Kleene algebra with tests. ACM Trans. Comput. Logic 1(1), 60–76 (2000)
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
Lipp, M., et al.: Meltdown: reading kernel memory from user space. In: USENIX Security Symposium (2018)
Madiot, J.-M., Pottier, F.: A separation logic for heap space under garbage collection. Proc. ACM Program. Lang. 6(POPL), 1–28 (2022)
Moiseenko, E., Podkopaev, A., Koznov, D.: A survey of programming language memory models. Program. Comput. Softw. 47(6), 439–456 (2021)
Nanevski, A., Ley-Wild, R., Sergey, I., Delbianco, G.A.: Communicating state transition systems for fine-grained concurrent resources. In: Shao, Z. (ed.) ESOP 2014. LNCS, vol. 8410, pp. 290–310. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54833-8_16
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL—A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)
Paulson, L.C.: Isabelle: A Generic Theorem Prover. Springer, Heidelberg (1994). https://doi.org/10.1007/BFb0030541
Pulte, C., Pichon-Pharabod, J., Kang, J., Lee, S.-H., Hur, C.-K.: Promising-ARM/RISC-V: a simpler and faster operational concurrency model. In: PLDI 2019, pp. 1–15. ACM (2019)
Ravichandran, J., Na, W.T., Lang, J., Yan, M.: PACMAN: attacking ARM pointer authentication with speculative execution. In: Proceedings of the 49th Annual International Symposium on Computer Architecture, ISCA 2022, pp.685–698. Association for Computing Machinery, New York (2022)
Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: IEEE Symposium on Logic in Computer Science (LICS), pp. 55–74. IEEE Computer Society (2002)
Treiber, R.K.: Systems Programming: coping with Parallelism. RJ5118. Technical report, IBM Almaden Research Center (1986)
Sarkar, S., Sewell, P., Alglave, J., Maranget, L., Williams, D.: Understanding POWER multiprocessors. In: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, pp. 175–186. Association for Computing Machinery, New York (2011)
Sewell, P., Sarkar, S., Owens, S., Nardelli, F.Z., Myreen, M.O.: x86-TSO: a rigorous and usable programmer’s model for x86 multiprocessors. Commun. ACM 53(7), 89–97 (2010)
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
Svendsen, K., Pichon-Pharabod, J., Doko, M., Lahav, O., Vafeiadis, V.: A separation logic for a promising semantics. In: Ahmed, A. (ed.) ESOP 2018. LNCS, vol. 10801, pp. 357–384. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-89884-1_13
Thornton, J.E.: Parallel operation in the Control Data 6600. In: Proceedings of the October 27–29, 1964, Fall Joint Computer Conference, Part II: Very High Speed Computer Systems, AFIPS 1964, pp. 33–40. ACM (1964)
Tomasulo, R.M.: An efficient algorithm for exploiting multiple arithmetic units. IBM J. Res. Dev. 11(1), 25–33 (1967)
Trippel, C., Lustig, D., Martonosi, M.: MeltdownPrime and SpectrePrime: automatically-synthesized attacks exploiting invalidation-based coherence protocols. CoRR, abs/1802.03802 (2018)
Turon, A., Vafeiadis, V., Dreyer, D.: GPS: navigating weak memory with ghosts, protocols, and separation. SIGPLAN Not. 49(10), 691–707 (2014)
Wehrheim, H., Bargmann, L., Dongol, B.: Reasoning about promises in weak memory models with event structures (extended version). CoRR (2022). https://arxiv.org/abs/2211.16330
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
Acknowledgements
We thank Duong Dinh for help with modelling Meltdown, and Scott Heiner, Roger Su, Kait Lam, Nicholas Coughlin, Kirsten Winter, Graeme Smith and the anonymous reviewers for feedback.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2023 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Colvin, R.J. (2023). A Fine-Grained Semantics for Arrays and Pointers Under Weak Memory Models. In: Chechik, M., Katoen, JP., Leucker, M. (eds) Formal Methods. FM 2023. Lecture Notes in Computer Science, vol 14000. Springer, Cham. https://doi.org/10.1007/978-3-031-27481-7_18
Download citation
DOI: https://doi.org/10.1007/978-3-031-27481-7_18
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-27480-0
Online ISBN: 978-3-031-27481-7
eBook Packages: Computer ScienceComputer Science (R0)