An operational model for multiprocessors with caches

被引：0
作者：
Joshi S. [1 ]
Prasad S. [1 ]
机构：
[1] Indian Institute of Technology Delhi, India
来源：
IFIP Advances in Information and Communication Technology | 2010年 / 323 AICT卷
关键词：
All Open Access; Bronze; Green;
D O I：
10.1007/978-3-642-15240-5_27
中图分类号：
学科分类号：
摘要：
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. © IFIP International Federation for Information Processing 2010.
引用
收藏
页码：371 / 385
页数：14
相关论文
共 10 条
  • [1] Adve S.V., Gharachorloo K., Shared Memory Consistency Models: A Tutorial, Computer, 29, 12, pp. 66-76, (1996)
  • [2] Adve S.V., Hill M.D., Weak Ordering-A new definition, SIGARCH Comput. Archit. News, 18, 3 A, pp. 2-14, (1990)
  • [3] Arvind N.N., Maessen J.-W., Nikhil R.S., Stoy J.E., A Lambda Calculus with Letrecs and Barriers, Proceedings of the 16th Conference On Foundations of Software Technology and Theoretical Computer Science, pp. 19-36, (1996)
  • [4] Boudol G., Petri G., Relaxed Memory Models: An Operational Approach, POPL '09: Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium On Principles of Programming Languages, pp. 392-403, (2009)
  • [5] Handy J., The Cache Memory Book, (1993)
  • [6] Joshi S., Prasad S., An Operational Model for Multiprocessors With Caches, (2010)
  • [7] Lamport L., How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs, IEEE Transactions on Computers, 100, 28, pp. 690-691, (1979)
  • [8] Owens S., Sarkar S., Sewell P., A Better x86 Memory Model: X86-TSO, TPHOL 2009. LNCS, 5674, pp. 391-407, (2009)
  • [9] 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, pp. 379-391, (2009)
  • [10] Wright A.K., Felleisen M., A Syntactic Approach to Type Soundness, Information and Computation, 115, pp. 38-94, (1992)
1