Formal Analysis of Distributed Shared Memory Algorithms
Abstract
Abstract Views: 57
The memory coherence problem occurs while mapping shared virtual memory in a loosely coupled multiprocesses setup. Memory is considered coherent if a read operation provides the same data written in the last write operation. The problem has been addressed in the literature using different algorithms, although the correctness of a distributed algorithm remains questionable. Formal verification is the principal term for a group of techniques that routinely use an analysis established on mathematical transformations to conclude the rightness of the hardware or software behavior in divergence to dynamic verification techniques. The current study employed UPPAAL model checker to model the Dynamic Distributed algorithm for shared virtual memory given by K. Li and P. Hudak. The results showed that the Dynamic Distributed algorithm for shared virtual memory partially fulfils its functional requirements.
Downloads
References
P. Hudak and K. Li, “Memory coherence in shared virtual memory systems,” ACM Trans. Comput. Sys., vol. 7, no. 4, pp. 321–359, Nov. 1989, doi: https://doi.org/10.1145/75104.75105
C. Baier and J.P. Katoen, Principles of model checking, MIT Press Cambridge, 2008.
E. M. Clarke and J. M. Wing, “Formal methods: State of the art and future directions,” ACM Comput. Sur., vol. 28, no. 4, pp. 626–643, Dec. 1996, doi: https://doi.org/10.1145/242223.242257
N. Ibrahim and I. Khalil, “Verifying web services compositions using Uppaal,” in Proc.1st IEEE Int. Conf. Comput. Sys. Indust. Inform., Sharjah, UAE, Dec. 18–20, 2012, doi: https://doi.org/10.1109/ICCSII.2012.6454365
J. Bengtsson, W. O. D. Griffioen, K. J. Kristoffersen, K. G. Larsen, F. Larsson, P. Pettersson, and W. Yi, “Verification of an audio protocol with bus collisionusing uppaal,” in Proc. Comput. Aid. Verific. 8th Int. Conf., CAV'96 New Brunswick, USA, July 31–August 3, 1996, pp. 244–256. [6] A. Blanchard, N. Kosmatov, M. Lernerre and F. Loulergue, “A Case Study on Formal Verification of the Anaxagoros Hypervisor Paging System with Frama-C,” in Proc. FMICS Formal Meth. Indus. Critic. Sys. 20th Int. Work., Oslo, Norway, June 22–23, 2015, pp.15–30.
V. Chennareddy and J. K. Deka, “Formally Verifying the Distributed Shared Memory Weak Consistency Models,” in Proc. Int. Conf. Adv. Comput. Commun., Mangalore, India, Dec. 20–23, 2006, pp. 455–460, doi: https://doi.org/10.1109/ADCOM.2006.4289935
A. F. G. David, K. G. Larsen, A. Legay, M. Mikucionis, and D. B. Poulsen, “Uppaal smc tutorial,” Int. J. Softw. Tools. Technol. Transfer., vol.17, pp. 397–415, 2014, doi: https://doi.org/10.1007/s10009-014-0361-y
D. Fabian and R. Marik, “Configuration dynamics verification using Uppaal,” in
Proc. 15th Int. Config. Works., Vienna, Austria, August 29–30, 2013, pp. 35–42.
Y. Fei, H. Zhu, and X. Li, “Modeling and verification of nlsr protocol using uppaal.” in Proc. Int. Symp. Theor. Aspec. Soft. Eng., Guangzhou, China, Aug. 29–31, 2018, pp. 108–115, doi: https://doi.org/10.1109/TASE.2018.00022
F. S. Gonçalves, D. Pereira, E. Tovar, and L. B. Becker, “Formal Verification of AADL Models Using UPPAAL,” in Proc. VII Braz. Symp. Comput. Sys. Eng., Curitiba, PR, Brazil, Nov. 6–10, 2017, pp. 117–124, doi: https://doi.org/10.1109/SBESC.2017.22
C. Gerking, S. Dziwok, C. Heinzemann, and W. Schäfer, “Domain-specific model checking for cyber-physical systems,” in Proc. 12th Work. Model-Driven Eng., Verific. Valid., Ottawa, Canada, 2015, pp. 18–27.
P. Bulychev, et al., “Uppaal-smc: Statistical model checking for priced timed automata,” in Proc. Workshop Quanti. Aspec. Program. Lang. Sys., 2012, pp. 1–16, doi:https://doi.org/10.48550/arXiv.1207.1272 [14] K. G. Larsen, P. Pettersson, and W. Yi, “Uppaal in a nutshell.” Int. J. Softw,” Tools Technol. Trans., vol. 1, no. 1, pp. 134–152, 1997.
S. Wimmer and P. Lammich, “Verified model checking of timed automata,” in Proc. Tools Algor. Construc. Anal. Syst., 2018, pp. 61–78, doi: https://doi.org/10.1007/978-3-319-89960-2_4
Copyright (c) 2022 Muhammad Atif, Mudassar Naseer, Ahmad Salman Khan
This work is licensed under a Creative Commons Attribution 4.0 International License.
UMT-AIR follow an open-access publishing policy and full text of all published articles is available free, immediately upon publication of an issue. The journal’s contents are published and distributed under the terms of the Creative Commons Attribution 4.0 International (CC-BY 4.0) license. Thus, the work submitted to the journal implies that it is original, unpublished work of the authors (neither published previously nor accepted/under consideration for publication elsewhere). On acceptance of a manuscript for publication, a corresponding author on the behalf of all co-authors of the manuscript will sign and submit a completed the Copyright and Author Consent Form.
