Counter Abstractions in Model Checking of Distributed Broadcast Algorithms: some case studies

Abstract

The automated, formal veri cation of distributed algorithms is a crucial, although challenging, task. In this paper, we study the properties of distributed algorithms solving the reliable broadcast problem in various failure models. We investigate the suitability of a direct Satis ability Modulo Theories (SMT) approach to model these algorithms in order to validate safety properties. In a previous work, we modeled distributed algorithms using the declarative framework of array-based systems. In this work, we try also a simulation of array-based systems via counter systems. In fact, this simulation does not indeed introduce spurious runs violating the safety properties we want to formally verify in a signi cant class of problems. We report the related performance evaluations of some SMT-based modelcheckers (essentially, our tool MCMT and tools like Z, nuXmv). The experimental results are interesting because they show on one hand that state-of-the-art SMT-based technology can handle problems arising in fault-tolerant environments, and on the other hand that di erent heuristics and search strategies (e.g. acceleration versus abstraction) can have practical impact.

-

The validation of fault-tolerant distributed algorithms like those in [ 7, 25 ] is a crucial, although challenging, task. This kind of algorithms may support coordinated actions of distributed systems in critical applications such as, e.g., industrial plant monitoring through wireless sensors and actuators networks, eet coordination, intelligent transport applications, or aerospace applications. Hence, guaranteeing certain safety properties of the algorithms is compulsory. The processes executing these algorithms communicate to one another, their actions depend on the messages received, and their number is arbitrary. These characteristics are captured by so called reactive parameterized systems, that is, systems composed by an arbitrary number N of processes (\parameterized"), whose behavior depends on the interactions with the environment (\reactive"), namely, with the other processes.

We are interested in formally validating or refuting safety properties of reactive parameterized systems encoding fault-tolerant algorithms. This is a daunting task given their intrinsic in nite-state nature. In this paper, we consider in particular distributed algorithms to solve the reliable broadcast problem (see, e.g., [24]) in the presence of crash, send-omission, general-omission, and byzantine failures. In particular, our goal is to analyze the extent to which a direct encoding into Satis ability Modulo Theories (SMT) problems can be adopted for automated formal veri cation of these algorithms.

In our opinion, array-based systems [ 17 ] o er the most suitable formal model for these veri cation tasks; however, only quite recently decision procedures for arrays with cardinality constraints were designed and implemented [ 1 ] (see also [ 14 ] for a related framework) and a model checker exploiting them in a fully automated setting is still under construction. Our current tool MCMT - `Model Checker Modulo Theories' [ 18 ] implements array-based speci cations, but the impossibility of expressing in a direct way cardinality constraints causes di culties in handling veri cation of fault-tolerant distributed algorithms whenever threshold guards are involved (although sometimes ad hoc abstraction strategies may be successfully used).

In this paper, we report some experiments using counter systems [ 13 ] to specify the problems we consider. Whereas array-based modelizations are su ciently faithful and close to the original informal speci cations drawn from the literature, the same does not happen for counter systems: the latter can often only simulate the original algorithms and such simulation may sometimes be the fruit of an a-priori reasoning on the characteristics of the algorithm, embedded into the model. Despite this fact, all runs from the array-based speci cations are represented in the simulations with counters systems (this is in fact the formal content of the notion of a `simulation'), thus safety certi cations for the simulating model apply also to the original model. The advantage of this approach is that, as it is evident from our experiments, veri cation of counters systems performs well and is much more supported from the existing technology. In conclusion, whereas array-based speci cations remain one of the mainstreams for veri cation of distributed algorithms (due to their expressivity), a exible approach should not disregard counter speci cations as powerful tools to check subgoals and to solve subproblems tting a more restrict syntax.

The paper is organized as follows: in Section 2, we report some generalities about model-checking of in nite state systems and about our approaches. In Section 3, we introduce reliable broadcast problems and comment on crucial aspects of their modelizations with counter systems, compared with array-based systems presented in a previous work [ 2 ]. Finally, in Section 4 we report a performance evaluation of the veri cation with di erent state-of-the-art SMT-based tools. 2

Preliminaries

The behavior of a reactive system can be modeled through a transition system, which is a triple T = (W; W0; R) such that W is the set of possible con gurations of the system { expressed in terms of the state of each component process { W0 W is the set of initial con gurations, R W W is the transition relation: w1Rw2 describes how the system may evolve in one step. A safety problem for a subset Bad

W consists in determining whether there is a path woRw1Rw2

Rwn within (W; R) leading from w0 2 W0 to wn 2 Bad. We say that (W 0; W00; R0) (with safety problem Bad0) simulates (W; W0; R) (with safety problem Bad) i there is a relation W W 0 such that (i) for all w 2 W there is w0 2 W 0 such that w w0; (ii) if w w0 and w 2 W0 then w0 2 W00; (iii) if w w0 and w 2 Bad then w0 2 Bad0; (iv) if w w0 and wRv there is a path w0R0w10 wn0R0v0 with v v0. It is evident that the existence of such a simulation guarantees that if there is no path in (W 0; W00; R0) leading from W00 to Bad0, then there is no path in (W; W0; R) leading from W0 to Bad. Thus one can model-check (W 0; W00; R0) (w.r.t. Bad0) instead of (W; W0; R) (w.r.t. Bad), in case there is a simulation of the former to the latter (notice however that the existence of a path in (W 0; W00; R0) from W00 to Bad0 does not imply that an analogous path exists in (W; W0; R) because the latter essentially has `more runs', i.e. `more paths'). When we speak of simulations in the paper, we refer to the above notion of simulation: in fact, checking the existence of such a relation satisfying conditions (i)-(iv) above in our examples is a matter of more or less straightforward details. It is not clear whether such details can be checked automatically (they are speci c to each example); this might be seen a weak point of the method, however it should be pointed out that the substantial content of the veri cation task is in fact lifted to the simulating model, where it is checked automatically.

Various approaches are studied in the literature in order to formally verify safety properties. The problems we address in this paper are typically in nitestate: although the behavior of a single process could often be described by a nite state automaton, the family of systems is in nite due to the parameter N 2 N indicating the number of the component processes. In the in nite-state case an exaustive search through the states (in the style of textbooks like [ 9 ]) is not possible; states must be handled symbolically through logical formulae. In addition, satis ability tests for these formulae need to be discharged when a modelchecker performs its analysis; these satis ability tests are typically constrained by theories describing both data (integers, Booleans, reals, ...) or datatypes (arrays, lists, ...). This is where SMT solvers may be of help.

Essentially, an SMT-solver (Z3 [ 11 ], Yices [ 15 ], MathSAT [ 8 ], CVC4 [ 4 ],...) is an integrated framework for automated reasoning, involving a SAT-solver, a congruence closure solver, a solver for the manipulation of arithmetic expressions, and so on. Among further theories that might be supported by such solvers we have arrays, bit-vectors, non-linear arithmetic, etc.; quanti ed formulae are occasionally supported too, but with limitations due to well-known undecidability results. By itself, an SMT-solver cannot solve a model-checking problem, but a main application of SMT-solvers is within model-checking frameworks, where the model-checker (acting as a client) asks the SMT-solver (acting as a server) to discharge the satis ability tests it generates. First of all, the transition system must be speci ed via a logical formalism and the choice of the appropriate formalism requires a careful balance between expressivity and e ciency. When a logical formalism is chosen, the transition system is speci ed via a set of variables x, the initial and unsafe con gurations are speci ed via formulae W0(x), Bad(x) and the transition relation is speci ed via a formula R(x; x0). When this formal framework is xed, the SMT-solver can be used for instance as follows. If we are supplied an invariant I(x), the SMT-solver can check whether Bad(x) ^ I(x) is satis able, thus proving in the negative case that states in Bad are not reachable. The SMT-solver can also certify that I is actually an invariant, by checking formally that the initial set of states is included in I and that the system cannot exit I (starting from a set in I) when executing a step of the transition R. All this amounts to check the unsatis ability of the following two formulae W0(x) ^ :I(x)

I(x) ^ R(x; x0) ^ :I(x0) : Even when the above satis ability tests are e ective and feasible (because the underlying logic is not too expressive), the trouble is that invariants can be far from trivial and one cannot expect a user to be able to supply them in full details.

To sum up, the problems we need to face when trying to use an SMT-based approach to model-checking are two-fold: (i) choosing a formalization; (ii) de ning a search strategy for invariants. Whereas (ii) typically depends on the technology implemented in each model checker (we shall brie y turn on this below too, when we describe the tools), (i) is a modelisation problem relying on the user's choices: we discuss our own choices in next subsection. 2.1

Choosing a formalization

We discuss two methods for describing distributed algorithms. First, we have the array speci cation relying on the notion of an array-based system [ 17 ]. An array-based system is a transition system where a con guration, or system state, is represented as a collection of arrays whose length is not a priori bounded and whose i-th elements represent the state of process pi. Array-based systems can be enriched by adding to variables representing arrays also variables representing shared data, like integers, Booleans, etc. This is the more natural and widely applicable approach, and is well suited for parameterized systems; this formalization is adopted by tools like MCMT [ 18 ] and Cubicle [ 10 ]. Relevant properties need quanti ers to be expressed: for instance, the violation of mutual exclusion is expressed as 9z19z2 (z1 6= z2 ^ a[z1] = critical ^ a[z2] = critical) (1) where a maps every process to its location.

Counter systems is the formalization we take into consideration in this work. In a counter system, we can only use integer variables to describe the system state, i.e., we can just count the number of processes which are in each possible location (or, more generally, satisfying a predicate). The method is suitable in case the behavior of a process in a reactive parameterized system is driven by conditions of the type: if (number of received messages is in [min, max])

then perform action; where action can be a location change, a message send, etc. The counters speci cation may be used when processes are indistinguishable, and it does not matter \who" performs an action but rather \how many" do it (so called thresholdguarded algorithms [ 20, 21 ]). Counter speci cations have been used to formalize broadcast protocols [ 12, 16 ], cache coherence protocols [ 13 ] and are the basic formalism accepted by automata-based tools like FAST [ 3 ]. The main advantage of counter speci cations is that only integer variables are used; quanti ers are not needed (for instance in this setting (1) can be formulated simply as critical > 1), so much more support is available from existing solvers. The drawback is that this approach may not be expressive enough: when processes are structured as a ring, as a linear order or as a graph, nothing can be done within it. Even in case processes are unstructured, the use of counters models may require some form of abstraction. Take for instance a byzantine environment: correct processes either send or do not send a message to all other processes, but byzantine faulty processes may behave non-symmetrically, i.e. they may maliciously send corrupted messages only to a subset of processes in order to fool them. In this case, it is not su cient just to count the number of processes having sent a message. This problem may be overcome by introducing some form of abstraction (see below, or see the interval abstractions of [ 20 ] for another solution); abstractions, however, may cause spurious behavior, so in principle there is no guarantee that counters formalizations may work when they are combined with such abstractions. Otherwise said, abstractions produce just simulations, in the formal sense explained above.

On the other hand, in order for array-based model-checkers to be able to perform in a natural way arithmetic reasoning about the cardinality1 of the set of processes satisfying certain properties, an integrated framework (combining cardinality constraints and array-like speci cations) would be desirable. The problem is not that of changing the formal model (array-based systems are appropriate), but to enrich the logic supported to reason about such formal model. The enrichment should be appropriately designed to combine expressivity with computational e ciency (see [ 1 ] for recent promising results in this direction). 2.2

The tools

Whereas for array speci cations the Model Checker Modulo Theories (MCMT) [ 18 ] is our reference tool, for counter speci cations, it is possible to use also other SMT-based model-checkers (we choose Z [ 19 ] and nuXmv [ 6 ]) because counter speci cations only involve integer variables. In detail: - MCMT is an SMT-based model checker able to verify the properties of in nitestate reactive parameterized systems. Although speci cally designed for array1This is required, for example, to express resilience properties, i.e., assumptions of the kind \at most k processes will fail", where k is a symbolic constant (see below for a more detailed discussion on this).

based systems, it can handle counter speci cations too. MCMT exploits Yices [ 15 ] as the underlying SMT-solver. It has suitable options for abstraction/re nement search; however, MCMT abstraction is tailored to arraybased systems and so MCMT abstraction is too peculiar to be really operative in case of pure counter speci cations. On the other hand, MCMT implements also some form of acceleration; by using acceleration the tool may become competitive for counter speci cations, because it is able to describe in one shot the e ect of executing some loops any nite number of times. - Z is the Z3 module operating with Horn clauses speci cations; the formalism of Horn clauses is becoming a common speci cation language for model checkers. Using this formalism, we can specify the safety problems addressed in the counter speci cations of this paper. As a search mechanism, Z employs an IC3-based algorithm - a sophisticated abstraction/re nement search driven by the property to be checked. - nuXmv is the evolution for in nite-state systems of the symbolic model checker NuSMV; it uses MathSat as the underlying SMT-solver and implements state-of-the-art abstraction/re nement algorithms like IC3.

Of course, a comparison of the di erent tools is not easy and is not our main goal. Our aim is more modest: we just want to show that, by introducing rather natural and simple modeling techniques, current SMT-technology can successfully deal with our benchmarks. 3

Considered Class of Problems

In this section, we discuss the modeling of fault-tolerant distributed algorithms using counter systems. We consider four algorithms, namely, the reliable broadcast algorithms for crash (CBA), send-omission (SOBA), or general-omission (GOBA) failures described in [ 7 ], and the algorithm for a broadcast primitive with byzantine failures (BBP) described in [25]. We discuss just the relevant aspects of modelization; interested readers may nd the complete models at http: //users.mat.unimi.it/users/orsini/dbaMC_experiments.html. In the next section, we report some performance evaluation. 3.1

CBA, SOBA, and GOBA algorithms

Let G be a group of cooperating processes. The Reliable Broadcast problem requires that, when a process in G sends a message m, either all the correct processes in G deliver m to their users, or none of them delivers m, in spite of failures. In CBA, processes may prematurely stop performing any action; the halt may occur in the middle of a broadcast. In SOBA, processes may either crash, or transiently omit to send some messages requested by the algorithm. In GOBA, processes in addition may transiently omit to receive some messages. A correct process is a process that does not fail in any way for the whole algorithm Algorithm 1 Pseudo-code for CBA and SOBA Initialization: if (p is the sender) then estimate[p] else estimate[p] state[p] undecided; End Initialization m; coord id[p] ?; coord id[p] run. More formally, an algorithm correctly solves the Reliable Broadcast problem if it satis es the Agreement property: Agreement: If a correct process decides to deliver a message m, then all correct processes decide to deliver m.

To guarantee the algorithm correctness, up to t processes may fail (resilience), with t N 1 for CBA and SOBA, and t (N 1)=2 for GOBA. The system must be synchronous, in the sense that both the time for a message to arrive to its destination, and the time for a process to execute an algorithm step, are upper bounded. Hence, the algorithms evolve in rounds whose length is nite. For the sake of space, in this work we focus on the modelization of SOBA through counter systems; similar mechanisms are used for GOBA, while CBA is a special case. The pseudo-code for both CBA and SOBA is reported by Algorithm 1: by ignoring the underlined instructions, CBA is obtained; for SOBA, consider all the instructions in the pseudocode regardless of the fact that they are underlined or not. In [ 2 ], the discussion of how to model both CBA and SOBA using the array-based method is reported.

The counters modelization uses only global variables that count how many processes are in a certain state. In particular, we count (i) the number of either correct or faulty undecided processes owning or not the message m to be reliably broadcast to the group of processes (undC=F (m= ?)),2 (ii) the number of either correct or faulty processes that have decided (decC=F (m= ?)), (iii) the round number, and (iv) the number of either requests or nacks received by the current coordinator. Initially, the round number is 1, no process has undertaken any action, and only the sender { which is also the rst coordinator { owns m. This is described by initializing (undC(m) + undF (m)) = 1. The unsafe formula to be refuted, negating the Agreement property, is expressed as: ' = (decC(m) > 0 ^ decC(?) > 0).

In Round 1, every type and number of undecided processes may send a request, and the steps are freely interleaved. As an example, the guard enabling the transition of undecided correct processes with no message is: // prototype of a state update transition if (round = 1) then 1: undC(?) undC(?) 1; 2: req(?) req(?) + 1; 3: doneC(?) doneC(?) + 1; The support variables doneC=F (m= ?) are used to count the number of undecided processes that perform a transition, and to restore the appropriate initial values when switching to the successive round, with updates of the form undX(y) doneX(y), while the done variables are reset to 0. The round is incremented when all processes are moved to done, that is, when undC(m) + undF (m) + undC(?) + undF (?) = 0.

An interesting aspect is the modeling of send-omission failures. When using array theory, MCMT implicitly adopts the crash failure model [ 2 ], in that transitions describe the actions of alive processes. The behavior of faulty processes only omitting to send messages is fully described, whereas faulty crashed processes do nothing since their crashing (and if transitions do not cover all the possible cases, then the processes falling into the unspeci ed cases are considered crashed). The above solution is based on an (implicit) quanti ers relativization technology, which is not available anymore when counter abstractions are adopted; so in counter systems, we have to maintain the accounting of all the processes. To this purpose, in every round we added transitions similar to the prototype above but without line 2: a faulty process may omit to send the request but it is counted among the triggered processes. Processes that crash are modeled as processes that { from the failure on { only perform those transitions.

Many kinds of transitions may be accelerated by changing the state of d processes (rather than 1) at a time, for any d greater than 0 and not greater than the global number of processes involved in the transition. In this case, the prototype above would be: // prototype of an accelerated state update transition if (round = 1 ^ 9d; 0 < d undC(?)) then

1: undC(?) undC(?) d; 2 Thus e.g. undC(m) counts the number of undecided correct processes owning m, whereas undF (?) counts the number of undecided faulty processes not owning m, etc. 2: req(?) req(?) + d; 3: doneC(?) doneC(?) + d; As an important heuristics, some model checkers (like MCMT) are supposed to produce by themselves the above accelerated form in order to prevent divergence and to speed up the veri cation for all possible values of the variable d in the indicated range, thus reproducing all cases of subsets of processes sending their requests and subsets of processes failing to do this. This acceleration does not introduce spurious traces.

A critical aspect of counter modelization is the determination of the most recently distributed estimate (lines 4, 8 of Algorithm 1). We describe the solution we adopted in our simulating model. If the coordinator receives just one type of requests (i.e., either req(m) = 0 or req(?) = 0), then that value is taken as the estimate e. Otherwise, two global variables lastE and agC are used. The former is set to e every time the current coordinator succeeds in sending its estimate to at least one process. The latter is initialized to 0 and set to 1 the rst time a coordinator reaches a correct process, which will report the estimate to all the successive coordinators. In the successive phases, if f lagC > 0 then the coordinator takes lastE as its estimate; otherwise, the algorithm behavior is nondeterministic: both e = m and e = ? are allowed.

Di erently from the array-based implementation, there is no memory about what processes are or have already taken the role as a coordinator: this is an example of an abstraction we are forced to make because of the adoption of counters formalization (this abstraction, fortunately, does not introduce spurious behavior). In Round 2, both cases of a correct and a faulty coordinator are explored, depending on whether the corresponding sets of processes are not empty. The two branches are distinguished by properly setting a global ag correct coordinator. In the case of a correct coordinator, all undecided processes adopt its estimate in one transition, and Round 3 is skipped, according to the following code (where e is supposed equal to m): if (e = m ^ correct coordinator) then

undC(m) undC(m) + undC(?); undF (m) undF (m) + undF (?); In the case of a faulty coordinator, transitions adopt the schema of the prototype above, so that processes are allowed to update their estimate { and their state and associated counter is changed accordingly { or alternatively to move to done thus simulating the send-omission failure of the coordinator. Moreover, at any time a transition allows to move to the successive round (describing the case where no further messages are sent by the coordinator). The residual number of undecided processes not yet triggered is the number of processes enabled to send a nack. This is modeled similarly to Round 1, with the simpli cation that it is su cient one process sending the nack to switch to the successive round. Round 4 (di usion of the Decide by the coordinator) is modeled after Round 2. 3.2

Byzantine broadcast primitive

In [25], an algorithm implementing a broadcast primitive for byzantine failures (BBP) is proposed, aiming at substituting authentication obtained by unforgeAlgorithm 2 Byzantine broadcast primitive Initialization: k round number when p broadcasts m ; Round k:

Phase (2k-1): process p sends Init(p,m,k); Phase 2k: 8 process does: if (received Init(p, m, k) from p in Phase 2k 1) then send Echo(p, m, k) to all; if (received Echo(p, m, k) from N t distinct processes in Phase 2k) then Accept(p, m, k); Round r k+1: 8 Phase (2r 1), 2r: 8 process does if (received Echo(p, m, k) from N 2t distinct processes in previous phases ^ not sent echo yet) then send Echo(p, m, k) to all; if (received Echo(p, m, k) from N t distinct processes in this and previous phases) then Accept(p, m, k); able signatures. Byzantine failures allow faulty processes to behave arbitrarily, i.e. omitting to send and/or receive messages, sending messages with a wrong content, or even coalescing to fool correct processes. The resilience in this case is t (N 1)=3. The algorithm attempts to achieve its goal through the re-di usion of a message m sent by a source p, on behalf of the receiving processes, trying to aggregate a majority of correct processes supporting the acceptance of m. The pseudo-code is supplied by Algorithm 2. The algorithm aims at guaranteeing the following properties: Correctness: If a correct process p broadcasts (p,m,k) in round k, then every correct process accepts (p,m,k) in the same round.

Relay: If a correct process accepts (p,m,k) in round r k then every other correct process accepts (p,m,k) in round r + 1 or earlier.

Unforgeability: If process p is correct and does not broadcast (p,m,k), then no correct process ever accepts (p,m,k).

This algorithm signi cantly di ers from those in sec.3.1. All algorithms are synchronous. Yet, in the previous algorithms, for each round a di erent kind of message is exchanged, and all messages of that type must arrive within that round. By contrast, in BBP just one type of message is exchanged, i.e. the Echo messages, and processes consider the cumulative number of Echo's received so far. This is the reason why in our model we abstract from the round value, and just di erentiate two phases: (i) initialization, depending on the property to be validated, and executed just once; (ii) actions undertaken by correct processes depending on the number of Echo's each one of them received so far. The evolution of correct processes is reproduced by continuously triggering the transitions of phase (ii).

In our model, we consider di erent process states depending on the received messages. For correct processes, four states are possible: the initial state (IT ), the receivedInit (RI) state, the sentEcho (SE) state and the Accepted (AC) state. Fig. 1 represents the state transitions: arcs are labeled with a pair htriggering event, performed actioni { with one of the two elements possibly empty { and describe all the possible interleavings of events. In our counter speci cation, four global variables named after the states are used to count the number of processes in each state. According to Algorithm 2 and to the number of received Echo's, correct processes move from one state to the other as shown in Fig. 1. These transitions are modeled simply by updating the number of processes in the four states, and accumulating the number of newly generated messages, which will be counted by the processes successively (phase (ii)).

The behavior of faulty processes is modeled indirectly through a global variable F counting the number of Echo's generated by faulty processes and received by the correct process taking the next transition. F is updated by two transitions that may freely interleave with the others, which respectively increment or decrement F while always guaranteeing that 0 F t. The decrement is the abstraction we introduce to describe the possibility that a faulty process does not send its messages to all the correct processes (the abstraction consists in the fact that in this way we allow messages to be in a sense \withdrawn"). In our experiments, this abstraction does not introduce spurious behavior (for a di erent abstraction, using interval abstract domains, see [ 20 ]). It is worth to notice that correct processes are unable to distinguish whether an Echo was generated by either a correct or a faulty process. Hence, in the transitions modeling correct behavior, just the cumulative value (SE + F ) is considered.

As far as the validation is concerned, we produced one model for every property to be validated; all models include the same transitions and they di er just in the initialization. Unforgeability is a safety property, while both Correctness and Relay are liveness properties. Yet, most of the available in nite-state model checkers are not able to verify liveness properties. In order to deal with this problem, we change liveness properties into safety properties by exploiting the round indication in the assertion: since the round where the 'good event' (i.e. the event mentioned in the liveness property) has to take place is known, the problem can be reformulated as a safety property (even better, as a bounded model checking property). In the following, for each property we supply both the corresponding unsafe formula, and the initial state: { Correctness: the unsafe formula is: 'C := ((SE+F ) < (N t)^(IT +RI) = 0). Initially all correct processes are in RI state. { Unforgeability: the unsafe formula is: 'U := (AC > 0). Initially all correct processes are in IT state. { Relay: to refute acceptance on behalf of the correct processes, it must be the case that either (i) there are still processes in IT but the Echo messages are not su cient to move them to either SE or AC state; or (ii) there are still processes in SE state but the Echo messages are not enough to move them to AC state. The two conditions above are described by the following unsafe formulas, which are checked separately: 'RA := ((SE + F ) < (t + 1) ^ IT > 0 ^ RI = 0) 'RB := (AC < (N t) ^ (IT + RI) = 0 ^ (SE + F ) < (N t)): For both RelayA and RelayB, initially the number of Echo's sent by correct processes equals SE + AC and processes may be in whatever of the four states, but it must be AC > 0. 4

Performance Evaluation

We implemented the models described in the previous section in MCMT; the MCMT models have been automatically translated into equivalent formalizations in either Z and nuXmv, in order to gain some understanding of the behavior of the analyzed approaches. The translators we developed yield a twofold advantage: they allow to model an algorithm only once, and they allow to perform a fair comparison amongst tools. It should be noticed that verifying counter speci cations is undecidable in general, thus there is no guarantee that our tools converge. To achieve convergence in practical cases, one needs sophisticated methods: these include acceleration (in the case of MCMT) or IC3-like abstraction/re nement (in the case of Z and nuXmv). All measures have been conducted on an Intel Core i5-2500 CPU @ 3.30GHz with 8 GB RAM, running Debian GNU/Linux stretch/sid x86 64. The experiments have been conducted with MCMT version 2.5.2 leveraging Yices 1.0.40, Z version 4.4.2, and nuXmv version 1.0.1.3

Table 1 reports the results obtained with the best combination of parameters for each tool, which we supply in our website. The Model column identi es the considered algorithm and property to be validated, and the failure model in which the validation was performed. The Result column reports the outputs of the model checkers: for all tests all the model checkers supplied the same output. For MCMT, we also report the maximum Depth of the explored tree, and the number of Nodes (formulae describing system states) composing the explored tree, as an indication of the computation overhead in the various cases.

The results show that all the considered tools solve the algorithms e ciently. MCMT is not as engineered as the other two tools, but its performance is nonetheless comparable although not as good. Results lead to the conclusions 3After the submission of this paper, a new version 1.1.0 of nuXmv was released; we repeated the experiments with the new release without noticing substantial di erences. that pure SMT is a technology suitable to perform the automatic veri cation of fault-tolerant distributed algorithms, without the need of transforming those systems into nite-state systems.

One word about heuristics needed to prevent divergence: as we already mentioned, MCMT can only use acceleration for counters systems, whereas Z and nuXmv use sophisticated forms of abstraction/re nement. Since acceleration is just a preprocessing technique, one can manually include accelerated transitions in the speci cation les for Z and nuXmv too; however, we did not notice signi cant improvement doing that in the above benchmarks (but the overhead is also modest). On the other hand, the most di cult benchmark (namely the counters formalization of GOBA) has been solved only by MCMT, thus showing that plain acceleration without abstraction may also be the winning choice in some cases. 5

Conclusions and Related Work

In this paper, we showed how Satis ability Modulo Theories may be e ectively used to perform automated formal veri cation of fault-tolerant distributed algorithms. Algorithms for the Reliable Broadcast problem have been modeled using the counter speci cation paradigm. This paradigm is well-known [ 13 ], but to the best of our knowledge, this is the rst modelization of algorithms for crash, send-omission and general omission failures using this paradigm. In all cases, the veri cation converged and promising performances have been obtained, showing that SMT is a formalism powerful enough to manipulate this sort of problems.

A series of papers related to ours is [ 20, 22, 23 ]; in these papers, abstractions leading to counters formalizations are introduced for a large set of fault-tolerant distributed algorithms (including those from Subsection 3.2 above). An interesting speci cation formalism, namely threshold automata, is introduced. Roughly speaking, threshold automata are counter automata in which integer variables are divided into two groups: the variables in the rst group measure the number of processes in each location, whereas the variables in the second group (called `shared variables') measure the progress of the system and, as such, cannot be decremented. It is assumed that in each cycle of the control ow of the automaton, shared variables cannot increase either; under these assumptions, it is proved in [22] that the system diameter is nite, thus allowing bounded model checking to be complete for veri cation. Optimizations in the trace enumerations are designed in [23]; once relevant traces are identi ed, the whole veri cation task can be discharged by an SMT-solver checking the actual feasibility of such traces. Overall, this approach seems to be quite powerful and scalable, whenever abstractions needed for encoding algorithms and problems into the proposed formalism are available (it is not clear for instance, whether our examples from Subsection 3.1 can t this framework).

As a future work, we plan to model the whole algorithm for Reliable Broadcast in the presence of byzantine failures. The idea is to come back to array-based systems like in [ 2 ], but using recent achievements from [ 1 ] in order to be able to capture some advantages of counter formalizations inside the framework of arraybased systems. The challenge is that of keeping the e ciency of counter systems documented in this paper in a more expressive and more exible context, allowing direct formalizations and avoiding ad hoc simulations/abstractions. This would be in some sense similar to the approach taken in the forthcoming paper [ 5 ], where array speci cations with cardinality constraints are joined to the machinery of Horn clauses solving (the di erence is that we plan to use complete [ 1 ] or at least more aggressive decision procedures for generating and discharging proof obbligations involving counting quanti ers fragments).

The algorithms considered in this paper work for certain values of resilience, which have been inferred in the literature only through informal, verbal proofs. Another interesting aspect would be to use model checkers in order to automatically discover resilience thresholds in the veri cation process, as those thresholds that separate safe and unsafe executions. 21. A. John, I. Konnov, U. Schmid, H. Veith, and J. Widder. Towards Modeling and Model Checking Fault-Tolerant Distributed Algorithms. In Proc. Int'l SPIN Symposium on Model Checking of Software, volume 7976 of Lecture Notes in Computer Science, pages 209{226. Springer, Jul. 2013. 22. I. Konnov, H. Veith, and J. Widder. On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability. In Proc. of CONCUR, LNCS, pages 125{140, 2014. 23. I. Konnov, H. Veith, and J. Widder. SMT and POR beat Counter Abstraction: Parameterized Model Checking of Threshold-Based Distributed Algorithms. In Proc. of CAV, LNCS, 2015. 24. M.C. Pease, R.E. Shostak, and L. Lamport. Reaching agreement in the presence of faults. J. ACM, 27(2):228{234, 1980. 25. T.K. Srikanth and S. Toueg. Simulating authenticated broadcasts to derive simple fault-tolerant algorithms. Distributed Computing, 2(2):80{94, 1987.

References

1. F. Alberti , S. Ghilardi , and E. Pagani . Counting Constraints in Flat Array Fragments . In Proc. IJCAR, Lecture Notes in Computer Science , 2016 . Preliminary version in arXiv: 1602 . 00458 .

2. F. Alberti , S. Ghilardi , E. Pagani , S. Ranise , and G.P. Rossi . Universal guards, relativization of quanti ers, and failure models in model checking modulo theories . Journal on Satis ability, Boolean Modeling and Computation (JSAT) , 8 : 29 { 61 , 2012 .

3. S. Bardin , J. Leroux , and G. Point . Fast extended release . In Proc. of CAV , pages 63 { 66 , 2006 .

4. C. Barrett , C.L. Conway , M. Deters , L. Hadarean , D. Jovanovic , T. King , A. Reynolds , and C. Tinelli . CVC4. In Proc. Int'l Conf. on Computer Aided Veri cation (CAV) , volume 6806 of Lecture Notes in Computer Science, pages 171 { 177 . Springer, 2011 .

5. N. Bj rner, K. von Gleissenthall, and A. Rybalchenko . Cardinalities and universal quanti ers for verifying parameterized systems . In Proc. of the 37th ACM SIGPLAN conference on Programming Language Design and Implementation (PLDI) , 2016 .

6. R. Cavada , A. Cimatti , M. Dorigatti , A. Griggio , A. Mariotti , A. Micheli , S. Mover , M. Roveri , and S. Tonetta . The nuXmv Symbolic Model Checker . In Proc. 26th Int'l Conf. on Computer Aided Veri cation (CAV) , volume 8559 of Lecture Notes in Computer Science, pages 334 { 342 . Springer, Jul. 2014 . https://nuxmv.fbk. eu/.

7. T.D. Chandra and S. Toueg . Time and message e cient reliable broadcasts . In Proc. 4th Int'l Workshop on Distributed Algorithms , volume 486 of Lecture Notes in Computer Science, pages 289 { 303 . Springer, 1991 .

8. A. Cimatti , A. Griggio , B. Schaafsma , and R. Sebastiani . The MathSAT5 SMT Solver . In Proc. Int'l Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) , volume 7795 of Lecture Notes in Computer Science. Springer, 2013 .

9. E. M. Clarke , O. Grunberg , and D. A. Peled . Model Checking. MIT Press, 1999 .

10. S. Conchon , A. Goel , S. Krstic , A. Mebsout , and F. Za di. Cubicle: A Parallel SMT-based Model Checker for Parameterized Systems . In Proc. 24th Int'l Conf. on Computer Aided Veri cation (CAV) , volume 7358 of Lecture Notes in Computer Science, pages 718 { 724 . Springer, Jul. 2012 .

11. L. de Moura and N. Bj rner. Z3: An e cient SMT solver . In Proc. 14th Int'l Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) , volume 4963 of Lecture Notes in Computer Science, pages 337 { 340 . Springer, Mar. 2008 . https://github.com/Z3Prover/z3.

12. G. Delzanno, J. Esparza , and A. Podelski . Constraint-based analysis of broadcast protocols . In Proc. of CSL , volume 1683 of LNCS , pages 50 { 66 , 1999 .

13. Giorgio Delzanno . Constraint-based veri cation of parameterized cache coherence protocols . Formal Methods in System Design , 23 ( 3 ): 257 { 301 , 2003 .

14. C. Dragoj , T. Henzinger , H. Veith , J. Widder , and D. Zu erey. A logic-based framework for verifying consensus algorithms . In Proc. of VMCAI , 2014 .

15. B. Dutertre and L. de Moura. The Yices SMT solver . Technical report , SRI International, 2006 . http://yices.csl.sri.com.

16. J. Esparza , A. Finkel , and R. Mayr . On the veri cation of broadcast protocols . In Proc. of LICS , pages 352 { 359 . IEEE Computer Society, 1999 .

17. S. Ghilardi , E. Nicolini , S. Ranise , and D. Zucchelli . Towards SMT Model Checking of Array-based Systems . In Proc. Int'l Joint Conf. on Automated Reasoning (IJCAR) , volume 5195 of Lecture Notes in Computer Science, pages 67 { 82 . Springer, Aug. 2008 .

18. S. Ghilardi and S. Ranise . MCMT: a Model Checker Modulo Theories . In Proc. Int'l Joint Conf. on Automated Reasoning (IJCAR) , volume 6173 of Lecture Notes in Computer Science, pages 22 { 29 . Springer, Jul. 2010 . http://users.mat. unimi.it/users/ghilardi/mcmt/.

19. K. Hoder , N. Bj rner , and L. De Moura . Z - an e cient engine for xed points with constraints . In Proc. of CAV , LNCS, 2011 .

20. A. John , I. Konnov, U. Schmid, H. Veith , and J. Widder . Parameterized model checking of fault-tolerant distributed algorithms by abstraction . In Proc. Int'l Conf. on Formal Methods in Computer-Aided Design (FMCAD) , pages 201 { 209 , Aug . 2013 .