A scheduler for SCADA-based multi-source fusion systems

A scheduler for SCADA-based multi-source fusion systems Rafael Corchuelo ∗, Miguel Toro University of Seville, ETSI Informática, Avda. Reina Mercedes s/n, Sevilla E-41012, Spain Keywords: Multi-source fusion SCADA systems Schedulers a b s t r a c t In this article, we report on our experience regarding devising, implementing, and deploying a scheduler for multisource fusion in the context of SCADA systems (Supervisory Control and Data Acquisition). They are challenging because they commonly rely on low-end boards with very limited computing, memory, and storage capabilities, but have to run hundreds if not thousands of agents that co-ordinate by means of complex multi-way rendezvouses. Our work was carried out in the context of a solar plant in which we could easily confirm that not scheduling the rendez-vouses fairly may easily drive the system into as many as 3 779.10 critical-failure states per hour, whereas a straightforward solution to the problem can reduce the figure to 1 094.76 critical-failure states per hour. Unfortunately, that is far from zero, which is the ideal number. In the literature, there are several proposals to deal with this problem, but most of them could not be adapted to our context, namely: some of them can deal with two-way rendez-vouses only, whereas ours involve an average of 12.89 agents; others require to instrument the agents, but many of them are hardware devices that cannot be modified; a few others cannot work with rendez-vouses that can get intermittently enabled and disabled along an execution, which makes them of little interest in our context; and some require to use shared memory, which is an advanced hardware feature that is not supported by our low-end computing boards. The two proposals that we managed to adapt were not efficient enough in our context since they led to an average of 1 102.77 and 1 458.65 criticalfailure states per hour, respectively. That motivated us to work on a new proposal that does not have any of the previous problems. It relies on a incremental approach that was implemented very efficiently using bounded counters and queues. Furthermore, the experimental results and the corresponding statistical analysis confirm that it works very well in practice. 1. Introduction We work in the context of multi-source fusion systems that support industrial production plants. Such systems are commonly supported by Supervisory Control and Data Acquisition (SCADA) systems [8] that run a collection of agents that work co-ordinately so that the plants work safely and productively. The agents can be sensors, which are devices that sense the physical world and produce data, processors, which apply rules to the data in order to make decisions regarding which actions must be performed, and actuators, which perform the selected actions in the physical world. Such fusion systems have some common features, namely: a) Typically, several sensors, processors, and actuators must co-ordinate in order to carry out a single piece of work. This implicitly requires implementing multi-way co-ordination protocols that are far more involved than in the case of two agents. b) Furthermore, the sensors and the actuators are hardware devices that communicate by means of standardised protocols, which means that the chances that they can be instrumented ∗ Corresponding author. E-mail addresses: [email protected] (R. Corchuelo), [email protected] (M. Toro). are very scarce. Instrumentation refers to changing the code of an agent so that it can be integrated into a new framework. c) In addition, the same agent may require co-ordination with several independent groups of agents, which implies that they must make decisions that do not neglect any of the groups too often because that might easily result in critical-failure states. d) Another issue is that the computing boards on which they run are very simple; in particular, it is not generally expected that they can provide shared memory. e) Last, but not least, their computing, memory, and storage capabilities are very scarce, which is not commonly due to budget constraints, but technical problems and verification requirements [39] . Remote-method invocation is the de-facto standard used in the context of SCADA systems. It is very adequate in cases in which the interactions amongst the agents can be easily implemented by means of message-passing protocols. Unfortunately, the complexity of the protocols increases as the number of agents involved in a piece of co-ordinated work increases. For instance, think of a system in which there are several actuators that must open or close some pumps depending on the decisions that they gather from several processors that need data from several sensors. Implementing a protocol that co-ordinates this piece of work is far from trivial and the result is not commonly simple to verify and test. Using a standard rendez-vous library helps abstract away from the details involved in the co-ordination and focus on the work to be done. Open MPI [33,40] is a well-known library in this context, but there are others that are specifically tailored for web services [15,27], reconfigurable systems [52], integration technologies [18–20], or Java systems [32]. Rendez-vouses help raise the level of abstraction, which is very appealing. Unfortunately, our experience proves that the scheduler must be carefully designed so that every rendez-vous that is enabled sufficiently often is executed sufficiently often since, otherwise, the system may easily enter critical-failure states. In our experimental study, we confirmed that a scheduler that does not take the problem into account may lead to as many as 3 779.10 critical-failure states per hour; we also confirmed that a straightforward solution can reduce the figure to 1 094.76 critical-state failures per hour, which is still very far from zero. A critical-failure state is a situation in which a part of the system is not working well. If such a state lasts for too long, then the system might malfunction, which may result in serious component damage, production interruptions, environmental pollution, or human injuries, just to mention a few common problems. Such states are typically due to a component that is malfunctioning (e.g., faulty sensors or actuators, or processors that work wrongly due to faulty boards, network failures, or wrong rules), but also due to actuators that do not perform their actions timely due to scheduling problems, which is our focus in this article. When the system enters such a state, the engineers get an alarm and execute an automated recovery procedure first; if it does not work, then the engineers override the system and try to keep it under control. If no solution is found, then the system is stopped and reset, which results in production interruptions and business losses. The previous problem is related to a liveness property called fairness [16,25,34,53]. In the literature, there are many proposals to enforce fairness, but most of them cannot be adapted to our context: some proposals were designed to deal with two-way rendez-vouses only [3,5,35,49,56,57,60], but typical rendez-vouses in our context coordinate many more agents; others require to instrument the agents to build a scheduler into them [1,4,7,10,26], which can only be simulated by means of wrappers that are not generally possible to implement in low-end computing boards; some of them [4,7] cannot deal with rendezvouses that get intermittently enabled or disabled along an execution, which hinders applying them to our context; and some of them require to use shared memory [42], which is an advanced hardware feature that is not available in low-end computing boards. There are two proposals that could be adapted [30,45], but our experimental analysis confirms that they are not efficient enough in our context because they drove our experimental system into as many as 1 102.77 and 1 458.65 criticalfailure states per hour, respectively. In this article, we report on the design of a scheduler for multi-source fusion systems that are supported by SCADA systems. We introduce it at a high level of abstraction that helped us prove that it is correct and complete; we also delve into how to implement it efficiently using bounded counters and queues, which is accompanied by a detailed study on the impact on correctness, completeness, time complexity, and space complexity; we deployed our proposal to a solar plant and performed a series of experiments that confirm that it is able to run the system without entering any critical-failure states; the intuitive conclusions were confirmed to be statistically sound using a well-established statistical method. The rest of the article is organised as follows: Section 2 presents the related proposals and compares them to ours, Section 3 presents the scheduler, Section 4 delves into its implementation, Section 5 reports on the experimental analysis, and, finally, Section 6 summarises our conclusions. 2. Related work In this section, we present the related work. First, we summarise the literature and then discuss on the problems that motivate our work. 2.1. Summary of the literature We have found several architectures that were specifically designed to support distributed multi-source fusion systems, namely: Wang et al. [54] presented an architecture that arranges agents into four layers: a sensor driver layer, a logical sensor layer, a fusion unit layer, and a task unit layer; Lyu et al. [38] , presented a three-layer architecture in which sensors are deployed to the bottom layer and report to a gateway layer that keeps the processors in the application layer away from their peculiarities; de Alba et al. [13] presented an architecture in which processors are implemented in a distributed blackboard that helps them work co-ordinately; and Rodríguez et al. [44] devised a similar architecture that was implemented using an agent-oriented platform. The previous articles implicitly assume that there is a scheduler that is provided by the underlying implementation platform. Our focus is on the design of such a scheduler in a context in which computing power, memory, and storage are scarce and fairness must be enforced to prevent the system from entering critical-failure states. Fairness is a liveness property that basically requires the scheduler to make decisions that allow both the system and its individual components to progress as quickly as possible [16,25,34,53] . Olderog and Apt [42] set the foundations to enforce fairness by means of a scheduler for non-deterministic multi-choice commands. Their idea was to augment each thread with a collection of local counters that track how many times each alternative in a multi-choice command may be neglected in spite of being enabled. This simple idea set the foundation for many succeeding proposals, including ours. The idea to enforce fairness using a scheduler was soon adopted in the context of distributed systems [48] , where fairness is used to ensure that no resource remains idle forever or that no agent can starve forever. In the context of information fusion, there are some proposals that focus on resources that can be accessed by means of specificpurpose IoT networks [38,47] or general-purpose communication networks [11,23,36,46,50] ; there are also some proposals that deal with arbitrary resources [3,5,35,49,56,57,60] . Regarding agents, there are several proposals that focus on allocating them to the data centres [12] , the machines [22,31,41,55,58,59] , or the cores [14,24,43] that have more computing power available, since this helps prevent starvation. The previous proposals were devised in the context of systems whose agents interact by means of remote-method invocations. The problem is far more involved when the agents interact by means of rendezvouses, chiefly if they co-ordinate more than two agents, aka. multiway rendez-vouses. The subject of fairness in the previous proposals are the resources or the agents; in our context, the subject is a set of rendez-vouses: guaranteeing that they are executed fairly is the cornerstone to guaranteeing that the agents can progress. Francez and Forman [17] adapted Olderog and Apt’s [42] proposal to this context. Some authors soon started to work on solutions that do not require any shared memory. Unfortunately, this research path was not straightforward because Tsay and Bagrodia [51] proved that no scheduler can guarantee fairness unless the agents ready only one rendez-vous stochastically, arbitrary delays can be introduced in the presence of a rendez-vous that is known to be enabled, or every computational step in every agent can be controlled by the scheduler. (Joung [29] characterised the exact subset of topologies in which these impossibility results hold.) The first research path was explored by Joung [30] , the second one was explored by Ruiz et al. [45] , but, to the best of our knowledge, nobody has explored the third one since it does not seem realistic. Recently, André et al. [1] , Bensalem et al. [4] , Bonakdarpour et al. [7] , Brook et al. [10] , and Jongmans and Arbab [26] have focused on enforcing fairness by instrumenting the agents so that a distributed scheduler is built into them. 2.2. Discussion A good solution to implement a scheduler for multi-source fusion systems that are supported by SCADA systems must fulfil the following requirements: –It must support multi-way rendez-vouses. We need a solution that supports both two-way and multi-way rendez-vouses since the latter are very common in our context. For instance, in our experimental analysis we dealt with a system in which the rendezvouses co-ordinate an average of 12.89 agents. –It must not require to instrument the agents. We need a solution that does not rely on instrumentation since the sensors and the actuators are black boxes that are provided by third-party vendors. The reader might argue that they might be wrapped using proxies that simulate the instrumentation; although that solution makes sense in a general context, it is not appropriate in our context because the proxies must be deployed to additional computing boards or share the existing computing boards with the processors. –It must implement a strong fairness notion. Some authors have worked on a weaker notion of fairness that is not as stringent as ours. Instead of requiring a rendez-vous to be enabled from time to time, they require the rendez-vouses to be permanently enabled from a specific point in the execution onwards, which is far too restrictive in our context. –It must not require any shared memory. We need a solution that does not require any shared memory, since the usual hardware that is available in our context does not support this feature. –It must be efficient in terms of both time and space. We need a solution with a low time and space complexity due to the small computing, memory, and storage capabilities of the hardware used in our context. The proposal by Olderog and Apt [42] does not deal with multi-way rendez-vouses, but multi-choice commands; this means that it provides a foundation, but adapting it, if possible, is not straightforward. Unfortunately, it requires to instrument the source code of the agents to which it is applied, which is not possible in a context in which sensors and agents are black boxes provided by third parties; it also requires shared memory, which is not available in our context; furthermore, the proposal requires to know the status of each alternative before making a decision on which must be executed, which is not efficient enough. The proposals that focus on resource that are connected through a communications network [11,23,36,38,46,47,50] do not seem easy to adapt because they depend on a variety of parameters that are highly dependent on the network and difficult to extrapolate to other contexts, e.g., signal strength or waveform. The proposals that focus on general resources [3,5,35,49,56,57,60] might be applicable by mapping each rendez-vous onto a shared resource for which the agents have to compete; the problem is that they were not designed to deal with resources that must be shared by two or more agents. The proposals that focus on agents [12,14,22,24,31,41,43,55,58,59] are not applicable because their goal is to guarantee that agents can progress by allocating them to the computing devices that have more computing power available, independently from whether they co-ordinate or not with others; in these proposals, an agent that is readying a rendez-vous is considered to be waiting for input/output, which excludes it from the collection of agents whose progress must be guaranteed. The adaptation of Olderog and Apt’s [42] proposal by Francez and Forman [17] can deal with multi-way rendez-vouses, but it requires to instrument the agents, which is not possible in our context in the case of sensors and actuators, and it requires to know the status of every rendezvous before making a decision on which must be executed, which is inefficient. The stochastic approach by Joung [30] might be used, but our experimental results prove that it is far too inefficient in our context; furthermore, it cannot deal with systems in which a single agent can stop executing naturally (i.e., it was programmed to work for a finite period of time only) or systems in which an agent increases its execution time monotonically (e.g., an agent that processes a log in a non-incremental manner). The approach by Ruiz et al. [45] might also be used in our context, but our experimental results also prove that it is not efficient enough because it requires to perform some global computations that are costly and it periodically requires to freeze the whole system to know the status of every rendez-vous. The recent proposals by André et al. [1] , Bensalem et al. [4] , Bonakdarpour et al. [7] , Brook et al. [10] , and Jongmans and Arbab [26] also require to instrument the agents to build a distributed scheduler into them, which is not generally possible in our context due to the limitations of the computing boards; furthermore, Bensalem et al.’s [4] and Bonakdarpour et al.’s [7] proposals deal with a weaker level of fairness that cannot deal with rendez-vouses that get enabled or disabled depending on the logic of the system. Summing up: none of the proposals in the literature seems to be appropriate in our context, which motivated us to work on a new one. 3. The scheduler In this section, we describe the scheduler. First, we present some preliminaries, then describe the proposal, and finally prove that it is correct and complete. 3.1. Preliminaries Our preliminaries focus on the mathematical foundations and some fundamental concepts regarding systems, executions, and fairness. Definition 1 (Mathematical foundations) . A transition is a tuple of the form 𝐶 1 𝑒 ⟶𝐶 2 , where C 1 denotes a source configuration, C 2 denotes a target configuration, ⟶denotes a transition relation on configurations, and e denotes the event that fires the transition from the source to the target configuration. A configuration is a tuple that models the data and the execution state of a system. A transition chain is a sequence of transitions of the form ⟨𝐶 𝑖 𝑒 𝑖 +1 ⟶𝐶 𝑖 +1 ⟩𝑖 ≥ 0 . We use notation ∃∞x : P ( x ) to mean that there are infinitely many values of x that satisfy predicate P . A map is a correspondence amongst the elements of two sets; we represent them using notation { 𝑘 𝑖 ↦𝑣 𝑖 } 𝑛 𝑖 =1 , where { 𝑘 1 , 𝑘 2 , …, 𝑘 𝑛 } is the domain of the map and { 𝑣 1 , 𝑣 2 , …, 𝑣 𝑛 } is its range ( n ≥ 0). If ≤ is an order on the range of map 𝜇, then 𝜇 denotes its flattening, which is defined as a reordering of the domain such that 𝜇( 𝜇( 𝑖 )) ≤ 𝜇( 𝜇( 𝑖 + 1)) , for every 1 ≤ i < n, n ≥ 0); simply put: 𝜇 sorts the domain of map 𝜇according to its range. We use RND to denote a random variable that is uniformly distributed in the set of natural numbers. Definition 2 (Systems) . A system is a tuple ( R, A ), where R denotes a set of rendez-vouses and A denotes a set of agents. A rendez-vous is a component that allows several agents to exchange data co-ordinately; they have a state that is composed of variables that the agents that coordinate on them can read and/or write. Rendez-vouses that co-ordinate only two agents are referred to as two-way rendez-vouses, whereas rendez-vouses that co-ordinate more than two agents are referred to as multi-way rendez-vouses. An agent is a component that consumes and/or produces the data that are exchanged through the rendez-vouses; the agents can be further classified as sensors, which sense the physical world and write data to the rendez-vouses, processors, which read data from the rendez-vouses, process them, and write the results to the rendez-vouses, and actuators, which read data from the rendez-vouses and perform actions in the physical world. Agents execute scripts that can either perform some local computation, ready some rendez-vouses, or execute a rendez-vous (which allows it to perform co-ordinated computations). There are a variety of technologies available to write the scripts [15,18–20,27,32,40,52]. An agent may ready several rendezvouses at the same time, but only one of them may be selected for execution because agents are single-threaded in our context. Remark 1. Multi-source information fusion is a process that combines data from many sources to produce an output that is somewhat useful. The previous idea fits our model perfectly: data are gathered from the physical world using sensors, they are processed using processors that produce an output, which is fed into some actuators that perform actions. Our model assumes that the agents co-ordinate by means of rendez-vouses, which can co-ordinate two or more agents. We are interested in multi-source fusion systems that are supported by SCADA systems [8]. (SCADA stands for Supervisory Control and Data Acquisition.) Such systems are commonly used to monitor and control the individual components of industrial plants in fields as diverse as telecommunications, water and waste control, oil and gas refining, transportation, or energy, just to mention a few examples. Typical SCADA systems are composed of sensors and actuators that are provided by different vendors and processors that are implemented in-house. The sensors and the actuators are very commonly implemented as black-box devices that communicate by means of standardised protocols; simply put: the chances that they can be instrumented are scarce (by instrumentation we mean changing their source code so as to adapt them to specific purposes). The processors are commonly deployed to low-end computing boards that provide very little computing power (in the range of a few MIPS), memory (in the range of a few KiB), or storage (in the range of a few hundreds of KiB). Definition 3 (Executions). We assume that the operational semantics of the technology used to implement a system was defined by means of a transition relation ⟶ on configurations of the form ( 𝑎1 , 𝑎2 , … , 𝑎𝑛 , 𝑟1 , 𝑟2 , … , 𝑟 𝑚 ), where each ai denotes the data and the execution state of an agent and each rj denotes the data and execution state of a rendez-vous ( n ≥ 0, m ≥ 0, 1 ≤ i ≤ n, 1 ≤ j ≤ m ). An execution of a system is a transition chain of the form ⟨𝐶 𝑖 𝑟 𝑖 +1 ⟶𝐶 𝑖 +1 ⟩𝑖 ≥ 0 , which indicates that rendez-vous 𝑟 𝑖 +1 is executed to transition from configuration C i to configuration 𝐶 𝑖 +1 ( i ≥ 0). A rendez-vous is said to be enabled if every agent that can ready it is readying it; we use notation enabled ( r, C ) to denote that rendez-vous r is enabled in configuration C . Definition 4 (Fairness) . Fairness is a liveness property that requires that no rendez-vous that is enabled from time to time in an execution is executed finitely many times (possibly never). Formally speaking, execution ⟨𝐶𝑖 𝑟 𝑖 +1 ⟶𝐶 𝑖 +1 ⟩𝑖 ≥ 0 is fair as long as ∀𝑟 ∶ (∃∞𝑖 ∶ 𝑒𝑛𝑎𝑏𝑙𝑒𝑑( 𝑟, 𝐶 𝑖 )) ⇒ (∃∞𝑖 ∶ 𝑟 = 𝑟 𝑖 ) . In the literature, there are some authors who consider a weaker notion that requires that no rendez-vous that is enabled permanently from a configuration onwards is executed finitely many times. Formally speaking, the previous execution is weakly fair if ∀𝑟 ∶ (∃𝑘 ∶ ∀𝑖 ≥ 𝑘 ∶ 𝑒𝑛𝑎𝑏𝑙𝑒𝑑( 𝑟, 𝐶 𝑖 )) ⇒(∃∞𝑖 ∶ 𝑟 = 𝑟 𝑖 ) . We focus on the initial formulation since it is more general and stringent [16] . Remark 2. The notion of fairness is intimately related to the idea of infiniteness. The systems in which we are interested are designed to work twenty-four hours a day, seven days a week. Theoretically, their executions are infinite; for practical purposes that means that their lengths are not bounded by any pre-defined constant. Implementing fairness is challenging insofar the scheduler must guarantee that no rendez-vous that is enabled from time to time is executed finitely many times (possibly never). Note that one cannot check the previous property in finite time just taking a look at a partial execution. One the contrary, one must prove that the scheduler cannot produce any unfair executions by means of a theoretical analysis that commonly relies on a reductio ad absurdum argument. That is: one must assume that the scheduler may produce an unfair execution and then find a sequence of entailments that result in contradictions. In practice, enforcing fairness is appealing because it helps give every rendez-vous that is enabled from time to time a fair chance to be executed. In our context, this is particularly important in order prevent the system from entering critical-failure states that might result in disaster. Example 1. Fig. 1 provides an excerpt from the definition of the system that we used in our experimental analysis. The actual system has 10 158 sensors of 321 different types, 124 processors of 97 different types, 2 034 actuators of 112 different types, and 215 rendez-vouses that co-ordinate 12.89 agents in average. Thus, the example focuses on a tiny part that exhibits a common co-ordination pattern that allows us to illustrate many of the core concepts. Fig. 1 .a sketches the scripts that are executed by a specific type of sensor, a specific type of processor, and a specific type of actuator when they co-ordinate on a collection of rendez-vouses of a specific type. Fig. 1 .b sketches an instantiation of this system with three sensors, three processors, three actuators, and three rendez-vouses. We implicitly assume that there is a loader that instantiates the agents and the rendez-vouses and distributes them according to a predefined topology; we also assume that the loader provides an integer index to each agent or rendez-vous, which is passed as parameter i to the corresponding scripts. The sensor script consists in a loop that senses data from the physical world and immediately readies rendez-vouses RV ( i ) and 𝑅𝑉 ( 𝑖 + 1) in order to send the data to agents that can also ready these rendezvouses (we implicitly assume that 𝑖 + 1 is computed modulo the number of rendez-vouses in the system). The processor script consists in a loop that readies rendez-vous RV ( i ); when it is executed, the script reads the data sent by the corresponding sensor, applies a rule to compute an action, and writes the action to the rendez-vous. The actuator script also consists in a loop that first readies rendez-vous RV ( i ) and then performs the action that it reads from that interaction. Recall that the script of the sensors and the actuators is built in the corresponding hardware devices; one can only configure the rendez-vouses to which they broadcast their data or the rendez-vouses from which the actuators read them. Note how simple it is to specify such a complex system using rendezvouses since each of them encapsulates the protocol required to synchronise multiple entities so that they can exchange data co-ordinately. This sample system sketches a pattern that is very common in practice: three different agents need to co-ordinate (a sensor, a processor, and an actuator) and there are some agents that may ready several rendez-vouses in order to provide their data to different agents (the sensors). Realise that this is an instance of the well-known Dining Philosophers problem; the reader can consult any textbook on distributed algorithms to realise how difficult it is to implement a solution to this problem using a protocol that relies on remote-method invocation [37] . Note, too, that a solution in which the sensors or the processors buffer data is not possible because of the tiny amount of memory or storage that is available in our context. In such a context, only a piece of data can be stored and it must be distributed to the agents that are interested in it at a specific point in time. Missing some data is not important as far as the system executes fairly. Unfortunately, our experiments prove that fairness does not happen naturally and must then be enforced by the scheduler, cf. Section 5 . For instance, an execution of the previous system in which rendez-vouses RV (1) and RV (2) are executed intermittently and rendez-vous RV (3) is never executed happens too often in practice, which may easily drive the system into critical-failure states. 3.2. Description Our proposal works as follows: the scheduler associates a priority with every rendez-vous; the priority is a counter that indicates the number of times that a rendez-vous may be rejected for execution despite it is enabled; the scheduler arranges the rendez-vouses in a sequence in decreasing priority order (the smaller a counter, the higher the priority); it then searches the sequence for the first rendez-vous that is enabled; if it does not exist, then the system terminates; if it exists, then it is executed and its priority is reset to a random natural value, whereas the Fig. 1. Sketch of a sample system. priorities of the rendez-vouses before it are kept and the others are increased by one. The key is that the scheduler needs to find only the first enabled rendez-vous in decreasing order of priority; the other rendezvouses may be enabled or disabled, but the scheduler guarantees that they will be executed if they are enabled from time to time. To formalise this idea, we need to generalise the transition relation ⟶that defines the operational semantics of our systems so that it works on extended configurations of the form ( C, 𝜌), where C denotes a configuration of the system and 𝜌is a map that associates a priority with each rendez-vous. In the initial configuration, we assume that the state of every agent and rendez-vous is initialised to default values. We also assume that the initial priority map is initialised so that every rendezvous gets a priority using random variable RND . After that, the system executes according to the following inference rule: 𝐶 𝜌( 𝑘 ) ⟶𝐶 ′ ∀1 ≤ 𝑖 < 𝑘 ∶ ¬𝑒𝑛𝑎𝑏𝑙𝑒𝑑( 𝜌( 𝑖 ) , 𝐶) 𝑒𝑛𝑎𝑏𝑙𝑒𝑑( 𝜌( 𝑘 ) , 𝐶) ( 𝐶 , 𝜌) 𝜌( 𝑘 ) ⟶( 𝐶 ′, 𝑢𝑝𝑑𝑎𝑡𝑒 ( 𝜌, 𝑘 )) The rule has three antecedents and a consequent. The first antecedent requires that the system can transition from configuration C to configuration C ′ by executing rendez-vous 𝜌( 𝑘 ) , for some k ; the second antecedent constraints the value of k so that no rendez-vous in 𝜌 in a position before k is enabled; the third antecedent requires the rendezvous at position k in 𝜌 to be enabled. Summing up, the antecedents of the inference rule constraint k so that it denotes the position in 𝜌 of the first enabled rendez-vous, if any. The consequent states that if such a k exists, then the system can transition from configuration C to configuration C ′ , but the priorities must be updated as follows: upda te ( 𝜌, 𝑘 ) = { 𝑟 ↦𝜌( 𝑟 ) ∣∃1 ≤ 𝑗 ≤ 𝑘 − 1 ∶ 𝑟 = 𝜌( 𝑗 ) } ∪ { 𝑟 ↦RND ∣𝑟 = 𝜌( 𝑘 ) } ∪ { 𝑟 ↦𝜌( 𝑟 ) − 1 ∣∃𝑘 + 1 ≤ 𝑗 ≤ |𝜌|∶ 𝑟 = 𝜌( 𝑗 ) } Simply put: the update keeps the priority of the rendez-vouses before position k , resets the priority of the selected rendez-vous, and increases the priority of the other rendez-vouses. 3.3. Correctness Proving that the scheduler is correct amounts to proving that it cannot generate any unfair executions. Theorem 1 (Correctness) . The scheduler does not generate any unfair executions. Proof. We proceed by reductio ad absurdum. Assume that the scheduler generates the following execution: 𝜆= ⟨( 𝐶 𝑖 , 𝜌𝑖 ) 𝑟 𝑖 +1 ⟶( 𝐶 𝑖 +1 , 𝜌𝑖 +1 ) ⟩𝑖 ≥ 0 If 𝜆is unfair, that means that there must exists a rendez-vous r that is enabled from time to time in 𝜆, but it is executed finitely many times only (possibly never). Let R denote the set of rendez-vouses. It can be partitioned into R 1 , which has the rendez-vouses that are executed finitely many times in 𝜆, and R 2 , which has the rendez-vouses that are executed infinitely many times. There must exist a configuration ( C z , 𝜌z ) ( z ≥ 0) such that it is the last configuration in 𝜆that is reached by executing a rendez-vous in R 1 . Consider now a succeeding transition of the following form: ( 𝐶 𝑖 , 𝜌𝑖 ) 𝑟 𝑖 +1 ⟶( 𝐶 𝑖 +1 , 𝜌𝑖 +1 ) ( 𝑖 ≥ 𝑧 ) Assume that 𝜌𝑖 is of the form ⟨𝑟 1 , …, 𝑟 𝑞−1 , 𝑟 𝑞 , 𝑟 𝑞+1 …, 𝑟 𝑛 ⟩. Assume, too, that the neglected rendez-vous is r q . If neither 𝑟 1 , 𝑟 2 , …, 𝑟 𝑞−1 are enabled, this is contradictory because the scheduler would have checked them and would have selected 𝑟 = 𝑟 𝑞 for execution since it is the first enabled rendez-vous in 𝜌𝑖 . Consequently, there must exists an index p (1 ≤ p < q ) such that r p is the first enabled rendez-vous in 𝜌𝑖 , i.e, 𝑟 𝑝 = 𝑟 𝑖 +1 . +1 This means that when rp is executed, 𝜌i is updated before reaching configuration ( 𝐶𝑖 +1, 𝜌𝑖 +1 ) so that the counter of the preceding rendez-vouses remain unchanged whereas the counter associated with rp is assigned a random natural value (possibly zero), and the counters associated with the rest, including rq , are decreased by one. Realise that the counters of the rendez-vouses before rp are reset to random natural values or remain constant every time that they are checked, whereas the counter of rendez-vous rq is decreased by one every time that it is not checked. Then, there must exist a configuration ( Cs , 𝜌s ) (s ≥ z) such that rq is enabled and 𝜌s (r q ) must be necessarily the minimum counter in that configuration. Consequently, rq is the first rendez-vous in 𝜌𝑠 and must have been selected for execution in that configuration, which concludes the proof. □ 3.4. Completeness Proving that the scheduler is complete amounts to proving that it can generate the whole set of fair executions, which we do in two steps: first, we introduce a lemma that proves that every execution of a system can be characterised with a series of priority maps in which the rendez-vous that is executed in each transition has priority one; next, we prove that the scheduler can generate executions with such priority maps, which renders it complete. Lemma 1 (A characterisation of priority maps). Let 𝜆 be a fair execution of the following form: 𝜆 = ⟨ ( 𝐶𝑖 , 𝜌𝑖 ) 𝑟𝑖 ⟶ ( 𝐶 𝑖 +1 , 𝜌𝑖 +1 ) ⟩𝑖 ≥ 0 The following is a characterisation of the priority maps in which the rendez-vous that is executed in each transition has priority one: 𝜌𝑖 ( 𝑟 ) = ⎧ ⎪ ⎪ ⎨ ⎪ ⎪ ⎩ min { 𝑗 ≥ 𝑖 ∣𝑟 = 𝑟 𝑗+1 } − 𝑖 + 1 if ∃𝑠 ≥ 𝑖 ∶ 𝑟 = 𝑟 𝑠 +1 max { 𝑗 ≥ 𝑖 ∣𝑒𝑛𝑎𝑏𝑙𝑒𝑑( 𝑟, 𝐶 𝑗 )} − 𝑖 + 1 if (∄𝑠 ≥ 𝑖 ∶ 𝑟 = 𝑟 𝑠 +1 ) ∧ (∃𝑠 ≥ 𝑖 ∶ 𝑒𝑛𝑎𝑏𝑙𝑒𝑑( 𝑟, 𝐶 𝑠 )) 0 otherwise Proof. The intuition behind the definition is as follows: 1. Case 1: rendez-vous r is eventually executed from configuration ( C i , 𝜌i ) onwards. In this case, the value assigned to 𝜌i ( r ) is the number of configurations between ( C i , 𝜌i ) and the first succeeding configuration, including ( C i , 𝜌i ), in which r is executed. 2. Case 2: rendez-vous r is eventually enabled but never executed. In this case, the value assigned to 𝜌i ( r ) is the number of configurations between ( C i , 𝜌i ) and the configuration in which r is enabled for the last time, which might also be ( C i , 𝜌i ). 3. Case 3: rendez-vous r is never enabled from configuration C i onwards. In this case, we define 𝜌𝑖 ( 𝑟 ) = 0 . The proof is straightforward: the rendez-vous that is executed in each transition falls within Case 1, so 𝜌𝑖 ( 𝑟 𝑖 +1 ) = min { 𝑗 ≥ 𝑖 ∣𝑟 = 𝑟 𝑗+1 } − 𝑖 + 1 = 𝑖 − 𝑖 + 1 = 1 ; note, too, that the only smaller counter is zero, but according to the definition, this value is assigned to rendez-vouses that are never again enabled. Thus, the rendez-vous executed in each transition has priority one. □ Theorem 2 (Completeness) . The scheduler can generate the whole set of fair executions of a system. Proof. Our goal is to prove that the scheduler can generate executions in which the priority map in each configuration is characterised by the previous lemma. Consider any transition of the following form: ( 𝐶 𝑖 , 𝜌𝑖 ) 𝑟 𝑖 +1 ⟶( 𝐶 𝑖 +1 , 𝜌𝑖 +1 ) ( 𝑖 ≥ 0) Configuration ( C 0 , 𝜌0 ) is special since it must be constructed by means of a procedure that initialises the data and execution state of every agent and rendez-vous and also initialises the priority map to random natural numbers. That is, nothing prevents the scheduler from generating a priority map as characterised by the previous lemma. Thus, we have to focus on the succeeding transitions. In a configuration ( C i , 𝜌i ) ( i ≥ 1), 𝜌𝑖 has the following structure: 𝜌𝑖 = ⟨ 𝜌𝑖 ( 𝑟 )=0 ⏞⏞⏞⏞⏞⏞⏞⏞⏞ 𝑟 1 , …, 𝑟 𝑧 −1 , 𝜌𝑖 ( 𝑟 )=1 ⏞⏞⏞⏞⏞⏞⏞⏞⏞ 𝑟 𝑧 , …, 𝑟 𝑧 + 𝑝 , 𝜌𝑖 ( 𝑟 ) > 1 ⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞ 𝑟 𝑧 + 𝑝 +1 , …, 𝑟 𝑛 ⟩( 𝑧 ≥ 1 , 𝑝 ≥ 0) That is, there can be 𝑧 − 1 initial rendez-vouses whose priority equals zero, next 𝑝 + 1 rendez-vouses whose priority equals one, and then 𝑛 − 𝑧 − 𝑝 rendez-vouses whose priority is greater than one ( 𝑧 − 1 ≥ 0 , 𝑝 + 1 ≥ 1 , 𝑛 − 𝑧 + 𝑝 ≥ 0) . Therefore, there are three cases to analyse: 1. Case 𝑟 ∈{ 𝑟 1 , 𝑟 2 , …, 𝑟 𝑧 −1 } : the rendez-vouses whose priority is zero are not enabled in ( C i , 𝜌i ) or any succeeding configuration. Otherwise, we can apply the first or the second case of the definition of 𝜌i and they both lead to counters greater than or equal to one. Therefore, if these rendez-vouses are permanently disabled from configuration ( C i , 𝜌i ) onwards, then 𝜌𝑖 +1 ( 𝑟 ) = 0 , which is consistent with the update that the scheduler performs because it does not modify the counters that are associated with the disabled rendez-vouses at the beginning of 𝜌𝑖 . 2. Case 𝑟 ∈{ 𝑟 𝑧 , 𝑟 𝑧 +1 , …, 𝑟 𝑧 + 𝑝 } : the executed rendez-vous belongs to the set of rendez-vouses whose priority equals one, so it is one of the rendez-vouses in this case. We can assume that r z is selected for execution because any arrangement of the rendez-vouses with the same priority is valid according to the definition of the scheduler. Thus, there are two sub-cases: (a) Case 𝑟 = 𝑟 𝑧 : in this case, 𝜌𝑖 +1 ( 𝑟 ) ≥ 0 , which is consistent with the update performed by the scheduler since it resets the counter of rendez-vous r to a random natural value. (b) Case 𝑟 ∈{ 𝑟 𝑧 +1 , …, 𝑟 𝑧 + 𝑝 } : in this case, the scheduler decreases the counter associated with r by one, so we need to prove that 𝜌𝑖 +1 ( 𝑟 ) = 0 , which indicates it will be permanently disabled from configuration ( C i , 𝜌i ) onwards. Indeed, because if 𝜌𝑖 +1 ( 𝑟 ) was greater than zero, this would imply that r might be enabled at least one more time from configuration ( 𝐶 𝑖 +1 , 𝜌𝑖 +1 ) onwards, that is 𝜌i ( r ) should be greater or equal than two. Consequently, if this value is greater than zero in configuration ( 𝐶 𝑖 +1 , 𝜌𝑖 +1 ) , given that rendez-vous r has not been selected for execution in configuration ( C i , 𝜌i ), then 𝜌𝑖 ( 𝑟 ) = 1 + 𝜌𝑖 +1 ( 𝑟 ) ≥ 2 should hold, which contradicts the idea that 𝜌𝑖 +1 ( 𝑟 ) might be greater than zero. 3. Case 𝑟 ∈{ 𝑟 𝑧 + 𝑝 +1 , 𝑟 𝑧 + 𝑝 +2 , …, 𝑟 𝑛 } : the scheduler decreases the counter associated with r by one, i.e., we need to prove that 𝜌𝑖 +1 ( 𝑟 ) = 𝜌𝑖 ( 𝑟 ) − 1 . Indeed, because if 𝜌i ( r ) was greater than one, this would mean that there exists 𝜌i ( r ) configurations before r is selected or enabled for the last time, including ( C i , 𝜌i ). Therefore, this happens one less time in configuration ( 𝐶 𝑖 +1 , 𝜌𝑖 +1 ) , i.e., 𝜌𝑖 +1 ( 𝑟 ) = 𝜌𝑖 ( 𝑟 ) − 1 . We have now explored every possible case and we have proved that the scheduler can update the priority map in each transition according to the characterisation of the previous lemma, which concludes the proof. □ 4. The implementation In this section, we describe the implementation. First, we present some preliminaries on how to implement maps, then describe the implementation of the scheduler, next analyse its time and space complexity, and, finally, analyse the impact of implementing it using bounded counters. 4.1. Preliminaries The key to an efficient implementation is to select the right data structures. Our implementation relies heavily on maps, which we use to store a rendez-vous specification map in which each rendez-vous is mapped onto the agents that can eventually ready it, a readiness map in which they are mapped onto the agents that are readying them in a particular configuration, and a priority map in which they are mapped onto their corresponding priority counters. Fig. 2. Main method of the scheduler. The specification and the readiness map can be implemented using a hash-table approach since the key to performance is to be able to fetch the sets of agents that may ready or are readying each rendez-vous as efficiently as possible. No other operation is performed on them. The priority map requires a careful selection of the implementation because we need to flatten it many times. Unfortunately, a hash-table approach does not allow to perform this operation efficiently. Fortunately, Brodal [9] devised a priority map implementation that performs the following operations in O (1) worst-case time: makeQueue (), which returns a new empty queue, isEmpty ( 𝜌), which returns whether queue 𝜌 is empty or not, select ( 𝜌), which returns the element with the maximum priority in queue 𝜌, insert ( 𝜌, e, p ), which inserts element e with priority p into queue 𝜌; additionally, it implements the following operation in O (log n ) worst-case time: delete ( 𝜌), which deletes the element with the minimum priority from queue 𝜌and returns it. Furthermore, it does not require more than O ( n ) space to store a queue with n elements. This makes Brodal’s [9] approach a very good choice in our context. 4.2. Scheduler implementation Fig. 2 shows the main method of the scheduler. It works on a set of rendez-vouses R and a specification map T that indicates which processes must ready each rendez-vous so that it becomes enabled. First, it initialises queue 𝜌, which implements the priority map, and readiness map C , which keeps track of which agents have readied which rendezvouses. The former is initialised so that each rendez-vous is assigned a random natural value and the latter is initialised so that each rendezvous is assigned an empty set of agents. The method then starts its main loop, which consists of the following steps: a) it first waits for a notification of the form Ready ( S ) from any agent a , which indicates that it is readying the rendez-vouses in set S ; b) it then loops over S and updates map C to record that agent a is readying that subset of rendez-vouses; c) it then invokes method transition , which implements the inference rule that specifies the scheduler and returns the updated priority map and the rendez-vous selected for execution, if any; c) if the transition method returns a non-empty map and a non-null rendez-vous, then that rendezvous may be executed immediately, which requires to send an execute notification to the agents that had readied it and to update the corresponding readiness sets. The main method terminates when method transition returns an empty priority map, which means that no rendezvous is enabled and the system has stopped. Fig. 3 .a shows the ancillary transition method. It works on a priority map 𝜌, a readiness map C , and a specification map T . It firsts iterates over the priority map to find the first rendez-vous that is enabled. The iteration is implemented in a loop in which the rendez-vouses in queue 𝜌 are iteratively transferred to the ancillary queue 𝜌′ . In each iteration, the highest priority rendez-vous is first selected from queue 𝜌; if the set of processes that have readied that rendez-vous equals the set of processes indicated by the specification map T , then that rendez-vous is enabled. In this case, we transfer all of the elements that remain in 𝜌to queue 𝜌′ by means of the ancillary transferAll method; otherwise, we move the disabled rendez-vous from queue 𝜌to queue 𝜌′ using the transferOne method. If one rendez-vous is found to be enabled, then transition returns queue 𝜌′ , which is an updated version of 𝜌, and the rendez-vous selected for execution; otherwise, it returns an empty queue and a null rendezvous. The ancillary transferOne and transferAll methods are shown in Fig. 3 .b and c. Both methods require their parameters to be in/out because Brodal’s [9] proposal assumes that queues are handled by reference. Method transferOne works on two queues 𝜌and 𝜌′ ; it transfers the rendez-vous with the maximum priority in queue 𝜌to queue 𝜌′ ; the priority is not changed at all since the highest-priority rendez-vous is assumed to be disabled. Method transferAll works on two queues 𝜌and 𝜌′ , too; it transfers all of the rendez-vouses in 𝜌to 𝜌′ so that the highestpriority one (which is assumed to be enabled) gets its priority reset to a random natural number and the remaining ones get their priorities increased. 4.3. Complexity analysis In this section, we prove that the scheduler does not require more than O ( m log m ) time to process a ready notification from an agent and it does not consume more than O ( n m ) space, where m denotes the number of rendez-vouses and n denotes the number of agents. These upper bounds are sensible to implement the scheduler in a SCADA context in which computing power, memory, and storage space are very limited. The sketch of the proof is as follows: first, Lemma 2 proves that method transferOne does not require more than O (log m ) time and O (1) space; next, Lemma 3 proves that method transferAll does not require more than O ( m log m ) time and O (1) space; then, Lemma 4 proves that method transition does not require more than O ( m log m ) time and O ( m ) space; finally, Theorem 3 proves the time and space upper bounds regarding the scheduler. Lemma 2 Method. transferOne. Let m denote the number of rendez-vouses in a system. A call to transferOne ( 𝜌, 𝜌′ ) does not require more than O (log m ) time and it does not consume more than O (1) space. Proof. A call to transferOne ( 𝜌, 𝜌′ ) wraps a call to delete , which can be completed in O (log m ) worst-case time, followed by a call to insert , which can be executed in O (1) worst-case time. The call requires to temporarily store the element retrieved from 𝜌before inserting it in 𝜌′ , which does not exceed O (1) space. As a conclusion, a call to transferOne ( 𝜌, 𝜌′ ) does not require more than O (log m ) time and it does not consume more than O (1) space. □ Lemma 3 Method. transferAll. Let m denote the number of rendez-vouses in a system. A call to transferAll ( 𝜌, 𝜌′ ) does not require more than O ( m log m ) time and it does not consume more than O (1) space. Proof. The first two statements do not require more than O (log m ) time since they call the delete and the insert methods on a queue that has a maximum of m elements. The main loop calls again the delete and the insert methods a maximum of 𝑚 − 1 times; in each iteration, the size of queue 𝜌decreases by one. Thus, the following is an upper bound to the time required to execute the main loop: log ( 𝑚 − 1) + log ( 𝑚 − 2) + log ( 𝑚 − 3) + ⋯ + log 2 + log 1 = Fig. 3. Ancillary methods. = 𝑚 −1 ∑ 𝑖 =1 log ( 𝑚 − 𝑖 ) < 𝑚 ∑ 𝑖 =1 log 𝑚 = log 𝑚 ∏ 𝑖 =1 𝑚 = log 𝑚 𝑚 = 𝑚 log 𝑚 Therefore, a call to transfer ( 𝜌, 𝜌′ ) does not require more than O ( m log m ) time. Furthermore, the call requires only a temporary variable to store the elements that are transferred from 𝜌to 𝜌′ , which means that it does not require more than O (1) space. □ Lemma 4 Method. transition. Let m denote the number of rendez-vouses in a system. A call to transition ( 𝜌, C, T ) does not require more than O ( m log m ) time and it does not consume more than O ( m ) space. Proof. The first two statements run in O (1) worst-case time. The main loop is executed a maximum of m times; in each iteration, the call to method select does not require more than O (1) time, the check for enablement can be implemented in O (1) worst-case time using hashed sets (a trivial implementation would not consume more than O ( n ) time, where n denotes the number of agents in the system), and the call to the transferOne method was proved not to consume more than O (log m ) time. So the main loop does not require more than O ( m log m ) time to execute; in the final iteration it might call method transferAll , which does not require more than O ( m log m ) time. The final check to return the value of the method does not require more than O (1) time. The call requires to store a Boolean variable and a new queue 𝜌′ , only. As a conclusion, a call to transition ( 𝜌, C, T ) does not require more than O ( m log m ) time and it does not consume more than O ( m ) space. □ Theorem 3 (The scheduler) . Let m and n denote the number of rendezvouses and agents in a system, respectively. The scheduler does not require more than O ( m ) time to initialise, it does not require more than O ( m log m ) time to process a ready notification from an agent, and it does not require more than O ( n m ) space. Proof. The initialisation sentences do not require more than O ( m ) time to execute because creating queue 𝜌and readiness map C can be accomplished in O (1) worst-case time; the initialisation loop iterates over the set of rendez-vouses and initialises their priorities and the sets of agents that are readying them in O (1) worst-case time. Thus, the conclusion is that the scheduler does not require more than O ( m ) time and more than O ( m ) space to initialise. The main loop blocks on the receive statement until an agent sends a ready notification. It then updates the readiness map, which can be easily implemented in O ( m ) worst-case time, calls the transition method, which does not require more than O ( m log m ) time, and, if possible, sends an execute notification to a subset of agents, which does not require more than O ( m ) time, and updates the readiness map, which does not require more than O ( m ) time. As a conclusion, the scheduler does not require more than 𝑂(3 𝑚 + 𝑚 log 𝑚 ) ⊆𝑂( 𝑚 log 𝑚 ) time to process a ready notification from an agent. The scheduler must store the set of rendez-vouses, which requires O ( m ) worst-case space, and the specification map, which does not require more than O ( n m ) space. Furthermore, it must store queue 𝜌, which requires O ( m ) worst-case space, readiness map C , which requires O ( n m ) worst-case space, and every call to method transition requires O ( m ) worst-case space. As a conclusion, the scheduler does not require more than 𝑂( 𝑚 + 𝑛 𝑚 ) ⊆𝑂( 𝑛 𝑚 ) space. □ 4.4. Impact of using bounded counters The counters on which our proposal relies must be implemented using data registers that provide a limited range of integer or natural numbers. In the following theorems, we analyse the impact of using bounded counters on correctness and completeness. Theorem 4 (Correctness preservation) . An implementation in which counters range in interval [− |𝑅 |+ 1 , 0] , where R denotes the set of rendezvouses in a system, preserves correctness. Proof. The proof follows from reductio ad absurdum. Assume that an implementation of the scheduler produces an unfair execution of the following form: 𝜆= ⟨( 𝐶 𝑖 , 𝜌𝑖 ) 𝑟 𝑖 +1 ⟶( 𝐶 𝑖 +1 , 𝜌𝑖 +1 ) ⟩𝑖> 0 Obviously, 𝜌0 must set every counter to zero since this is the only random natural value that can be generated. If 𝜆is unfair, it implies that there exists an element r ∈R that is enabled from time to time, but it is executed finitely many times only (possibly never). The set of rendez-vouses R can be partitioned into sets R 1 and R 2 so that R 1 is the subset of rendez-vouses that are executed finitely many times in 𝜆and 𝑅 2 = 𝑅 ⧵𝑅 1 . There is also a z ≥ 0 such that the rendez-vouses executed from configuration ( C z , 𝜌z ) onwards belong to set R 2 . If rendez-vous r is enabled from time to time in 𝜆, then there are infinitely many configurations ( C s , 𝜌s ) ( s ≥ z ) in which both 𝑟 𝑠 +1 and r are enabled. Without any loss of generality, we can assume that 𝜌𝑠 is of the form 𝜌𝑠 = ⟨𝑟 1 , 𝑟 2 , …, 𝑟 𝑝 −1 , 𝑟 𝑝 , 𝑟 𝑝 +1 , …𝑟 𝑛 ⟩( 𝑝 > 0) and that r p is the rendez-vous selected for execution in configuration ( C s , 𝜌s ). Obviously, the counter associated with the neglected rendez-vous must have a value Fig. 4. Schema of our solar power plant. greater than or equal to 𝜌s ( r p ); otherwise, it would be before r p in 𝜌𝑠 and, given that it is enabled, it would have been selected, which contradicts our hypothesis. Therefore, the neglected rendez-vous must be after r p in 𝜌𝑠 . In this situation, the counter associated with r p is reset to zero, that is, it must be at the rear of 𝜌𝑠 +1 in the next configuration. Without any loss of generality, we can assume that it is the last rendez-vous in 𝜌𝑠 +1 because if there are other rendez-vouses with the same priority any ordering is valid according to the definition of the scheduler. Consequently, the priorities associated with 𝑟 𝑝 +1 , 𝑟 𝑝 +2 , …, 𝑟 𝑛 in the next configuration are decreased by one; that is, there should exist a configuration ( C q , 𝜌q ) ( q ≥ s ) such that the priority associated with the neglected rendez-vous must be necessarily higher than the priority associated with any other rendez-vous and it should be at the beginning of 𝜌𝑞 . Since its counter is not altered, it should be selected when a configuration in which it is enabled is reached, which contradicts our hypothesis. Furthermore, a priority may be increased |𝑅 |− 1 times in the worst case because the corresponding rendez-vous can remain unchecked |𝑅 |− 1 times at most. As a conclusion, an implementation that provides counters in range [− |𝑅 |+ 1 , 0] preserves correctness. □ Theorem 5 (Completeness preservation) . An implementation that implements priorities with bounded counters does not preserve completeness. Proof. Assume that we have bounded counters that range in the integer interval [− |𝑅 |+ 1 , 𝑚 ] , for some m ≥ 0, i.e., |𝑅 |+ 𝑚 different integer values are available. Assume that there exists a fair execution in which rendez-vous r is selected only once at configuration ( 𝐶 |𝑅 |+ 𝑚 , 𝜌|𝑅 |+ 𝑚 ) . Realise that 𝜌0 ( r ) should be at least |𝑅 |+ 𝑚 + 1 , which is out of range. As a conclusion, implementing the scheduler with bounded counters does not preserve completeness. □ Remark 3. Common computing boards provide data registers that allow to operate with integer counters in range [−2 𝑏 −1 , 2 𝑏 −1 − 1] or natural counters in range [0 , 2 𝑏 − 1] , where b denotes the number of bits of the data registers. The largest priority that a rendez-vous may have is − |𝑅 |+ 1 . Thus, implementing the priorities using integer counters amounts to wasting the values in range [−2 𝑏 −1 , − |𝑅 |] , which are quintessential to generate as many fair executions as possible. Thus, our proposal is to implement the priorities using natural counters, which range in interval [0 , 2 𝑏 − 1] , and then use a simple linear translation in which − |𝑅 |+ 1 corresponds to 0 and 2 𝑏 − |𝑅 |corresponds to 2 𝑏 − 1 . This way, the priorities range in an interval in which no value is wasted. 5. Experimental analysis In this section, we describe our experimental analysis. First, we describe the solar plant in which we performed our experiments, then report on the experimental environment, the baselines and the competitors, and finally present our experimental results and analyse them statistically. The experimentation was performed in the context of an industrial research project with a company that wished to explore new models that minimise the gap between the specification produced by their research team and the implementation carried out by their engineering team [6] . Due to non-disclosure clauses, we cannot report on every detail from an engineering point of view, but we can provide an overall picture that is enough to assess our proposal from a scientific point of view. 5.1. Description of the system Solar plants have proven to be very efficient and eco-friendly because they use molten salt and water that can be recycled many times and do not significatively pollute the environment. They have recently become economically feasible due to the positive balance between production costs and sales benefits [28] . Fig. 4 sketches the solar plant in which we conducted our experiments. The flow to generate electricity starts at the cold tank, which stores molten salt at roughly 290° C. At such temperatures, the salt is a fluid that can be easily pumped into the solar tower, where it is heated up to 565° C thanks to the solar radiation that is concentrated there by means of an array of heliostats. The salt is then pumped into the hot tank, where it can be stored at about 390° C. The salt is then pumped from the hot tank into the steam generator, where heat is transferred to water, which boils and becomes steam that is pumped into a standard turbine that generates electricity. The salt is returned to the cold tank, where it can start a new cycle and the steam is condensed, deareated (a process that removes dissolved oxygen), and returned to the water tank. The flows of salt, steam, and water need to be carefully controlled so that the plant works optimally depending on the weather conditions and the amount of electricity that must be produced. In the actual system, there are 10 158 sensors, 124 processors, and 2 034 actuators. There are 321 types of sensors, which produce data regarding temperature, pressure, voltage, intensity, conductibility, vibrations, acoustics, force, or strain, just to mention a few examples. There are 97 types of processors, which execute rules that were learnt using a variety of machine-learning procedures, try to recover the system automatically when it enters a critical-failure state, or send data and statistics to an external machine-learning system that improves the rules incrementally. There are 112 types of actuators, most of which are pumps that help keep the flows of molten salt, water, and steam under control. There are also 215 rendez-vouses that co-ordinate 12.89 agents in average; the smallest rendez-vouses are two-way and the largest ones are 34-way. 5.2. The experimentation environment The sensors and the actuators are provided by many different vendors, but they all communicate by means of industrial standards that help integrate them with a variety of technologies, including ours. The processors were developed in-house and they were deployed to an array of 124 Arduino Mega 2560 REV3 boards, each of which is equipped with one ATmega2560 CPU that delivers up to 16 MIPS when