DocumentCode :
3264087
Title :
Formally Verifying the Distributed Shared Memory Weak Consistency Models
Author :
Chennareddy, Venkateswarlu ; Deka, Jatindra Kumar
Author_Institution :
D.E. Shaw India Software Private Ltd., Hyderabad
fYear :
2006
fDate :
20-23 Dec. 2006
Firstpage :
455
Lastpage :
460
Abstract :
A specification and verification methodology for distributed shared memory (DSM) consistency models specifically weak consistency model is proposed. For this, we designed and implemented abstract DSM System. In DSM system, sequential consistency unnecessarily reduces the performance of the system because it does not allow to reorder or pipeline the memory operations. Relaxed memory consistency allows reordering of memory events and buffering or pipelining of memory accesses. So that relaxed consistency improves the performance of the DSM system. For any critical system, it is very important to develop methods that increase our confidence in the correctness of such systems. One of such methods for checking the correctness of critical system is formal verification. For verification of weak consistency models we specify the weak consistency properties and are verified on abstract DSM system using CADP tool box.
Keywords :
distributed shared memory systems; formal specification; formal verification; CADP tool box; distributed shared memory; formal verification; weak consistency model; Application software; Hardware; Performance evaluation; Pipeline processing; Power system modeling; Scalability; Software systems; State-space methods; System testing; Topology;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Advanced Computing and Communications, 2006. ADCOM 2006. International Conference on
Conference_Location :
Surathkal
Print_ISBN :
1-4244-0716-8
Electronic_ISBN :
1-4244-0716-8
Type :
conf
DOI :
10.1109/ADCOM.2006.4289935
Filename :
4289935
Link To Document :
بازگشت