Formal Specification of Memory Coherence Protocol

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.

@article{Khan2018,
  title     = {Formal Specification of Memory Coherence Protocol},
  journal   = {International Journal of Advanced Computer Science and Applications},
  volume    = {9},
  number    = {8},
  year      = {2018},
  publisher = {The Science and Information Organization},
  author    = {Jahanzaib Khan and Muhammad Atif and Muhammad Khurram Zahoor Bajwa and Muhammad Sohaib Mahmood and Sobia Usman},
  doi       = {10.14569/IJACSA.2018.090881},
  url       = {https://doi.org/10.14569/IJACSA.2018.090881}
}