We apply the In nite-State Model Checking to formally specify and validate protocol skeletons for distributed systems with asynchronous communication and synchronous access to local data structures. More precisely, we validate the Redis Pub/Sub key-value Server. Redis is based on a publish-subscribe architecture used in Cloud Storage and Internet of Things ecosystems. For the considered protocol, we present a formal speci cation that combines ideas coming from round-based and shared-memory speci cation languages. The resulting model is validated via the SMT-based In nite-state Model Checker Cubicle. In this setting we use unbounded arrays to model (1) arbitrary collections of publishers and subscribers, (2) unbounded shared memory used as a communication media between processes. Our model is validated using the symbolic backward reachability algorithm implemented in the tool. The peculiarity of the algorithm is that, upon termination, the resulting correctness proof is guaranteed to hold for every number of process instances.
Protocols designed to operate in distributed systems are often de ned for an
arbitrary number of components interacting via asynchronous communication.
Formal speci cation languages like Petri nets can be used to model skeletons
and abstractions of this kind of systems. In this setting the coverability decision
problem [
In this paper we focus our attention on the application of Cubicle [
Cubicle captures in a natural way the combination of these two types of models. First of all, it provides declaration of multi-dimensional unbounded arrays. For instance, the declaration array Sub[proc,proc]; denotes a bidimensional array in which indexes range over an unbounded set of process identi ers. In our case study, each row of an unbounded matrix can be used to model a protocol phase, e.g., the current con guration of a subscriber group. Each cell in a row can then be used to represent the current state of a subscriber, publisher, message, and so on. Furthermore, Cubicle transitions can specify both local and global modi cations to groups of array cells. Atomic global updates are obtained by using universally quanti ed transitions. Asynchronous updates can be obtained by splitting a global update in a series of local updates executed non-deterministically.
The resulting model is validated through the SMT-based veri cation engine
of Cubicle. Cubicle implements a symbolic backward reachability algorithm in
which sets of con gurations are represented via formulas in fragments of First
Order Logic that combine Presburger Arithmetics and the Theory of Arrays
[
The paper is organized as follows. We rst introduce our case-study. We then propose a formalization guided by the above described combination of ideas coming from round-based and shared memory speci cation models and by functional requirements of the protocol. We then discuss validation results obtained via the Cubicle engine. Finally, we discuss related work and address some future research directions. Redis is a Publish/Subscribe (Pub/Sub) system that can be used as key-value server. Redis is used in microservice applications to ensure consistency of updates of distributed databases. The underlying publish/subscribe protocol can indeed be used to propagate local updates to a given key to a set of connected services. In the original Pub/Sub implementation clients can use three types of commands: PUBLISH, SUBSCRIBE, and UNSUBSCRIBE. To track subscriptions, Redis uses a global variable pubsub channels which maps channel names to sets of subscribed client objects. A client object is a virtual image of a TCPconnected client maintained in the server. When a client submits a SUBSCRIBE command for a given channel, its client object gets added to the set of clients for that channel name as shown in Fig. 1. To PUBLISH, Redis looks up the subscribers in the pubsub channels variable, and for each client, it schedules a job to send the published message to the corresponding client socket. To optimize the management of connection failures (e.g. clients close their connections), Redis annotates each client with its set of subscribed channels, and keeps this in sync with the main pubsub channels structure. This way, instead of iterating over every channel, Redis only needs to visit the channels the client was subscribed to. Fig. 2 illustrates the con guration obtained from Fig. 1 when adding the above mentioned auxiliary structure. At the implementation level the pubsub channels is de ned as an hash table to optimize key-search and hash table resizing. To summarize, the algorithm for the PUBLISH and (UN)SUBSCRIBE operations are informally de ned as follows.
{ To PUBLISH, hash the channel name to get a hash chain. Iterate over the hash chain, comparing each channel name to our target channel name. Once the target channel name is found, get the corresponding list of clients. Iterate over the linked list of clients, sending the published message to each client. { To SUBSCRIBE, nd the linked list of clients as before. Append the new client to the end of the linked list (constant time). Also, add the channel to the client's hash table (constant time). { To UNSUBSCRIBE, nd the linked list of clients for the channel, as before.
Then iterate over the entire list and remove the client.
Further optimizations are related to lazy resizing strategies of hash tables and bit-level representation of hash tables and channel names. We do not describe these features here and focus instead on the protocol skeleton used in the Redis server. 3
To model the Redis architecture and extract correctness requirements, we will rst focus on some peculiarities and properties of the underlying Pub/Sub protocol. First of all, we remark that the object manipulated in the Server data structures represent TCP client connections. A TCP connection can be viewed as a perfect channel in which messages are delivered in the same order as they are sent. Under this assumption, we can restrict ourselves to failures due to network connections drops or to explicit client disconnections. Furthermore, we will assume that (1) the Redis implementation ensures the synchronization between the di erent data structures maintained in the server, (2) each data structure (e.g. pubsub channel) is maintained consistent via standard concurrency control abstractions (concurrent data structures, synchronized blocks, etc). These assumptions allows us to focus on a model with two di erent layers: (1) a synchronous layer used to model updates of the data structure maintained by the Redis server. (2) an asynchronous layer used to model responses. More precisely, subscribe requests will be modeled via synchronous updates of an abstraction of the pubsub channel data structure, whereas publish requests will be modeled in two phases: a synchronous step used to update the server data structures and and asynchronous one used to send noti cations to subscribers.
Another important observation is related to the expected behavior of the
Pub/Sub protocol. Subscribe and unsubscribe requests can be submitted any
time to a Redis server. Thus, at least in principle, it is impossible to
guarantee that, for a xed topic, a given update will reach all subscribers that are in
the pubsub channel during the completion of a publish request. For instance,
a subscriber can join the server right after the update has been distributed to
all TCP connection objects but before it is actually received by all clients, an
unsubscribe request can be received by the server before the completion of the
publish request of another client, a TCP connection might drop during the
protocol execution, etc. To model the above mentioned scenarios, it is convenient
to adopt a round-based view of the protocol behavior. In each round we use a
shared memory model to specify the current state of the pubsub channel. More
speci cally, we use two unbounded arrays Sub and Msg, indexed on round and
process indenti ers, to model: (1) the state of subscribers in di erent rounds
of the protocol, and (2) messages waiting to be delivered to subscribers in that
round. Notice that each row of the two matrices is associated to a distinct round.
A round consists of synchronous steps in which either a (non deterministically
selected) subscriber joins a group associated to a given topic or a publisher
prepares the message to be sent to the current set of subscribers. The asynchronous
phase of a round consists in the distribution of noti cations to the subscriber
group. Rounds are used here as a conceptual tool to model di erent phases of
the protocol. In real execution traces several phases may overlap. Following the
methodology discussed in [
We do not consider here any order between round identi ers. The reason is that we rely on TCP connections for maintaining the order between a sequence of updates sent by the same publisher. However our goal is to show the correspondence between updates sent by a publisher and received by a subscriber within the same round. To ensure this property, we need to ensure freshness of every newly created subscriber group, and ensure that object preparation is done synchronously (or using some form of serialization step).
In our model we apply some additional abstractions. Firstly, we focus on a single channel name (topic), assuming that the synchronization of the data structure associating clients to topics and topics to clients are done correctly in the protocol implementation of the Redis server Secondly, we consider only noti cations with two possible values, namely One and Two, since we two values are enough to show a possible inconsistency between a publisher and a subscriber view of the same update.
Figure 3 summarizes the intuition of the model that we will formally specify using Cubicle's input language in the rest of the section.
We rst de ne types and array variables to model publishers, subscribers, and pending object messages in di erent rounds. type pstate = Idle | Busy | One | Two type sstate = SIdle | SOne | STwo type mstate = Null | MOne | MTwo array Pub[proc] : pstate array P[proc,proc] : pstate array S[proc,proc] : sstate array Sub[proc,proc] : bool array Msg[proc,proc] : mstate More speci cally, the interpretation of the declared data structures is as follows: { pstate de nes the publisher state, { sstase de nes the subscriber state, { mstate is used to model the state of the shared-memory, { Pub models the state of publishers: Pub[n] is initially Idle and it is set to
Busy after the selection of a round number. { P models the state of publishers after the selection of a round number, i.e., Pub[t,n]=One [resp. Two] means that, in round t, n has chosen to send One [resp. Two]. { Sub models a subscriber group in a speci c round, i.e., Sub[t; p] = T rue if, in round t, p belongs to the subscriber group. { S models the state of subscribers after the selection of round numbers. { nally, Msg models the ow of messages from publishers to subscribers, i.e., Msg[t,p] identi es a message that, in round t, has to be delivered to subscriber p. The initial con guration is de ned via the following Cubicle statement. init (t n) {
Pub[n] = Idle && P[t,n] = Idle && S[t,n] = SIdle && Sub[t,n] = False &&
Msg[t,n] = Null The above statement must be interpreted as a conjunctive formula universally quanti ed over t and n. In other words in the initial con guration Pub,P and S are in idle state, there are no subscription groups and no message objects. The rst transitions speci es the subscription step of a given client. transition subscribe(t n) requires {
Msg[t,n] = Null && Msg[t,t] = Null && forall_other r. (Msg[t,r] = Null) } { Sub[t,n] := True; } For a subscriber to join a group at round t, the rule requires the absence of message objects in the same round. Since the initial con guration does not put any constraint on groups, any subscriber group can be generated by using this rule until a given round identi er t remains fresh.
The second transition combines an asynchronous request done by a publisher with a synchronous step done by the Redis server in order to prepare message objects for every subscriber of the current round. transition publish1(t n) requires {
Pub[n] = Idle && Msg[t,n] = Null && Msg[t,t] = Null && forall_other r. (Msg[t,r] = Null) } { Pub[n] := Busy; P[t,n] := One; Msg[p,q] := case | p=t && q=n : MOne | p=t && Sub[t,q]=True : MOne | _ : Msg[p,q]; In this rule a publisher with identi er n selects a fresh round number (in which subscribers could have formed a group with arbitrary shape) and then prepares message objects for every subscriber associated to that round number. The rst case p=t && q=n : MOne of the update rule is used to insert at least a MOne message in the current round (in case there are no other subscribers). The second case p=t && Sub[t,q]=True : MOne assigns the state MOne to the message object of every subscriber. The state of the message objects of other rounds or other indexes remains unchanged.
The following rule is used to select value T wo and assign state M T wo to message objects. transition publish2(t n ) requires {
Pub[n] = Idle && Msg[t,n] = Null && Msg[t,t] = Null && forall_other r. (Msg[t,r] = Null) } { Pub[n] := Busy; P[t,n] := Two; Msg[p,q] := case | p=t && q=n : MTwo | p=t && Sub[p,q]=True : MTwo | _ : Msg[p,q];
The combined e ect of the previous rules is that of storing the type of noti cation (One or Two), in a non-deterministically chosen, unused round identi er t, and of initializing the state of every cell ht; qi (current round t, subscriber q) of the Msg matrix with the corresponding states (MOne for One and MTwo for Two).
Finally, we assume that publishers can reset their state and return to the Idle state in order to start a new round (and possibly send a di erent value). transition reset(n) requires {
Pub[n] = Busy We now come to the de nition of the noti cation phase. Noti cations are generated by non-deterministically delivering message objects to subscribers. } { } {
Pub[n] := Idle;
ttransition notify1(t n) requires {
S[t,n] = SIdle && Msg[t,n] = MOne transition notify2(t n) requires {
S[t,n] = SIdle && Msg[t,n] = MTwo
S[t,n] := STwo; 4
Our correctness requirement must necessarily be formulated with respect to a given round. More speci cally, we would like to show that only when a subscriber group remains stable for a long enough period (that we identify as a round), then every noti cation sent by the publisher will be received by every subscriber in the group. This kind of property is similar to correctness criteria used in consensus protocols like Paxos. Under this hypothesis, unsafe con gurations can be speci ed using the following judgements adopted by Cubicle to specify bad con gurations: } } { } } } } The subscriber state S stores in a local state the value of the received message for the current round number. unsafe (t m n) {
P[t,m] = One && S[t,n] = STwo } } unsafe (t m n) {
P[t,m] = Two && S[t,n] = SOne unsafe (t n) {
P[t,n] = Two && S[t,n] = SOne unsafe (t n) {
P[t,n] = One && S[t,n] = STwo Cubicle interprets this kind of formulas as existentially quanti ed over the parameter names. Therefore, the judgements specify con gurations in which, through the shared-memory model of subscription and message objects, values read by subscribers are di erent from those published by publishers in the same round.
The Cubicle veri cation engine is based on symbolic backward exploration. Cubicle operates over sets of existentially quanti ed formulas called cubes. The search procedure maintains a set V and a priority queue Q resp. of visited and unvisited cubes. Initially, let V be empty and let Q contain the cubes representing bad states. At each iteration, the procedure selects the highest-priority cube from Q and checks for intersection with the formula denoting the initial con gurations (satis ability of conjunction of and formulas in the initial conditions). If the test fails, it terminates reporting a possibile error trace. If the test passes, the procedure proceeds to the subsumption check, i.e., implication between formulas. If subsumption fails, then add to V , compute all cubes in predt (for every t), add them to Q, and move on to the next iteration. If the subsumption check succeeds, then drop from consideration and move on. The algorithm terminates when a safety check fails or Q becomes empty. When an unsafe cube is found, Cubicle actually produces a counterexample trace.
Formulas containing universally quanti ed formulas (generated during the
computation of predecessors) are over-approximated by existentially quanti ed
formulas. In presence of universally quanti ed guards the class of formulas
manipulated by the backward reachability loop of Cubicle in not closed under
preimage. To handle such formulas, Cubicle implements a safe but over-approximate
pre-image computation. Given a cube 9i: and a guard G of the form 8j: (j),
the pre-image replaces G by the conjunction V 2 (j;i) (j) of instances over
the permutation of (j; i). In other words, in order to handle universally
quantied guards, Cubicle applies a declarative (and syntactic) version of the monotone
abstraction introduced in [
When applying Cubicle to our formal model of the Redis Pub/Sub protocol enriched with judgments expressing bad con gurations, the tool proves the model correct in few seconds. More speci cally, Cubicle visits 20 nodes with at most 3 process indexes, 970 xpoint checks, and 806 calls to the Alt-Ergo SMT solver. Since Cubicle operates over unbounded arrays, the above result provides a correctness proof of the considered model for any number of publishers and subscribers. The proof certi cate can be obtained by taking the (negation of the) set of assertions (formulas) collected during the xpoint computation. When
D I C
3 0 0 Yes
3 0 0 Yes
3 0 6 Yes
3 0 8 Yes
3 0 0 No
Fig. 4. Experimental results: V=visited nodes, F= xpoint tests, S=solver calls,
M=max process number, D=deleted node, I=number of invariants (brab),
C=property checked (Yes/No).
invoked using the BRAB algorithm with parameter 2 the tool infers 6
invariants that reduce the visited nodes to 12, the xpoint checks to 518, and the
number of calls to the solver to 291. The execution time remains unchainged.
When invoked using the BRAB algorithm with parameter 3 the tool infers 8
invariants at the cost of a signi cant increase of the execution time. The table
in Fig. 4 summarizes the results obtained with the di erent heuristics provided
by Cubicle. In Fig. 4, in order to check robustness, we also consider variations,
as such as Redis1, of the above discussed model. Redis1 is obtained by
removing from the publisher rules the the rst case in the Msg update action, namely
| p=t && q=n : MOne in publish1 and | p=t && q=n : MTwo in publish2.
When validated in Cubicle, this modi cation leads to the following error trace
(in the Cubicle output notation):
pub1(#1,#2)->Sub(#1, #3)->pub2(#1,#3)->notify2(#1,#3)->unsafe[
We have presented an application of the SMT-based In nite-state Model Checker
Cubicle to the veri cation of a parameterized model of the Pub/Sub architecture
implemented in the Redis server. The formal speci cation is based on the
combination of a round-based interpretation of the protocol behavior with a shared
memory representation of the updates to its internal data structures. This work
is strictly related, although applied in a di erent class of protocols, with our
recent work on the application of logic-based declarative methods for the
verication of distributed systems [
Theor. Comput. Sci., 256(1-2):63{92, 2001. 22. S. Ghilardi and S. Ranise. Backward reachability of array-based systems by SMT solving: Termination and invariant synthesis. Logical Methods in Computer Science, 6(4), 2010. 23. A. Mebsout. Inference d'invariants pour le model checking de systemes parametres. (Invariants inference for model checking of parameterized systems). PhD thesis, University of Paris-Sud, Orsay, France, 2014. 24. T. Tsuchiya and A. Schiper. Veri cation of consensus algorithms using satis ability solving. Distributed Computing, 23(5-6):341{358, 2011. 25. http://users.mat.unimi.it/users/ghilardi/mcmt/.