Formalization and Verification of the Message Delivery Mechanism of Apache Pulsar

Apache Pulsar is a distributed publish-subscribe messaging system that employs a compute-storage separation architecture, which is well-suited for cloud-native environments. Message delivery mechanism is the core function in Pulsar, mainly for transferring data between different objects. The reliability of the message delivery mechanism of Pulsar raises extensive concerns for better application. In this paper, we use process algebra CSP to model the components of Pulsar. By implementing the model using model checker PAT, we mathematically examine the message delivery mechanism of Pulsar. We verify six properties: deadlock freedom, divergence freedom, data consistency, sequentiality, reliability and persistent storage. The verification results indicate that Pulsar satisfies all these properties, demonstrating that it has good performance and can provide robust message transmission services.