Towards model checking electrum specifications with LTSmin

Universidade do Minho Escola de Engenharia Departamento de Informática Bruno Miguel Sousa Cancelinha Towards model checking Electrum specifications with LTSmin October 2019 Universidade do Minho Escola de Engenharia Departamento de Informática Bruno Miguel Sousa Cancelinha Towards model checking Electrum specifications with LTSmin Master dissertation Master Degree in Computer Science Dissertation supervised by Professor Doutor Alcino Cunha Professor Doutor Paulo Sérgio Almeida October 2019 DIREITOS DE AUTOR E CONDIÇÕES DE UTILIZAÇÃO DO TRABALHO POR TERCEIROS Este é um trabalho académico que pode ser utilizado por terceiros desde que respeitadas as regras e boas práticas internacionalmente aceites, no que concerne aos direitos de autor e direitos conexos. Assim, o presente trabalho pode ser utilizado nos termos previstos na licença abaixo indicada. Caso o utilizador necessite de permissão para poder fazer um uso do trabalho em condições não previstas no licenciamento indicado, deverá contactar o autor, através do RepositóriUM da Universidade do Minho. Atribuição CC BY https://creativecommons.org/licenses/by/4.0/ i ACKNOWLEDGEMENTS When writting the acknowledgments of a master thesis, we are not just acknowledging the people who were close by and helped on the construction of the whole dissertation. Rather it is my view that we are acknowledging everyone who accompanied us in these past five years. I am certantily not the same person I was five years ago, and I am sure I wont be the same person five years from now. But that transformation cannot be attributed to a single person or a group, but to everyone I have ever interacted with; in the sense that every person I stumble upon during my life, in some way or another, changes me and the path I am following. I cannot therefore thank individually each one who helped bringing me here, since I would either have inadequately long acknowledgments or I would have committed the terrible disgrace of missing someone. With that cleared out, I must thank those who, like me, where thrown into a new world five years ago and who have been supporting me ever since. I also send my thanks: To those friendships that begun on Wednesday nights, and prolonged during the years. To those whom culture and the joy of argumentation brought us together. To those that I have recently met through activism. To those with whom I have lived with, and had to put up with me. To everyone I have ever drank tea with. To everyone I have ever loved. To the people at CeSIUM with whom I have learned so much. To the volunteers of CoderDojo and the kids we teach. To the community around Include Braga. To all my professors and teachers. To the cafés that provided the tranquil environment that allowed for this dissertation to be written. To my long-lasting friends in Chaves that sometimes had to assume I went missing. To my family and our pets. Finally I must also acknowledge, this time by name, those who directly helped in the development of this dissertation. Namely Professor Alcino Cunha for always keeping the ambition and motivation high; Professor Paulo Sérgio Almeida, for always bringing a different perspective on things; Nuno Macedo whom was always ready to help me and discuss my problems; Alfons Laarman for having the patience of answering my long list of questions on LTSmin. ii iii This work is financed by the ERDF – European Regional Development Fund through the Operational Programme for Competitiveness and Internationalisation - COMPETE 2020 Programme and by National Funds through the Portuguese funding agency, FCT - Fundação para a Ciência e a Tecnologia, within project POCI-01-0145-FEDER-016826. STATEMENT OF INTEGRITY I hereby declare having conducted this academic work with integrity. I confirm that I have not used plagiarism or any form of undue use of information or falsification of results along the process leading to its elaboration. I further declare that I have fully acknowledged the Code of Ethical Conduct of the University of Minho. iv RESUMO Model checking é uma técnica comum de verificação; garante a consistência e integridade de qualquer sistema fazendo uma exploração exaustiva de todos os possíveis estados. Devido à grande quantidade de intercalações possíveis entre eventos, modelos de sistemas distribuídos muitas vezes acabam por gerar um número de estados muito grande. Nesta dissertação vamos explorar os efeitos de partial order reduction — uma técnica para mitigar os efeitos da explosão de estados — implementando uma linguagem semelhante ao Electrum com LTSmin. Vamos também propor um event layer por cima do Electrum e uma análise sintática para extrair informação necessária para que esta técnica possa ser implementada. Palavras-chave : Alloy, Electrum, Model checking, LTSmin, Partial order reduction, TLA + v ABSTRACT Model checking is a common verification technique to guarantee the consistency and integrity of any system by an exhaustive exploration of all possible states. Due to the large amount of interleavings, models on distributed systems often end up with a huge state-space. In this dissertation we will explore the effects of partial order reduction — a technique to mitigate the effects of this state-explosion problem — by implementing an electrum-like language with LTSmin. We will also propose an event layer over Electrum and a syntactic analysis to extract valuable information for this technique to be implemented. Keywords: Alloy, Electrum, Model checking, LTSmin, Partial order reduction, TLA+ vi CONTENTS 1 introduction 1 2 model checking 3 2.1Modelling 3 2.2Specification 4 2.2.1CTL 5 2.2.2LTL 6 2.3Verification 8 2.3.1Model checking for CTL 8 2.3.2Automata-based model checking for LTL 9 2.3.3Bounded model checking for LTL 12 2.4Partial order reduction 14 3 electrum 17 3.1Language 17 3.1.1Showcase example - Poolboy 17 3.1.2Modeling the system 18 3.1.3Specifying the system 27 3.2Analyzing the model 29 3.2.1Validation 30 3.2.2Verification 31 3.3Backend overview 33 4 ltsmin 35 4.1PINS architecture 35 4.2Specifying in PINS 37 4.2.1Showcase Ring leader election example 37 4.2.2Modelling ring leader election in C 38 4.2.3Analysing with LTSmin 44 4.3Guard-based partial order reduction 44 4.3.1A stubborn approach 45 4.3.2Calculating necessary enabling sets 46 4.3.3Defining the DNA matrix for ring leader election 48 4.4Results 49 5 taino:an electrumesque front-end for ltsmin 50 5.1The language 50 vii 2.2. Specification 4 1.Sis the set of all possible system states. 2.S0⊆Sis the set of initial states. 3.R⊆S×Sis the relation that defines the transition from one state to the other. 4.L:S→2AP is the labelling function that labels each state with the set of atomic propositions from AP true in that state. Relation R is assumed to be total i.e. for every s∈S there is a s0∈S where hs,s0i ∈ R , meaning that for every state s there is a transition to another state s0 . We will mostly denote s R s0instead of hs,s0i ∈ R. From the Kripke structure we can infer the notion of paths. A path — denoted by π — is an infinite sequence of states; π=s0s1s2. . . represents the path starting on state s0 and where ∀i≥0 : hsi,si+1i ∈ R . We will also use πi to be the i -th state from path π , πi to denote the sub-path of π beginning in the i th state, Paths(s) represents all possible paths beginning in state s , and Paths(M) represents all possible paths of model M . These notions will be useful for defining the semantics of our specification logic. 2.2 specification Most of the software requirements are specified in a natural language; however, natural languages are frequently susceptible to ambiguity and cannot be easily translated to logical formulas. Formal logic specifications, on the other hand, allow for a unique interpretation. In general, these specifications fall into two categories: liveness properties, usually characterised by "Eventually something good will happen"; and safety properties, of the kind "Something bad never happens". Such notions of "eventually" and "always" (negation of "never") refer to the evolution of a system without explicitly referring to time. We can describe these notions in a formal language using temporal operators. We have an intuitive understanding of what these terms ("eventually" and "always") mean, however we must define them in the context of Kripke structures as well as show how atomic propositions can be validated in them. This can be achieved by a powerful logic called temporal logic. Temporal logic is an expansion of classical logic to support reasoning over time. In computer science there are two main temporal logic formalisms: branching time and linear time, which are ilustrated by Figure 1. In branching time (Figure 1b), the semantics is defined on a computation tree unrolled from a initial state of the Kripke structure; while in linear time (Figure 1a), the semantics is defined over the set of computational paths of the Kripke struucture. 2.2. Specification 5 a0 b0 d0c0 ... a0 b0 d1c0 ... a0 b1 d2c2 ... (a) Representation of linear time a0 b1 b0 c0 d1 d0 c2 d2 ... ... ... (b) Representation of branching time Figure 1: Two representations of the same computation in linear and branching time 2.2.1CTL Computation Tree Logic (CTL) is a branching time temporal logic. The interpretation of CTL formulas is defined both in terms of states and paths. Because of its branching-time nature which, with a single tree, allows us to reason about multiple computations, properties defined in CTL are capable of expressing notions such as "in some computations X happens". CTL formulas are classified into state formulas and path formulas. State formulas assert properties over a state and quantify propositions over paths beginning in that state, whereas path formulas describes temporal properties over one path. CTL state formulas are defined by the following grammar: Φ::=true |false |a|Φ1∨Φ2|Φ1∧Φ2| ¬Φ| ∃ϕ| ∀ϕ Being AP a set of atomic propositions and a∈AP , and ϕ a path formula. Path formulas, on the other hand, are defined by: ϕ::=e Φ|Φ|♦Φ|Φ1UΦ2|Φ1RΦ2 Where Φis a state formula. Omitting ¬,∧and ∨, the above symbols are read as: ∃ϕThere exists at least one computation path where ϕholds. ∀ϕϕholds for all computation paths. c ΦΦholds in the next state. ΦΦalways holds. ♦ΦEventually Φwill hold. Φ1UΦ2Φ1holds until Φ2. Φ1RΦ2Φ1releases Φ2. 2.2. Specification 6 Given a model M and a state formula Φ we say Φ holds in M ( M|=Φ ) if and only if ∀s∈S0:M,s|=Φ , that is, Φ holds for every initial sate of M . We define the satisfaction relation ( |= ) by: Let AP be a set of atomic propositions, p∈AP , Φ,Φ1 , and Φ2 be state formulas and ϕbe a path formula, and 6|=be the negation of |=, M,s|=p⇐⇒ p∈L(s) M,s|=¬Φ⇐⇒ M,s6|=Φ M,s|=Φ1∧Φ2⇐⇒ M,s|=Φ1∧M,s|=Φ2 M,s|=Φ1∨Φ2⇐⇒ M,s|=Φ1∨M,s|=Φ2 M,s|=∀ϕ⇐⇒ ∀π∈Paths(s):M,π|=ϕ M,s|=∃ϕ⇐⇒ ∃π∈Paths(s):M,π|=ϕ We have just defined |= for state formulas, now let us define it for path formulas. With all the above assumptions and let πbe a path in M, M,π|=e Φ⇐⇒ M,π1|=Φ M,π|=Φ⇐⇒ ∀i≥0 : M,πi|=Φ M,π|=♦Φ⇐⇒ ∃i≥0 : M,πi|=Φ M,π|=Φ1UΦ2⇐⇒ ∃i>0 : M,πi|=Φ2∧ ∀0≤j<i:M,πj|=Φ1 M,π|=Φ1RΦ2⇐⇒ ∀i>0 : M,πi|=Φ2∨ ∃0≤j<i:M,πj|=Φ1 To understand the difference between the path quantifiers, imagine the following two properties: ∃♦Φ(1) ∀♦Φ(2) They are both stating that eventually Φ will hold. However, property 1is true if at least one of the computational paths satisfies ♦Φ , while for property 2to be true all computational paths must satisfy ♦Φ . In figure 2ait is represented a model that satisfies property 1but not property 2, and the model represented in figure 2bsatisfies both properties. 2.2.2LTL Linear Temporal Logic (LTL) is a linear time temporal logic and was actually suggested before CTL by Pnueli (1977). It consists only of path formulas, thus it is unable to define properties 2.2. Specification 7 Φ ... ... ... (a) Model that satisfies property (1) Φ Φ ... ... ... Φ (b) Model that satisfies property (2) Figure 2: The representation of properties (1) and (2) in branching time involving unrestrained quantification over paths. By definition, LTL formulas apply to all computational paths, as if it was a CTL formula with a single implicit ∀. The syntax of LTL is given by the following grammar: ϕ::=true |f alse |a| ¬ϕ|ϕ1∧ϕ2|ϕ1∨ϕ2|e ϕ|ϕ|♦ϕ|ϕ1Uϕ2|ϕ1Rϕ2 All those symbols are read exactly the same as in CTL, however their semantics change because we do not have a satisfaction relation for state formulas, only for path formulas. So we say that ϕ holds in model M ( M|=ϕ ) if and only if ∀π∈Paths(M)·M,π|=ϕ . The reader might notice that, although the syntax is very similar, the semantics is not. The satisfaction relation of LTL is defined differently using only path formulas. Let AP be a set of atomic propositions, p∈AP, and πnbe a sub-path of πbeginning in the n-th state, M,π|=p⇐⇒ p∈L(π0) M,π|=¬ϕ⇐⇒ M,π6|=ϕ M,π|=ϕ1∧ϕ2⇐⇒ M,π|=ϕ1∧M,π|=ϕ2 M,π|=ϕ1∨ϕ2⇐⇒ M,π|=ϕ1∨M,π|=ϕ2 M,π|=e ϕ⇐⇒ M,π1|=ϕ M,π|=ϕ⇐⇒ ∀i≥0 : M,πi|=ϕ M,π|=♦ϕ⇐⇒ ∃i≥0 : M,πi|=ϕ M,π|=ϕ1Uϕ2⇐⇒ ∃i>0 : M,πi|=ϕ2∧ ∀0≤j<i:M,πj|=ϕ1 M,π|=ϕ1Rϕ2⇐⇒ ∀i>0 : M,πi|=ϕ2∨ ∃0≤j<i:M,πj|=ϕ1 2.3. Verification 8 2.3 verification Verification is basically a way to get all states where a formula is valid. Let M=hS,S0,R,Li be a Kripke structure representing a reactive system, and φ be a temporal logic formula. The set of states where formula φis valid is denoted by [[φ]]M={s∈S|M,s|=φ} So, for some formula φ to be valid in model M , all the initial states from M must be in [[φ]]M, that is, M|=φ⇐⇒ S0⊆[[φ]]M In this section we will first look at two ways of verifying CTL formulas by explicit model chekcing and symbolic model checking. Later we will briefly take a look at how LTL formulas can be verified using Büchi automata, and how LTL formulas can be converted into CTL formulas. Lastly we will look at mechanisms to speedup the verification of both LTL and CTL formulas. 2.3.1Model checking for CTL Since we wont be using CTL model checking in this dissertation, we will just take a general overview of how model checking is performed in CTL. Explicit model checking The first model checking tools verified formulas by transversing an explicit state machine, a technique called explicit model checking. Explicit model checking is an approach that checks the validity of some temporal logic formula by explicitly transversing a state machine. In explicit model checking for CTL, most operators are seen to be redundant and only five basic operators are used ( ¬,∨,∃e ,∃ U ,∃ ) 1 , and the set of states where some formula is valid is, most of the times pretty direct. For instance, the states [[¬φ]] = S\[[φ]] , i.e., the states where some formula ¬φis valid is the set of all states minus those where φis valid. To check φ1∃U φ2 , for instance, we first find [[φ2]]M and then we transverse the graph backwards using the converse of relation R ( R◦ ) and register the states from all paths π where ∀s∈π:s∈[[φ1]]M. Checking ∃φ is more complicated. First, the model is reduced to only those states which do satisfy φ , then the state machine is broken down into nontrivial strongly connected components (SCC), with the goal of finding a terminal SCC reachable from an initial state, thus trivially ensuring the satisfiability pf ∃φ . This procedure is efficient because a linear 1For an easier notation, we say Φ1∃U Φ2instead of ∃(Φ1UΦ2) 2.3. Verification 9 time algorithm to calculate strongly connected components has been proposed by Tarjan (1972). Symbolic model checking Symbolic model checking was first proposed by McMillan (1993) who figured out that one could specify a state machine implicitly by using propositional logic with ordered binary decision diagrams (OBDDs). The first insight is to consider that it is possible to represent the set of formulas can be represented symbolically by a propositional formula. And that most LTL properties can be expressed with either ∃φand ∃U, which can be calculated by finding the fixpoint. Given a function f , a fixpoint x is such that x=f(x) . In symbolic model checking, a CTL formula is transformed by a function called predicate transformer denoted by τ:P(S)→ P(S) . We can then calculate [[φ]] for any formula φ by finding a fixpoint of some τ . For most formulas we need one of two types of fixponts, a least fixpoint or a greater fixpoint, denoted by µand υrespectively. [[∃φ]] = υZ·φ∧ ∃ e Z [[φ1∃U φ2]] = µZ·φ2∨(φ1∧ ∃ e Z) Having defined ∃e Z to be a quantified boolean formula (QBF), we can now define the semantics of CTL temporal operators as being the least or the greatest fixpoint of specific predicate transformers. These formulas can then be efficiently calculated using binary decision diagrams. Although this technique is used to calculate symbolic model checking of CTL formulas, Clarke et al. (1994) demonstrated that LTL model checking can be reduced to CTL model checking under fairness contraints. They have sucessfully translated LTL formulas into SMV models, this ways introducing LTL model checking into SMV. 2.3.2Automata-based model checking for LTL Vardi and Wolper (1986) proposed a technique to verify LTL properties by using nondeterministic Büchi automata (NBA), a structure first suggested by Büchi (1990). The key idea is to translate the entire transition system and the negation of the LTL property we want to verify into a Büchi automaton (representing the counter-examples) and then check if there is some intersection between the languages of both automata. This is the technique used by the model checkers SPIN (Holzmann (1997)) and LTSmin (Kant et al. (2015)). 2.3. Verification 10 A Büchi automata Ais a finite automata defined by A=hS,Σ,ρ,S0,Fi, where 1. S is a set of states 2.Σis an alphabet 3.ρ:S×Σ→2Sis a nondeterministic transition function 4.S0⊆Sis the set of initial states 5.F⊆Sis the set of accepting states As we stated previously, we are aiming to prove M|=φ where M is a kripke structure and φ an LTL formula. Being AM and A¬φ a Büchi automata for the model and for the LTL formula respectively, and L(A) the language of some Büchi automata. The main challenge becomes: L(AM)∩ L(A¬φ) = ∅ Since several standard techniques exist to check the emptiness of an automata, in order to verify an LTL property we just need to know how to calculate the intersection of two automata and how to translate an LTL formula into a Büchi automata. Intersection of automata A generalised NBA (GNBA) is similar to a regular NBA but, instead of having a single set of accepting states F , it has a set of sets of accepting states F . It is easy to understand how NBA can be translated into a GNBA: Everything is the same and F={F}. For two Büchi automata A1=hS1,Σ,δ1,S01,F1i and A2=hS2,Σ,δ2,S02,F2i there is some other Büchi automata Asuch that: L(A) = L(A1)∩ L(A2) This new Büchi automata A is a GNBA and can be calculated as the cross product of the two auomata, that is: A=A1⊗ A2=hS1×S2,Σ,δ,S01×S02,Fi Where δis the conjunction of both δ1and δ2, and Fis given by: F={F1×S2|F1∈ F1} ∪ {S1×F2|F2∈ F2} 2.3. Verification 11 Translating an LTL formula into a Büchi automaton First we need to present a couple of definitions on Büchi automata: Let word v of length |v| over alphabet Σ in the automaton A denote a possible sequence of transitions of A. We say that a run of A over the word v is the sequence of states possible by going through each transition of v. A run is said to be an accepting run if the sequence of states ends in some accepting state of F. Finally, we say that A accepts a word v if and only if there is an accepting run of A over v . For example, the automaton below – where q0 is the only accepting state – accepts the empty word (e), a,ba,bba,bbaa,abaa, et cetera, but not ab, for example. q0q1 a b a b A language of an automata L(A)is the set of all words accepted by the automata. All LTL formulas can be represented by a Büchi automaton, we will now look at some examples of this translation. Suppose we have an alphabet Σ={φ,ψ}. Let us start with a simple example: the LTL property φ means that φ is valid in every state, that is, there is a transition φ in every state. We can intuitively consider a language for that formula or at least some words for it. The empty word e is a word in L(Aφ) , as is, φ , φφ,φφφ, et cetera. This way, the corresponding Büchi automata for forumla φis: q0 φ For a more complex property p1=(φ⇒♦ψ)we have: e∈ L(p1) ψ∈ L(p1) ¬φ,φ,ψ∈ L(p1) . . . Therefore we have the following Büchi automaton: 2.3. Verification 12 q0q1 ¬φ∨ψ true ψ true 2.3.3Bounded model checking for LTL In bounded model checking, we aim to find paths of lenght k which break a given propositional formula. If no path of size k is found, then the search continues for paths larger than k . We can reduce this into a satisfiability formula with propositional logic and pass it to a SAT solver. Bounded model checking was introduced by Biere et al. (1999) and presented as a fast way to calculate minimal length counterexamples, and one that uses less space when compared to approaches based on binary decision diagrams as is the case with symbolic model checking. In this subsection we will study how it is possible to translate LTL formulas into propositional logic formulas that can be checked by a SAT solver. Semantics Although the aim is to get a finite k -sized prefix of a (possibly infinite) path, such prefix can still represent an infinite path if there is a back loop, that is, if the successor of the last state is another state inside the prefix. This little nuance makes huge differences when looking at the semantics for LTL. Take a look at the formula φ which states that " φ will always be true", in a non-looping finite path of size k such formula cannot be truthfully verified since φ might not hold for some state after k . When defining the semantics for bounded model checking we must be mindful of whether we are talking about looping or non-looping paths. In non-looping paths we consider that φ is always false. The semantics for φRψ also changes as we have to exclude the possibility where φ always holds and ψ is not in the bounded path. This effectively eliminates the duality between  and ♦ since we can no longer say that ¬φ≡ ¬♦φ, and between Rand Usince ¬(φUψ)6≡ (¬φ)R(¬ψ). Translation Now we will take a look at the problem of reducing an LTL formula into a CNF formula understandable by a SAT solver. We will represent the finite sequences of states s0,s1, . . . , sk composing the k-sized path that satisfy an LTL formula φin a Kripke model Mby [[M,φ]]k. 2.3. Verification 13 To define [[M,φ]]k , we must first define [[M]]k that represents all possible k -sized paths in M and then we restrict that sequence to those paths in [[φ]]k We define [[M]]k formally as follows: Let M=hS,S0,R,Libe a Kripke structure, si∈Sand s0∈S0, [[M]]k=I(s0)∧ k−1 ^ i=0 hsi,si+1i ∈ R Where Irepresents the condition for the initial state. Now to calculate [[φ]]k we must be careful to distinguish from non-looping and looping paths because of the two different semantics. We assume that φ was converted into negation normal form. Let us start by expanding [[φ]]k to [[φ]]i k where i is the current position in the k-sized prefix, and define it for non-looping paths: [[p]]i k=pi [[¬p]]i k=¬p(si) [[φ∧ψ]]i k= [[φ]]i k∧[[ψ]]i k [[φ∨ψ]]i k= [[φ]]i k∨[[ψ]]i k [[φ]]i k=∅ [[♦φ]]i k=∨k j=i[[φ]]j k [[ e φ]]i k=i f i <k then [[φ]]i+1 kelse ∅ [[φUψ]]i k=∨k j=i([[ψ]]j k∧ ∧j−1 n=i[[φ]]n k) [[φRψ]]i k=∨k j=i([[φ]]j k∧ ∧j n=i[[ψ]]n k) When dealing with looping paths , the notation [[φ]]i k is not sufficient so we expand it to l[[φ]]i k where l represents where the loop starts. Let φ and ψ be two LTL formulas, k,i,j∈N and l,i≤k,succ(si)be the successor state of sisuch that succ(i) = i+1 and succ(k) = l 3.1. Language 20 we mentioned previously; in the above specification, we use the keyword in instead. extends means that all other sets expanding the same superset are disjoint, however in is much more loose and means, in the above declaration of alive , that any Actor can be in the subset alive. Only actors that are alive can be blocked, so we keep blocked as a subset of alive. The keyword in should not be confused with the set membership operator ( ∈ ) of set theory, in fact it more appropriately represents the operator subset (⊆). Having all our actors defined, let us now move on to Poolboy itself. 1abstract sig Message {} 2 3one sig MaxOverflow in Int {} 4 5one sig Poolboy { 6var free : set Actor, -- Every free actor poolboy has 7var overflow : one Int,-- The number of overflow workers poolboy gave 8var waiting : set Client, -- Clients waiting for workers 9var mailbox : set Message, -- Mailbox where Poolboy recives messages 10 size : one Int -- The initial size of free 11 } Poolboy is defined as one signature; this is the multiplicity keyword. In this case, since Poolboy is a unary relation (i.e. just a set), it just represents its size. In Alloy and Electrum the multiplicity of a relation can be: no An empty set one A set with only one element lone A set with either one element or none some A set with one or more elements Considering that our system only has one Poolboy, the set representing it must also limit its multiplicity to one. The other relations that are defined in sig Poolboy also have diverse multiplicities. But note that when the relation’s range is defined as set it has no size restrictions. Any given Erlang actor has a mailbox . However, we have limited this to just Poolboy itself, because the client’s mailboxes will be abstracted in our model. Otherwise, we could have relation mailbox declared inside the signature Actor. Messaging system In the above code snippet we not only declared sig Poolboy but also another signature Message . There is nothing new on that declaration so we can move on to define every 3.1. Language 21 message. There are a lot of messages in this system, so it would be unwise to explain all of them in detail in the present document. We will use the definition of Checkin as an example. 1sig Checkin extends Message { 2client : Client, -- Client issuing the checkin 3actor : Actor -- Checkin actor 4} Remember that Checkin is the act of returning a worker to Poolboy, therefore the message has the reference to the client issuing the checkin and the worker that is being checked in. In the above example we define the message Checkin with two relations: client , the client issuing the checkin; and actor , the worker being returned. By default, the multiplicity of relations declared inside signatures is one. Notice that we did not explicitly force a worker to be checked in — choosing instead to have any kind of actor —, this is because some of the bugs found by Thompson were caused by the client sending an invalid worker. Now that we have the messages defined, we shall move on to specifying how these messages are sent and received. 1pred sendMessage[m : Message] { 2mnot in Poolboy.mailbox 3mailbox’ = mailbox + Poolboy→m 4} 5 6pred readMessage[m : Message] { 7min Poolboy.mailbox 8mailbox’ = mailbox - Poolboy→m 9} Apredicate is a boolean-valued function, meaning it can only be either true or false. sendMessage has one parameter, mof type message.mis actually a set of multiplicity one. The dot join ( . ) is actually a very important operator, it represents the composition of relations. It is not the same as the mathematical composition of functions, nevertheless I will borrow its symbol ( ◦ ) to define it in a formal language: Let ha1,a2,..., ani ∈ R represent a n-ary pair which belongs to the relation R, R◦S={ha1,a2, . . . , an−1,an+1, . . . , an+mi | ha1,a2, . . . , ani ∈ R∧ han,an+1, . . . , an+mi ∈ S} As you can see, to join two pairs we check if the last atom of the first pair is equal to the first atom of the second pair; if they are, then the new pair starts with the atoms of the first and ends with those from the second omitting the matched atom. When joining (or composing) two relations we join every matching pair. 3.1. Language 22 In line 2in the declaration of pred sendMessage , we compose Poolboy and mailbox . Remember that Poolboy is a unary relation with only one element and mailbox is a relation between the only atom from Poolboy and a set of messages, so by composing the two we get only the set of messages. One can read line 2quite naturally: message m is not in Poolboy’s mailbox. We already figured out that Poolboy.mailbox is the set of messages received by Poolboy, and because every thing is a set in Alloy/Electrum, m is also a set. Remember, not in represents the mathematical symbol 6⊆. The apostrophe following mailbox means: the value of mailbox in the immediately following state instance. Please remember that mailbox relates Poolboy with a set of messsages. In Alloy and Electrum, the pair ha,bi is denoted by a→b , however, since everything is a set, the → operator more accurately represents the mathematical cartesian product ( × ). So, when in Alloy we write A→Bbeing Aand Bboth sets, we are saying: A×B={ha,bi:a∈A∧b∈B} In line 3, because Poolboy and m are both sets with multiplicity one, the result of Poolboy→m is also a set of multiplicity one with a pair relating the only atom of Poolboy and m. Finally, Alloy includes the typical set operators: +The union of two sets (∪) &The intersection of two sets (∩) -The difference of two sets (\) Since mailbox is a set of pairs, by adding this new pair ( Poolboy→m ) we are, in effect, adding just a new message. With all that in mind, we can now read line 3as the next instance of mailbox is equal to the current instance with a new message. This is not imperative programming sendMessage does not actually send any message, rather it is more helpful to think of it as a predicate that is true if and only if a given message mis not currently in Poolboy.mailbox but will be in the next state. Events Now, if we try to run our system nothing meaningful will happen, the initial state will be generated at random and the variable sets will change chaotically. This is because we have just yet specified what objects our system has, now we have to define how they will behave. Firstly we begin by defining the initial state: 1fact init { 2Poolboy.overflow = 0 3gte[MaxOverflow, 0] 4Poolboy.free = alive & Worker 3.1. Language 23 5Poolboy.size = #Poolboy.free 6no waiting 7no workers 8no blocked 9no mailbox 10 } A fact limits all possible generated traces to only those that satisfy a given formula. If the formula does not contain any temporal operator — as is the case above —, then it only applies to the initial state. This is a pretty straight forward declaration, the only two new elements from the above listing are: gte which is a predicate that asserts MaxOverfow to be greater than or equal to 0 ; and #Poolboy.free read as the cardinality of the set Poolboy.free, that is the number of elements in the set Poolboy.free. Having our initial state specified, we can now focus on defining what can happen in the system. Because there are a lot of actions that can happen, we will just show one as an example. 1pred clientSendCheckin[cli : Client, act : Actor] { 2cli in (Client & alive) - blocked 3act in cli.workers 4 5some msg : Checkin { 6msg.client = cli 7msg.actor = act 8sendMessage[msg] 9} 10 workers’ = workers - cli→act 11 12 alive’ = alive 13 blocked’ = blocked 14 free’ = free 15 overflow’ = overflow 16 waiting’ = waiting 17 } The predicate above is divided in three parts: firstly we restrict the given parameters, then we specify what should change and finally we specify what should not change, this last part is called the frame condition. We begin by specifying which Clients and Actors can be the parameters of this action, in this case we say that cli can only be an alive client which is not blocked, and act is one of cli ’s workers. Then we move to specify what changes, in this case a Checkin message should be sent and act should be removed from cli ’s workers. Here, at line 5, the keyword 3.1. Language 24 some represents an existential quantification over msg , in first-order logic using standard mathematical notation this line would translate to, ∃msg ∈Checkin : . . . Universal quantification ( ∀ ) is also possible by using the keyword all . Lastly, we define the frame conditions, i.e. what doesn’t change in this action, by going through every variable relation and force it to stay static. Again, this is not imperative programming. clientSendCheckin does not make any changes in the system per se, more like the other way around, clientSendCheckin is only true, if and only if the conjunction of all those predicates that compose it is true. Having specified every other action, we now have to limit the traces to only those that represent meaningful actions by defining a new fact. 1fact traces { 2always ( 3some c : Client | ClientSendCheckout[c] or 4some c : Client, w : Worker | ClientSendCheckin[c, w] or 5some c : Client | ClientSendTimeout[c] or 6PbCheckoutReady or 7PbCheckoutFull or 8. . . 9) 10 } The above code snippet is actually quite interesting, it is the first time we encounter a linear temporal logic operator: always which is often denoted by  . If we did not include the always operator, we would only be limiting the first state and allow our model to behave chaotically after that. The above predicate traces is of shape A , where A is the disjunction of every possible action. This restricts the trace to behave in a specific ways. We have just described how the system will behave by defining a few predicates, let us call this the predicate idiom to specify events. However Electrum is quite versatile and this is but one possible way of defining the system evolution. This approach has its problems: to begin with it is difficult to examine the counter-example traces, since we only see the side-effects and have to extrapolate what event has happened between two consecutive states — which can be nearly impossible if two concurrent events happen at the same time. We must model our system in such a way that it is clear what is happening. As such, we introduce a new signature that represents the current event (or events) that is (resp. are) taking place. Let us call it signature idiom to specify events. 1one var abstract sig Event {} 3.1. Language 25 We define the abstract signature Event so that every event that can happen in the system extends it. We made Event a one arity set so that only one event takes place at a time, where it to be a no arity set, the system would be static and no event possible. To better understand this new approach, we will encode the event clientSendCheckin using asignature: 1var sig ClientSendCheckin extends Event { 2var cli : Client, 3var act : Actor 4} Right now, signature ClientSendCheckin shows the actors involved in the event — in this case a client and an actor — but does not define what the event does, to specify that we add the following fact: 1fact { 2all event : ClientSendCheckin { 3event.cli in (Client & alive) - blocked 4event.act in event.cli.workers 5 6some msg : Checkin { 7msg.c = event.cli 8msg.a = event.act 9sendMessage[msg] 10 } 11 workers’ = workers - event.cli→event.act 12 } 13 } Facts that apply to all atoms of a single signature are best written as signature facts, so that referencing the signature is implicit. We expand our declaration of signature ClientSendCheckin to include signature facts. 1var sig ClientSendCheckin extends Event { 2var cli : Client, 3var act : Actor 4} { 5cli in (Client & alive) - blocked 6act in cli.workers 7 8some msg : Checkin { 9msg.c = cli 10 msg.a = act 11 sendMessage[msg] 12 } 13 workers’ = workers - cli→act 3.1. Language 26 14 } Notice how we now have no need to write event.cli since cli implicitly refers to the relation defined in the signature. We have no need to explicitly state the frame condition, this is due to the way we will specify what traces are possible. With the predicate idiom we would write the fact trace and explicitly state what actions can occur, in this approach we look for what variables change and imply that some event took place. For example: the only events that change overflow are PbCheckoutReady , PbCheckinOverflow and PbExitOverflow , therefore if overflow changed, one of these events must have taken place. In Electrum we write it the following way: 1fact updated { 2always ( 3(blocked’ != blocked 4implies some ClientSendCheckout + ClientSendTimeout + ActorExit + 5PbCheckoutReady + PbCheckoutOverflow + PbCheckinWaiting + PbExitWaiting) and 6 7(workers’ != workers 8implies some ClientSendCheckin + ActorExit + PbCheckoutReady + 9PbCheckoutOverflow + PbCheckinWaiting + PbExitWaiting) and 10 11 (alive’ != alive 12 implies some ActorExit + PbCheckoutOverflow + PbCheckinOverflow + 13 PbExitWaiting + PbExitReady) and 14 15 (free’ != free 16 implies some PbCheckoutReady + PbCheckinReady + 17 PbExitOverflow + PbExitReady) and 18 19 (overflow’ != overflow 20 implies some PbCheckoutOverflow + PbCheckinOverflow + PbExitOverflow) and 21 22 (waiting’ != waiting 23 implies some PbCheckoutFull + PbTimeout + PbCheckinWaiting + PbExitWaiting) and 24 25 (mailbox’ != mailbox 26 implies some ClientSendCheckout + ClientSendCheckin + ClientSendTimeout + 27 ActorExit + PbCheckoutReady + PbCheckoutOverflow + PbCheckoutFull + 28 PbTimeout + PbCheckinWaiting + PbCheckinOverflow + PbCheckinReady + 29 PbExitWaiting + PbExitOverflow + PbExitReady) 30 ) 31 } 3.1. Language 27 3.1.3Specifying the system We have just went through the process of modeling the system. Now we will go through each of the requirements we identified in subsection 3.1.1and specify properties in Electrum for each of them. Formalization Let us recap the requirements we identified previously: 1. There should never be more workers that those allowed by the configuration file. 2. If a client receives a worker, it must be blocked. 3. If a client sends a checkout request when there are available workers, provided it doesn’t timeout, it will receive a worker. We now have to translate this properties from English to temporal relational logic, the specification logic of Electrum. 1. There should never be more workers that those allowed by the configuration file. This is a typical safety property where we are expecting something bad to never happen, in this case we expect that there should never be more workers than those allowed. The configuration file has the number of workers ( size ) and the maximum overflow ( maxOver f low ) — i.e. how many more workers can Poolboy give —, so the total number of workers allowed by the configuration file is size +maxOver f low . Let us assume that #totalWorkers represents the total number of workers in the system; then in LTL the property is, (#totalWorkers ≤size +maxOver f low) And reads always the total number of workers is less or equal to the initial size plus the maximum overflow. The next requirement is a bit more complex, 2. If a client receives a worker, it must be blocked. This is a safety property, because we are expecting that the proposition remains true through the execution of the system. Let Rw(c) be true if and only if client c receives a worker and B(c)is true if and only if client cis blocked. (∀c∈Client :Rw(c) =⇒B(c)) As you can see it becomes quite simple. We now must translate all these specifications from pure LTL to Electrum. 3.1. Language 28 3. If a client sends a checkout request when there are available workers, provided it doesn’t timeout, it will receive a worker. This is a liveness property because we are expecting something good to eventually happen; in this case, the client will eventually get a worker. However, the client has to first send a checkout request and there must be available workers and the client must not timeout. TLA+ actually has a nice symbol to represent these types of properties, they call it leads to ( ), but it is only "syntactic sugar" and does not add anything new to LTL because A B is defined as (A⇒♦B) (Lamport (2003)). With that said, we will use the purely LTL syntax; any discerning reader will notice the similarities: ∀c∈Client :(Co(c)∧over f low <maxOver f low ∧ ¬T(c) =⇒♦Rw(c)) Where Co(c) is true if and only if client c sends a checkout message, T(c) is true if and only if client ctimes out, and Rw(c)is true if and only if client creceived a worker. Property specification We will now go through each of the requirements we formalize and translate them in Electrum. The first one is quite simple: (#totalWorkers ≤size +maxOver f low) Before we start specifying the property, we need to get the total workers in the system, for that we will use a function ( fun ). A function is basically a way of reusing the same expression. Every function must specify what it returns and can have multiple arguments. 1fun total_workers : set Worker { 2Poolboy.free + Client.workers 3} In the above example, our function has no arguments and returns a set of Worker with all the workers being used in the system. When we say all workers in the system we mean those workers that are available in Poolboy and those that are being used by some Client , so the total set is the union of these two. Now we can move on to specify the property in Electrum. We will be using an assertion assert which is a predicate that we can later check. 1assert maximum_workers { 2always lte[#total_workers, add[Poolboy.size, MaxOverflow]] 3} We have already introduce the keyword always as being the Electrum keyword for  , so let us move to the next specification: 3.2. Analyzing the model 29 (∀c∈Client :Rw(c) =⇒B(c)) Let us first define what receive worker ( Rw ) actually means: we know that a client has received a worker if the cardinality of its set of workers has increased by one, so that is exactly what we specify in Electrum: 1pred receive_worker[c : Client] { 2#c.workers’ = add[#c.workers, 1] 3} A client cis only blocked if and only if cin blocked: 1assert timeout_is_safe { 2always ( 3all c1 : Client { 4receive_worker[c1] implies c1 in blocked 5} 6) 7} ∀c∈Client :(Co(c)∧over f low <maxOver f low ∧ ¬T(c) =⇒♦Rw(c)) Now the last one is also pretty straightforward, we can use the definition of receive_worker we used previously. The full property is as follows: 1assert client_gets_worker { 2always ( 3all c1 : Client { 4(c1 in (ClientSendCheckout.cli - Timeout.c) 5and lt[Poolboy.overflow, MaxOverflow]) 6implies (eventually receive_worker[c1]) 7} 8} Line 4of the above listing may be a bit confusing so let us break it down. What we are saying is client c1 is the client who sent the checkout (take a look at the definition of ClientSendCheckout in Appendix A) but does not have any Timeout messages. 3.2 analyzing the model In the last section, we have defined three main properties that are to be verified in Electrum. However, we have not shown how to actually analyze them. In this section we will examine how one can analyze a model in Electrum. 4.1. PINS architecture 36 2. NextState Returns the successor(s) state(s) 3. StateLabel The labelling function In LTSmin, a state is represented by a state vector with N slots. Actions are grouped into transition groups, typically grouping instantiations of the same action with different parameters, which must also be specified; as well as the names and types for each slot in the state vector, transition group and label. All of these are required for any sort of model checking. But — either for more complex analysis like timed systems or probabilistic models, or to enable high performance algorithms — more information must be provided. In their paper Kant et al. (2015) divide this extra information in a few levels of extensions ( A1 to A∞ ) according to their usage. We will only take a look at levels A1 and A2 , as the usage of A3 is beyond the scope of this thesis. Table 1sums up all the extra information as well as the usage for each layer. The first level we explore is A1, the read and write dependency level. Information about these dependencies allow for projections over the state vector, improving performance for both caching, state compression, and symbolic tools; it is also needed to calculate partial order reduction. An action is said to be read independent from a slot in the state vector if the action is possible for any value of the slot and the resulting state is the same. Intuitively, an action is said to be write independent from a slot in the state vector if the slot is not changed by the action. The second level down is A2 , necessary to calculate partial order reduction. It adds more dependency information on transition guards, labels, and actions. Transition guards are a subset of all labels; for each transition group, we associate a set of guards — the preconditions for the group to be enabled — which are evaluated conjunctively, that is, all guards must be enabled for the group to be as well. A label is independent from a slot in the state vector if changing the slot value does not change the valuation of the labelling function. As we noted in 2.4, the notion of independence between actions is crucial to partial order reduction. This independence is called accordance in the terminology used in LTSmin, and a Level Used for Function Description B0 Basic model checking InitialState Returns the initial state B0 NextState Returns the next state B0 StateLabel Labelling function A1 Optimizations and partial order reduction ReadMatrix Read dependency matrix A1 WriteMatrix Write dependency matrix A2 Partial order reduction GuardMatrix Guard/transition group matrix A2 StateLabelM State label dependency matrix A2 DoNotAccord Actions dependency matrix A∞Other usages GetMatrix Predefined X×Ymatrix Table 1: Overview table of the extensions 4.2. Specifying in PINS 37 dependency relation is passed to PINS by a DoNotAccord matrix. We will have a detailed definition of this relation in section 4.3; for now the definition for independence of actions, described before, should suffice. PINS also allows for other generic matrices to be added and used by GetMatrix. This can be used to improve precision of partial order reduction, although we will ignore it in our development. This is all the information necessary to calculate partial order reduction. In the next section we will describe a leader election algorithm and we will take a look at how to specify it in PINS with C code via the dlopen interface. 4.2 specifying in pins Before we try to understand how to translate a language front-end into PINS, we must first figure out how to model a system. Since we also want to test the partial order reduction optimizations of LTSmin, it is best to choose an example with a lot of asynchronous message passing where many actions are independent of one another, in such a way that would maximize the number of interleavings. One such system is the ring leader election which we will describe in the following subsection. 4.2.1Showcase Ring leader election example In order to test the performance of partial order reduction of LTSmin, we chose to model a system with multiple independent actions that would, without any reduction, generate a myriad of identical traces. For that reason, we have found that a ring election would be the ideal system to model. We chose to specify a ring election where all processes are arranged in a ring and each sends messages to one neighbour (say, to the right) and receives message from the other neighbour (from the left). The full algorithm is described in Algorithm 1. In our model we will have a fixed number of processes. Each process has an inbox in which it receives messages from other processes; the maximum value they know of; the notion of whether it knows the leader or not; and its current stage – or state –, which tells us if the process is either sending a message or waiting to receive one. We will now define the initial state and every action that can occur in this system. Initial state In the initial state, each inbox is empty, the maximum id known by each process is its own id, no process knows the leader and every process is ready to send. 4.2. Specifying in PINS 38 Algorithm 1Ring election algorithm for a generic process i 1:procedure Elect 2:id ←getId() 3:max ←id 4:knowLeader ←f alse 5:sendi+1(id) 6:while receivei(mid)do 7:if mid >max then 8:max ←mid 9:sendi+1(max) 10:else if mid =max ∧ ¬knowLeader then 11:knowLeader ←true 12:sendi+1(max) Sending When the process is ready to send, it sends the maximum value it knows of to its neighbour and waits until it has received a new value. Receiving The id received by the process can be either smaller than, greater than, or equal to, its maximum id. If a process receives an id that is smaller than its maximum, it just discards the message and awaits a new message. If the received id is greater than the maximum, then the maximum is replaced and propagated. Finally, if the received id is the same as the maximum, that means that we have found our leader a we must propagate the news to our neighbour. 4.2.2Modelling ring leader election in C Dynamic loading (DL) allows for libraries to be loaded during a program execution. It is, therefore, a very useful technique for implementing extensions to other programs. In UNIX systems, the dlopen API is able to open libraries and prepare them for later use. 1 LTSmin takes advantage of this feature in order to support other language front-ends for PINS; although we can, just as easily, take advantage of this feature to specify any model. For the case of this example, we will use the model we just established, and are now going to specify it in C. First we will take a look at the file structure. Later we will be adding the information that we have previously described in section 4.1. 1http://tldp.org/HOWTO/Program-Library-HOWTO/dl-libraries.html 4.2. Specifying in PINS 39 File structure As it is to be expected, we can have as much files as we want; however, to try to keep it simple, we will have just the dlopen implementation in C, as well as a C file where functions such as InitialState and NextState are declared. We will refer to the dlopen implementation C file as simply the dlopen implementation file ( dlopen-impl.c ), and to the C file and his header as the specification file ( spec.c ) and header file ( spec.h ). Depending on what we are modelling, further files can be added as we will later see. Defining the state, actions and types As we noted earlier, in PINS the state is represented by a state vector with a fix size of slots. Therefore, in defining the state, we must also specify what each slot represents in our model. Before we define the state, we must define the existing types of our model. The lts-type.h file in the ltsmin library declares a couple of types that can be used. In this example, we need an int type, an action type for each transition, and a bool type for each label and for the know_leader . We must also declare the size of our state vector, for that we declare a function in the specification file state_length. 1lts_type_t ltstype=lts_type_create(); 2 3// set the length of the state 4lts_type_set_state_length(ltstype, state_length()); 5 6// add an "int" type for a state slot 7int int_type = lts_type_put_type(ltstype, "int", LTStypeSInt32 , NULL); 8 9// add an "action" type for edge labels 10 int action_type = lts_type_put_type(ltstype, "action", LTStypeEnum, NULL); 11 12 // add a "bool" type for state labels 13 int bool_type = lts_type_put_type (ltstype, "bool", LTStypeBool, NULL); First, because we intend to create a parameterized model, we will declare in our header file a fixed number of processes, in this case 4. 1#define N 4 Although the primary elements in our model are the processes, we must shun from having a slot with all the information regarding a single process, as that would concentrate too much information on a single slot and it would not allow us to make use of valuable high-performance algorithms as partial order reduction. Instead, we will have a slot for each component — i.e., the inbox, the maximum value, the state, and the knowledge of a leader — of each process. We will assume that all process ids are sequential and that they are in the interval [1, N] , in that way we can later use the 0 to represent nothing (akin to the null value 4.2. Specifying in PINS 40 of programming languages). The inbox will allow processes to send and receive messages from other processes. For now, because LTSmin does not have a "set type" we will have to introduce it later. We will define function macros in our header file so we can refer to the slot in the state vector later. 1#define NR_VARS 4 2 3#define INBOX(proc) ((proc - 1) *NR_VARS) 4#define MAX(proc) ((proc - 1) *NR_VARS + 1) 5#define KNOW_LEADER(proc) ((proc - 1) *NR_VARS + 2) 6#define STATE(proc) ((proc - 1) *NR_VARS + 3) In the dlopen implementation file we are required to set a name for each slot and its type. 1for (int i=1; i <= N; i++) { 2sprintf(name, "inbox_%d", i); 3lts_type_set_state_name(ltstype, INBOX(i), name); 4lts_type_set_state_typeno(ltstype, INBOX(i), int_type); 5 6(...) 7} Similarly, state label types and action types must also be specified. The full specification can be found on appendix B. The action type must also be populated with the different possible action names: 1for (int i = 1; i <= N; i++) { 2sprintf(name, "send_%d", i); 3pins_chunk_put(m, action_type, chunk_str(name)); 4 5(...) 6} Finally, we validate the type and set it. 1lts_type_validate(ltstype); 2GBsetLTStype(m, ltstype); Initial state, next state and state label In the initial state every inbox is set to 0 , Since we have not yet declared the "set type" for now we will ignore the initial value of inbox, we will add it when introducing the set type. The maximum value is set to the process id. We declare the initial state function in the specification file. 4.2. Specifying in PINS 41 1int initial[NR_VARS *N]; 2int*initial_state(void*model) { 3for(int i = 1; i <= N ; i ++) { 4initial[MAX(i)] = i; 5initial[KNOW_LEADER(i)] = 0; 6initial[STATE(i)] = STATE_SEND; 7} 8 9return initial; 10 } Finally, we set it as the initial state in the dlopen implementation file. 1int*initial = initial_state(m); 2GBsetInitialState(m, initial); Before we define the next state function, we must first define the various actions that can occur. We divide each action in two functions: the preconditions (called labels) and the postconditions (used in order to calculate the next state). The next state function, declared in the specification file, takes an action group, the state, and a callback function and its arguments. For each possible action we call a function that must calculate the next state. 1int next_state(void*model, int group, int*src, TransitionCB callback, void*args); In addition to the action label functions, we need to define a goal function that represents the property we want to verify. In this case, our goal is that every process knows the leader, therefore the label goal function is as follows: 1int label_goal(int*src) { 2int i; 3for(i = 1; i <= N && src[KNOW_LEADER(i)]; i++); 4return i > N; 5} Finally, we define the state label function that, for a given label and a state, returns whether the label is valid in that state. It simply uses the previously defined label functions. For simplicity we assume that each action has only a single guard, in that way the event reference (the integer that references the event) is the same for its label. With this in mind, we declare the state label function in our specification file. 1int state_label(void*model, int label, int*src); And set it in the dlopen implementation file 1GBsetStateLabelLong(m, (get_label_method_t) state_label); 4.2. Specifying in PINS 42 Introducing sets LTSmin has no default set type, nonetheless it does allow for a generic chunk type to be used. We declare the set type in the dlopen implementation file. 1int set_type = lts_type_put_type(ltstype, "set", LTStypeChunk, NULL); The chunk type can be any serializable type; we used an external set library and defined auxiliary getters and setters for the state vector in our specification file. 1SSET get_sset(void*model, int*src, int idx); 2int set_sset(void*model, int idx, SSET set); Now we can use the above functions whenever we want to take (or put) sets in the state vector. For instance, the initial value for inbox is now: 1initial[INBOX(i)] = set_sset(model, INBOX(i), sset_init()); Dependency matrices In our specification file, we define the dependency matrices as we described in the previous section 4.1; in the case below, we relate each action with the slots in the state vector read by it. 1/*Read Matrix 2*inbox max know state 3*SEND 0 1 0 1 4*RECV_SMALL 1 1 0 1 5*RECV_EQ 1 1 0 1 6*RECV_GRT 1 1 0 1 7*/ 8int rm[NR_ACTIONS *N][NR_VARS *N]={0}; 9void set_read_matrix() { 10 for(int p = 1; p <= N; p++) { 11 rm[SEND(p)][MAX(p)] = 1; 12 rm[SEND(p)][STATE(p)] = 1; 13 14 rm[RECV_SMALL(p)][INBOX(p)] = 1; 15 rm[RECV_SMALL(p)][MAX(p)] = 1; 16 rm[RECV_SMALL(p)][STATE(p)] = 1; 17 18 rm[RECV_EQ(p)][INBOX(p)] = 1; 19 rm[RECV_EQ(p)][MAX(p)] = 1; 20 rm[RECV_EQ(p)][STATE(p)] = 1; 21 22 rm[RECV_GRT(p)][INBOX(p)] = 1; 23 rm[RECV_GRT(p)][MAX(p)] = 1; 24 rm[RECV_GRT(p)][STATE(p)] = 1; 4.2. Specifying in PINS 43 25 } 26 } 27 28 int*read_matrix(int row) { 29 return rm[row]; 30 } Afterwards, we set them in the dlopen implementation file by copying and setting them. PINS includes some functions to interact with dependency matrices (dm). First, a dependency matrix must be created with dm_create . Then its values are set [to true] by the dm_set function. Besides the write and read matrices, a combined matrix is also defined which, intuitively, combines the values of both matrices. 1set_read_matrix(); 2matrix_t*rm = malloc(sizeof(matrix_t)); 3dm_create(rm, group_count(), state_length()); 4for (int i = 0; i < group_count(); i++) { 5int*aux = read_matrix(i); 6for (int j = 0; j < state_length(); j++) { 7if (aux[j]) { 8dm_set(cm, i, j); 9dm_set(rm, i, j); 10 } 11 } 12 } 13 GBsetDMInfoRead(m, rm); This process is similar for other matrices, except for GuardMatrix which is a bit different. Guard matrix relates each transition group with the guards used by it. As we said before, for simplicity we say that each transition group has only one guard which is referenced by the same integer as the action. Therefore, the C code declared in the dlopen implementation is pretty straightforward: For each group there is only one guard with the same reference as the group. 1guard_t** guards = malloc(group_count() *sizeof(guard_t*)); 2for(int i = 0; i < group_count(); i++) { 3guards[i] = malloc(sizeof(guard_t) + sizeof(int)); 4guards[i]->count = 1; 5guards[i]->guard[0] = i; 6} 7GBsetGuardsInfo(m, guards); Having completed the model, we are now ready to analyze it. We will see how in the next subsection. 4.3. Guard-based partial order reduction 44 4.2.3Analysing with LTSmin We now have three C files (plus the additional set library files), we compile them to object files as: 1gcc -c -I/usr/local/include/ltsmin -I. -std=c99 -fPIC spec.c 2gcc -c -I/usr/local/include/ltsmin -I. -std=c99 -fPIC dlopen-impl.c And generate a shared object. 3gcc -shared -o spec.so dlopen-impl.o spec.o We can now pass this shared object to PINS as well as any property we want to check and a file where the counter-example trace will be written. In this case, we want to check that eventually every process will get to know the leader forever. Since we defined goal to be the label that is true if every process knows the leader, we can simply call: 1pins2lts-seq spec.so --ltl="<> goal" --trace=solution.gcf It is also possible to check for invariants. For example, if we want to check that the goal is never achieved, we can call 1pins2lts-seq espec.so --invariant="! goal" --trace=solution.gcf Because we know that goal is eventually possible, the invariant is violated and a counterexample is printed to solution.gcf. We can pretty-print solution.gcf by running: 1ltsmin-printtrace solution.gcf It is also possible to use partial order reduction by adding the flag por , although we do not yet have the do not accord matrices set up so no reduction must be possible. We will define the do not accord matrix after explaining the partial order reduction algorithm in subsection 4.3.3. 1pins2lts-seq espec.so --invariant="! goal" --trace=solution.gcf --por LTSmin implements a quite unique partial order reduction algorithm which abstracts away the notion of processes. We will explore this algorithm in the following section. 4.3 guard-based partial order reduction Most partial order reduction algorithms are based on the notion of processes. Some techniques construct program graphs, others rely on internal ordering of the actions of processes. In pursuing a truly language independent model checker, Laarman et al. (2016) developed a partial order reduction algorithm – based on stubborn sets – that is process agnostic. Instead of depending on program counters, their algorithm uses a guard-based approach. Throughout this section we will describe this guard-based partial order reduction. 4.3. Guard-based partial order reduction 45 4.3.1A stubborn approach The main idea of partial order reduction is to calculate only a representative subset of the enabled transitions to explore in a state, thus not generating the whole state graph. This guard-based algorithm is centred on stubborn sets introduced by Valmari. To understand what stubborn sets are, we first need to define a couple of concepts. As we hinted at in section 2.4, all partial order reduction techniques crucially rely on independence between actions. In guard-based POR, this concept is called accordance; We define accordance as: Definition 1. (Accordance) Two transitions t and t0 are said to accord if one of the following criteria is true: 1. Their shared variables are disjoint from the write sets; 2.tand t0are never co-enabled; 3.tand t0do not disable each other and their actions commute. With this, a do not accord set ( DN A ) is defined as the set of transitions pairs that do not accord. We also use DN Atto represent the set of transitions that do not accord with t. In guard-based partial order reduction, the necessary enabling and disabling sets are also a key concept. Definition 2.(Necessary enabling/disabling set) 1. The set Nt is said to be a necessary enabling set for transition t if and only if for t to be enabled, at least one transition in Ntmust first occur. 2. Conversely, the set Nt is said to be a necessary disabling set for transition t if and only if, for tto be disabled at least one transition in Ntmust first occur. A stubborn set is thus defined as: Definition 3.(Stubborn set) A set Tsis said to be stubborn in state sif, for all t∈ Ts: 1. If there is some enabled transition in s, then Tsmust be non-empty; 2. If tis disabled in state s, then there is a transition in Tscapable of enabling it; 3. If tis enabled in s, then all other transitions that do not accord with tare also in Ts. Now the partial order algorithm is pretty much any algorithm capable of generating a subset of transitions in a state that matches Definition 3. Algorithm 2shows us exactly that, by guaranteeing that each new transition added to the set satisfies the conditions above. In Algorithm 2,en(s)is the set of all enabled transitions in state s, and f ind_nes(t,s)is a function that returns a set with all the necessary enabling sets Nt (there can be many sets for the same transition). We will later see how to calculate the necessary enabling set, for now, let us showcase how the algorithm works. 5.1. The language 52 Taino does not yet support the keyword some , therefore the receiving events must be parameterized with the received message, and the pre-condition must check whether such message is actually part of the node’s inbox or not. We can see this in action in the definition of receiveEqual. 1event receiveEqual[n : Node, m : Int] { 2n.state = Receive 3min n.inbox 4n.max = m 5 6elected’ = elected + m 7n.inbox’ = n.inbox - m 8n.state’ = Send 9} Besides the event declaration, we also introduce a new declaration that is not available in regular Electrum. This is the init declaration where the initial state of the system is specified. This keyword is also introduced to simplify the transition to PINS. Because of some restrictions of LTSmin, it is not possible to define multiple initial states and the definition of init must be deterministic. Although in theory this restriction could be overcome by adding a non-deterministic transition from a blank state to all possible initial states. In Taino, the initial state is declared as follows: 1init { 2no elected 3 4Node$1.max = 1 5Node$1.succ = Node$2 6no Node$1.inbox 7Node$1.state = Send 8 9(. . .) 10 }for 4 Node, 4 Int Node\$1 refers to an atom of the signature Node, it simply refers to the first node. If there are multiple definitions for the same relation Taino will stick to the last defined, except if the relation is constant in which case the first definition is the one that remains. This has to do with the way the init is translated to LTSmin which will be revealed in the next section. Please note that the semantics of the scope definition is slightly different to that of Electrum; in Taino we are stating that there are exactly four nodes and four ints in this model. Finally, we will write predicates to check our goal. In this case, we want to check that eventually forever one (and only one) Node will be elected. We do this by defining a predicate and then checking it. As we already mentioned, most model checkers have a different language for describing the system and for specifying properties over the system. 5.2. Translating to LTSmin 53 Although both Alloy and Electrum are exceptions to this rule, LTSmin is not; which makes it impossible to use LTL operators inside predicates, events, facts, or functions. We allow for LTL properties to be declared inside the check and, contrary to Electrum, Taino only allows for one check to be declared. A check must always reference the predicate to be tested and can also have temporal operators. 1pred only_one_elected { 2one elected 3} 4 5check { 6eventually always only_one_elected 7} The full specification can be found at Appendix C, and it shall be quite simple to anyone familiarized with the syntax of Electrum or Alloy. Now, in the following section, we show how this model is translated into LTSmin. 5.2 translating to ltsmin Translating a highly abstract modelling language to LTSmin requires us to reason about very minute details and confront the hard differences between these two tools. During this section we will be describing how we can store the Taino notion of the state in the state vector of LTSmin and introduce a mode of indexation. We later use these concepts to initialise the state and to define a next state function. Finally we will show how we can retrieve dependency information purely from a static analysis of the modelling language. 5.2.1Defining the state The most important element we must reason about is the state; which, due to being arguably the least flexible element of PINS, requires a lot of attention. Recall that for PINS the state is a fixed size vector of values. We must find a way such that we can transpose the Taino/Electrum notion of state to this fixed sized vector. The relations and signatures which are not variable need not be considered as they can be expressed as C macros, enumerators, or functions. For instance, because static signatures do not change over time, they are not represented in the state, but are rather represented by an enum. Variable sets can be described by equating each set with a slot in the state vector; in the ring leader election, for instance, the elected set can be represented by just a slot in the vector. We are still left with the problem of defining the state for variable relations. At first it is tempting to equate each relation to each slot on the state 5.2. Translating to LTSmin 54 vector. For instance, we would have a slot for max that would be a set of relations, something like, following the notation presented when we introduced Electrum, max ={hNode1, 1i,hNode2, 2i, . . . , hNoden,ni} This seems like a reasonable suggestion, but it would mean that every action on max , even if taken by different nodes, would change the same slot in the state vector. Take event receiveGreater1 for instance. We understand that events receiveGreater of two different nodes are completely independent as they only access the part of the relation belonging to each respective node. However, when the complete relation max is in a single slot, this means that any event changing it is conflicting with any other event also accessing it. Thus, if we have a slot of the state vector dedicated to each relation, we could not take advantage of partial order reduction, as pretty much no event would accord with each other. A finer partition must be established to ensure that partial order reduction can still be applied. Take a look at the definition of max again. Even though the relation is marked as variable, the only part of it which really changes is the right-hand part. We can therefore omit the left-hand element of the relation and store the value of max for each Node in different state slots. We apply this rationale to every relation declared in the model, thus we have a state akin to the one depicted in Figure 7. We make it easier to refer to a specific slot in the state vector, by combining C macros with enumerators. This makes the translation from one language to the other much smoother. In the following example, we are defining all state slots in an enum for a scope of two nodes to make the example smaller. 1typedef enum state_names { 2NODE1_MAX, 3NODE1_INBOX, 4NODE1_STATE, 5NODE2_MAX, 6NODE2_INBOX, 7NODE2_STATE, 8ELECTED, 9STATE_LENGTH 10 } STATE_VAR; 11 12 #define size_of_Node 3 13 14 #define Node(i) (NODE1_MAX + ((i-1) *size_of_Node)) 15 #define max(i) (Node(i) + 0) 16 #define inbox(i) (Node(i) + 1) 17 #define state(i) (Node(i) + 2) 18 #define elected ELECTED 1see Appendix C. 5.2. Translating to LTSmin 55 Node$1.max Node$1.inbox Node$1.state Node$2.max Node$2.inbox Node$2.state elected Figure 7: Representation of the state vector The resulting configuration of the state reveals the restriction to the Taino join operator ( . ) which is used to refer to specific slots in the state vector and does not have the full expressiveness of the set operator of Electrum and Alloy. This, at least in this implementation, severely restricts the expressiveness of an Taino when compared to Electrum. 5.2.2Initial state Having understood the definition of the state in LTSmin, figuring out how to set it initially is not much more complex. Take a look at the definition of init in our model (Appendix C). First, the elected set is declared to be empty, this simply means that we have to initialise its slot with an empty set. As for simple attributions as is the case of max , the value on the analogous slot of the state vector is set to that in the model. Although the definition of the initial state is pretty straightforward, not everything declared inside the body of init belongs to the state vector. You may also have noticed that constants are also defined as well as the scopes for each signature. As for scopes, we can just use enumerators to refer to specific atoms, in such a way that Node$1 would translate to NODE1, hence a scope for four nodes translates to: 1typedef enum Node{ 2NODE1 = 1, 3NODE2, 4NODE3, 5NODE4 6} NODE_T; In the case of constant relations, as in succ , a function is defined that receives the left-hand side of the "join operator" ( . ) and returns the corresponding value. Taino does not allow for constant relations of different multiplicities. The succ constant relation can thus end up looking something like: 1int succ(int i){ 2switch(i) { 3case NODE1: 4return NODE2; 5.2. Translating to LTSmin 56 5case NODE2: 6return NODE3; 7case NODE3: 8return NODE4; 9case NODE4: 10 return NODE1; 11 } 12 return 0; 13 } In this way, we can later refer to the slot for the inbox of the successor of Node$1 ( Node$1.succ.inbox ) as inbox(succ(NODE1)) . The restrictions of this "join operator" may now be clearer, as it is purely used to index the state vector and not as a join of two sets. 5.2.3Defining Next state The indexation by enumerators and C macros described in the previous subsections are now very useful to translate events into actual LTSmin. But we also need to enumerate all transitions possible, for that we will through each event and parameterize it to create an enum. 1typedef enum trans_labels { 2RECEIVEEQUAL_NODE1_INT1, 3RECEIVEEQUAL_NODE1_INT2, 4(...) 5RECEIVEEQUAL_NODE4_INT1, 6RECEIVEEQUAL_NODE4_INT2, 7(...) 8SEND_NODE4, 9LABEL_GOAL 10 } TRANSITIONS; You can see that the number of transitions grows exponential to the number of parameters for each event. In Taino the pre-conditions and post-conditions of each event are described together, LTSmin however isolates transitions from its guards. Therefore, each event translates to two functions: one for the label and another for the transition itself. In Taino, we assume that each transition only has one guard which is the conjunction of all pre-conditions. For a specific example, let us look at event receiveGreater . It generates the following label function: 1int label_receive_greater(void*model, int*src, int n, int m){ 2// n.state = Receive 3int p1 = src[state(n)] == RECEIVE_T; 4 5.2. Translating to LTSmin 57 5// m in n.inbox 6SET n_inbox_set = get_set(model, src, inbox(n)); 7int p2 = set_exists(n_inbox_set, m); 8set_free(n_inbox_set); 9 10 // gt[m, n.max] 11 int p3 = gt(m, src[max(n)]); 12 13 return p1 && p2 && p3; 14 } The comments are added here to better show what relates to the Taino specification. Note that functions like get_set allocate the set in memory and set_free ensures that the memory is safely freed as soon as it is no longer needed; this is the reason for declaring a temporary n_inbox_set. The label function uses the snake case version of the event name given in the model with a label_ prefix, this is the standard for all label functions of events. Apart from the reference to the model and to the state vector ( src ), the label function also receives the arguments of the event, in this case the node nand message mwhich are represented by integers. The function that calculates the next state for this event is not much more complex, in fact it takes advantage of the label function to confirm that the event is going to happen. The mindset behind the translation of the post-conditions is that it simply changes the state vector with new values. This is why the syntax for events in Taino is so restrictive, it expects to assign new values to slots in the state vector. Besides the arguments that are received by the label function, this function also receives the destination state vector – i.e., the state vector of the following state – and a copy vector ( cpy ) which tells PINS which slots in the state vector have not changed and can thus be copied. This copy vector is used by PINS to perform some optimizations. 1int specm_receive_greater(void*model, int*src, int*dst, int*cpy, int n, int m){ 2int succs = 0; 3SET n_inbox_dst; 4SET m_set; 5SET n_inbox_set; 6 7if (label_receive_greater(model, src, n, m)) { 8// n.max’ = m 9dst[max(n)] = m; 10 11 // n.inbox’ = n.inbox - m 12 n_inbox_set = get_set(model, src, inbox(n)); 13 m_set = set_init_one(m); 14 n_inbox_dst = set_difference(n_inbox_set, m_set); 15 set_free(n_inbox_set); 5.2. Translating to LTSmin 58 16 set_free(m_set); 17 dst[inbox(n)] = set_set(model, inbox(n), n_inbox_dst); 18 set_free(n_inbox_dst); 19 20 // n.state’ = Send 21 dst[state(n)] = SEND_T; 22 23 cpy[max(n)] = 0; 24 cpy[inbox(n)] = 0; 25 cpy[state(n)] = 0; 26 27 succs++; 28 } 29 return succs; 30 } The comments were also added to highlight the translation from the Taino model to C. Like the label function, this function also ensures that all allocated memory is freed as soon as it is no longer needed. Taino does not yet support non-determinism in actions; but in order to support it, instead of these three vectors, the function should receive three vectors of vectors (for each resulting state) and return the number of successor states ( succ ) – which is incremented as each new successor state is constructed. Here, because we do not have non-determinism, the succ variable is incremented just once. You can see the powerful application of the indexation scheme we have been describing, it not only makes the translation easier, it also ensures the resulting C code is human readable. With these functions, the NextState function of LTSmin, simply checks for which action is happening and calls the respective event function with its arguments. 5.2.4Calculating dependency matrices As we noted when we introduced LTSmin back in chapter 4, the dependencies are crucial to calculate partial order reduction, so we must ensure that we can get all information needed by a syntactic analysis. It is very clear how to get the information needed to calculate read and write dependencies with events. Each event is composed of various expressions. Thus, to calculate read dependencies, one must only look for the elements of the state vector which are in the expression, ignoring the ones with an apostrophe ’ . Whilst for write dependencies we simply look to the expressions with the apostrophe. With is information, it is possible to generate a function that sets the read and write dependency matrices, like the excerpt below: 5.3. The Taino project 59 1int wm[LABEL_GOAL][STATE_LENGTH] = { 0 }; 2void set_write_matrix() { 3wm[RECEIVEEQUAL_NODE1_INT1][ELECTED] = 1; 4wm[RECEIVEEQUAL_NODE1_INT1][NODE1_INBOX] = 1; 5wm[RECEIVEEQUAL_NODE1_INT1][NODE1_STATE] = 1; 6wm[RECEIVEEQUAL_NODE1_INT2][ELECTED] = 1; 7wm[RECEIVEEQUAL_NODE1_INT2][NODE1_INBOX] = 1; 8wm[RECEIVEEQUAL_NODE1_INT2][NODE1_STATE] = 1; 9... 10 } The calculation for accordance is significantly more complex. Recall the definition of accordance (Definition 1), where for two transitions t and t0 to accord one of the following criteria must be met: 1. Their shared variables are disjoint from the write sets; 2.tand t0are never co-enabled; 3.tand t0do not disable each other and their actions commute. At first, we tried calculating if two events do not accord by just looking at their shared variables (criteria 1). However, this definition was not accurate enough and, due to the recursive nature of the stubborn set algorithm (Algorithm 2), would wrongly identify too many according events as not according. This lead to no partial order reduction being possible for a simple example like this ring leader election. We later were able to introduce a very simple analysis to check if two events can be co-enabled. We do this by solely looking at pre-conditions that check for two different values in the slot vector. For instance, we can say that, send and receiveEqual are never co-enabled for the same node as the pre-condition for send is n.state = send , whilst in receiveEqual we have n.state = receive . This, admittedly naïve, analysis was sufficient to define a more precise accordance between two events for this model. As for the third criteria, we assumed that if two events did not share the same variables, then they could never disable each other, although a method to assert if two events commute is also essential, and requires deeper investigation. 5.3 the taino project Taino is written in Haskell and it is responsible to translate the Taino modelling language to LTSmin. This is achieved in three steps: first, the original Taino model is parsed into an abstract syntax tree (AST); this AST is then converted into a more flexible data structure that can be queried to write the three different files ( spec.c , spec.h , and dlopen.c ). This schema is represented in Figure 8. 5.4. Results 60 Parser Evaluator spec.c spec.h dlopen.c Taino model Figure 8: Representation of the Taino architecture Time (seconds) Nr. of states nr nodes w/o POR w/ POR w/o POR w/POR 4 0.01 0.01 160 133 5 0.03 0.05 441 325 6 0.09 0.14 1215 836 7 0.23 0.42 3132 1846 8 0.64 1.02 8045 4025 9 2.31 2.78 20783 9033 10 8.18 11.23 53536 20056 11 29.59 35.46 137777 44143 12 105.35 97.45 354675 96389 Table 3: Tests for property always at most one elected The parser was implemented using megaparsec 2 , which takes de taino model and builds an abstract syntaxt tree. Later, the evaluator splits the abstract syntax tree in the various elements of the model: signatures, enums, events, init, predicates, et cetera. This in turn makes it easier to generate the three files needed. Lastly, we have three models each responsible to generate each file (spec.c,spec.h, and dlopen.c). 5.4 results We tested our implementation by checking different properties and different models of the ring leader election. We checked to see how much state reduction we could get out of LTSmin guard-based algorithm, and to see how that reduction would translate into a hopefully shorter time to check the properties. We have run tests on three properties: 1. Always at most one elected; 2. Eventually always one elected; 3. As soon as everyone agrees on the leader, all mailboxes should be empty. 2https://hackage.haskell.org/package/megaparsec 5.4. Results 61 Time (seconds) Nr. of states nr nodes w/o POR w/ POR w/o POR w/POR 4 0.01 0.02 263 209 5 0.03 0.05 737 505 6 0.11 0.16 2005 1181 7 0.37 0.49 5359 2709 8 1.25 1.49 14169 6129 9 4.69 5.86 37213 13713 10 23.03 17.07 97349 30389 11 85.76 77.6 254049 66781 12 275.11 225.04 662245 145673 Table 4: Tests for property eventually always one elected The first two properties should be true, LTSmin will not be able to find a counter-example and will have to search the entire state space. The third property will not be true in our model, and LTSmin should find a counter-example relatively easily; we do not expect partial order reduction to be much of an improvement. Table 3shows the results for the first property. Even though partial order reduction was able to drastically reduce the number of states, the necessary overhead of calculations for such reduction did not compensate. On Table 3only with twelve nodes did the reduced state space begun to compensate for the overhead of calculations. For the second property, which results can be found in Table 4. Again, only with ten nodes does partial order reduction begin to have a positive impact. Finally, because LTSmin is able to immediately find a counter-example for property 3, the partial order reduction overhead is simply counter-productive. Table 5shows how much impact the partial order reduction overhead has. Time (seconds) nr nodes w/o POR w/ POR 4 0 0.01 5 0 0.02 6 0.01 0.04 7 0.01 0.06 8 0.01 0.11 9 0.02 0.18 10 0.02 0.27 11 0.03 0.4 12 0.05 0.58 Table 5: Tests for the emptiness of the mailboxes when everyone agrees on the leader A POOLBOY SPECIFICATION 1open util/integer 2open util/boolean 3 4one var abstract sig Event {} 5abstract sig Actor {} 6abstract sig Message {} 7 8one sig MaxOverflow in Int {} 9 10 var sig alive in Actor {} 11 var sig blocked in alive {} 12 13 sig Worker extends Actor {} 14 15 sig Client extends Actor { 16 var workers : set Worker 17 } 18 19 one sig Poolboy { 20 var free : set Actor, -- Every free actor poolboy has 21 var overflow : one Int, -- The number of overflow workers poolboy gave 22 var waiting : set Client, -- Clients waiting for workers 23 var mailbox : set Message, -- Mailbox common to every actor **** 24 size : one Int -- The initial size of free 25 } 26 27 fun unused_workers : set Worker { 28 Worker - ( Client.workers + Poolboy.free + alive ) - ( Poolboy.mailbox & Exit ).a 29 } 30 31 ------------------ MESSAGES ----------------------- 32 33 sig Checkout extends Message { 34 c : Client, -- Client issuing the checkout 35 b : Bool -- Blocking or non blocking 68 69 36 } 37 38 sig Checkin extends Message { 39 c : Client, -- Client issuing the checkin 40 a : Actor -- Checkin actor 41 } 42 43 sig Exit extends Message { 44 a : Actor -- The actor exiting 45 } 46 47 sig Timeout extends Message { 48 c : Client 49 } 50 51 pred sendMessage[m : Message] { 52 m not in Poolboy.mailbox 53 mailbox’ = mailbox + Poolboy->m 54 } 55 56 pred readMessage[m : Message] { 57 m in Poolboy.mailbox 58 mailbox’ = mailbox - Poolboy->m 59 } 60 61 -------------------- EVENTS ------------------------------------------------ 62 63 var sig ClientSendCheckout extends Event { 64 var cli : Client, 65 var blk : Bool 66 } { 67 cli in (Client & alive) - blocked 68 69 some msg : Checkout { 70 msg.c = cli 71 msg.b = blk 72 sendMessage[msg] 73 } 74 75 blocked’ = blocked + cli 76 } 77 78 var sig ClientSendCheckin extends Event { 79 var cli : Client, 80 var act : Actor 81 } { 82 cli in (Client & alive) - blocked 70 83 act in cli.workers 84 85 some msg : Checkin { 86 msg.c = cli 87 msg.a = act 88 sendMessage[msg] 89 } 90 workers’ = workers - cli->act 91 } 92 93 var sig ClientSendTimeout extends Event { 94 var cli : Client 95 } { 96 cli in blocked 97 98 some msg : Timeout { 99 msg.c = cli 100 sendMessage[msg] 101 } 102 103 blocked’ = blocked - cli 104 } 105 106 var sig ActorExit extends Event { 107 var act : Actor 108 } { 109 act in Worker -- non byzantine 110 act in alive 111 112 some msg : Exit { 113 msg.a = act 114 sendMessage[msg] 115 } 116 117 alive’ = alive - act 118 blocked’ = blocked - act 119 workers’ = workers - Client->act 120 } 121 122 var sig PbCheckoutReady extends Event {} { 123 some free 124 125 some msg : Checkout { 126 readMessage[msg] 127 128 some w : Poolboy.free { 129 w in alive 71 130 free’ = free - Poolboy->w 131 workers’ = workers + msg.c->w 132 } 133 134 blocked’ = blocked - msg.c 135 } 136 } 137 138 var sig PbCheckoutOverflow extends Event {} { 139 no free 140 lt[Poolboy.overflow, MaxOverflow] 141 142 some msg : Checkout { 143 readMessage[msg] 144 145 some w : unused_workers { 146 alive’ = alive + w 147 workers’ = workers + msg.c->w 148 } 149 150 blocked’ = blocked - msg.c 151 } 152 Poolboy.overflow’ = add[Poolboy.overflow, 1] 153 } 154 155 var sig PbCheckoutFull extends Event {} { 156 no free 157 (lte[MaxOverflow, 0] or gte[Poolboy.overflow, MaxOverflow]) 158 159 some msg : Checkout { 160 readMessage[msg] 161 isTrue[msg.b] implies Poolboy.waiting’ = Poolboy.waiting + msg.c 162 else (waiting’ = waiting and blocked’ = blocked - msg.c) 163 } 164 } 165 166 var sig PbTimeout extends Event {} { 167 some msg : Timeout { 168 readMessage[msg] 169 Poolboy.waiting’ = Poolboy.waiting - msg.c 170 } 171 } 172 173 var sig PbCheckinWaiting extends Event {} { 174 some msg : Checkin, cli : Poolboy.waiting { 175 readMessage[msg] 176 72 177 Poolboy.waiting’ = Poolboy.waiting - cli 178 workers’ = workers + cli->msg.a 179 blocked’ = blocked - cli 180 } 181 } 182 183 var sig PbCheckinOverflow extends Event {} { 184 no waiting 185 gt[Poolboy.overflow, 0] 186 187 some msg : Checkin { 188 readMessage[msg] 189 alive’ = alive - msg.a 190 } 191 Poolboy.overflow’ = sub[Poolboy.overflow, 1] 192 } 193 194 var sig PbCheckinReady extends Event {} { 195 no waiting 196 Poolboy.overflow = 0 197 198 some msg : Checkin { 199 readMessage[msg] 200 Poolboy.free’ = Poolboy.free + msg.a 201 } 202 } 203 204 var sig PbExitWaiting extends Event {} { 205 some msg : Exit, cli : Poolboy.waiting { 206 readMessage[msg] 207 208 some w : unused_workers { 209 alive’ = alive + w 210 workers’ = workers + cli->w 211 } 212 213 Poolboy.waiting’ = Poolboy.waiting - cli 214 blocked’ = blocked - cli 215 } 216 } 217 218 var sig PbExitOverflow extends Event {} { 219 no waiting 220 gt[Poolboy.overflow, 0] 221 222 some msg : Exit { 223 readMessage[msg] 73 224 Poolboy.free’ = Poolboy.free - msg.a 225 } 226 227 Poolboy.overflow’ = sub[Poolboy.overflow, 1] 228 } 229 230 var sig PbExitReady extends Event {} { 231 no waiting 232 Poolboy.overflow = 0 233 234 some msg : Exit, w : unused_workers { 235 readMessage[msg] 236 Poolboy.free’ = Poolboy.free - msg.a + w 237 alive’ = alive + w 238 } 239 } 240 241 ---------------- UPDATE FACTS ---------------------------------------------- 242 243 fact updated { 244 always ( blocked’ != blocked 245 implies some ClientSendCheckout + ClientSendTimeout + ActorExit + 246 PbCheckoutReady + PbCheckoutOverflow + PbCheckinWaiting + PbExitWaiting) 247 248 always ( workers’ != workers 249 implies some ClientSendCheckin + ActorExit + PbCheckoutReady + 250 PbCheckoutOverflow + PbCheckinWaiting + PbExitWaiting ) 251 252 always ( alive’ != alive 253 implies some ActorExit + PbCheckoutOverflow + PbCheckinOverflow + 254 PbExitWaiting + PbExitReady) 255 256 always ( free’ != free 257 implies some PbCheckoutReady + PbCheckinReady + PbExitOverflow + PbExitReady) 258 259 always ( overflow’ != overflow 260 implies some PbCheckoutOverflow + PbCheckinOverflow + PbExitOverflow) 261 262 always ( waiting’ != waiting 263 implies some PbCheckoutFull + PbTimeout + PbCheckinWaiting + PbExitWaiting) 264 265 always ( mailbox’ != mailbox 266 implies some ClientSendCheckout + ClientSendCheckin + ClientSendTimeout + ActorExit + 267 PbCheckoutReady + PbCheckoutOverflow + PbCheckoutFull + PbTimeout + PbCheckinWaiting + 268 PbCheckinOverflow + PbCheckinReady + PbExitWaiting + PbExitOverflow + PbExitReady) 269 } 270 74 271 ---------------- FACTS ---------------------------------------------------- 272 273 fact init { 274 Poolboy.overflow = 0 275 gte[MaxOverflow, 0] 276 Poolboy.free = alive & Worker 277 Poolboy.size = #Poolboy.free 278 no waiting 279 no workers 280 no blocked 281 no mailbox 282 } 283 284 -------------------------------------------------------------------------------- 285 286 fact ensure_justice { 287 always ( all m : Message { 288 sendMessage[m] implies (eventually readMessage[m]) 289 }) 290 291 always ( all c : Client { 292 c in Poolboy.waiting implies (eventually c not in Poolboy.waiting) 293 }) 294 --eventually always no waiting 295 } 296 297 pred workers_available { 298 some Poolboy.free or 299 lt[Poolboy.overflow, MaxOverflow] 300 } 301 302 pred receive_worker[c : Client] { 303 #c.workers’ = add[#c.workers, 1] 304 } 305 306 assert maximum_workers { 307 always lte[#total_workers, add[Poolboy.size, MaxOverflow]] 308 } 309 check maximum_workers for 6 310 311 assert client_gets_worker { 312 all c1 : Client { 313 always ( 314 (c1 in (ClientSendCheckout.cli - Timeout.c) and lt[Poolboy.overflow, MaxOverflow]) 315 implies (eventually receive_worker[c1])) 316 } 317 } check client_gets_worker 75 318 319 assert timeout_is_safe { 320 always ( 321 all c1 : Client { 322 receive_worker[c1] implies c1 in blocked 323 } 324 ) 325 } check timeout_is_safe 326 327 fun total_workers : set Worker { 328 Poolboy.free + Client.workers 329 } 330 331 332 run eventually_receive { 333 some c : Client | eventually receive_worker[c] 334 }for 4 but 14 Event 335 336 run specific_trace{ 337 some ClientSendCheckout ; 338 some PbCheckoutReady ; 339 some ClientSendCheckin 340 }for 4 but 3 Event 341 342 run { 343 eventually some PbExitWaiting 344 }for 4 but 14 Event B LTSMIN MODEL b.1 specification file header (spec.h) 1#ifndef RING_H 2#define RING_H 3 4#include "sSet.h" 5#include <ltsmin/pins.h> 6 7#define N 6 8#define NR_VARS 4 9#define NR_ACTIONS 4 10 11 #define INBOX(proc) ((proc - 1) *NR_VARS) 12 #define MAX(proc) ((proc - 1) *NR_VARS + 1) 13 #define KNOW_LEADER(proc) ((proc - 1) *NR_VARS + 2) 14 #define STATE(proc) ((proc - 1) *NR_VARS + 3) 15 16 #define NEXT(proc) ((proc % N) + 1) 17 #define PREV(proc) (((proc + (N-2)) % N) + 1) 18 19 // transition labels 20 #define SEND(i) ((i-1) *NR_ACTIONS) 21 #define RECV_SMALL(i) ((i-1) *NR_ACTIONS + 1) 22 #define RECV_EQ(i) ((i-1) *NR_ACTIONS + 2) 23 #define RECV_GRT(i) ((i-1) *NR_ACTIONS + 3) 24 25 // label values 26 #define LABEL_GOAL (NR_ACTIONS *N) 27 28 /** 29 *@brief calls callback for every successor state of src in transition group "group". 30 */ 31 int next_state(void*model, int group, int *src, TransitionCB callback, void *arg); 32 33 /** 76 B.1. Specification file header (spec.h) 77 34 *@brief returns the initial state. 35 */ 36 int*initial_state(void*model); 37 38 /** 39 *@brief returns the read dependency matrix. 40 */ 41 void set_read_matrix(); 42 int*read_matrix(int row); 43 44 /** 45 *@brief returns the write dependency matrix. 46 */ 47 void set_write_matrix(); 48 int*write_matrix(int row); 49 50 /** 51 *@brief returns the state label dependency matrix. 52 */ 53 void set_label_matrix(); 54 int*label_matrix(int row); 55 56 /** 57 *@brief returns the guard dependency matrix. 58 */ 59 void set_dna_matrix(); 60 int*guard_matrix(int row); 61 62 /** 63 *@brief returns the do not accord matrix. 64 */ 65 int*do_not_accord_matrix(int row); 66 67 /** 68 *@brief returns whether the state src satisfies state label "label". 69 */ 70 int state_label(void*model, int label, int*src); 71 72 /** 73 *@brief returns the number of transition groups. 74 */ 75 int group_count(); 76 77 /** 78 *@brief returns the length of the state. 79 */ 80 int state_length(); B.2. Specification file (spec.c) 84 263 264 return i > N; 265 } 266 267 int label_send(int proc, int*src) { 268 return (src[STATE(proc)] == STATE_SEND); 269 } 270 271 int label_receive_smaller(void*m, int proc, int*src) { 272 int i, elems[100], max_proc = src[MAX(proc)]; 273 SSET inbox_proc = get_sset(m, src, INBOX(proc)); 274 int size = sset_to_list(inbox_proc, elems, 100); 275 for(i = 0; i < size && elems[i] >= max_proc; i++); 276 277 return (src[STATE(proc)] == STATE_RECEIVE && 278 size > 0 && i < size); 279 } 280 281 int label_receive_equal(void*m, int proc, int*src) { 282 SSET inbox_proc = get_sset(m, src, INBOX(proc)); 283 int max_proc = src[MAX(proc)]; 284 285 return (src[STATE(proc)] == STATE_RECEIVE && 286 sset_in(inbox_proc, max_proc)); 287 } 288 289 int label_receive_greater(void*m, int proc, int*src) { 290 int i, elems[100], max_proc = src[MAX(proc)]; 291 SSET inbox_proc = get_sset(m, src, INBOX(proc)); 292 int size = sset_to_list(inbox_proc, elems, 100); 293 for(i = 0; i < size && elems[i] <= max_proc; i++); 294 295 return (src[STATE(proc)] == STATE_RECEIVE && 296 size > 0 && i < size); 297 } 298 299 int ring_send(void*m, int from, int to, int*src, int*dst, int*cpy) { 300 int succs = 0; 301 302 if (label_send(from, src)) {//src[STATE(from)] == STATE_SEND) { 303 SSET inbox_to = get_sset(m, src, INBOX(to)); 304 305 inbox_to = sset_add(inbox_to, src[MAX(from)]); 306 307 dst[INBOX(to)] = set_sset(m, INBOX(to), inbox_to); 308 309 dst[STATE(from)] = STATE_RECEIVE; B.2. Specification file (spec.c) 85 310 311 cpy[INBOX(to)] = 0; 312 cpy[STATE(from)] = 0; 313 314 succs++; 315 } 316 317 return succs; 318 } 319 320 int receive_equal(void*m, int proc, int*src, int*dst, int*cpy) { 321 int succs = 0; 322 323 // MAX_i \in INBOX_i 324 SSET inbox_proc = get_sset(m, src, INBOX(proc)); 325 int max_proc[1] = { src[MAX(proc)] }; 326 327 // if (src[STATE(proc)] == STATE_RECEIVE && sset_in(inbox_proc, max_proc[0])) { 328 //if (src[STATE(proc)] == STATE_RECEIVE && src[INBOX(proc)] == src[MAX(proc)]) { 329 if (label_receive_equal(m, proc, src)) { 330 dst[KNOW_LEADER(proc)] = 1; 331 // inbox’ = inbox - { max } 332 sset_difference(&inbox_proc, sset_from_list(max_proc, 1)); 333 dst[INBOX(proc)] = set_sset(m, INBOX(proc), inbox_proc); 334 dst[STATE(proc)] = STATE_SEND;//sset_cardinality(inbox_proc) == 0 ? STATE_SEND : STATE_RECEIVE; 335 336 cpy[KNOW_LEADER(proc)] = 0; 337 cpy[INBOX(proc)] = 0; 338 cpy[STATE(proc)] = 0; 339 340 succs++; 341 } 342 343 return succs; 344 } 345 346 int receive_greater(void*m, int proc, int*src, int*dst, int*cpy) { 347 int succs = 0; 348 349 int i, elems[100], max_proc = src[MAX(proc)]; 350 SSET inbox_proc = get_sset(m, src, INBOX(proc)); 351 int size = sset_to_list(inbox_proc, elems, 100); 352 for(i = 0; i < size && elems[i] <= max_proc; i++); 353 354 //if (src[STATE(proc)] == STATE_RECEIVE && size > 0 && i < size) { 355 if(label_receive_greater(m, proc, src)) { B.3. Dlopen implementation file (dlopen.c) 86 356 int new_max_proc[1] = { elems[i] }; 357 dst[MAX(proc)] = new_max_proc[0]; 358 sset_difference(&inbox_proc, sset_from_list(new_max_proc, 1)); 359 dst[STATE(proc)] = STATE_SEND; //sset_cardinality(inbox_proc) == 0 ? STATE_SEND : STATE_RECEIVE; 360 dst[INBOX(proc)] = set_sset(m, INBOX(proc), inbox_proc); 361 362 cpy[MAX(proc)] = 0; 363 cpy[INBOX(proc)] = 0; 364 cpy[STATE(proc)] = 0; 365 366 succs++; 367 } 368 369 return succs; 370 } 371 372 int receive_smaller(void*m, int proc, int*src, int*dst, int*cpy) { 373 int succs = 0; 374 375 int i, elems[100], max_proc = src[MAX(proc)]; 376 SSET inbox_proc = get_sset(m, src, INBOX(proc)); 377 int size = sset_to_list(inbox_proc, elems, 100); 378 for(i = 0; i < size && elems[i] >= max_proc; i++); 379 380 if (label_receive_smaller(m, proc, src)) { 381 //src[STATE(proc)] == STATE_RECEIVE && size > 0 && i < size) { 382 int e[1] = { elems[i] }; 383 SSET rem = sset_from_list(e, 1); 384 385 sset_difference(&inbox_proc, rem); 386 387 dst[INBOX(proc)] = set_sset(m, INBOX(proc), inbox_proc); 388 389 cpy[INBOX(proc)] = 0; 390 391 succs++; 392 } 393 394 return succs; 395 } b.3 dlopen implementation file (dlopen.c) 1#include <ltsmin/pins.h> B.3. Dlopen implementation file (dlopen.c) 87 2#include <ltsmin/pins-util.h> 3#include <ltsmin/dlopen-api.h> 4#include <ltsmin/ltsmin-standard.h> 5#include <ltsmin/lts-type.h> 6 7#include <spec.h> 8#include "sSet.h" 9 10 #define SIZE 128 11 12 // set the name of this PINS plugin 13 char pins_plugin_name[] = "ring"; 14 15 16 static void sl_group (model_t model, sl_group_enum_t group, int *state, int *labels) { 17 switch (group) { 18 case GB_SL_ALL: 19 get_guard_all(model, state, 1, labels); 20 return; 21 case GB_SL_GUARDS: 22 get_guard_all(model, state, 0, labels); 23 return; 24 default: 25 return; 26 } 27 } 28 29 void pins_model_init(model_t m) { 30 char name[SIZE]; 31 32 // create the LTS type LTSmin will generate 33 lts_type_t ltstype=lts_type_create(); 34 35 // set the length of the state 36 lts_type_set_state_length(ltstype, state_length()); 37 38 // add an "int" type for a state slot 39 int int_type = lts_type_put_type(ltstype, "int", LTStypeSInt32 , NULL); 40 41 // add an "action" type for edge labels 42 int action_type = lts_type_put_type(ltstype, "action", LTStypeEnum, NULL); 43 44 // add a "bool" type for state labels 45 int bool_type = lts_type_put_type (ltstype, "bool", LTStypeBool, NULL); 46 47 // add an "int" type for a state slot 48 int set_type = lts_type_put_type(ltstype, "set", LTStypeChunk, NULL); B.3. Dlopen implementation file (dlopen.c) 88 49 50 // set state name & type 51 for (int i=1; i <= N; i++) { 52 sprintf(name, "inbox_%d", i); 53 lts_type_set_state_name(ltstype, INBOX(i), name); 54 lts_type_set_state_typeno(ltstype, INBOX(i), set_type); 55 56 sprintf(name, "max_%d", i); 57 lts_type_set_state_name(ltstype, MAX(i), name); 58 lts_type_set_state_typeno(ltstype, MAX(i), int_type); 59 60 sprintf(name, "know_leader_%d", i); 61 lts_type_set_state_name(ltstype, KNOW_LEADER(i), name); 62 lts_type_set_state_typeno(ltstype, KNOW_LEADER(i), int_type); 63 64 sprintf(name, "state_%d", i); 65 lts_type_set_state_name(ltstype, STATE(i), name); 66 lts_type_set_state_typeno(ltstype, STATE(i), int_type); 67 } 68 69 // edge label types 70 lts_type_set_edge_label_count(ltstype, 1); 71 lts_type_set_edge_label_name(ltstype, 0, "action"); 72 lts_type_set_edge_label_type(ltstype, 0, "action"); 73 lts_type_set_edge_label_typeno(ltstype, 0, action_type); 74 75 // state label types 76 lts_type_set_state_label_count (ltstype, label_count()); 77 78 for (int i = 1; i <= N; i++) { 79 sprintf(name, "label_send_%d", i); 80 lts_type_set_state_label_name (ltstype, SEND(i), name); 81 lts_type_set_state_label_typeno (ltstype, SEND(i), bool_type); 82 83 sprintf(name, "label_receive_smaller_%d", i); 84 lts_type_set_state_label_name (ltstype, RECV_SMALL(i), name); 85 lts_type_set_state_label_typeno (ltstype, RECV_SMALL(i), bool_type); 86 87 sprintf(name, "label_receive_equal_%d", i); 88 lts_type_set_state_label_name (ltstype, RECV_EQ(i), name); 89 lts_type_set_state_label_typeno (ltstype, RECV_EQ(i), bool_type); 90 91 sprintf(name, "label_receive_greater_%d", i); 92 lts_type_set_state_label_name (ltstype, RECV_GRT(i), name); 93 lts_type_set_state_label_typeno (ltstype, RECV_GRT(i), bool_type); 94 } 95 B.3. Dlopen implementation file (dlopen.c) 89 96 lts_type_set_state_label_name (ltstype, LABEL_GOAL, "goal"); 97 lts_type_set_state_label_typeno (ltstype, LABEL_GOAL, bool_type); 98 99 // done with ltstype 100 lts_type_validate(ltstype); 101 102 // make sure to set the lts-type before anything else in the GB 103 GBsetLTStype(m, ltstype); 104 105 // setting all values for all non direct types 106 for (int i = 1; i <= N; i++) { 107 sprintf(name, "send_%d", i); 108 pins_chunk_put(m, action_type, chunk_str(name)); 109 110 sprintf(name, "receive_smaller_%d", i); 111 pins_chunk_put(m, action_type, chunk_str(name)); 112 113 sprintf(name, "receive_equal_%d", i); 114 pins_chunk_put(m, action_type, chunk_str(name)); 115 116 sprintf(name, "receive_greater_%d", i); 117 pins_chunk_put(m, action_type, chunk_str(name)); 118 } 119 120 // set state variable values for initial state 121 printf("Loading initial state...\n"); 122 int*initial = initial_state(m); 123 /*for(int i = 0; i < N; i++) { 124 char data[1024]; 125 int length = sset_serialize(sset_init(), data, 1024); 126 initial[INBOX(i)] = pins_chunk_put(m, set_type, chunk_ld(length, data)); 127 }*/ 128 GBsetInitialState(m, initial); 129 130 // set function pointer for the next-state function 131 GBsetNextStateLong(m, (next_method_grey_t) next_state); 132 133 // set function pointer for the label evaluation function 134 GBsetStateLabelLong(m, (get_label_method_t) state_label); 135 136 // create combined matrix 137 matrix_t*cm = malloc(sizeof(matrix_t)); 138 dm_create(cm, group_count(), state_length()); 139 140 // set the read dependency matrix 141 set_read_matrix(); 142 matrix_t*rm = malloc(sizeof(matrix_t)); B.3. Dlopen implementation file (dlopen.c) 90 143 dm_create(rm, group_count(), state_length()); 144 for (int i = 0; i < group_count(); i++) { 145 int*aux = read_matrix(i); 146 for (int j = 0; j < state_length(); j++) { 147 if (aux[j]) { 148 dm_set(cm, i, j); 149 dm_set(rm, i, j); 150 } 151 } 152 } 153 GBsetDMInfoRead(m, rm); 154 155 // set the write dependency matrix 156 set_write_matrix(); 157 matrix_t*wm = malloc(sizeof(matrix_t)); 158 dm_create(wm, group_count(), state_length()); 159 for (int i = 0; i < group_count(); i++) { 160 int*aux = write_matrix(i); 161 for (int j = 0; j < state_length(); j++) { 162 if (aux[j]) { 163 dm_set(cm, i, j); 164 dm_set(wm, i, j); 165 } 166 } 167 } 168 GBsetDMInfoMustWrite(m, wm); 169 170 // set the combined matrix 171 GBsetDMInfo(m, cm); 172 173 // set the label dependency matrix 174 set_label_matrix(); 175 matrix_t*lm = malloc(sizeof(matrix_t)); 176 dm_create(lm, label_count(), state_length()); 177 for (int i = 0; i < label_count(); i++) { 178 int*aux = label_matrix(i); 179 for (int j = 0; j < state_length(); j++) { 180 if (aux[j]) dm_set(lm, i, j); 181 } 182 } 183 GBsetStateLabelInfo(m, lm); 184 185 // set the do not accord dependency matrix 186 set_dna_matrix(); 187 matrix_t*dnam = malloc(sizeof(matrix_t)); 188 dm_create(dnam, group_count(), group_count()); 189 for (int i = 0; i < group_count(); i++) { B.3. Dlopen implementation file (dlopen.c) 91 190 int*aux = do_not_accord_matrix(i); 191 for (int j = 0; j < group_count(); j++) { 192 if (aux[j]) dm_set(dnam, i, j); 193 } 194 } 195 GBsetDoNotAccordInfo(m, dnam); 196 197 198 guard_t** guards = malloc(group_count() *sizeof(guard_t*)); 199 for(int i = 0; i < group_count(); i++) { 200 guards[i] = malloc(sizeof(guard_t) + sizeof(int)); 201 guards[i]->count = 1; 202 guards[i]->guard[0] = i; 203 } 204 GBsetGuardsInfo(m, guards); 205 206 // set group info 207 sl_group_t*group_all = malloc(sizeof(sl_group_t) + label_count() *sizeof(int)); 208 group_all->count = label_count(); 209 memcpy(group_all->sl_idx, label_indices(), group_all->count *sizeof(int)); 210 211 sl_group_t*group_guards = malloc(sizeof(sl_group_t) + guard_count() *sizeof(int)); 212 group_guards->count = guard_count(); 213 memcpy(group_guards->sl_idx, label_indices(), group_guards->count *sizeof(int)); 214 215 GBsetStateLabelGroupInfo(m, GB_SL_ALL, group_all); 216 GBsetStateLabelGroupInfo(m, GB_SL_GUARDS, group_guards); 217 GBsetStateLabelsGroup(m, sl_group); 218 } C TAINO RING LEADER ELECTION 1enum State { Send, Receive } 2 3var sig elected {} 4 5sig Int {} 6 7sig Node { 8var max : one Int, 9succ : one Node, 10 var inbox : set Int, 11 var state : one State 12 } 13 14 event send[n : Node] { 15 n.state = send 16 17 n.succ.inbox’ = n.succ.inbox + n.max 18 n.state’ = receive 19 } 20 21 event receiveSmall[n : Node, m : Int] { 22 n.state = Receive 23 m in n.inbox 24 lt[m, n.max] 25 26 n.inbox’ = n.inbox - m 27 } 28 29 event receiveGreater[n : Node, m : Int] { 30 n.state = Receive 31 m in n.inbox 32 gt[m, n.max] 33 34 n.max’ = m 35 n.inbox’ = n.inbox - m 92 93 36 n.state’ = Send 37 } 38 39 event receiveEqual[n : Node, m : Int] { 40 n.state = Receive 41 m in n.inbox 42 n.max = m 43 44 elected’ = elected + m 45 n.inbox’ = n.inbox - m 46 n.state’ = Send 47 } 48 49 init { 50 no elected 51 Node$1.max = 1 52 Node$1.succ = Node$2 53 no Node$1.inbox 54 Node$1.state = Send 55 56 Node$2.max = 2 57 Node$2.succ = Node$3 58 no Node$2.inbox 59 Node$2.state = Send 60 61 Node$3.max = 3 62 Node$3.succ = Node$4 63 no Node$3.inbox 64 Node$3.state = Send 65 66 Node$4.succ = Node$5 67 no Node$4.inbox 68 Node$4.state = Send 69 Node$4.max = 4 70 71 } for 4 Node, 4 Int 72 73 pred only_one_elected { 74 one elected 75 } 76 77 check { 78 eventually always only_one_elected 79 }