Abstract
Modern multiprocessors are equipped with local caches, to enhance program performance. However, the presence of caches can lead to the violation of sequential consistency [7] assumptions regarding program order and write atomicity. With respect to such relaxed memory models [1], we provide an operational description of program execution (in the style of [4]) that accounts for cache effects. In particular, we provide an operational characterization of cache invalidation and update policies and an abstract characterization of cache consistency. The programming model consists of a simple imperative language extended with common synchronization primitives such as locks or barrier instructions. The main results show that by precluding certain data races or by placing certain synchronization constraints, sequentially consistent behavior can be obtained for multiprocessor execution even in the presence of local caches.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Adve, S.V., Gharachorloo, K.: Shared Memory Consistency Models: A Tutorial. Computer 29(12), 66–76 (1996)
Adve, S.V., Hill, M.D.: Weak Ordering—A new definition. SIGARCH Comput. Archit. News 18(3a), 2–14 (1990)
Arvind, N.N., Maessen, J.-W., Nikhil, R.S., Stoy, J.E.: A Lambda Calculus with Letrecs and Barriers. In: Proceedings of the 16th Conference on Foundations of Software Technology and Theoretical Computer Science, London, UK, pp. 19–36. Springer, Heidelberg (1996)
Boudol, G., Petri, G.: Relaxed Memory Models: An Operational Approach. In: POPL ’09: Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages, pp. 392–403. ACM, New York (2009)
Handy, J.: The Cache Memory Book. Academic Press Professional, Inc., San Diego (1993)
Joshi, S., Prasad, S.: An Operational Model for Multiprocessors with Caches. Technical report, Indian Institute of Technology Delhi (2010), http://cse.iitd.ac.in/~sanjiva/OpCache.pdf
Lamport, L.: How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs. IEEE Transactions on Computers 100(28), 690–691 (1979)
Owens, S., Sarkar, S., Sewell, P.: A Better x86 Memory Model: x86-TSO. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOL 2009. LNCS, vol. 5674, pp. 391–407. Springer, Heidelberg (2009)
Sarkar, S., Sewell, P., Nardelli, F.Z., Owens, S., Ridge, T., Braibant, T., Myreen, M.O., Alglave, J.: The semantics of x86-CC multiprocessor machine code. ACM SIGPLAN Notices 44(1), 379–391 (2009)
Wright, A.K., Felleisen, M.: A Syntactic Approach to Type Soundness. Information and Computation 115, 38–94 (1992)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 IFIP
About this paper
Cite this paper
Joshi, S., Prasad, S. (2010). An Operational Model for Multiprocessors with Caches. In: Calude, C.S., Sassone, V. (eds) Theoretical Computer Science. TCS 2010. IFIP Advances in Information and Communication Technology, vol 323. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15240-5_27
Download citation
DOI: https://doi.org/10.1007/978-3-642-15240-5_27
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-15239-9
Online ISBN: 978-3-642-15240-5
eBook Packages: Computer ScienceComputer Science (R0)