Abstract
Various consistency models for replicated distributed systems (DSs) have been developed and are usually implemented in the middleware layer. Causal consistency (CC) is a widely used consistency model appropriate for distributed applications like discussion groups and forums. One of the known distributed algorithms for CC is based on logical time synchronization with Fidge vector clocks that use the concepts of the hold-back and delivery queues for each replica. The basics of the algorithm and its assumptions are presented in the article. Then, a novel formal hierarchical colored Petri net model of a DS with CC support and three constituting replicas is presented. The proposed model operates based on the presented distributed algorithm for CC support with potential randomness for delays in message delivery. The article tries to answer the question: is a given distributed history (DH) a valid image of a causal-consistent distributed system (CCDS)? The proposed model validates a DH via model checking. The question is answered by the execution of the proposed model and the generation of its state space graph (SSG). Required model checking functions are developed for automatically analyzing SSG for (1) extracting the existence of the answer and (2) extraction of the shortest proof scenarios that can generate the given input DH. The model was used to analyze four case study examples. The article presents three effective techniques for decreasing the state space explosion problem. Results show that the colored Petri net model of a CCDS can automatically validate a DH using model checking.