Formal Specification of Memory Coherence Protocol
Journal Title: International Journal of Advanced Computer Science & Applications - Year 2018, Vol 9, Issue 8
Abstract
Memory coherence is the most fundamental re-quirement in a shared virtual memory system where there are concurrent as well as loosely coupled processes. These processes can demand a page for reading or writing. The memory is called coherent if the last update in a page remains constant for each process until the owner of that page does not change it. The ownership is transferred to a process interested to update that page. In [Kai LI, and Paul Hudak. Memory Coherence in Shared Virtual Memory Systems, 1986. Proc. of Fifth Annual ACM Symposium on Principles of Distributed Computing.], algorithms ensuring memory coherence are given. We formally specify these protocols and report the improvements through formal analysis. The protocols are specified in UPPAAL, i.e., a tool for modeling, validation and verification of real-time systems.
Authors and Affiliations
Jahanzaib Khan, Muhammad Atif, Muhammad Khurram Zahoor Bajwa, Muhammad Sohaib Mahmood, Sobia Usman
Keywords
Related Articles
- EP ID EP376684
- DOI 10.14569/IJACSA.2018.090881
- Views 108
- Downloads 0
Student Facial Authentication Model based on OpenCV’s Object Detection Method and QR Code for Zambian Higher Institutions of Learning
Facial biometrics captures human facial physiological data, converts it into a data item variable so that this stored variable may be used to provide information security services, such as authentication, integrity manag...
A General Model for Similarity Measurement between Objects
The problem to detect the similarity or the differ-ence between objects are faced regularly in several domains of applications such as e-commerce, social network, expert system, data mining, decision support system, etc....
A New Hybrid Network Sniffer Model Based on Pcap Language and Sockets (Pcapsocks)
Nowadays, the protection and the security of data transited within computer networks represent a real challenge for developers of computer applications and network administrators. The Intrusion Detection System and Intru...
A Proposed Multi Images Visible Watermarking Technique
Visible watermarking techniques are proposed to secure digital data against unauthorized attacks. These techniques protect data from illegal access and use. In this work, a multi visible watermarking technique that allow...
Realtime Application of Constrained Predictive Control for Mobile Robot Navigation
This work addresses the implementation issue of constrained Model Predictive Control (MPC) for the autonomous trajectory-tracking problem. The chosen process to control is a Wheeled Mobile Robot (WMR) described by a disc...