NSQ (New Simple Queue) is a real-time distributed messaging platform implemented by Go language. It's designed to operate at scale stably and eficiently handle billions of messages per day. Its decentralized topology guarantees fault tolerance, high availability, and reliable message delivery. Operationally, NSQ is elastic to configure and deploy. With the broad application of the NSQ message system, its security and stability have attracted extensive concentration. Therefore, it is crucial to conduct a rigorous analysis and verification of NSQ's properties. In this paper, we employ process algebra CSP (Communicating Sequential Processes) to model the core functional modules of the NSQ. In addition, we utilize the model checker PAT (Process Analysis Toolkit) to verify five properties of the model, including divergence freedom, reachability, scalability, availability, and flow controllability. The verification results demonstrate that the NSQ system satisfies all the above properties, proving that the system has high flexibility and robustness while providing credible and eficient message delivery.
1. Introduction to ensure high availability and reachability of messages, which increases system complexity. Therefore, excellent In the rapidly evolving era of the Internet, the explosion message middleware should have high message processof users and services creates severe challenges for net- ing eficiency, robustness, stability, and scalability. work applications. Conventional monolithic and vertical NSQ [6] has emerged from these excellent middlewares service architectures can no longer deal with such a vol- in recent years. It is a distributed messaging platform ume of data. Distributed services are gradually becoming based on Go language [9] with outstanding performance, the mainstream architecture. As a foundational segment robustness, and usability. This messaging platform is a in distributed message systems, middleware [1] is impor- user-friendly middleware for real-time messaging sertant in decoupling, asynchronous communication, trafic vices, capable of managing hundreds of millions of mesclipping, and other issues. It can improve the perfor- sages. In addition, NSQ is fitted to the current concurrent mance and stability of applications. Therefore, message Internet ecosystem due to Go’s native strengths in concurqueue as a critical middleware acquires more attention rency. Go is a programming language with concurrency in the Internet field. features, and its concurrency model was developed based
With the evolution of technology, message queues on the process communication concept of CSP (Comare gradually maturing, resulting in a series of outstand- municating Sequential Processes) [10, 11]. This feature ing middleware, including ActiveMQ [2], RabbitMQ [3], makes the Go-based NSQ distributed system well-suited Kafka [4], and RocketMQ [5]. These services decouple to the producer-consumer concurrency problem. Therecomplex systems and enable asynchronous operations fore, it is becoming popular within businesses and has to reduce response times, providing a better user experi- also attracted the attention of researchers. ence. Although the introduction of middleware can sig- NSQ is suitable for distributed applications and sysnificantly improve the performance of a system, we must tems that require asynchronous messaging, such as Social consider its potential problems and challenges, such as Media, Gaming, and other industries that require high reduced availability due to unstable message queues and concurrency. Until now, existing studies primarily fodata inconsistencies due to concurrent communication. cus on comparing diferent message queues performance, The system needs to introduce additional mechanisms operability, and other characteristics [8] or delve into practical applications of NSQ [7]. To the best of our knowledge, there has yet to be research about the verification of its properties, which are significant for users.
And the fundamental attributes of the system still need to be proven.
Employing a formal verification approach to verify NSQ’s fundamental properties ofers rigorous proof and • Topic: It is a distinct stream of messages. An NSQ instance can have multiple Topics, each of which can have one or more Channels. • Channel: It is a logical grouping of consumers subscribed to a given Topic. Each Channel receives a copy of all the messages for that Topic.
The Topic and Channel in the NSQ system are implemented by Go’s channel data type. Go-chan builds on the idea of channel in CSP, it allows data transfers and synchronization operations between concurrent processes.
A channel with cache space are also the natural way to express queue structure. Therefore, essentially NSQ’s Topic/Channel is a bufered queue for message.
After learning the basic terms, we can introduce the NSQ system further from two core workflows: Message multi-cast and Message consumption. assurance, ensuring the system’s correctness, reliability, and stability. This approach enhances confidence and credibility in the design, implementation, and deploy- 2.1.1. Message Multi-cast ment of the system, which is paramount for developers and users. Consequently, this paper bridges this research NSQ designs nsqd to handle multiple data streams congap by adopting formal methods to analyze the NSQ sys- currently. Each Topic can have one or more Channels. tem. We utilize process algebra CSP to formally model Topics multicast the received messages to Channels, and the core functional modules and basic workflow of the each Channel receives copies of messages. In practice, NSQ such as message publishing, subscription, registra- Channels map to downstream services that subscribe the tion, and querying. Subsequently, leveraging the model Topics. Topics and Channels are not preconfigured but checker PAT [12], we verify five properties of the model, are created upon the first publication or subscription. including Divergence Freedom, Reachability, Scalability, Within nsqd, Topics and Channels independently bufer Availability, and Flow Controllability. Experimental re- data to prevent lagging consumers from afecting other sults demonstrate that the NSQ distributed message plat- Channels. Messages are delivered to a randomly client form can guarantee all these properties, proving that the when all clients are ready, achieving load balancing. system has outstanding flexibility and robustness. 2.1.2. Message Consumption
The remainder of this paper is organized as follows. Unlike many conventional message queues, NSQ maxiSection II briefly describes the NSQ system and process mizes performance and throughout by pushing data to algebra CSP. In Section III, we use CSP to model four the client instead of waiting for it to pull. This concept fundamental components in the NSQ message system. is called the RDY (Ready) state, constituting a form of Furthermore, in Section IV, we employ the model check- client-side flow control. This RDY state is a pivotal perforing tool PAT to implement the constructed models and mance parameter, allowing clients to modulate message verify five properties we defined. Finally, we summarize by adjusting the RDY value. Once clients establish conthis paper and discuss future work in Section V. nections and subscriptions, they assert control over the 2. Background lfow of messages from nsqd by dynamically updating the RDY value.
In this section we give a brief description of the NSQ’s architecture and process algebraic language CSP.
A typical architecture of the NSQ system is displayed in Fig. 1. Before furthering into the transmission mechanism of the NSQ, we should familiar with the following terms: • nsqd: The NSQ daemon responsible for receiving and delivering messages. nsqd instances manage the actual message storage and distribution. • nsqlookupd: The NSQ lookup daemon that manages topology information. It receives registration information and provides service discovery. 2.2. CSP Process Algebra CSP [10, 11] is a formal mathematical method that is widely applied in the design and verification of concurrent systems. This language has been successfully applied in modeling and verifying various concurrent systems and protocols [13, 14]. Parts of the CSP syntax used in this paper is defined as follows: , ::= | ? → | ! → | □ | || | ||| | [||] | ◁▷ | ; • SKIP: The process terminates properly. • ? → : The process receives a value from channel c and assigns it to variable u, then starts P. • ! → : The process sends value v to channel c and then starts executing process P. • □ : It depicts a general choice between process P and process Q. • |||: It illustrates interleaving. Processes P and Q run simultaneously and do not share any operations or variables. • ◁▷: It portrays the execution of process P if the boolean expression b is true; otherwise, process Q will be executed. 3. Modeling In this section, we construct the model of NSQ distributed architecture as illustrated in Fig. 1.
For a more detailed understanding of how the components within the NSQ system communicate and interact, we have laid out explanations for the fundamental building blocks used in the model: Sets, Messages, and Communication Channels.
Table 1 shows the definitions we defined for the relevant sets employed in the modeling process. The Module set contains all modules of the NSQ messaging system. The ID set consists of unique identifiers for each object within the system. Commands describe the instructions managing interactions within the NSQ, such as message publication (PUB) and subscription (SUB). The Data set indicates the topological information queried by components, and the Ack set is internal feedback.
Based on the above collections, we give the definition of the Message transferred between components: = {.... | = {.... | ∈ , ∈ , ∈ , ∈ } ∈ , ∈ , ∈ , ∈ {, , }} = {. | ∈ } denotes the set of request messages, means the set of responses, and represents the set of transmitted data.
Next, we define the Channels responsible for communication between the modules and refer to these Channels with the label _ . • ComCL: channels between consumer and nsqlookupd. • ComPD: channels between producer and nsqd. • ComDL: channels between nsqd and nsqlookupd. • ComCD: channels between consumer and nsqd. We also define the channels used internally by components with the label _ . These channels have cache space and are responsible for caching messages. Fig. 2 shows all the channels we have defined. • MsgTPC: message cache channels of Topics. • MsgCHA: message cache channels of Channels. • MsgCON: message cache channels of consumers.
The NSQ system embodies an intricate workflow. Due to the page limit, we only present part of the core modeling codes in this section.
The whole () as below: () = |||∈ ,∈,∈,∈ ⎛ [| _ |] ⎞ ⎝ [| _ |] ⎠ [| _ |] It describes the concurrent model where producers, ℎ() is responsible for pushing messages nsqds, nsqlookupds, and consumers run in parallel and to clients by load balancing strategy. In the NSQ mescollaborate over the [| _ |] channels. The denotes the producer ID, and means the set of . Other characters such as , are similar.
The producer is responsible for generating and sending messages to corresponding Topics. It communicates with the nsqd directly and publishes messages to the nsqd module through the channel. () = ⎛ !... .. → ⎜ ?..... → ⎜ { [] == 1; } ; ⎜ ◁ == 1▷ { + +; } → () ︂) saging system, this strategy is achieved by employing a random distribution strategy, wherein messages are randomly dispatched to clients subscribed to the same Channel. [] signifies the number of messages can process from a specific . We use the ℎ[] array to mark whether is in the state of pushing messages to . nsqd only sends messages to clients who can process messages. We model this process using the General Choice in CSP. () =
(, ) ⎞ ⎛ ?... .. → ⎟⎟⎟ ⎜⎜
︂( ⎟⎠ ⎜⎜⎜ !.. →
◁ [] == 0 ▷ ⎝ !..... → ︂) ; ⎞ ⎟ ⎟ ⎟ ⎟ ⎟ ⎠ ⎟
⎛ ?... ..ℎ. → ⎟ ⎟ ; ⎝ { ,,ℎ[] = −1} → ⎞ ⎠ ⎜⎝ !..ℎ. → ⎛ ?.....ℎ. → ⎜ { ,,ℎ[] + +} → ⎟ ⎞ ⎟ ⎠ ⎜⎝ (︂ ⎜ ⎜ ⎜ ⎜ ⎜ ⎝ ◁ == 0▷ ⎛ ()
→ ⎛ !... ..2 → ◁ [0] == 1&& [1] == 1▷ ⎞ ⎜ ?....2. →
We define two type . 0 sends messages with message id 0, 1 while 1 with id 2. The producers publish three messages to simulate the practical operation of the NSQ. Furthermore, we re- □ strict that 1 must wait for 0 to finish sending before it sends the message. 3.4. nsqd The nsqd is daemon that receives, queues, and delivers messages to clients. It handles multiple streams of data at once through the unique design of Topic and Channel. We modeled three core functions of nsqd.
The entire nsqd process execute as flowing: () = ()||| ()||| ℎ(); The () is the main execution loop that drives the core functions of the NSQ daemon. It is responsible for constantly listens requests from other components and processes them according to predefined logic. We model four basic command handling logics, including , , and .
Multicasting and delivery of messages is a core function of nsqd.
The relationship between Topics and Channels is established through multicast, ensuring that each Channel receives a copy of all messages associated with a given Topic. This logic is implemented by the () process. ⎞ □ ⎟ ⎟ ⎠ □ ⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎝ ⎜ ⎝ ⎜ ⎝ ⎛ ?... ..ℎ → ⎛ (, ); ⎜ ℎ{
(, , ) ⎜ ◁ [] == 0▷ ⎛ ⎛ ℎ{
ℎ,[ℎ] = 1; } → ⎠ ◁ℎ,[ℎ] == 0 ▷ ⎜ ⎜ { ℎ2,,ℎ[] = 1; ]} → ⎜ { [] = 1; } → ⎝ !.... . → ⎞ ⎟ ⎟ ⎞ ⎞ ⎟ ⎠ ⎞ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎠ ⎟ ⎟ ; ⎟ ⎟ (, , )
ℎ,[ℎ] = 1; } → ⎠ ⎟ (); ℎ() = □ ⎜⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎝ ⎜ ⎜ ⎝ ⎜ ◁
︂( ⎛ ⎛ ?..ℎ. ⎞ ⎞ ⎜ ⎜ !...
{ℎ[] = 1; } → ..ℎ. {ℎ[] = 0; } →
ℎ2,,ℎ[] == 1 )︂ & [] > 0 ▷ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎠ ⎟ ; ⎟ ⎟ ⎟ ⎟ ⎟ ⎠ ℎ();
The nsqlookupd daemon manages the system’s topology information. nsqlookupd provides discovery and registration services, which decouple consumers from producers. The formal modeling of nsqlookupd is as follows. () = () ||| () ||| ();
The () process handles the registration requests sent by nsqd through the channel,and record nsqd instance by []. [] stores all the registered Topics on the nsqlookupd, and 2[][] holds the corresponding nsqd addresses for each Topic. Similarly, ℎ,[ℎ] and 2[][ℎ][] serve same functions for Channels.
() = ?... ..ℎ → {[] = 1; } → ⎛ ⎛ { ⎜⎜⎜ ⎝ 2[][[]]==11;;} → ⎜ ◁ℎ == −1▷ ⎜ ⎜ ⎛ ℎ{ ⎜⎝⎜⎜⎜⎜⎜⎜ ⎜⎝⎜⎜⎜⎜ 2ℎ2[[][[][,ℎ]]=[=]ℎ[11;;]]==11;; } →
(); ⎞ ⎞ ⎠ ⎟ ⎟ ⎟ ⎟ ⎟ ⎞ ⎟⎟ ;
⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎠ ⎠ () formalizes nsqlookupd’s responses to queries from consumers and nsqd instances using General Choice. (, ) provides all the stored nsqd address information associated with a specific Topic in nsqlookupd. Similarly, the ℎ(, ) returns Channels list under the specified Topic. () = ⎛ ?... . → ⎜ (, ); ⎜⎝ !..... → ⎞ ⎟ ⎟ ⎠ □ ⎛ ?... . → ⎜ ℎ(, ); ⎜⎝ !.....ℎ → ();
We also modeled the response of nsqlookupd to connection errors. When nsqlookupd encounters connection timeouts with nsqd, it will receive signal through and then remove all information associated with the corresponding nsqd from its records. This process ensures that the information stored on nsqlookupd remains consistently available.
When a consumer is initiated, it queries nsqlookupd for the addresses of nsqd instances associated with the target Topics. Upon receiving the addresses, it subscribes to all of these instances. Only after these can the consumer activate processes for message retrieval and processing.
Therefore, the modeling of consumer is as follows: ,,ℎ() = ,(); (() ||| ()) ; ,() = ( : 0..) :
◁ [] == 0▷ ⎛ {[] = 1; } → ⎞ ⎜⎜⎜⎜⎜⎜⎜⎜⎜⎜⎜⎜⎝⎜ ⎜⎜⎜⎜⎜⎜⎜⎛⎜⎝⎜⎜⎜⎜⎜⎜⎜⎛⎜⎝{(︂◁(..=!?[..:0].=.=..).1:,.▷(,,.→())→;}︂); ; ⎟⎟⎟⎟⎟⎟⎟⎞⎠ ⎟⎟⎟⎟⎟⎟⎟⎞⎟⎠⎟ ⎟⎟⎟⎟⎟⎟⎟⎟⎟⎟⎟⎟⎠⎟ ;
◁ == 1 ▷ ,,() = ◁ [] == 1▷ ⎛ !... ..2ℎ[] → ⎜ ?.... . → ⎜⎝ {[] = 1; } → {[] = 1} → ⎞ ⎟⎟ ; ⎠
The above formula models the process of a consumer connecting to nsqdlookupds and nsqds. The consumer sends a request to the nsqd through channel. It records connection information in [] and updates the value of . In the formula, the value of is set to 1, indicating the consumer’s readiness to process one message from .
..ℎ.{[] − −
; } → ⎛ (︂ {[] + +; } → )︂ ⎞ ⎝⎜⎜⎜⎜⎜ ◁⎝⎛2[!,[,]=().=]=−1.▷.;}ℎ→.{ ⎠⎞ ⎠⎟⎟⎟⎟⎟ ;
,,() ⎞
() = ⎟⎟ ; ?... ⎠
After completing the subscription, the consumer main- Topic and associated two Channels. defines consumer process. In our experiment, we use nonde- information, which assists us in conrfiming the status of tains a TCP connection with nsqd to be ready to receive messages. The diminishing of [] value implies a decrease in the amount of messages consumers can handle. [] keeps track of the message attempts number. −1 and will release []. Otherwise, the message is cached in the channel for further processing.
() is the message-handling module of the
signifies successful processing terministic to model the message-processing behavior.
We also model aborting re-queuing when the message attempts exceed the maximum value. deifnes the maximum number of message attempts allowed by the system. () = ⎝ ⎛ ⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎝ ⎜ ⎜⎜ ⊓ ⎜ ⎜ ⎝ ⎜ ⎜ ⎝ ?...ℎ. → ⎛ !... ..ℎ.{
[] = −1; } → {[] + +; } → ◁ [] > ▷ ⎛ !. ⎛ !.
.. ..ℎ.{ [] = −1;
} → {[] + +; } → ....ℎ.{
[] + +; } → {[] + +; } → ⎞ ⎠ ⎞ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎠ ⎞ ⎟ ⎟ ⎠ ⎞ ⎟ ⎟ ⎠ (); 4. Verification In this section, we use the model-checking tool PAT to realize the formal model constructed in section III, and verify its properties. At the same time, the results of properties verification are also shown at the end.
This part presents details of the modeling implementation with the PAT tool, mainly concerning the definition of constants, array variables and channels.
# 2; # 2; # 1; # 3; # 2; # 2; # 2;
We define constants as above to materialize the architecture of the NSQ system in Fig. 1. , , , and represent the number of producer, nsqd, nsqlookupd, and consumer. and denote that each nsqd has one the number of messages.
[][] = [0, 0, 0, 0]; ℎ[][] = [0, 0, 0, 0]; [][] = [0, 0, 0, 0]; [][ ] = [0, 0, 0, 0, 0, 0]; In addition, We define some arrays to store system processes. [][] is used to record the number of messages the consumer can process. ℎ[][] marks whether the nsqd is in the state of pushing messages to the consumer. [][] logs information about registered instances of nsqd on nsqlookupd. [][ ] tracks the status of messages processed on the consumer.
Furthermore, we have implemented the relevant channels in PAT based on the definitions provided earlier. We use multidimensional arrays to store channels between diferent entities is to avoid resource contention. ℎ [ ][] 0; ℎ [][] 0; ℎ [][ ] ; ℎ [][ ][] ; The channel definitions can be categorized into two types: _ are used for inter-component communication, where the channel size is set to 0 to achieve process synchronization. Cache channels _ are used within components, where the channel size is set to . These channels are utilized for process synchronization and message bufering.
Given that the NSQ message system operates with multiple producers, nsqds, nsqlookupds, and consumers, we employ a combination of interleaving and loop functions to realize the system’s implementation. The comprehensive definition of the NSQ system is presented as follows. cesses () run interspersed in the PAT. ||| : {0.. }@ (); statement means that multiple pro() = ||| : {0.. − 1}; : {0.. − 1}; : {0.. − 1}; : {0.. − 1}; : {0.. − 1}; ℎ : {0.. − 1} () ‖ (, , ℎ) ︂)
In this section, we verify the properties of the constructed model with the model checker PAT. These properties present the flexibility and robustness of NSQ distributed messaging platform.
In NSQ system, if messages can always flow and be handled in the correct way as they should, avoiding invalid or infinite loops, then we think the system is divergence free. It is crucial for message systems because the correctness and stability of the system depends on the correct handling and delivery of messages.
PAT provides the primitive to verify the divergence freedom of the system: # () ; information about the available components of the system forever, and when instances of nsqd are abnormal, it deletes all information about the corresponding instances. We defined a new system to verify the high availability of NSQ. An event of 0 is added to the original system, which will be triggered when all messages are finished. 2() = ()||| ⎛ ||| : {0.. − 1} ⎜ ⎛ [ℎ] ⎜ @ ⎝ !.0.. ⎝ . → ; ⎞ ⎞ ⎟
⎟ ⎠ ⎠
The above formula describes the new system, and we Data reachability is the basic property of message queue. verify in the PAT whether nsqlookupd maintains the list NSQ ensures at least one delivery of a message using the of available nsqd. The definition and assertion are as and , but it does not guarantee data order. In follows: our experiment, we track the attempts of messages with [][ ], where the value of −1 indi- # { cates the message is finished. Therefor, the definitions of [0][0] == 0 && [0][1] == 1 reachability and assertions are as follows: && [1][0] == 0 && [1][1] == 1}; # ℎ{
[0][0] == −1 && && [0][1] == −1 && [1][0] == −1 [1][1] == −1
# 2() |=<> ;
&& [0][2] == −1 && [1][2] == −1}; NSQ can dynamically adjust messages’ processing rate # () |=<> ℎ; by changing the consumer’s RDY value. To verify this property, we need to demonstrate that nsqd can push
As the model we constructed has two consumers sub- messages only if the consumer’s is greater than scribing to diferent Channels under the same Topic, each 0. Therefore, we introduce the ℎ[][] array consumer will receive a copy of all messages sent by pro- to store nsqds’ status, which indicate whether ducers and finish them all eventually. Symbol <> means is pushing data to . Combined with the that the system can finally reach ℎ state. [][] array, we give the following definition and assertion.
The NSQ system realizes a distributed decentralized architecture with nsqlookupd, which shows scalability. nsqlookupd manages the topological information of the system and allows nsqd instances to be added for horizontal scaling. In our experiments, the [][] is initially set to 0, denoting that no nsqd instances are available. When the value changes to 1, it indicates that nsqd instances were dynamically added, demonstrating the system’s scalability.
# {
[0][0] == 1 && [0][1] == 1 && [1][0] == 1 && [1][1] == 1}; # () |=<> ; 4.2.4. Availability nsqlookupd serves as a distributed directory service that supports fault tolerance and redundancy. It maintains # 00 {[0][0] > 0}; # · · · # ℎ00 {ℎ[0][0] = 0}; # ℎ · · · # () |=
(ℎ00 U 00) &&(ℎ01 U 01) &&(ℎ10 U 10) &&(ℎ11 U 11);
Our model has four message subscription connections as show in Fig.2. ℎ00 defines the state when 0 stops pushing messages to the 0, and 00 defines the state in which the 0 is ready to receive messages from 0. The rest of definitions are similar. We use the Untill(U) syntax from Linear Timing Logic (LTL) to describe the event that the nsqd stops pushing messages until the Rdy of the corresponding consumer is larger than zero. This formula verifies if the system can realize flow control. [1] Bernstein, P. A. (1996). Middleware: a model for distributed system services. Communications of the
ACM, 39(2), 86-98. [2] Snyder, B., Bosnanac, D., & Davies, R. (2011). ActiveMQ in action (Vol. 47). Greenwich Conn.: Manning. [3] Rostanski, M., Grochla, K., & Seman, A. (2014, Figure 3: Verification Results of the NSQ System September). Evaluation of highly available and faulttolerant middleware clustered architectures using RabbitMQ. In 2014 federated conference on computer 4.3. Verification and Results science and information systems (pp. 879-884). IEEE. [4] Wang, G., Koshy, J., Subramanian, S., Paramasivam, Depending on the definitions and assertions provided K., Zadeh, M., Narkhede, N., ... & Stein, J. (2015). Buildabove, we use model checker PAT to verify five proper- ing a replicated logging system with Apache Kafka. ties of the NSQ system, including Divergence Freedom, Proceedings of the VLDB Endowment, 8(12), 1654Reachability, Scalability, Availability, and Flow Control- 1655. lability. The model checker PAT verifies properties by [5] Yue, M., Ruiyang, Y., Jianwei, S., & Kaifeng, Y. (2017, searching for counterexamples in the system’s state space October). A MQTT protocol message push server or reaching the limits of state exploration. based on RocketMQ. In 2017 10th International Con
We present a summary of the verification statistics ference on Intelligent Computation Technology and in Fig. 3, including Visited States, Total Transitions, Time Automation (ICICTA) (pp. 295-298). IEEE. Used, and Estimated Memory Used. [6] NSQ: A realtime distributed messaging platform,
The verification results of all five properties indicate https://nsq.io/ that the NSQ message queue satisfies all the above prop- [7] Lai, X., Wang, H., Zhao, J., Zhang, F., Zhao, C., erties, proving that the system has high flexibility and & Wu, G. (2020, May). HBase Connection Dynamic robustness while providing credible delivery of messages. Keeping Method Based on Reactor Pattern. In Journal of Physics: Conference Series (Vol. 1544, No. 1, p.
012122). IOP Publishing. [8] Raje, S. N. (2019). Performance Comparison of Mes5. Conclusion and Future Work sage Queue Methods (Doctoral dissertation, University of Nevada, Las Vegas).
In this paper, we focus on the core functionalities of the [9] Togashi, N., & Klyuev, V. (2014, April). Concurrency NSQ message platform, including message publishing, in Go and Java: performance analysis. In 2014 4th registration, subscription, and querying. With CSP, we IEEE international conference on information science formalized critical components of the NSQ architecture, and technology (pp. 213-216). IEEE. such as producers, consumers, nsqd, and nsqlookupd. [10] Brookes, S. D., Hoare, C. A. R, & Roscoe, A. W. Using the model checker PAT, we conducted a rigorous (1984). A theory of communicating sequential proanalysis of the constructed NSQ model, verifying five fun- cesses. Journal of the ACM (JACM), 31(3), 560-599. damental properties: Divergence Freedom, Reachability, [11] Hoare, C. A. R. (1985). Communicating sequential Scalability, Availability, and Flow Controllability. These processes (Vol. 178). Englewood Clifs: Prentice-hall. properties underscore NSQ’s capacity to handle real-time [12] PAT: Process Analysis Toolkit. An Model Checker distributed message delivery at scale, confirming its high and Refinement Checker for Concurrent and Reallfexibility and robustness while ensuring dependable mes- time System. https://pat.comp.nus.edu.sg/ sage transmission. [13] Xiao, L., Zhu, H., Xu, Q., & Vinh, P. C. (2022). Mod
Nonetheless, besides the robustness of message queues, eling and verifying pso memory model using CSP. the security of data is extremely important for users. In Mobile Networks and Applications, 27(5), 2068-2083. the future, we will continue to enhance the formalized [14] Xu, J., Yin, J., Zhu, H., & Xiao, L. (2023). Formalizamodeling and verification of NSQ by refining workflows. tion and verification of Kafka messaging mechanism We will also delving into the system’s security aspects to using CSP. Computer Science and Information Sysadvance our research outcomes continually. tems, 20(1), 277-306.