We present a formal model of publish/subscribe network architectures in which a central communication broker is in charge of distributing messages to clients subscribed to certain topics. We consider different semantics for the internal structured of the server and for the notification phase. We discuss applicability of an SMT-based infinite-state model checker to the proposed model and decidability results for abstractions obtained hiding the internal structure of a server.
are confined in the local data of worker threads. In our setting the shared data consists of the current subscribers list. Copy-on-write data structures [30] are a possible implementation of this synchronisation techniques that can be used to avoid race conditions on shared data structures. Copy-on-write data structures are particularly useful when book-keeping session data in a distributed application. Indeed they automatically produce a snapshot of the share data structures (lists, sets, etc) when combined with iterators (i.e. to scan a set/list) . The semantics of copy-on-write concurrent data structures typically provide a mechanism to generate snapshots on demand (e.g. when an iterator needs to scan the structure) producing an exception (that will be handled by the user) in case of simultaneous read and write access from multiple threads. In our model we will not model exception handling and assume that snapshots are generated and confined in a worker thread when necessary. Extending the semantics towards a more complex modeling of copy-on-write is an interesting direction for refining the model. The use of worker threads allows us to model the publishing of a message asynchronously w.r.t. to other operations executed on the server (e.g. registration of new clients, etc). Under the considered semantics for copy-on-write data structures, we will then show that computations in the resulting model can be transformed into round-based executions that are simpler to analyse (they reduce the number of possible interleavings) with respect to a more liberal interleaving model. 2
We use Id to denote a denumerable set of identifiers of client instances. Furthermore, we define Q as the finite set of client state labels, A as the finite set of action labels, and M as the finite set of message labels. For brevity, we assume that action labels have one of the following form: local, that denotes a local transition, subscribe, that denotes a subscription request, unsubscribe, that denotes an unsubscription request, publish(m) with m ∈ M , that denotes a publish request for message m ∈ M .
The above listed type of actions are strictly related to the communication model typical of publish/subscribe architecture based on a client-server architecture in which every message is delivered to all subscribers via a central server (or, more in general, via a cluster/federation of servers). A client specification P is a tuple hQ, q0, Ri, where Q is a finite set of states, q0 ∈ Q is the initial state, and R ⊆ Q × A × Q defines state transitions induced by action labels. In other words a client specification can be viewed as a finite state automata with labelled transitions that statically define its behaviour.
A client configuration is a tuple hi, s, b, f i, where i ∈ Id is the client identifier generated after a connection request, s ∈ Q is the current client state, b ∈ 2M is the set of messages received so far, and f ∈ {>, ⊥} is a flag that defines the connection status of the client with respect to the global network, namely > corresponds to the normal operating status, whereas ⊥ corresponds to a disconnection event. We assume that disconnected clients cannot roll back to a normal status, i.e., when they restart they will be assigned a new identifier, their internal state being completely reset. The client specification hQ, q0, Ri can naturally be extended with enabling conditions for transitions in R based on the presence of certain messages in the current message list (e.g. hq1, local, q2i only if message m1, . . . , mr have already been received). We will not discuss this extension in this paper.
For a fixed n ≥ 1, a server configuration is defined by a tuple hL, W1, . . . , Wni, where L ∈ 2Id is a finite set of identifers that represents the list of subscribed clients and, for each i : 1, . . . , n with n > 1, Wi represents the current state of the i-th worker thread used by the server to deliver messages. More specifically, Wi can be either ⊥ or hmi, Rii with mi ∈ M and Ri ⊆ 2Id. In the former case it denotes an idle thread, whereas in the latter it denotes initialized threads in which Ri is the current snapshot of the subscription list, and mi is the message to be delivered. The use of a snapshot R of the current subscription list of the server is based on implementations of read/write operations on shared data structures based on snapshots/copy-on-write data structutes used in concurrent programming to avoid race conditions. The initialisation of a worker thread with the snapshot of the subscriber list allows the server to proceed asynchronously with the delivery of a message to all subscribers. In our model we consider a fairly realistic scenario in which the server employs a fixed number or worker threads for this kind of task. Furthermore, we model the semantics of a publish message asynchronously: the server first spawns (when available) a new task with a copy of the current subscriber list. The worker can then deliver the message to the active clients. The initial server configuration is the tuple h∅, I1, . . . , Ini where Ii = ⊥ for i : 1, . . . , n.
A global configuration is defined by a tuple hS, Ci, where S = hL, W1, . . . , Wni is a server configuration, and C = {c1, . . . , ck} is a finite set of client configurations such that cj = hij, sj, bj, fji for j : 1, . . . , k. We use N to denote the set of network configurations.
For fixed sets A, Q, M , and given a client specification P = hQ, q0, Ri, and n > 1, a Pub/Sub Network P S is defined via a transitions system defined through a binary relation over network configurations. More precisely, the relation →⊆ N × N is defined as the least relation satisfying one of the conditions listed below. We show next some example of transitions such as P ublish and N otif y. • Publish Transition: • Notify Transition:
P ublish hS, {hi, s, b, f i} ∪ Ci → hS0, {hi, s0, b, f i} ∪ Ci under the assumptions: f = >, hs, publish(m), s0i ∈ R, S = hL, W1, . . . , Wni, q ∈ {1, . . . , n}, Wq = ⊥, S0 = hL, W1, . . . , Wq0, . . . , Wni, and Wq0 = hm, Li, With this rule a client instance sends a publish request to the server. The server acknowledges the request passing the message to an idle worker thread together with a snapshot of the current subscriber list L. The client updates its local state according to R.
N otif y hS, Ci → hS0, C0i under the following assumptions C = {c1, . . . , ck}, ci = hidi, si, bi, fii for all i ∈ {1, . . . , k}, S = hL1, W1, . . . , Wni, Wq = hm, L2i for some q ∈ {1, . . . , n}, S0 = hL1, W1, . . . , Wq0, . . . , Wni, Wq0 = ⊥, C0 = {c01, . . . , c0k} where for all j : 1, . . . , k, cj = hidj, sj, bj, fji, if idj ∈ L2 and fj = >, then c0j = hidj, sj, b0j, fji and b0j = bj ∪ {m}, c0j = cj, otherwise. With this rule we model notification of message m via a global action performed by worker thread Wq = hm, L2i whose effect is to update the message list of each active client instance whose identifier is included in the list L2. The remaining client instances (their identifier is not in the list or they are inactive) remain unchanged. After notification the worker thread resets its state to idle ⊥ and returns available for distributing other published message.
The semantics of copy-on-write concurrent data structures in concurrent programming languages such as Java [30] is in general more complex than the model described above. Indeed, copy-on-write data structures typically provide a mechanism to generate snapshots on demand (e.g. when an iterator needs to scan the structure) producing an exception (that will be handled by the user) in case of simultaneous read and write access from multiple threads. In our semantics we do not model exception handling and focus instead on the confinement of snapshots of a shared data structure in worker threads. 3
In our work we have applied the above described formal language to build a verifiable (parameterised) model that can be validated via the SMT-based Infinite-state Model Checker Cubicle. In this setting we use unbounded arrays to model arbitrary collections of publisher and subscriber processes as well as an unbounded shared data structure used as a communication media between processes. The evolution of the shared memory through the different rounds is modelled using a bi-dimensional unbounded arrays indexed both on round numbers and process identifiers. Each row of such a matrix can then be used to model the different phases of a protocol round, e.g., the formation of a subscriber group.
The resulting model can be validated through the SMT-based Infinite-state Model Checker Cubicle.
Cubicle implements a symbolic backward reachability algorithm in which sets of configurations are
represented via formulas in fragments of First Order Logic that combine Presburger Arithmetics and
the Theory of Arrays [
In [