Programmer-centric conditions for itanium memory consistency
作者： Lisa Higham , LillAnne Jackson , Jalal Kawash
DOI: 10.1007/11947950_7
关键词:
摘要: We formulate a programmer-centric description of the memory consistency model provided by Itanium architecture. This allows reasoning about programs at non-operational level in natural way, not obscured implementation details underlying However, our definition is tight. provide two very similar definitions and show that specification lies between two. These are motivated slightly different implementations load-acquire instructions.
springer.com
sci-hub.st 参考文章(11)
Yue Yang, Ganesh Gopalakrishnan, Gary Lindstrom, Konrad Slind, Analyzing the Intel Itanium Memory Ordering Rules Using Logic Programming and SAT Lecture Notes in Computer Science. pp. 81- 95 ,(2003) , 10.1007/978-3-540-39724-3_9
Lisa Higham, LillAnne Jackson, Jalal Kawash, Capturing Register and Control Dependence in Memory Consistency Models with Applications to the Itanium Architecture Lecture Notes in Computer Science. pp. 164- 178 ,(2006) , 10.1007/11864219_12
Ganesh Gopalakrishnan, Yue Yang, Hemanthkumar Sivaraj, QB or Not QB: An Efficient Execution Verification Tool for Memory Orderings Computer Aided Verification. pp. 401- 413 ,(2004) , 10.1007/978-3-540-27813-9_31
Lisa Higham, Lillanne Jackson, Jalal Kawash, Specifying memory consistency of write buffer multiprocessors ACM Transactions on Computer Systems. ,vol. 25, pp. 1- 42 ,(2007) , 10.1145/1189736.1189737
Lisa Higham, LillAnne Jackson, Translating between itanium and sparc memory consistency models Proceedings of the eighteenth annual ACM symposium on Parallelism in algorithms and architectures - SPAA '06. pp. 170- 179 ,(2006) , 10.1145/1148109.1148138
S.V. Adve, K. Gharachorloo, Shared memory consistency models: a tutorial IEEE Computer. ,vol. 29, pp. 66- 76 ,(1996) , 10.1109/2.546611
Rajeev Joshi, Leslie Lamport, John Matthews, Serdar Tasiran, Mark Tuttle, Yuan Yu, Checking Cache-Coherence Protocols with TLA+ Formal Methods in System Design. ,vol. 22, pp. 125- 131 ,(2003) , 10.1023/A:1022969405325
Arvind Arvind, Jan-Willem Maessen, Memory Model = Instruction Reordering + Store Atomicity ACM SIGARCH Computer Architecture News. ,vol. 34, pp. 29- 40 ,(2006) , 10.1145/1150019.1136489
Yue Yang, G. Gopalakrishnan, G. Lindstrom, K. Slind, Nemos: a framework for axiomatic and executable specifications of memory consistency models international parallel and distributed processing symposium. pp. 31- 39 ,(2004) , 10.1109/IPDPS.2004.1302944
A. Adir, H. Attiya, G. Shurek, Information-flow models for shared memory with an application to the PowerPC architecture IEEE Transactions on Parallel and Distributed Systems. ,vol. 14, pp. 502- 515 ,(2003) , 10.1109/TPDS.2003.1199067