Notes

Outline

Asynchronous Multi-Agent ASMs An Introduction Egon Börger Dipartimento di Informatica, Universita di Pisa http://www.di.unipi.it/~boerger

Slide 2

"Definition of Async ASMs" Definition of Async ASMs Small Examples Mutual Exclusion Dining Philosophers Multiple Read One Write Network Algorithms Master Slave Consensus Load Balance Leader Election Echo Phase Synchronization Simple Properties of Async ASMs References

Recalling Basic ASMs: computation step Basic ASM: a finite set of rules, executed by a single agent self, of form If Condition Then Updates A computation step of a basic ASM: In the current state (well-defined global structure) S: determine all the fireable rules in S (s.t. Cond is true in S) compute all expressions ti,t occurring in updates f(t1,…,tn):=t this includes reading of the monitored functions, supposed to have well-defined stable values for each execution step execute simultaneously all these function updates

Recalling Basic ASMs: next state The updating yields a next state S’, which is well-defined by the updates - and by possible changes of the monitored function values, thought of as resulting from implicit actions of the environment environment actions are assumed to be “located” with respect to a machine step in such a way that their result is ready when the machine is going to perform its next step (implicit environment-controller separation principle)

Distributed Runs: State Stability Problem In runs of asynchronously cooperating independent agents, the possible incomparability of moves - coming with different data, clocks, moments and duration of execution -  makes it difficult to uniquely define a global state where moves are executed to locate changes of monitored fcts in the ordering of moves The coherence condition in the definition of asynchronous multi-agent ASM runs below postulates well-definedness for a relevant portion of state in which an agent is supposed to perform a step, thus providing a notion of “local” stable view of “the” idealized state in which an agent makes a move.

Async ASM Runs: Environmental Changes Changes of monitored functions can be made explicit as resulting from moves of one or more environment agents. Such monitored moves - moves of “unkown” agents, as opposed to the controlled moves of the explicitly given agents - are often thought of as implicitly given, e.g. by speaking of “time moments” in which changes of monitored functions take place.

Defining Asynchronous Multi-Agent ASMs An Async ASM is a family of pairs (a, ASM(a)) of agents a Î Agent (a possibly dynamic set) basic ASMs ASM (a) A Run of an async ASM is a partially ordered set (M, < ) of “moves” m of its agents s.t.: finite history: each move has only finitely many predecessors, i.e. {m’ | m’ < m } is finite for each mÎM sequentiality of agents: for each agent a Î Agent, his moves  {m | mÎM, a performs m} are linearly ordered by < coherence: each (finite) initial segment X of  (M, < ) has an associated state s (X) – think of it as the result of all moves in X with m executed before m’ if m<m’– which for every maximal element mÎX is the result of applying move m in state  s(X-{m})

Linearizing Initial segments of runs of an async ASM Linearization Lemma. Let X be a finite initial segment (downward closed subset) of a run of an async ASM. Each linearization of X yields a run with the same final state. Proof:  follows from the coherence condition

"Definition & Simple Properties of..." Definition & Simple Properties of Async ASMs Small Examples Mutual Exclusion Dining Philosophers           See Reisig 1998, Sect. 10 Multiple Read One Write Network Algorithms Master Slave Consensus Load Balance Leader Election Echo Phase Synchronization Exercises and References

Exclusive use of shared resources: problem statement Goal: Design a distributed algorithm  that allows every interested agent to eventually use some shared resource in exclusive use prevents two users to use the shared resource simultaneously Agent: set of agents each equipped with resource: Resource (different agents may have the same resource) owner: Resource ® Agent  recording the current user of a given resource

Exclusive use of shared resources: single agent view The algorithm has to manipulate updates of owner in such a way that every attempt by an agent to become owner of his resource will eventually succeed Every single agent would like to execute alternately the following two rules:

Dining Philosophers  illustrating exclusive use of shared resources

"Definition of Async ASMs" Definition of Async ASMs Small Examples Mutual Exclusion Dining Philosophers Multiple Read One Write   See Reisig 1998, Sect. 24 Network Algorithms Master Slave Consensus Load Balance Leader Election Echo Phase Synchronization Simple Properties of Async ASMs References

Multiple Reads One Write : problem statement  (non-exclusive and exclusive resource sharing) Goal: Design a distributed algorithm allowing at each step one agent to start a read or a write operation in a given file, up to  max-read>0 simultaneous reads but only 1 write (not overlapping with any read) Below we define agent rules for read/write access to files which in a distributed run of an async ASM (of agents all of which are equipped with those rules) reach the requested goal NB. In the example we do not define the partial order for such distributed runs.

Multiple Reads One Write : Agent Signature Agent : set of agents which are allowed to access files for read/write operations finished:File ® Bool indicating whether an agent has finished his current file operation File: set of files equipped with user : Nat  indicating the number of agents which are currently reading or writing the file max-read,max-write maximal number of agents allowed to simultaneously use the file for reading/writing

Multiple Reads One Write: agent rules for act=read/write

"Definition of Async ASMs" Definition of Async ASMs Small Examples Mutual Exclusion Dining Philosophers Multiple Read One Write Network Algorithms Master Slave Agreement  See Reisig 1998, Sect. 30 (Fig.30.1), 75 Consensus Load Balance Leader Election Echo Phase Synchronization Simple Properties of Async ASMs References

Master/Slave Agreement : problem statement Goal: Design a distributed algorithm for a master launching orders to slave agents, to be confirmed by them and to be executed iff all of them confirm to the master the acceptance of the order. Algorithmic Idea: the master enquires about a job to be launched and then waits for answers from the slaves the slaves answer the enquiry and then wait for the order or the cancellation of the launched job from the master the master orders or cancels the job depending on whether all slaves answered to accept it or not Eventually the master becomes idle, with all slaves either idle too or executing the accepted job.

Master/Slave Agreement : Agent Signature master: a distinguished agent order: Order   external function yielding jobs to be sent to the slaves ctl_state: {idle, waitingForAnswer} Slaves:  a set of agents equipped with asked: {true,false}   recording whether a job request has been launched by the master to the slave answer : {accept,refuse,undef} recording whether a job request has been acceped by the slave ctl_state:{idle, waitingForOrder, busy} Initially ctl_state = idle, order = answer =undef, asked = false NB. Abstraction from message passing: functions asked, answer, order shared in writing resp.reading among slaves and master

Master/Slave Agreement ASMs

Master/Slave Agreement Correctness Proposition: In every run of a set of master and slaves, all equipped with the corresponding  master/slave ASM, after the master has started an Enquiry, eventually the master becomes idle and either all slaves become done or all slaves become busy executing the job ordered by the master Proof. Follows by run induction.

"Definition of Async ASMs" Definition of Async ASMs Small Examples Mutual Exclusion Dining Philosophers Multiple Read One Write Network Algorithms Master Slave Consensus  See Reisig 1998, Sect. 35 (Fig. 35.1), 80 Load Balance Leader Election Echo Phase Synchronization Simple Properties of Async ASMs References

Consensus in Networks: problem statement Goal: Design a distributed algorithm  for reaching consensus among homogeneous agents of finite connected networks (using only communication between neighbors, without broker or mediator, with abstract requests and answers). Algorithmic Idea: every agent (node) may launch a request to his neighbors and wait for the replies agree with the replies received from his neighbors reply to requests received from his neighbors until all agents agree (maybe never)

Consensus ASM: Agent Signature Agent : finite connected set (of nodes) Each agent equipped with: neighb Í Agent         (external function) Request Í {RequestFrom(n)|nÎneighb }                                                                 (controlled function) Reply Í {ReplyFrom(n)|n Î neighb }                                                                     (controlled function) ctl_state :  {pending, agreed} Initially ctl_state=pending, Request = empty, Reply = full chosenRule to control non-deterministic choice between LaunchNewRequest and Answer

Consensus Control State ASM

Async Consensus ASM : Stability property Proposition: In every distributed run of agents equipped with the consensus ASM, if the run terminates, then for every agent holds: ctl_state = agreed Reply = full Request = empty Proof (assuming that every enabled agent will eventually make a move): follows from the definition of LaunchNewRequest, Answer. When Reply=full at agent, then there is no RequestFrom(agent) in Request(n) for any n Î neighb(agent)

"Definition of Async ASMs" Definition of Async ASMs Small Examples Mutual Exclusion Dining Philosophers Multiple Read One Write Network Algorithms Master Slave Consensus Load Balance See Reisig 1998, Sect. 37 (Fig.37.1), 82 Leader Election Echo Phase Synchronization Simple Properties of Async ASMs References

Ring Load Balance: problem statement Goal: Design a distributed algorithm  for reaching workload balance among the agents of a ring (using only communication between right/left neighbors) keeping message passing mechanism and effective task transfer abstract, assuming fixed number of agents and total workload Algorithmic Idea: every agent (ring node) alternately sends a workload info mssg to his right neighbor a task transfer mssg to his left neighbor, transfering a task to balance the workload with the left neighbor updates his workload to balance it with his right neighbor so that eventually the difference between the workload of two nodes becomes £ 1 NB. Sending workload info mssg precedes task balancing

Ring Load Balance ASM: Agent Signature Agent : a ring of agents equipped with: leftNeighb, rightNeighb: Agent  (external functions) workLoad:  the current workload neighbLoad: current workload of leftNeighb transferLoad: workload transfered by rightNeighb ctl_state :  {informRightNeighb, checkWithLeftNeighb , checkWithRightNeighb } Initially ctl_state = informRightNeighb neighbLoad = transferLoad = undef

Ring Load Balance ASM

Async Ring Load Balance ASM : Correctness Proposition: In every distributed run of agents equipped with the ring load balance ASM, eventually the  workload difference between two neighboring nodes becomes £ 1. Proof (assuming that every enabled agent will eventually make a move): induction on the wieght of run workload differences. Let w = total workLoad of all nodes, a= |Agent|. Case 1: t|a. Then eventually workLoad(n)=w/a for every node n. Case 2: otherwise. Then eventually the workLoad of some neighboring nodes will differ by 1.

"Definition of Async ASMs" Definition of Async ASMs Small Examples Mutual Exclusion Dining Philosophers Multiple Read One Write Network Algorithms Master Slave Consensus Load Balance Leader Election See Reisig 1998, Sect. 32 (Fig.32.1/2), 76 Echo Phase Synchronization Simple Properties of Async ASMs References

Leader Election: problem statement Goal: Design a distributed algorithm  for the election of a leader in finite connected networks of homogeneous agents, using only communication (message passing) between neighbor nodes. Assumptions: network nodes (agents) are connected & linearly ordered leader = max (Agent) wrt the linear order < Algorithmic Idea: every agent (network node) proposes to his neighbors his current leader candidate checks the leader proposals received from his neighbors upon detecting a proposal which improves his leader candidate he improves his candidate  for his next proposal Eventually cand=max(Agent) holds for all agents

Leader Election: Agent Signature Agent : finite linearly ordered connected set < linear order of Agent (external function) leader = max (Agent) wrt the linear order < Each agent equipped with: neighb Í Agent                      (external function) cand: Agent                                (controlled function) proposals Í Agent                    (controlled function) ctl_state :  {proposeToNeighbors, checkProposals} Initially ctl_state=proposeToNeighbors, cand=self, proposals = empty

Leader Election Control State ASM

Leader Election: Correctness property Proposition: In every distributed run of agents equipped with the leader election ASM, eventually for every agent holds: cand=max(Agent) ctl_state = checkProposals proposals = empty Proof (assuming that every enabled agent will eventually make a move): induction on runs and on S{leader - cand(n)| n Î Agent} measuring “distances” of candidates from leader

Refining Leader Election: compute minimal path to leader Goal: refine the leader election algorithm to compute for each agent also a shortest path to the leader, providing a neighbor (except for leader) which is closest to the leader the minimal distance to the leader Idea: enrich cand and proposals by neighbor with minimal distance to leader: nearNeighb: Agent distance: Distance    (e.g. = Nat È{¥}) proposals: PowerSet(Agent x Agent x Distance) Initially      nearNeighbor = self         distance =0

ASM Computing Minimal Path To Leader

Minimal Path Computation: Correctness Proposition: In every distributed run of agents equipped with the ASM computing a minimal path to the leader, eventually for every agent holds: cand=max(Agent)=leader distance=minimal distance of a path from agent to leader nearNeighbor = a neighbor of agent on a minimal path to the leader (except for leader where nearNeighbor=leader) ctl_state = checkProposals proposals = empty Proof (assuming that every enabled agent will eventually make a move): induction on runs and on S{leader - cand(n)| n Î Agent} with side induction on the minimal distances in proposalsFor Max(proposals)

Exercises Refine the CHECK submachine of the leader election ASM by a machine which checks proposals elementwise. Prove that the refinement is correct. Hint: See Reisig op.cit. Fig.32.1 Adapt the ASM for the election of a maximal leader and for computing a minimal path wrt a partial order £ instead of a total order. Reuse the leader election ASM to define an algorithm which, given the leader, computes for each agent the distance (length of a shortest path) to the leader and a neighbor where to start a shortest path to the leader. Hint: See Reisig op.cit. Fig.32.2

"Definition of Async ASMs" Definition of Async ASMs Small Examples Mutual Exclusion Dining Philosophers Multiple Read One Write Network Algorithms Master Slave Consensus Load Balance Leader Election Echo See Reisig 1998, Sect. 33, 77 Phase Synchronization Simple Properties of Async ASMs References

Echo Algorithm : problem statement Goal: Design a distributed algorithm  that guarantees an initiator’s message being broadcast and acknowledged (‘echoed’) through a finite connected network, using only communication between neighbors Algorithmic Idea: the initiator (a distinguished node)  broadcasts an info to all his neighbors and waits for their acknowledgements every node which has been informed by some neighbor (‘parent’) node  informs all his other neighbor nodes and waits for their acknowledgements to come back, to then forward his own acknowledgement back to the parent node

Echo ASM: Agent Signature Agent : connected graph of agents initiator: Agent   distinguished element with control states {broadcast, waitingForEcho, echoArrived} and special ASM Each agent is equipped with: neighb Í Agent                        (external function) informedBy : Agent ® Bool      (abstract message passing) indicating whether a message (with info or acknowledgement) from a neighbor agent has been sent (arrived) parent : Agent               (building a spanning tree for acks) yields a neighbor node who has sent a messg which is to be acknowledged, once all other neighbor nodes have acknowledged  this mssg which has been forwarded to them ctl_state:{listeningToInfo,waitingForAck,informed } Initially initiator in ctl_state = broadcast, for all other agents: ctl_state = listeningToInfo, informedBy everywhere false, parent = undef

Initiator ASM for Echo algorithm

Echo Agent ASM for Agent ¹ Initiator

Async Echo ASM (initiator & agents): Correctness Proposition: In every run of a set of agents including an initiator, all equipped with the corresponding echo ASMs: the initiator terminates (termination) the initiator terminates only when all other agents have been informed about its originally sent mssg (correctness) Proof. Follows by run induction from two lemmas.

Echo ASM (initiator and agents): Correctness Lemma 1. In every run of the async echo ASM, each time an agent executes InformAllOtherNeighbors, in the spanning tree of  agents waitingForAck the distance to the initiator grows until leafs are reached. Proof. By downward induction on echo ASM runs Lemma 2. In every run of the async echo ASM, each time an agent executes InformParentNeighbor, in the spanning tree the distance to the initiator of nodes with a subtree of informed agents shrinks, until the initiator is reached. Proof. By upward induction on runs of the async echo ASM

Exercise Refine the asynch echo ASM to the case of a network with more than one initiator. Hint: Use a pure data refinement, recording the initiator’s identity when informing neighbors and letting the initiator wait for the echo to is own initiative.

"Definition of Async ASMs" Definition of Async ASMs Small Examples Mutual Exclusion Dining Philosophers Multiple Read One Write Network Algorithms Master Slave Consensus Load Balance Leader Election Echo Phase Synchronization See Reisig 1998, Sect. 36 (Fig.36.1), 81 Simple Properties of Async ASMs References

Phase Synchronization : problem statement Goal: Design a distributed algorithm  that guarantees synchronized execution of phases of computations, occurring at nodes of an undirected tree (connected acyclic network), using only communication between tree neighbors Algorithmic Idea: every agent (tree node) before becoming busy in a new phase has to synchronize with its neighbor nodes, moving the synchronization up along the tree structure wait until all agents are waiting for the phase increase to start increase its phase - when the phase shift becomes movable down - and move the phase shift further down along the tree structure until all nodes have become busy in the new phase

Phase Synchronization ASM: Agent Signature Agent : an undirected tree of agents equipped with: neighb Í Agent                   (external function) phase:  the current phase synchPartner, waitPartner: Agent                     yields the neighbor node an agent is synchronized with (in moving the synchronization up or down the tree) resp. waiting for (to reverse the previous upward synchronization downwards) ctl_state :  {busy, waiting } Initially ctl_state = busy,  phase = 0, synchPartner = waitPartner = undef

Slide 53

Phase Synchronization ASM : Correctness & Liveness Proposition: In every infinite run of the asynch phase synchronization ASM: in any state any two busy agents are in the same phase (correctness property) if every enabled agent will eventually make a move, then each agent will eventually  reach each phase (liveness property)

Phase Synch:  PhaseShiftMovableDown Lemma Lemma: For every phase p, whenever in a run a state is reached where for the first time    u.waitPartner(p)=v synchronizes with u in phase p,    every element of       subtree(u,v) Èsubtree(v,u)È{u,v}    is waiting in phase p   where subtree(x,y) = {n| n reachable by a path from                                               x without touching y}

Proof of PhaseShiftMovableDown Lemma Proof of the lemma follows from the following two claims. Claim 1. When Synchronization is moved up in phase(u)=p from busy u to to v=u.synchPartner(p), the elements of subtree(u,v) are waiting, u becomes waiting, and they all remain so until the next application of a Shift rule “MovePhaseShiftDown”. Claim 1 follows by induction on the applications of the Synchronization rule. n=1: true at the leaves n+1: follows by induction hypothesis and Synchronization rule from   subtree(u,v)= Èi<n subtree(ui,u) È {u0,...,un-1} for neighb(u}= {u0,...,un}  with v= un    (by connectedness)

Proof of PhaseShiftMovableDown Lemma Claim 2. For every infinite run and every phase p, a state is reached in which all agents are waiting in phase p and for some agent u its waitPartner in phase p synchronizes with u in phase p. Follows by induction on p.

"Definition of Async ASMs" Definition of Async ASMs Small Examples Mutual Exclusion Dining Philosophers Multiple Read One Write Network Algorithms Master Slave Consensus Load Balance Leader Election Echo Phase Synchronization Simple Properties of Async ASMs References

Analyzing Initial segments of runs of an async ASM Let m be a move of an agent in a run of an async ASM. Let Post(m) = {I| I initial segment & m is maximal in I}. Post (m) represents the multiplicity of states, resulting from the last move m and each depending via s(I) = s(I-{m}) from its “pre”-state. Let Pre(m) = {I-{m}| I Î Post(m) } representing the multiplicity of states in which move m can be performed. Pre(m)-Lemma. Pre(m) has minimal and maximal elements:           min Pre(m) ={m’|m’ < m}      max Pre(m) ={m’|not m’ ³ m}   Pre(m) = {I| I initial segment & min Pre(m) Í I Í max Pre(m) }.     Therefore Pre(m) is closed under union and intersection.

Characterizing Concurrent Moves in Runs of an Async ASM Concurrent-Moves Lemma. In runs of an async ASM, the concurrency (incomparability by the run order) of moves m,m’ of agents is equivalent to any of the following: minPre(m) ÈminPre(m’) Î Pre(m) ÇPre(m’) both moves can come after all the moves which come before any of the two Pre(m) ÇPre(m’) ¹ Æ There exist I,J Î Pre(m) with m’ Î I-J           before one of the moves, the other may be executed or not Proof. If m,m’ are concurrent, then  I = minPre(m) ÈminPre(m’) is an initial segment and minPre(m) ÍI Í maxPre(m), so that I Î Pre(m). By symmetry then I Î Pre(m’). Let J Î Pre(m) ÇPre(m’) and set I = J È{m’}. Then I Î Pre(m). Suppose I,J Î Pre(m) with m’ Î I-J. m’<m would imply m’ Î minPre(m) Í J and thus m’ÎJ.  m<m’ would imply m’ÏmaxPre(m) ÊI and thus m’ÏI. Therefore m, m’ are incomparable, i.e. concurrent.

Conditions for indisputability of terms Sufficient indisputability condition. If t Pre(m) is  not indisputable, then there is a move m’ concurrent with m which may change t. Proof by contradiction. By the Pre(m)-lemma, for every I Î Pre(m) one can reach s(I) from s(minPre(m) )  by applying moves concurrent to m. By assumption none of them may change t, so that Val s(I) (t) = Val s(minPre(m) ) (t). That would mean that t Pre(m) is indisputable. Necessary indisputability condition. If there is a move m’ concurrent with m which must change t, then t Pre(m) is  not indisputable. Proof . By the concurrent-moves lemma, there is a common initial segment I Î Pre(m) ÇPre(m’). Then also I È{m’} Î Pre(m), and since m’ must change t, I and I È{m’} have different values for t.

Stability and change of term values in initial segments Extending term evaluation from states to state sets: Val Pre(m) (t) =  c if all initial segments in Pre(m) have the same value c for t: " I Î Pre(m): Val s(I) (t) = c    We then say that Val Pre(m) (t) is indisputable, writing also that  t Pre(m) (or its value) is  indisputable  Val Pre(m) (t) =  undef otherwise Defn: move m may change the value of t iff m changes the value of t in some linearization of the given run, formally:              for some I Î Pre(m): Val s(I) (t) ¹ Val s(I È{m} ) (t) Defn:  m must change the value of t iff m changes the value of t in every linearization of the given run, formally:              for every I Î Pre(m): Val s(I) (t) ¹ Val s(I È{m} ) (t)

Moves with indisputable different term values compare Lemma. If the values of t Pre(m) and of  t Pre(m’) are different but both indisputable, then m and m’ are not concurrent but compare in the run order (i.e. m<m’ or m’<m). Proof. If t Pre(m) and  t Pre(m’) are indisputable and m,m’ are concurrent, then by the concurrent-moves lemma there is a common initial segment I Î Pre(m) ÇPre(m’) so that t Pre(m) =Val s(I) (t) = t Pre(m’)

Focused Terms Defn: A term t is focused in a given run if any move which may change its value must change it. Sufficient Condition for Focus. If the value of a term t may be changed only by one agent a, then it is focused. Proof. It suffices to show that t Pre(m) is indisputable because then t Post(m) is also indisputable, and the assumption that only a may change the value of t implies:  t Post(m) is different from t Pre(m) iff m changes t     By the sufficient indisputability condition, t Pre(m) is indisputable because moves concurrent to m must be moves of other agents than a, therefore by assumption none of them may change t. Synchronization Lemma. For a focused term t, t Pre(m) is indisputable iff , in the given partial order, m compares with all moves which change the value of t. Proof: follows from the indisputability and focus conditions.

References W.Reisig: Elements of Distributed Algorithms Springer-Verlag 1998 Y. Gurevich and D. Rosenzweig: Partially Ordered Runs: A Case Study. In: Abstract State Machines. Theory and Applications. (Ed. Y.Gurevich et al). Springer LNCS 1912, 2000, 131-150 E. Börger, R. Stärk: Abstract State Machines.  A Method for High-Level System Design and Analysis Springer-Verlag  2003, see  http://www.di.unipi.it/~AsmBook