Indian Journal of Science and Technology

Abstract

Causal consistency is one of the consistency models that categorizes events in a distributed system to those causally related, and those are not. In this paper, a new modeling of the causal consistency checking in a distributed shared memory is presented using the hierarchical colored Petri net, and its rules and properties are modeled with all details. Our proposed model takes a scenario of the performed processes in the distributed shared memory system as an input and determines whether this scenario is allowed with a causally consistent shared memory system or not. Modeling of the causal consistency using the hierarchical colored Petri net enables to study the state space of a distributed shared memories system and automatically identify, which write operations are causally related and which of them are not. Furthermore, state space analysis of the proposed model shows that in the last node of the state space graph, all processes of the distributed shared memory system are finished or not. Therefore, it is represented that the model of the distributed shared memory system is reached to definitive state or not, and checks the safety of the shared memory system's current state. Because of these features, the proposed model is used in industrial activities, particularly the computer-based distributed systems. In fact, pre-production modeling and simulation of the industrial systems using the hierarchical colored Petri net will be economically and very affordable.
Keywords: Causal Consistency, Hierarchical Colored Petri Net, Modeling, Shared Memory Systems, Verification