Jean Quilbeuf

Mathieu Barbier

Lukas Rummelhard

Christian Laugier

Axel Legay

Blanche Baudouin

Thomas Genevois

Javier Ibañez-Guzmán

Olivier Simonin

Statistical Model Checking Applied on Perception and Decision-making Systems for Autonomous Driving

Automotive systems must undergo a strict process of validation before their release on commercial vehicles. The currently-used methods are not adapted to latest autonomous systems, which increasingly use probabilistic approaches. Furthermore, real life validation, when even possible, often imply costs which can be obstructive. New methods for validation and testing are necessary.

In this paper, we propose a generic method to evaluate complex automotive-oriented systems for automation (perception, decision-making, etc.). The method is based on Statistical Model Checking (SMC), using specifically defined Key Performance Indicators (KPIs), as temporal properties depending on a set of identified metrics. By feeding the values of these metrics during a large number of simulations, and the properties representing the KPIs to our statistical model checker, we evaluate the probability to meet the KPIs. We applied this method to two different subsystems of an autonomous vehicles: a perception system (CMCDOT framework) and a decision-making system. An overview of the two system is given to understand related validation challenges. We show that the methodology is suited to efficiently evaluate some critical properties of automotive systems, but also their limitations.

I. INTRODUCTION

In the automotive industry the development and testing of human centric-systems must follow the guidelines of the ISO26262. In the automotive industry, this kind of testing can be divided in two:

• Vehicle-in-the-loop platform tests interactions between a human and the system in dangerous situation [START_REF] Bokc | Validation of the vehicle in the loop (vil); a milestone for the simulation of driver assistance systems[END_REF]. • Hardware-in-the-loop to test interactions between an embedded system, such as the Active Brake Control Systems [START_REF] Hwang | Development of hils systems for active brake control systems[END_REF], and the physics of a vehicle. For autonomous functionality higher than the level 3 as define by the SAE, drivers will not be responsible of most of driving decisions. As these systems will rely on machine learning and probabilistic methods, conventional methods for validation are not adapted. The vehicle shall operate in a various range of scenarios as well as dangerous situations, the validation and verification operations must be carried on simulations perform.

It allows to reduce cost and increase the coverage of system testing. The difficulty for the validation of an autonomous system are two-fold. First, the complexity and variety scenarios that autonomous vehicle will face is larger than in Advanced driver assistance systems (ADAS). Second, multiple systems will be in constant interaction. In this study we focus on a usecase that highlights these two difficulties: road intersection crossing. It is one of the most dangerous part of the road network with more than 8% of the total road fatalities in Europe [START_REF] Ibanez-Guzman | Vehicle to vehicle communications applied to road intersection safety, field results[END_REF]. Furthermore, there exists many variations of each scenario (number of vehicles, initial velocities, etc.). It is challenging for the perception because of the limited view range, partially-observed vehicles and because of the presence of multiple vulnerable users that could be potentially at risk. For the decision-making, the interactions between road users are complex to consider because of wrong behaviour of other drivers. Road intersection crossing has been identified as one use-case addressed in the Enable-3 European project [START_REF]Validation and testing of complex automated systems[END_REF]. This industry-driven project aspire to propose methods for validation and verification of automated cyber-physical systems (ACPS). The global architecture for validation and verification has been simplified to match our thematic and is illustrated in figure 1.

Examples of validation for highly-autonomous systems can be found in the aerospace domain [START_REF] Hinchey | Verification and validation of autonomous systems[END_REF], where formal methods are used to validate the behavior of a fleet of satellites. In the robotic domain, benchmarks allow researchers to compare their results in the same conditions [START_REF] Ulbrich | The opengrasp benchmarking suite: An environment for the comparative analysis of grasping and dexterous manipulation[END_REF], [START_REF] Althoff | Commonroad: Composable benchmarks for motion planning on roads[END_REF]. However benchmarks are often tailored for one specific kind of problem and are not representative enough of the variety of situation that an autonomous system may encounter to actually validate such a system. Waymo was recently confident enough in their system to remove the safety drivers for some tests. This was possible with an effort of 1 billion kilometers driven in a simulated environment [START_REF] Waymo | Waymo s safety report: how we are building a safer driver[END_REF]. Another way is to use formal methods to ensure the safety of the vehicle [START_REF] Shalev-Shwartz | On a formal model of safe and scalable self-driving cars[END_REF] but it would rather complex to do in uncertain environment.

The purpose of the paper is to demonstrate the use of a validation method (SMC) on two different systems that have been previously developed, namely Perception and Decision. The requirements for the testing in simulated environment are discussed for each system. Preliminary results for the decisionmaking system are presented as well as discussions on the challenges caused by the perception system.

Section II presents our validation approach based on statistical model checking. Section III describes the application of our approach on the perception system and the difficulty to find applicable metrics for its validation. Then Section IV shows a more complete application and interprets the results for the decision-making system.

II. STATISTICAL MODEL CHECKING

In the context of ACPS, it is not possible to afford validation through exhaustive techniques, that is by stating a property and checking that it holds in all reachable states. Indeed, this would require to model and traverse all the reachable states of the ACPS. Such a modelling is possible at a very abstract level, but requires a huge effort to be brought at a more detailed level. Furthermore, even if a very detailed model of the ACPS were provided, exploring all its reachable states would not be possible due to the very large state space. Stochastic algorithm are complex to validate with conventional methods, thus it is interesting to use probabilistic methods to evaluate them [START_REF] Jaynes | Probability theory: the logic of science[END_REF].

Statistical Model Checking (SMC) [START_REF] Hérault | Approximate probabilistic model checking[END_REF], [START_REF] Sen | On statistical model checking of stochastic systems[END_REF] provides an intermediate between test and exhaustive verification by relying on statistics. In order to perform SMC, one needs an executable model and a property to check. The executable model is expected to be stochastic, that is, to have some of its transition governed by probabilistic choices. Note that most ACPS simulations are already modelled as stochastic processes, because variations in the scenario are defined by The execution being stochastic, some traces will satisfy the property to check and some other will not. Therefore, we can define the probability that a trace satisfies a property. The main goal of SMC is to evaluate that probability. Note that a probability of satisfying a formula gives actually more information than a yes-or-no answer. Indeed, if the model does not satisfy the formula, there is an evaluation of how well it performs.

In order to perform SMC, one needs to be able to

• Generate traces of the execution of the system to validate. These traces have to be generated according to the probabilities in the model. • Write the property to check as a formula that can be decided on a finite trace, and a procedure for deciding whether a trace satisfy the property.

We present in Figure 2 an overview of the approach. On the left we have a simulator that provides stochastic execution of our system. On the bottom we have the property ϕ to check. On the top, we have some configuration for the SMC algorithm, such as the required accuracy. The SMC algorithm requires some simulations to the simulator. In turn the simulator provides a trace σ that is fed to the property checker. Finally the property checker returns its verdict to the SMC algorithm. At this point, if the SMC algorithm has enough information to return a result that meets the required accuracy, it does so. Otherwise, it asks for an additional simulation and the loop is run again. We give an intuition of SMC by illustrating it with the Monte-Carlo Algorithm. This algorithm estimates the probability p that a system satisfies a property P by checking P against a set of N random executions of the system. The estimation p is given by

p = 1 N N 1 f (ex i ) wheref (ex i ) = 1 ifex i |= P 0 otherwise
Using the formal semantics of the property language, the property is checked against each execution trace. The trace must be long enough to decide whether the property holds.

Of course, the larger is the set of simulations, the more precise is the result. The confidence bounds of the estimation are set by two positive real parameters and δ. The confidence is defined by the Chernoff bound that is stated as:

Pr (|p -p| ≤ ) ≥ 1 -δ
Assuming that p is value of the probability we want to evaluate and p is the estimation we compute, the formula means that the estimation error, i.e. the distance |p -p|, is bound by with a probability 1 -δ . In other words, the probability that the error in the estimation is greater that is δ. Once δ and have been set, we can compute the number of simulations N necessary to enforce the above formula. The quality of the approximation is high (and thus N is high as well) when and δ are close to 0. When and δ increase, the estimation is more approximate but requires less simulations to be computed.

A. Defining KPIs

In order to define and evaluate KPIs based on a set of simulations, we proceed as follows. We first identify with peoples in charge of developing the system some KPIs related to system under test and scenarios. We then express the KPIs as temporal formulas involving the identified metrics. Temporal formulas allow a finer formulation of KPIs by taking into account the evolution of the metrics during time. Let us consider acceleration as a metric. A rough formulation of a KPI concerning acceleration might be that the acceleration should be bounded, i.e. to guarantee the comfort of the passengers [START_REF] Yi | Nonlinear brake control for vehicle cw/ca systems[END_REF]. A finer formulation could be that the acceleration should generally be bounded, but the bound can be exceeded for a short period of time.

In order to express such formulas, we rely on BLTL, a bounded version of LTL [START_REF] Pnueli | The temporal logic of programs[END_REF]. The syntax of BLTL is as follows:

φ ::= p | φ ∨ φ | ¬φ | φ U ≤t φ | X ≤t φ.
A BLTL formula is expressed with respect to a trace. In our case a state is a sequence of states, one for each simulation step. Each state contains the value of each of the metrics at that current state. The symbol p represents a predicate expressed on the current state, for instance a comparison between a metric and a bound. The disjunction (∨) and the negation (¬) defined as usual. Finally, the temporal operators until (U ) and next (X) define properties about the time. Since we need to be able to decide whether a property holds on a finite trace, these operators are parameterized by a time bound t ∈ R. The formula X ≤t φ is true if φ is true in the state reached after t units of time from the current state. The formula φ 1 U ≤t φ 2 is true if 1) the formula φ 2 becomes true before t units of time from the current state and 2) the formula φ 1 remains true in every state before the one where φ 2 becomes true. For a formal definition of BLTL semantics, see [START_REF] Zuliani | Bayesian statistical model checking with application to stateflow/simulink verification[END_REF].

In practice, we often use the always (G) and eventually (F ) operators. Eventually is defined as F ≤t φ = true U ≤t φ and means that the formula φ should become true before t units of time happen. Always is defined as G ≤t φ = ¬F ≤t ¬φ and means that φ must always hold for the next t units of time. The CMCDOT Framework is a perception system, based on environment representation through probabilistic occupancy grids, a dense and generic representation [START_REF] Elfes | Using occupancy grids for mobile robot perception and navigation[END_REF], [START_REF] Moravec | Sensor fusion in certainty grids for mobile robots[END_REF], and Bayesian fusion, filtering and inference.

This type of Bayesian formalism [START_REF] Bessière | Bayesian Programming[END_REF] allows proper confidence estimation and combination, particularly important features when confronted with incomplete or even contradictory data coming from different sensors. A major feature of the system is its highly-parallelized design: from data fusion, to grid filtering, velocity inference and collision risk assessment, the methods have been designed to allow massive parallelization of computations, and so benefit from parallelcomputing devices [START_REF] Yguel | Efficient gpu-based construction of occupancy grids using several laser range-finders[END_REF], allowing real-time performances on embedded devices.

Sensor data is converted to occupancy estimation using specific sensor model, sensor occupancy estimates are then combined by Bayesian fusion in every grid cell (Fig. 3). The Conditional Monte Carlo Dense Occupancy Tracker (CM-CDOT) [START_REF] Rummelhard | Conditional monte carlo dense occupancy tracker[END_REF] itself is a generic spatial occupancy tracker, which then infers dynamics of the scene through a hybrid representation of the environment consisting of static and dynamic occupancy, empty spaces and unknown areas(Fig. 4). This differentiation enables the use of state-specific models (classic occupancy grids for motionless components and sets of moving particles for dynamic occupancy), as well as relevant confidence estimation and management of data-less areas. The approach leads to a compact model that dramatically improves the accuracy of the results and the global efficiency in comparison to previous approaches.

This method is particularly suitable for heterogeneous sensor data fusion (camera, lidars, radars etc. . . ). The occupancy of each cell over time can be estimated from various sensors data whose specific uncertainty (noise, measurement errors) are taken into consideration. Filtered cell estimates are thus much more robust, leading to a more reliable global occupancy of the environment, reducing false detections.

While most of risk estimation methods consist in detecting and tracking dynamic objects in the scene [START_REF] Fortmann | Multi-target tracking using joint probabilistic data association[END_REF], [START_REF] Khan | An mcmc-based particle filter for tracking multiple interacting targets[END_REF], the risk being then estimated through a Time to Collision (TTC) approach by projecting object trajectories to the future [START_REF] Labayrade | Experimental assessment of the rescue collision-mitigation system[END_REF], [START_REF] Kaempchen | Situation assessment of an autonomous emergency brake for arbitrary vehicle-to-vehicle collision scenarios[END_REF], the grid-based approach used in the CMCDOT framework [START_REF] Rummelhard | Conditional monte carlo dense occupancy tracker[END_REF] instead directly computes estimations of the position in the near future of every static and dynamic part of the grid, as well as the trajectory of the vehicle. These estimations are iteratively computed over short time periods, until a potential collision is detected, in which case a TTC is associated to the cell from which the colliding element came from (Fig. 5). In every cell, the associated TTCs are cumulated over different time periods (1, 2, 3 seconds for example) to estimate a cell-specific collision risk profile. Risk grids, and global aggregated risks, are thus generated, and later used to generate response impulses for the control system. This strategy [START_REF] Rummelhard | Probabilistic grid-based collision risk prediction for driving application[END_REF] avoids solving the complex problem of multiobject detection and tracking, while integrating the totality of the available information. It provides a probabilistic estimation of the risk associated to each part of the scene. B. Method Application 1) Simulation for perception: In this project, the simulation relies on the use of two frameworks: Gazebo and ROS. Gazebo allows for the representation and simulation of the environment, the ego vehicle and its sensors, as depicted in Figure 6. Each item in these three categories is matched with a visual representation and physical characteristics (dimensions, weight, friction, etc). The data acquisition and processing part of the simulation is carried out in ROS, where the data can be recorded, stored, and processed by the same code running on the actual vehicle. The communication between the ROS and Gazebo modules is carried out seamlessly thanks to the native use of ROS messages. In order for our simulation approach to be precise and fully exploitable, the simulation framework must provide the following elements:

• precise volume and shape of each vehicle, and surface reflectivity. • atmospheric conditions which might impact the vehicles' trajectory (wind gusts) or lidar detection (heavy rain or snow). • in order to establish the ground truth, a grid indicating the position of all simulated objects. This grid must reflect CMCDOT's occupation grid in the following aspects: origin position, grid direction, cell size. Currently, each lidar is simulated with the appropriate position on the ego vehicle, the same sampling frequency and the same data format as the physical sensor. To match the sensing uncertainty, a Gaussian noise can be added.

In order to be able to efficiently generate a large number of simulated environments, we have perfected a parameterbased approach which streamlines the process through which the dimensions and initial position and velocity of non-ego vehicles are specified.

Our simulation scenario aims at checking the behaviour of cars at a four-way crossroads. The rule governing this crossroad is that at any given moment in time, a maximum of one simulated vehicle is present on the crossroad. To simulate the different cases, we rely on the random generation of parameter sets (non-ego vehicle class, initial position and initial speed). The test cases are then run, and their results (perception results as in Figure 6) are stored alongside the parameter sets. The analysis of these datasets enables us to accurately measure the efficiency of our perception and control solution.

The strong advantage of this approach is the ease with which a large number of simulated scenarios can be generated, ran, and analyzed.

2) KPI definition: Contrary to most perception systems, outputs of CMCDOT are not a direct list of detected objects, but dynamic occupancy grid, a rich probabilistic representation of the entire surrounding space. While object detector metrics are already not perfectly defined, the topic of evaluation of occupancy grids (furthermore dynamic occupancy grids, incorporating at a cell level velocity field estimations) is an important subject [START_REF] Grewe | Evaluation method and results for the accuracy of an automotive occupancy grid[END_REF].

A first approach is to define a global indicator based on the direct estimates of the grid, in comparison to the ground truth. But if by qualitative analysis of results it is quite simple to evaluate if an occupancy grid is correct or not, an objective quantification of this quality is particularly complicated, each metrics focusing on a specific aspect, ignoring others (for example occupied / free space factor, cell by cell comparison, convolution-based metrics, etc.).

Another approach is to focus on specific applications of the method: the validation of the whole system itself is performed by statistical validation of its usages. In the case of the CMCDOT framework, a direct application of the perception system is an automatic braking system, based on aggregated risk estimates of the system. By comparing the difference in response of the system and expected behavior according to the ground truth, a partial evaluation of the system can be accessed.

In order to assess the correctness of the CMCDOT algorithm, we compare the output of the algorithm to the actual context of the car in the simulation. We focus on the risk of collision at 1, 2 and 3 seconds.

In order to evaluate the correctness of this output, we extract a traces of the simulation containing the following metrics: cmcdot_risk i and real_coll i for 1 ≤ i ≤ 3. The metric cmcdot_risk i indicate the probability of a collision in i s according to the CMCDOT algorithm. The metric real_coll i is a Boolean indicating whether a collision will occur if object continue to move with their current speed, according to their speed and position in the simulation.

We define one KPI for each time interval, parameterized by a threshold τ . We formalize our KPI through the property G ≤t (real coll i ⇒ (1cmcdot risk) < τ ) ∧ (¬real coll i ⇒ cmcdot risk) < τ ). This property states that if there is a risk of collision, the probability returned by CMCDOT must be high enough. Conversely, if there is no risk of collision, the probability returned by CMCDOT must be small enough.

IV. A SECOND VALIDATION APPLICATION: A DECISION-MAKING SYSTEM

A. Principle of the POMDP based decision-making

The decision-making system is a key component of an autonomous vehicle. Its task is to plan the movement of the vehicle taking into account the uncertainty in the situation measurement as well as the uncertain consequences of its action will have on the situation. Partially observable Markov decision process (POMDP) is a mathematical model that formalizes this two kind of uncertainties and has been used for planning in stochastic environment [START_REF] Kaelbling | Planning and acting in partially observable stochastic domains[END_REF].

With recent advancement on online-Pomdp solver [START_REF] Silver | Monte-carlo planning in large pomdps[END_REF](used in our work), complex problems such as road intersection crossing has been addressed in [START_REF] Liu | Situation-aware decision making for autonomous driving on urban road using online pomdp[END_REF]. The key element of our approach [START_REF] Barbier | A pomdpbased intention-expectation decision-making and key performance indicators for road intersections crossing[END_REF] is to take into account the difference between intention and expectation of drivers approaching an intersection (inspired from [START_REF] Lefèvre | Risk assessment at road intersections: Comparing intention and expectation[END_REF]) to enable partial cooperation. The intention corresponds to the manoeuvre actually performed by the drivers and could observed with the approach developed in [START_REF] Barbier | Classification of drivers manoeuvre for road intersection crossing with synthethic and real data[END_REF]. The expectation represent what the driver should do regarding the current situation and traffic rules. Situation where intention and expectation does not match could result in risky interactions. These two variables can be inferred from the physical state (Velocity and distance towards the intersection) of both vehicles. Our model is represented as a Bayesian network in Figure 7 that shows the interaction between variables. The reward function of the model is constructed to take into account: comfort, velocity, time to collision, traffic rules and differences between intention and expectation. The system interacts with the environment by selecting an acceleration that maximize the current estimations of the sum of future expected rewards. Because of the stochastic aspect of the model and its solvers a safe intersection crossing cannot be guaranteed. Thus, a large number of simulations is required to validate the model in order to ensure the safety. The two problems is that the scenario space is large because of the different regulations, initial speeds or different behaviours. Then, the parameter space for the model, especially its reward function, is as large and need to be correctly explored in order to find the functional range of the system. B. Method Application 1) Dedicated simulator development: The decision-making system interacts with the simulation trough observations that can be made on the situation and selected actions that have to be realized in the simulated environment. Thus the fidelity, that is how closely the simulator can generate environmental data and model the system that are not under test, is important. In our scenario, the micro-traffic simulation (vehicle state and interactions between vehicles) is more important than the macro-simulation (simulation of traffic as a group of vehicles). As our system selects actions, it expects the other vehicle to change its behaviour. For the ego vehicle, the dynamic model of the vehicle does not need to have an high fidelity but as we want, in the future, to compare results obtained against field operational testing, the possibility of having high fidelity model is a plus. The decision could be of different forms (trajectory, goal points, control input), so the communication between the system under test and the simulation models must be adaptable. Figure 8 represents the different scenarios that have to be tested (yield, stop controlled, or priority). Thus the simulator must generate the appropriate behaviour for each of the corresponding situations. Real life scenarios could be also be imported to increase the validity of the reproduced situation. It would require the importation of maps and perception data from other sources. Scaner [START_REF] Oktal | Scaner studio[END_REF], an automotive grade simulator, has been chosen to test the decision-making systems. It has been mostly used for vehicle in the loop testing. However, most of the features previously described are available, at various levels of maturity. It has simple but interactive models for road intersection crossing and map generation. Scaner features a batch testing function, that we found too complex to interface with the SMC.

2) KPI definition: In order to evaluate the quality of the decision algorithm, we define some Key Performance Indicators regarding the crossing of a intersection. First, we define two areas in the intersection: a critical area, that correspond to the actual intersection where stopped vehicles would block all branches of the intersection and a non-critic area, that correspond to the entry of the intersection where cars usually stop before crossing the other road. We count the number and total duration of stops in each area, a smaller number indicates a better quality of the algorithm. We also measure the total time needed to cross the intersection, where again a smaller number indicates a better quality. We measure the acceleration to evaluate the comfort of the passenger, where again a smaller number indicates a better quality.

For all metrics m whose smaller value indicates a better performance, we check whether m is bounded by a bound b. The formula G ≤t m ≤ b, with t corresponding to the time needed to cross the intersection, states that m is always smaller than b. Stating that the acceleration must always be smaller than a bound might be a constraint too strong. We thus propose a relaxed version of this KPI where the acceleration is allowed to be above the bound for a short period of time (1s). This is stated by the formula G ≤t F ≤1 acc ≤ b. The previous formula can be read as follows: at any point during the simulation, m will be smaller than b in less than 1s. In other words, it is not possible that m > b for more than 1s. The value of the bound b is defined w.r.t. the metric considered. Finally, to evaluate whether the intersection is crossed quickly enough, we set a maximum duration d for crossing the intersection and require that the intersection is crossed in less than d seconds, stated by F ≤d crossed .

3) SMC application: In order to obtain results, we selected for each metric some adequate bounds and plot the probability that the KPI is met for each bound. The Figure 9 represents the probability that the acceleration/deceleration remains below a certain bound when crossing the intersection, both for the strict (i.e. the bound is never exceeded) and the relaxed version (the bound is never exceeded for more than 1s). We see that there is a probability 0 that the acceleration stays below an absolute value of 0.8m.s -2 , and that it is always below 2m.s -2 . It corresponds to an acceptable range for human comfort and shows that in every scenario the decision-making system took actions to adapt the behaviour.

Figures 10 and 11 present the probability of respectively having a bounded number of stops and having a bounded total stop duration. We see that there is a probability 0.9 that the car does not stop in the critical zone. With that measure it can be said that most likely the ego vehicle will comply with the traffic law. However for the 0.1 probability that the vehicle stop whitin the intersection, causes for the subject to come to a stop must be investigate in order to find if it correspond to an emergency manoeuvre or a failure of the system. This could be done by introducing finer KPIs that would take into account the temporality of the problem.

In Figure 12 we show the probability to cross the intersection in less that a given duration. All this new information tells people in charge of the validation what is the most likely behaviour of the decision-making system. It also helps people working on designing the decision-making to find area of improvement in their systems.

V. CONCLUSION

In this paper we presented and demonstrated a pipeline for the validation of different ACPS on two different automotive use-cases. The application of our approach based on Statistical Model Checking to the decision-making system provides useful information to the designer of the system and to the people in charge of the validation. This valuable information is formulated through probability for our system to stay in a certain range of KPIs.

Future works include the definition of meaningful gridbased metrics for stating more discriminating KPIs about the perception system. We also plan to compare results obtained in the simulated environment with tests on proving ground to ensure the validity of our approach. Also more KPIs for the decision and perception could be introduced to accurately pinpoint the cause of identified failures.

Figure 1 .

 1 Figure 1. Interactions between the different elements of the proposed Validation pipeline. Dashed line represents future developments to connect the decision-and perception

Figure 2 .

 2 Figure 2. An overview of SMC

Figure 3 .

 3 Figure 3. Data fusion in an occupancy grid. Data from each of the 2 LiDARs are used to generate occupancy grids using sensor models, which are then fused by Bayesian fusion.

Figure 4 .

 4 Figure 4. Data representation in the CMCDOT formulation. The environment is divided into cells, to which are associated static, dynamic, empty and unknown coefficients. The dynamic part is allotted to weighted particles which sample the velocity space

Figure 5 .

 5 Figure 5. Collision risk estimation over time for a specific cell. The cell position is predicted according to its velocity, along with the mobile robot. This risk profile is computed for every cell, and then used to integrate over time the global collision risk.

Figure 6 .

 6 Figure 6. Simulated scenario for the CMCDOT algorithm (top),Output of CMCDOT (bottom)

Figure 8 .

 8 Figure 8. Simulated scenario for the decision-making. The ego vehicle (blue) is controlled by the decision-making system and have to interact with the other vehicle (white) with respect to the traffic rules

Figure 9 .

 9 Figure 9. Probability that the absolute value of the acceleration remains bounded, for the strict and the relaxed version.

Figure 10 .

 10 Figure 10. Probability of bounded occurences of stops, for critical and noncritical zones.

Figure 11 .

 11 Figure 11. Probability of a stop duration below a given bound, for critical and non-critical zones.

Figure 12 .

 12 Figure 12. Probability of crossing the intersection in less than a given time.

Table I LIST

 I OF VARIABLES EXTRACTED FROM THE SIMULATIONS.

	Name	Description	Unit
	t	Timestamp or time elapsed	s
	nc stops	Number of stops in the non-critical area
	c stops	Number of stops in the critical area
	t nc stops Duration of stops in non-critical area	s
	t c stops	Duration of stops in critical area	s
	acc	Acceleration	ms -2
	crossed	True if intersection is crossed

ACKNOWLEDGMENT

This work has been developed within the scope of "Institut de Recherche Technologique" NanoElec, founded by the French program "Investissements d'Avenir" ANR-10-AIRT-05.

This work has been conducted within the ENABLE-S3 project that has received funding from the ECSEL joint undertaking under grant agreement NO 692455. This joint undertaking receives support from the European Union's Horizon 2020 research and innovation programme and Austria, Denmark, Germany, Finland, Czech Republic, Italy, Spain, Portugal, Poland, Ireland, Belgium, France, Netherlands, United Kingdom, Slovakia, Norway.


D Efimov

N Barabanov

R Ortega

Robust stability under relaxed persistent excitation conditions

For linear time-varying systems with a persistently excited state matrix it is well-known that input-to-state stability is recovered. In this note a relaxed condition on persistence of excitation is studied together with related robust stability notions (input-to-state stability and integral input-to-state stability). The results are illustrated by simulations for scalar systems.

I. INTRODUCTION

The problems of stability and robust stability are one of the main issues studied in the theory of control. There are some special systems related to benchmark models or important problem statements whose stability has been analyzed in detail. One of such a problem deals with a time-varying linear dynamical system of the following form:

ṗ(t) = -γR(t)R (t)p(t) + b(t), t ≥ t 0 , (1)
p(t 0 ) ∈ R l , t 0 ∈ R,
where p(t) ∈ R l is the state, the functions R : R → R l×k and b : R → R l are (Lebesgue) measurable and essentially bounded; γ > 0. This problem is related with adaptive estimation and identification of linear regression models [START_REF] Sastry | Adaptive Control: Stability, Convergence and Robustness[END_REF]. The peculiarity of this system consists in the requirement imposed on the matrix function R, which is assumed usually to be persistently excited. It is a well-known fact [START_REF] Khalil | Nonlinear Systems[END_REF], that if R is persistently excited, then (1) is globally exponentially stable for b(t) ≡ 0, t ≥ t 0 and input-to-state stable (ISS) for any essentially bounded b.

Recently, several relaxed excitation notions have been proposed for R in [START_REF] Praly | Convergence of the gradient algorithm for linear regression models in the continuous and discrete time cases[END_REF], [START_REF] Barabanov | On global asymptotic stability of ẋ = -φ(t)φ (t)x with φ(t) bounded and not persistently exciting[END_REF] implying global (not uniform) asymptotic stability of [START_REF] Sastry | Adaptive Control: Stability, Convergence and Robustness[END_REF]. The goal of this note is to compare them and to establish relations with ISS and integral ISS (iISS) properties introduced in [START_REF] Sontag | On characterizations of the input-to-state stability property[END_REF], [START_REF] Angeli | Further equivalencies and semiglobal versions of integral input to state stability[END_REF].

The paper outline is as follows. Preliminaries (persistence of excitation and stability notions) are introduced in Section D. Efimov is with Inria, Univ. Lille, CNRS, UMR 9189 -CRIStAL, F-59000 Lille, France. N. Barabanov II. The relaxed excitation notions from [START_REF] Praly | Convergence of the gradient algorithm for linear regression models in the continuous and discrete time cases[END_REF], [START_REF] Barabanov | On global asymptotic stability of ẋ = -φ(t)φ (t)x with φ(t) bounded and not persistently exciting[END_REF] are discussed in Section III. Relations with ISS and iISS properties with respect to different perturbations (exogenous disturbances or measurement noises) are considered in Section IV. The scalar case and some results of simulation are presented in Section V. Some concluding remarks are given in Section VI. Denote by K + the class of continuous functions α : R + → R + , α ∈ K + belongs to the class K if α(0) = 0 and the function is strictly increasing. The function α ∈ K + belongs to the class K ∞ if α ∈ K and it increases to infinity. A continuous function µ : R + × R + → R + belongs to the class KL if µ(•, t) ∈ K ∞ for each fixed t ∈ R + and lim t→+∞ µ(s, t) = 0 for each fixed s ∈ R + .

II. PRELIMINARIES

Denote R + = {x ∈ R : x ≥ 0},

A. Persistence of excitation condition

A (Lebesgue) measurable and square integrable matrix function R : R → R l×k with the dimension l × k verifies the ( , ϑ)-Persistence of Excitation (PE) condition, if there exist constants > 0 and ϑ > 0 such that t+ t R(s)R (s)ds ≥ ϑI l for any t ∈ R, where I l denotes the identity matrix of dimension l × l. Lemma 1. [START_REF] Efimov | Design of impulsive adaptive observers for improvement of persistency of excitation[END_REF] Assume that in the system (1) the function R is continuous, bounded by ρ = sup t∈R |R(t)| < +∞, and ( , ϑ)-PE for some > 0, ϑ > 0. Then, for any t 0 ∈ R and any initial condition p(t 0 ) ∈ R l :

|p(t)| ≤ ζρ[e -0.5γζ -1 (t-t0) |p(t 0 )| + γ -1 ζ b ∞ ] ∀t ≥ t 0 for ζ = γη -1 e 2η and η = -0.5 -1 ln(1 - γϑ 1+γ 2 2 ρ 4 ).
Note that from the definition of PE property, in the conditions of the above lemma, ϑ ≤ ρ 2 , then γϑ 1+γ 2 2 ρ 4 ∈ (0, 0.5] for any γ > 0, > 0 and ϑ > 0. Therefore, η and ζ belong to (0, +∞).

B. Robust stability properties

The system (1) is called nonuniform ISS [START_REF] Karafyllis | Nonuniform in time input-to-state stability and the small gain theorem[END_REF] if there exist µ ∈ KL, σ ∈ K + and ν ∈ K such that for all t 0 ∈ R, all p(t 0 ) ∈ R l and (Lebesgue) measurable and essentially bounded b : R → R l :

|p(t)| ≤ µ(σ(t 0 )|p(t 0 )|, t -t 0 ) + ν( b ∞ ) ∀t ≥ t 0 .
The system (1) is called nonuniform iISS [START_REF] Karafyllis | Nonuniform in time input-to-state stability and the small gain theorem[END_REF] if there exist µ ∈ KL, σ ∈ K + , α ∈ K ∞ and ν ∈ K such that for all t 0 ∈ R, all p(t 0 ) ∈ R l and (Lebesgue) measurable and integrable b : R → R l :

α(|p(t)|) ≤ µ(σ(t 0 )|p(t 0 )|, t-t 0 )+ t t0 ν(|b(s)|)ds ∀t ≥ t 0 .
The system (1) is called uniform ISS or iISS if σ(s) = const for all s ∈ R.

III. RELAXED CONVERGENCE CONDITIONS FOR THE UNFORCED CASE

First, lest us consider the conditions of asymptotic stability of (1) for the case b(t) ≡ 0 for all t ∈ R. Then, to relax the PE condition we will assume that the parameters and ϑ are time-dependent:

Assumption 1. Assume that for any t 0 ∈ R there exist se- quences of positive numbers {t k } +∞ k=0 , { k } +∞ k=0 and {ϑ k } +∞ k=0
such that for all k ≥ 0:

t k+1 ≥ t k + k , t k + k t k R(s)R (s)ds ≥ ϑ k I l .
There are several results relating this assumption and asymptotic stability of (1):

Proposition 1. [4] Let Assumption 1 be satisfied and +∞ k=0 ϑ k γ -1 + γ t k + k t k |R(t)| 2 dt 2 = +∞.
(2)

Then the system (1) with b(t) ≡ 0 for all t ∈ R is globally asymptotically stable at the origin.

In [START_REF] Praly | Convergence of the gradient algorithm for linear regression models in the continuous and discrete time cases[END_REF] another condition of global asymptotic stability (GAS) for (1) has been established, which is based on the result given below that contains a small extension together with a proof: Proposition 2. Let b(t) ≡ 0 for all t ∈ R and Φ(t, t 0 ) be the transition matrix of (1) satisfying

∂ ∂t Φ(t, t 0 ) = -γR(t)R (t)Φ(t, t 0 ), t ≥ t 0 , Φ(t 0 , t 0 ) = I l ,
then for all t ≥ t 0 :

e -2γ t t 0 |R(s)| 2 ds I l ≤ Φ (t, t 0 )Φ(t, t 0 ) ≤ I l - t t0 R(s)R (s)ds γ -1 + γ t t0 |R(s)| 2 ds 2 .
Proof. For any t 0 ∈ R and p(t 0 ) ∈ R l denote p(t) = Φ(t, t 0 )p(t 0 ) (the solution of (1) with initial condition p(t 0 ) at initial time t 0 ) and consider an auxiliary Lyapunov function W (p) = p p, whose derivative for the system (1) has the form:

d dt W (p(t)) = -2γp (t)R(t)R (t)p(t) (3)
= -2γ|R (t)p(t)| 2 , then d dt W (p(t)) ≥ -2γ|R(t)| 2 W (p(t)) implying W (p(t)) ≥ e -2γ t t 0 |R(r)| 2 dr W (p(t 0 )),
which can be interpreted as

p (t 0 )Φ (t, t 0 )Φ(t, t 0 )p(t 0 ) ≥ p (t 0 )e -2γ t t 0 |R(r)| 2 dr p(t 0 )
providing the required lower estimate on Φ (t, t 0 )Φ(t, t 0 ) due to an arbitrary choice of p(t 0 ). From another side, since 0.5|a| 2 ≤ |b| 2 +|a-b| 2 for any a, b ∈ R l , for a = R (t)p(t 0 ) and b = R (t)p(t) we obtain:

0.5|R (t)p(t 0 )| 2 ≤ |R (t)p(t)| 2 + |R (t)(p(t 0 ) -p(t))| 2 . (4) Note that |R (t)(p(t) -p(t 0 ))| 2 = |R (t) t t0 ṗ(s)ds| 2 = γ 2 t t0 p (s)R(s)R (s)dsR(t)R (t) t t0 R(s)R (s)p(s)ds ≤ γ 2 |R(t)| 2 t t0 p (s)R(s)R (s)ds t t0 R(s)R (s)p(s)ds ≤ γ 2 |R(t)| 2 t t0 |R(s)||R (s)p(s)|ds 2 ≤ γ 2 |R(t)| 2 t t0 |R(s)| 2 ds t t0 |R (s)p(s)| 2 ds,
where the Cauchy-Schwarz inequality has been used on the last step. Integrating the obtained inequality we conclude that

t t0 |R (s)(p(s) -p(t 0 ))| 2 ds ≤ t t0 γ 2 |R(r)| 2 r t0 |R(s)| 2 ds × r t0 |R (s)p(s)| 2 dsdr ≤ γ 2 t t0 |R(s)| 2 ds 2 t t0 |R (s)p(s)| 2 ds.
Next, integrating (4) the following relation is derived:

0.5 t t0 |R (s)p(t 0 )| 2 ds ≤ t t0 |R (s)p(s)| 2 ds + t t0 |R (s)(p(s) -p(t 0 ))| 2 ds ≤ 1 + γ 2 t t0 |R(s)| 2 ds 2 t t0 |R (s)p(s)| 2 ds.
Finally, integrating (3) we obtain:

W (p(t)) -W (p(t 0 )) = -2γ t t0 |R (s)p(s)| 2 ds ≤ - γ t t0 |R (s)p(t 0 )| 2 ds 1 + γ 2 t t0 |R(s)| 2 ds 2 ,
or equivalently,

p (t 0 )Φ (t, t 0 )Φ(t, t 0 )p(t 0 ) ≤ p (t 0 )   Il - γ t t0 R(s)R (s)ds 1 + γ 2 t t0 |R(s)| 2 ds 2    p(t 0 ),
and since this inequality is satisfied for any p(t 0 ) ∈ R l , the desired upper estimated is substantiated.

This proposition provides generic properties of the transition matrix of (1), from which the stability conditions can be deduced:

Corollary 1. Let Assumption 1 be satisfied and

+∞ k=0   1 - ϑ k γ -1 + γ t k + k t k |R(t)| 2 dt 2    = 0
(5)

Then the system (1) with b(t) ≡ 0 for all t ∈ R is globally asymptotically stable at the origin.

Further, almost all the proofs are omitted for brevity of the presentation.

Remark 1. Since 0 < ϑ k ≤ t k + k t k |R(t)| 2 dt, sup x≥0
x 1+x 2 = 0.5 and ln(1 -s) ≤ -s for 0 < s < 1, by applying ln(•) to both sides of (5) we conclude:

-∞ = +∞ k=0 ln   1 - ϑ k γ -1 + γ t k + k t k |R(t)| 2 dt 2    ≤ - +∞ k=0 ϑ k γ -1 + γ t k + k t k |R(t)| 2 dt 2 and +∞ k=0 ϑ k γ -1 + γ t k + k t k |R(t)| 2 dt 2 ≤ +∞,
which implies [START_REF] Khalil | Nonlinear Systems[END_REF]. And vice versa, the estimate (2) also implies [START_REF] Sontag | On characterizations of the input-to-state stability property[END_REF], since using the inequality 1 -x ≤ e -x that is satisfied for all x ∈ R, and by applying e -(•) to both sides of (2) we obtain:

0 = e -+∞ k=0 ϑ k γ -1 +γ t k + k t k |R(t)| 2 dt 2 = +∞ k=0 e - ϑ k γ -1 +γ t k + k t k |R(t)| 2 dt 2 ≥ +∞ k=0   1 - ϑ k γ -1 + γ t k + k t k |R(t)| 2 dt 2    ≥ 0.
Thus, the conditions (2) and ( 5) are equivalent.

IV. ROBUSTNESS WITH RESPECT TO EXTERNAL INPUTS

Now, let us return to stability analysis of the perturbed system (1) with b(t) = 0. Proposition 3. Consider the system (1), then for any t 0 ∈ R and any

p(t 0 ) ∈ R l |p(t)| ≤ I l - t t0 R(s)R (s)ds γ -1 + γ t t0 |R(s)| 2 ds 2 × |p(t 0 )| + e γ t t 0 |R(s)| 2 ds t t0 |b(s)|ds for all t ≥ t 0 .
The latter result provides a generic auxiliary estimate on solutions of (1), which is used next to derive the stability conditions. To this end introduce a sequence

ρ k = t k+1 t k |R(t)| 2 dt ∀k ≥ 0.
Theorem 1. Consider the system (1) satisfying Assumption 1 with an additional constraint:

t k+1 = t k + k
for all k ≥ 0, and assume that the property (5) is valid.

If

sup k≥0    k e γρ k + k i=0 k j=i 1 - ϑ j γ -1 + γρ 2 j i e γρi    ≤ η t0 < +∞,
then for each t 0 ∈ R there exists a function t0 ∈ KL such that for all p(t 0 ) ∈ R l :

|p(t)| ≤ t0 (|p(t 0 )|, t -t 0 ) + η t0 b ∞ ∀t ≥ t 0 . (6)
If sup k≥0 e γρ k ≤ β t0 < +∞, then for each t 0 ∈ R there exists a function t0 ∈ KL such that for all p(t 0 ) ∈ R l :

|p(t)| ≤ t0 (|p(t 0 )|, t -t 0 ) + β t0 t t0 |b(t)|dt ∀t ≥ t 0 . (7)
Thus, the conditions of non-uniform ISS property (6) are rather sophisticated and discussed below, while it is worth to stress here that the swap "conditions" of non-uniform iISS property [START_REF] Efimov | Design of impulsive adaptive observers for improvement of persistency of excitation[END_REF] are very weak and satisfied, for example, if the system (1) is asymptotically stable for b = 0 and

A. Relation with PE conditions

Note that dependence of η t0 on the initial time t 0 ∈ R is important in the formulation of Theorem 1, since if a uniform result would be obtained, i.e. there exist η ∈ R + such that sup t0∈R η t0 ≤ η, then it implies global exponentially stability (GES) of (1) (and, consequently, fulfillment of PE condition [START_REF] Morgan | On the uniform asymptotic stability of certain linear nonautonomous differential equations[END_REF]), as it is shown in the following lemma: Lemma 2. Assume that for the system (1) there exist constants C 1 ≥ 1 and C 2 > 0 such that for all t 0 ∈ R and all initial conditions p(t 0 ) ∈ R l we have

|p(t)| ≤ C 1 |p(t 0 )| + C 2 b ∞ ∀t ≥ t 0 .
Then the system (1) with b(t) ≡ 0 for all t ∈ R is GES.

Proof. Pick up a number ∈ (0, 1/C 2 ) and set C 3 = 2C1 1-C2 . Consider a solution p(t) of the system (1) with |p(t 0 )| = 1 and b(t) ≡ 0 for all t ≥ t 0 . It is sufficient to prove that function y(t) = e (t-t0) p(t) is bounded. Function y(t) satisfies equation ẏ(t) = -γR(t)R(t) T y(t) + y(t).

We will prove that |y(t)| < C 3 for all t ≥ t 0 . Recall that C 1 ≥ 1 and, therefore, C 3 > 1. Since |y(t 0 )| = 1, we have |y(t)| < C 3 for all sufficiently small t ≥ t 0 . Assume, on the contrary to the claim existence of T > t 0 such that |y(T )| = C 3 . Choose the first T satisfying this property. Denote b(t) = y(t) on [t 0 , T ]. Then according to the assumption

|y(t)| ≤ C 1 + C 2 sup t∈[t0,T ] |y(t)| for all t ∈ [t 0 , T ]. Therefore, |y(t)| ≤ C 1 +C 2 C 3 = C 1 (1+ 2 C 2 1 -C 2 ) = C 1 1 + C 2 1 -C 2 < C 3 for all t ∈ [t 0 , T ].
The contradiction at t = T shows that |y(t)| < C 3 for all t ≥ t 0 , which completes the proof.

Corollary 2. If system (1) with b(t) ≡ 0 for all t ∈ R is not GES, then the assumption of Lemma 2 is not satisfied, and therefore the system (1) is not ISS.

The proof of Theorem 1 shows that for every t 0 ∈ R function ρ t0 (s, t-t 0 ) in ( 6) may be chosen as ρ t0 (s, t-t 0 ) = sk t0 (t -t 0 ) with a decreasing function k t0 : R + → R + . In such a case the following non-uniform counterpart of Lemma 2 can be formulated: Lemma 3. Assume for each t 0 ∈ R there exist a number η t0 > 0 and a continuous function t0 ∈ KL such that for all p(t 0 ) ∈ R l in the system (1) we have [START_REF] Angeli | Further equivalencies and semiglobal versions of integral input to state stability[END_REF]. Then for every t 0 ∈ R system (1) with b(t) ≡ 0 for all t ∈ R is GES on [t 0 , ∞).

Notice that the lemma implies that for every t 0 ∈ R function R satisfies the PE condition on interval [t 0 , ∞), that is, there exist positive real numbers m t0 and θ t0 such that

t+mt 0 t R(s)R (s)ds ≥ θ t0 I l
for all t ≥ t 0 . This condition is stronger than (5). Remark 2. Notice that in Theorem 1 and this lemma, the stability conditions of the system (1) are dependent on t 0 ∈ R (the function t0 and the parameter η t0 ). Hence, in both cases we have stability properties which are, in general, non uniform with respect to t 0 ∈ R, and there is no contradiction with Lemma 2.

B. Robustness with respect to measurement noise

The conditions of ISS obtained for (1) in Theorem 1 are rather restrictive and related with PE property of the matrix R, in the case when b in (1) plays the role of exogenous disturbance. These conditions can be significantly relaxed considering the case with b representing a measurement noise: [START_REF] Karafyllis | Nonuniform in time input-to-state stability and the small gain theorem[END_REF] where again p(t) ∈ R l is the state, the functions R : R → R l×k and b : R → R l are (Lebesgue) measurable and essentially bounded. For all k ≥ 0 denote a sequence

ṗ(t) = -γR(t)R (t) (p(t) + b(t)) , t 0 ∈ R, γ > 0,
φ k = ess sup t∈[t k ,t k+1 ) |R(t)| 2 , then ρ k ≤ k φ k .
Corollary 3. Consider the system (8) satisfying Assumption 1 with an additional constraint:

t k+1 = t k + k
for all k ≥ 0, and assume that the property (5) is valid.

If

γ sup k≥0    k φ k e γρ k + k i=0 k j=i 1 - ϑ j γ -1 + γρ 2 j i φ i e γρi    ≤ η t0 < +∞
then for each t 0 ∈ R there exists a function t0 ∈ KL such that for all p(t 0 ) ∈ R l the estimate (6) is satisfied.

If γ sup k≥0 φ k e γρ k ≤ β t0 < +∞,
then for each t 0 ∈ R there exists a function t0 ∈ KL such that for all p(t 0 ) ∈ R l the estimate ( 7) is satisfied.

Recall that the conclusion of Lemma 2 cannot be applied here for the ISS case, since the system [START_REF] Karafyllis | Nonuniform in time input-to-state stability and the small gain theorem[END_REF] in not in the form of (1).

V. SCALAR CASE

To illustrate the proposed in Theorem 1 result let us analyze the case with l = 1.

First, consider the system (1), then solutions can be calculated analytically for all t ≥ t 0 : Under conditions of Theorem 1 we obtain for all k ≥ 0:

p(t) = e -γ t t 0 R 2 (τ )dτ p(t 0 ) + t t0 e -γ t s R 2 (τ )
|p(t k+1 )| ≤ e -γϑ k |p(t k )| + t k+1 t k |b(s)|ds,
or for an essentially bounded input b:

|p(t k+1 )| ≤ e -γϑ k |p(t k )| + k b .
Recursively applying the above inequalities we get for any K ≥ 0:

|p(t K )| ≤ e -γ K-1 k=0 ϑ k |p(t 0 )| + t K t0 |b(s)|ds or |p(t K )| ≤ e -γ K-1 k=0 ϑ k |p(t 0 )| + K-1 k=0 k e -γ K-1 s=k+1 ϑs b , (9)
which results in the following condition of the system convergence for the case b = 0:

+∞ k=0 ϑ k = +∞,
and the asymptotic gain property is satisfied for any t

0 ∈ R if sup k≥1 k-1 i=0 i e -γ k-1 s=i+1 ϑs ≤ η(t 0 ) < +∞.
These estimates imply that a kind of iISS property is always presented in this case for asymptotically stable systems (1).

Example 1. Select R(t) = e t cos(t) 1 + e t , b(t) = sin(t), γ = 1, p(t 0 ) = 1
and impose k = ¯ = 0.25 ∀k ≥ 0,

ϑ k = t k+1 t k R 2 (t)dt, η k = k-1 i=0 i e -γ k-1 s=i+1 ϑs
are shown in figures 1 and 2 for t 0 = -10 and t 0 = -5, respectively. These plots demonstrate dependence of η on t 0 , and that the system is not uniformly GES (it is GAS) and possesses certain robustness against external inputs, as it has been established in Theorem 1.

Second, consider the system (8) and for simplicity assume that sup k≥0 φ k ≤ φ < +∞, φ i i e -γ k-1 s=i+1 ϑs < +∞, while iISS property is naturally yielded for any asymptotically stable system (8).

Example 2. Select t 0 ≥ 0,

R(t) = 1 √
1 + t , b(t) = 1 + sin(t), γ = 1, p(t 0 ) = 10, then the system is not exponentially stable (i.e. p(t) = p(t 0 ) 1+t0 1+t for t ≥ t 0 ≥ 0 with b(t) = 0), and impose k = ¯ = 0.5 ∀k ≥ 0. are shown in Fig. 3 for t 0 = 0.

VI. CONCLUSION

For a time-varying linear system under a relaxed notion of PE, several relations with ISS and iISS properties are established. It is shown that iISS is rather natural and it is satisfied almost always in this class of systems, and especially with respect to measurement noises. All proposed conditions are sufficient, and investigation of necessary counterpart can be a direction of future research.

  where R is the set of real numbers, N is the set of natural numbers. Let | • | denotes the Euclidean norm on R n (for n ∈ N) or the corresponding induced matrix norm. For a (Lebesgue) measurable and essentially bounded function b : R → R l denote b ∞ = sup t∈R |b(t)|.

  )| 2 dt < +∞ or sup k≥0 k < +∞, ess sup t≥0 |R(t)| < +∞.

  dτ b(s)ds and |p(t)| ≤ e -γ t t 0 R 2 (τ )dτ |p(t 0 )| + t t0 |b(s)|ds.

Figure 1 .Figure 2 .

 12 Figure 1. The results of simulation for (1) with t 0 = -10

Figure 3 . 1 k=0φ

 31 Figure 3. The results of simulation for (8) with t 0 = 0

  The plot of |p(t)| and the estimate on |p(t k )| from (10), together withϑ k = t k+1 t k R 2 (t)dt, φ k = sup t∈[t k ,t k+1 ) |R(t)| 2 , η k = k-1 i=0 φ i i e -γ k-1 s=i+1 ϑs

  is with Department of Mathematics, North Dakota State University, Fargo, ND 58102, USA. R. Ortega is with Laboratoire des Signaux et Systémes, École Supérieure d'Electricité (SUPELEC), Gif-sur-Yvette 91192, France. D. Efimov and N. Barabanov are with Department of Control Systems and Informatics, University ITMO, 49 av. Kronverkskiy, 197101 Saint Petersburg, Russia. The results of Section V were supported solely by the Russian Federation President Grant (No. 14.W01.16.6325-MD (MD-6325.2016.8)). The other research was partially supported by the Government of Russian Federation (Grant 08-08) and the Ministry of Education and Science of Russian Federation (Project 14.Z50.31.0031).


Vitaly Aksenov

Petr Kuznetsov

Anatoly Shalyto

On Helping and Stacks

A concurrent algorithm exhibits helping when one process performs work on behalf of other processes. More formally, helping is observed when the order of some operation in a linearization is fixed by a step of another process. In this paper, we show that no wait-free linearizable implementation of a stack using read, write, compare&swap and fetch&add operations can be help-free, correcting a mistake in an earlier proof by Censor-Hillel et al.

Introduction

In a wait-free data structure, every process is guaranteed to make progress in its own speed, regardless of the behavior of other processes [START_REF] Herlihy | Wait-free synchronization[END_REF]. It has been observed, however, that achieving wait-freedom typically involves some helping mechanism (e.g., [START_REF] Fatourou | A highly-efficient wait-free universal construction[END_REF][START_REF] Timnat | Wait-free linked-lists[END_REF][START_REF] Feldman | A wait-free multi-word compare-and-swap operation[END_REF][START_REF] Peng | Fa-stack: A fast array-based stack with wait-free progress guarantee[END_REF]). Informally, helping means that a process may perform additional work on behalf of other processes.

Censor-Hillel et al. [START_REF] Censor-Hillel | Help! In PODC[END_REF] proposed a natural formalization of the concept of helping, based on the notion of linearization: a process p helps an operation of a process q in a given execution if a step of p determines that an operation of q takes effect, or linearizes, before some other operation in any possible extension. It was claimed in [START_REF] Censor-Hillel | Help! In PODC[END_REF] that helping is required for any wait-free linearizable implementation of an exact order data type in a system provided with read, write, compare&swap and fetch&add shared memory primitives. Informally, a sequential data type is exact order if for some operation sequence, every change in the relative order of two operations affects the result of some other operations. As examples of exact order data types, Censor-Hillel et al. gave (FIFO) queue and (LIFO) stack.

We observe, however, that the stack data type is not exact order. As we show, in any sequential execution on stack, we can reorder any two operations op and op in such a way that no other operation will see the difference. Hence, the proof of help-free impossibility for exact order types given in [START_REF] Censor-Hillel | Help! In PODC[END_REF] does not apply to stack.

In this paper, we propose a direct proof that stack does not have help-free implementations. At first, we show the result for implementations using read, write and compare&swap operations in systems with at least three processes, and, then, extend the proof to those additionally using fetch&add in systems with at least four proccesses. The structure of the proofs generally follows the structure from the paper by Censor-Hillel et al. [START_REF] Censor-Hillel | Help! In PODC[END_REF], but the underlying reasoning is novel. Unlike their approach our proofs argue about the order of operations given their responses only after we empty the data structure. As a result, certain steps of the proof become more technically involved.

The paper is organized as follows. In Section 2 we present a computational model and necessary definitions. In Section 3 we recall the definition of helping and highlight the mistake in [START_REF] Censor-Hillel | Help! In PODC[END_REF]. In Section 4 we give our direct proof. In Section 5 we discuss the related work. And, finally, we conclude in Section 6.

Model and definitions

We consider a system of n processes p 1 , . . . , p n communicating via invocations of primitives on a shared memory. We assume that primitives are read, write and compare&swap. In our second technical contribution, we consider one more primitive fetch&add.

A compare&swap primitive takes a target location, an expected value and a new value. The value stored in the location is compared to the expected value. If they are equal, then the value in the location is replaced with the new value and true is returned (we say that the operation is successful ). Otherwise, the operation fails (i.e., the operation is failed ) and returns false.

A fetch&add primitive takes a target location and an integer value. The primitive augments the value in the location by the provided value and returns the original value.

A high-level concurrent object or a data type is a tuple (Φ, Γ, Q, q 0 , θ), where Φ is a set of operations, Γ is a set of responses, Q is a seq of states, q 0 is an initial state and a transition function θ ⊂ Q × Φ × Q × Γ , that determines, for each state and each operation, the set of possible resulting states and produced responses.

In this paper, we concentrate on a stack data type (further, we omit "data type" and simply refer to it as "stack"). It exports two methods push(•) and pop(). A push(x) operation pushes an element at the top of the stack. A pop() operations withdraws and returns the element from the top of the stack, or returns ⊥, if the stack is empty.

An implementation (or, simple object) of a high-level object O is a distributed algorithm A consisting of local state machines A 1 , . . . , A n . A i specifies the primitives p i needs to execute to return a response to an invoked operation on O. For simplicity, all implementations considered in this paper are deterministic. Nevertheless, as we pursue impossibility results, the proofs easily extend to randomized implementations. For the rest of the section we fix some implementation of stack.

A program of a process specifies a sequence of operations calls on an object. The program may include local computations and can choose which operation to execute depending on the results of the previous operations.

A history is a finite or infinite sequence of primitive steps. Each step is coupled with a specific operation that is being executed by the process performing this step. The first step of an operation always comes with the input parameters of the operation, and the last step of an operation is associated with the return of the operation. Given two histories h 1 and h 2 we denote by h 1 • h 2 the concatenation of h 1 and h 2 .

A schedule is a finite or infinite sequence of process ids. Given a schedule, an implementation and programs provided to the processes, one can unambiguously determine the corresponding history. And vice versa, given a history one can always build a schedule by substituting the steps of history to the process that performed it. Assuming a fixed program for each process (these programs will be clear from the context), and a history h, we denote by h • p i the history derived from scheduling process p i to take the next step (if any) following its program immediately after h.

The set of histories H induced by an implementation consists of all possible histories induced by all possible processes' programs with all possible schedules. Note that, by the definition, H is prefix-and limit-closed [START_REF] Lynch | Distributed Algorithms[END_REF].

A history defines a partial order on the operations: op 1 precedes op 2 in a history h (denoted: op 1 ≺ h op 2 ) if op 1 is completed before op 2 begins. A linearization L of a history h is a sequence of operations such that 1) L consists of all the completed operations and, possibly, some started but incompleted in h; 2) the operations have the same input and same output as corresponding operations in h; 3) L consistent with the data type; 4) for every two operations

op 1 ≺ h op 2 if op 2 is included in L, then op 1 preceds op 2 in L (op 1 ≺ L op 2 ).
An implementation of a data type is linearizable if each history from the set of histories has a linearization. A linearization function defined over a set of linearizable histories H maps every history in H to a linearization. Note that a linearizable implementations may have multiple linearization functions defined on the set of its histories.

An implementation is wait-free if every process completes its operation in a finite number of steps.

Helping and Exact Order Types

In this section, we recall the definitions of helping and exact order type in [START_REF] Censor-Hillel | Help! In PODC[END_REF] and show that stack is not exact order. Definition 1 (Decided before). For a history h in a set of histories H, a linearization function f over H, and two operations op 1 and op 2 , we say that op 1 is decided before op 2 in h with respect to f and H, if there exists no extension s ∈ H of h such that op 2 ≺ f (s) op 1 .

Definition 2 (Helping). A set of histories H with a linearization function f over H is help-free if for every h ∈ H, every two operations op 1 , op 2 , and a single computation step γ such that h • γ ∈ H it holds that if op 1 is decided before op 2 in h • γ and op 1 is not decided before op 2 in h then γ is a step in the execution of op 1 .

An implementation is help-free, if there exists a linearization function f such that the set of histories of this implementation with f is help-free.

Following the formalism of [START_REF] Censor-Hillel | Help! In PODC[END_REF], if S is a sequence of operations, we denote by S(n) the first n operations in S, and by S n the n-th operation of S. We denote by (S + op?) the set of sequences that contains S and all sequences that are similar to S, except that a single operation op is inserted somewhere between (or before, or after) the operations of S.

Definition 3 (Exact Order Types). An exact order type is a data type for which there exists an operation op, an infinite sequence of operations W , and a (finite or an infinite) sequence of operations R, such that for every integer n ≥ 0 there exists an integer m ≥ 1, such that for any sequence A from W (n + 1) • (R(m) + op?) and any sequence B from W (n) • op • (R(m) + W n+1 ?) at least one operation in R(m) has different results in A and B, where • is a concatenation of sequences.

It is shown in [START_REF] Censor-Hillel | Help! In PODC[END_REF] that exact order types require helping, when implemented with read, writes, and compare&swap primitives. The paper also sketches the proof of a more general result for systems that, additionally, use fetch&add. Further, it is claimed in [START_REF] Censor-Hillel | Help! In PODC[END_REF] that stack and queue are exact order types. Indeed, at first glance, if you swap two subsequent operations, further operations have to acknowledge this difference. However, the definition of an exact order type is slightly more complicated, as it allows not only to swap operations but also move them. This relaxation does not affect queue, but, unfortunately, it affects stack.

Theorem 1. Stack is not an exact order type.

Proof. We prove that for any fixed op, W , R and n there does not exist m that satisfies Definition 3. Note that the claim is stronger than what is needed to prove the theorem: it would be sufficient to prove that for all op, W and R, the condition does not hold for some n. In a sense, this suggests that stack is far from being exact order. Suppose, by contradiction, that there exists m that satisfies Definition 3 for fixed op, W , R and n. There are four cases for op and W n+1 : pop-pop, pushpop, pop-push or push-push. For each of these cases, we find two sequences from W (n + 1) • (R(m) + op?) and W (n) • op • (R(m) + W n+1 ?) for which all operations in R(m) return the same results. The contradiction implies that stack is not an exact order type.

-op = pop, W n+1 = pop. Then, W (n + 1) • op • R(m) and W (n) • op • W n+1 • R(m) satisfy, since W n+1 • op and op • W n+1 perform two pop operations. -op = push(a), W n+1 = pop. For the first sequence we take A = W (n + 1) • op • R(m). Now, we choose the second sequence B from W (n) • op • (R(m) + W n+1 ?). Let W n+1 pop in A the x-th
4 Wait-free stack cannot be help-free

In this section, we prove that there does not exist a help-free wait-free implementation of stack in a system with reads, writes, and compare&swaps. We then extend the proof to the case when a system has one more primitive fetch&add.

Help-free stacks using reads, writes and compare&swap

Suppose that there exists such a help-free stack implementation Q using read, write, and compare&swap primitives. We establish a contradiction by presenting a history h in which some operation takes infinitely many steps without completing.

We start with three observations that immediately follow from the definition of linearizability.

Observation 1 In any history h:

1. Once an operation is completed it must be decided before all operations that

have not yet started; 2. If an operation is not started it cannot be decided before any operation of a different process.

Lemma 1 (Transitivity). For any linearization function f and finite history h, if an operation op 2 is completed in h, an operation op 1 is decided before op 2 in h and op 2 is decided before an operation op 3 in h then op 1 is decided before op 3 in h.

Proof. Suppose that op 1 is not decided before op 3 in h then there exists a extension s of h for which

op 3 ≺ f (s) op 1 . Since op 2 is linearized in f (s) and op 1 is decided before op 2 then op 1 ≺ f (s) op 2 . Together, op 3 ≺ f (s) op 1 ≺ f (s) op 2
contradicting with op 2 being decided before op 3 in h.

Lemma 2. For any linearization function f and finite history h, if an operation op 1 of a process p 1 is decided before an operation op 2 of a process p 2 , then op 1 must be decided before any operation op that has not started in h.

Proof. Consider h , the extension of h, in which p 2 runs solo until op 2 completes. Such an extension exists, as Q is wait-free. By Observation 1 (1), op 2 is decided before op in h , and, consequently, by Transitivity Lemma 1, op 1 is decided before op in h . Since in h , only p 2 takes steps starting from h, op 1 must be decided before op in h -otherwise, h has a prefix h such that op 1 is not decided before op in h and op 1 is decided before op in h • p 2 -a contradiction with the assumption that Q is help-free. Now we build an infinite history h in which p 1 executes infinitely many failed compare&swap steps, yet it never completes its operation. We assume that p 1 , p 2 and p 3 are assigned the following programs: p 1 tries to perform op 1 = push(1); p 2 applies an infinite sequence of operations push(2), push(3), push(4), . . .; and p 3 is about to perform an infinite sequence of pop() operations.

The algorithm for constructing this history is given in Listing 1.1. Initially, p 1 invokes op 1 = push(1) and, concurrently, p 2 invokes op 2 = push(2). Then we interleave steps of p 1 and p 2 until a critical history h is located: op 1 is decided before op 2 in h • p 1 and op 2 is decided before op 1 in h • p 2 . We let p 2 and p 1 take the next step and, then, run op 2 after h • p 2 • p 1 until it completes. We will show that op 1 cannot complete and that we can reiterate the construction by allowing p 2 to invoke concurrent operations push(3), push(4), etc. In the resulting infinite history, p 1 takes infinitely many steps without completing op 1 .

1 h ← 2 op1 ← push(1) 3 id2
11 h ← h • p2 12 continue 13 break 14 h ← h • p2 15 h ← h • p1 16 while op2 is not completed 17 h ← h • p2 18 id2 ← id2 + 1
Listing 1.1: Constructing the history for the proof of Theorem 2

To ensure that at each iteration op 1 is not completed, we show that, at the start of each iteration of the outer loop (Line 5), the constructed history satisfies the following two invariants:

op 1 is not decided before op 2 or before any operation of p 3 ; the operations of p 2 prior to op 2 are decided before op 1 .

At the first iteration, the invariants trivially hold, since neither op 1 nor op 2 is started.

Observation 2 The order between op 1 and op 2 cannot be decided during (and right after) the inner loop (Lines 6-13).

Observation 3 Process p 3 never takes a step in h. Lemma 3. During (and right after) the execution of the inner loop (Lines 6-13) op 1 and op 2 cannot be decided before any operation of p 3 .

Proof. Suppose that during an execution of the inner loop op 1 or op 2 is decided before some operation of p 3 .

Before entering the inner loop, neither op 1 nor op 2 is decided before any operation of p 3 : op 1 is not decided because of the first invariant, while op 2 is not started (Observation 1 (2)). Thus, at least one step is performed by p 1 or p 2 during the execution of the inner loop.

Let us execute the inner loop until the first point in time when op 1 or op 2 is decided before an operation of p 3 . Let this history be h. Note, that because Q is help-free only one of op 1 and op 2 is decided before an operation of p 3 in h. Suppose, that op 1 is decided before some op 3 of p 3 , while op 2 is not decided before any operation of p 3 . (The case when op 2 is decided before some op 3 is symmetric)

Now, p 3 runs pop operations until it completes operation op 3 and then, further, until the first pop operation returns ⊥, i.e., the stack gets empty. Let the resulting extension of h be h .

Recall that op 2 is not decided before any operation of p 3 in h and, since Q is help-free and only p 3 takes steps after h, op 2 cannot be decided before any operation of p 3 in h . Hence, none of the completed operations of p 3 can return id 2 , the argument of op 2 due to the fact that all push operations have different arguments. Because the operations of p 3 empty the stack op 2 has to linearize after them, making op 3 to be decided before op 2 in h . By Transitivity Lemma 1, op 1 is decided before op 2 in h . Finally, since Q is help-free and only p 3 takes steps after h op 1 has to be decided before op 2 in h, contradicting Observation 2. Lemma 4. op 1 and op 2 cannot be completed after the inner loop (Lines 6-13).

Proof. Suppose the contrary. By Observation 1 (1), op 1 has to be decided before all operations of p 3 , contradicting Lemma 3.

Lemma 5. The execution of the inner loop (Lines 6-13) is finite.

Proof. Suppose that the execution is infinite. By Lemma 4, neither of op 1 and op 2 is completed in h. Thus, in our infinite execution either op 1 or op 2 takes infinite number of steps, contradicting wait-freedom of Q. Lemma 6. Just before Line 14 the following holds:

1. The next primitive step by p 1 and p 2 is to the same memory location.

2. The next primitive step by p 1 and p 2 is a compare&swap. 3. The expected value of the compare&swap steps of p 1 and p 2 is the value that appears in the designated address. 4. The new values of the compare&swap steps of p 1 and p 2 are different from the expected value.

Proof. Suppose that the next primitive steps by p 1 and p 2 are to different locations. Consider two histories:

h = h • p 1 • p 2 • complete op 1 • complete op 2 and h = h • p 2 • p 1 • complete op 1 • complete op 2 .
Let us look at the first two pop() operations by p 3 . Executed after h they have to return id 2 then 1, since op 1 is decided before op 2 in h and both of them are completed. While executed after h they have to return 1 then id 2 . But the local states of p 3 and shared memory states after h and h are identical and, thus, two pops of p 3 must return the same values -a contradiction. The same argument will apply when both steps by p 1 and p 2 are reads. Suppose that the next operation of p 1 is a write. (The case when the next operation of p 2 is write is symmetric) Consider two histories:

h = h • p 2 • p 1 • complete op 1 and h = h • p 1 • complete op 1 .
Let the process p 1 perform two pop() operations (op 1 and op 1 ) and p 2 complete its operation after h : op 1 and op 1 have to return 1 and id 2 , correspondingly, since op 1 and op 2 are completed and op 2 is decided before op 1 in h . Again, since the local states of p 1 and the shared memory states after h and h are identical, op 1 and op 1 performed by p 1 after h must return 1 and id 2 . Hence, op 2 has to be decided before op 1 in h = h • perform op 1 • perform op 1 and, by Lemma 2, op 2 has to be decided before any operation of p 3 in h. Since only p 1 performs steps after h in h and Q is help-free, op 2 has to be decided before any operation of p 3 at h, contradicting Lemma 3. Thus, both primitives have to be compare&swap.

By the same argument both compare&swap steps by p 1 and p 2 have the expected value that is equal to the current value in the designated memory location, and the new value is different from the expected. If it does not hold, either the local states of p 1 and the shared memory states after h•p 1 and h•p 2 •p 1 are identical or the local state of p 2 and the shared memory states after h • p 2 and h • p 1 • p 2 are identical.

Observation 4 The primitive step of p 2 in Line 14 is a successful compare&swap, and the primitive step of p 1 in Line 15 is a failed compare&swap.

Observation 5 Immediately after Line 14 op 2 is decided before op 1 .

Lemma 7. Immediately after Line 15 the order between op 1 and any operation of p 3 is not decided.

Proof. By Lemma 3, the order between op 1 and any operation of p 3 is not decided before Line 14. Because Q is help-free the steps by p 2 cannot fix the order between op 1 and any operation of p 3 . Thus, the only step that can fix the order of op 1 and some operation of p 3 is a step by p 1 at Line 15, i.e., a failed compare&swap.

Suppose that op 1 is decided before some operation op 3 of p 3 after Line 15. Let h be the history right before Line 14. Consider two histories h = h • p 2 • p 1 and h = h • p 2 . Let p 3 to solo run pop operations after h until it completes operation op 3 and then, further, until pop operation returns ⊥, i.e., the stack is empty. Since op 1 is decided before op 3 , some completed operation op 3 of p 3 has to return 1: if we now complete op 1 it should be linearized before op 3 . Now, let p 3 to perform after h the same number of operations as it did after h . Since the local states of p 3 and the shared memory states after h and h are identical (p 1 makes the failed compare&swap), op 3 after h has to return 1 as after h . Thus, op 1 is decided before op 3 in h . Since Q is help-free and p 1 does not take steps after h in h , op 1 has to be decided before op 3 before Line 14, contradicting Lemma 3. Lemma 8. At the end of the outer loop (Line 18) the order between op 1 and next op 2 = push(id 2 + 1) is not yet decided.

Proof. The operation op 2 is not started, thus, it cannot be decided before op 1 by Observation 1 [START_REF] Afek | A completeness theorem for a class of synchronization objects[END_REF].

Suppose that op 1 is decided before op 2 . By Lemma 2 op 1 has to be decided before all operations of p 3 , contradicting Lemma 7.

Thus after this iteration of the loop the two invariants hold (Observation 5 and Lemmas 7 and 8), and p 1 took at least one primitive step.

This way we build a history in which p 1 takes infinitely many steps, but op 1 is never completed. This contradicts the assumption that Q is wait-free.

Theorem 2. In a system with at least three processes and primitives read, write and compare&swap there does not exist a wait-free and help-free stack implementation.

Adding Fetch&Add

Now suppose that the implementation is allowed to additionally use fetch&add primitives. We prove that there is no wait-free and help-free stack implementation in a system with at least four processes.

Again, by contradiction, suppose that such an implementation Q exists. We build an infinite history h in which either p 1 or p 2 executes infinitely many failed compare&swap steps, yet it never completes its operation, contradicting waitfreedom. In h, processes p 1 , p 2 , p 3 and p 4 follow the following programs: for 1 ≤ i ≤ 2, p i tries to perform op i = push(i); p 3 applies an infinite sequence of operations push(3), push(4), push(5), . . .; and p 4 is about to perform an infinite sequence of pop() operations. The algorithm for constructing this history is given in Listing 1.2.

1 h ← 2 for i in 1..2: 3 opi ← push(i)
20 h ← h • p3 21 id3 ← id3 + 1
Listing 1.2: Constructing the history for the proof of Theorem 3

Similar to the proof of Theorem 2, we show that the following two invariants hold at the beginning of each iteration of the outer loop (Line 6):

the order between any two operations among op 1 , op 2 and op 3 is not decided; op 1 and op 2 are not decided before any operation of p 4 ; all the operations of p 3 prior to op 3 are decided before op 1 and op 2 .

At the beginning of the first iteration, the invariants hold trivially, since none of op i is started.

Observation 6

The order between op i and op j for 1 ≤ i = j ≤ 3 cannot be decided during (and right after) the inner loop (Lines 7-14).

Proof. From the first invariant, op i cannot be decided before op j prior to the inner loop (Lines 7-14). Since Q is help-free, during the inner loop op i can become decided before op j only after a step by p i which is impossible due to the check in Line 10.

Observation 7 Process p 4 never takes a step in h. Proof. Suppose that during an execution of the inner loop op 1 , op 2 or op 3 is decided before some operation of p 4 .

At the beginning of the loop, none of op 1 , op 2 and op 3 is decided before any operation of p 4 : op 1 and op 2 are not decided because of the second invariant, while op 3 is not yet started. Suppose that during the execution of the inner loop some op i becomes decided before some operations of p 4 .

Let us look at the execution and find the first point in time when some op k by p k is decided before some operation op 4 of p 4 . Using the same argument as in the proof of Lemma 3, we can show that op k has to be decided before any other op j contradicting Observation 6: we let p 4 run until the operation op 4 is completed and, further, while stack is not empty; op 4 becomes decided before op j ; by Transitivity Lemma 1, op k is decided before op j .

The proofs of the following two lemmas are identical to those of Lemmas 4 and 5. Lemma 10. For each i, 1 ≤ i ≤ 3, op i cannot be completed after the inner loop (Lines 7-14).

Lemma 11. The execution of the inner loop (Lines 7-14) is finite. Lemma 12. For all i, j,

1 ≤ i = j ≤ 3, op i is decided before op j in h • p i .
Proof. Consider an operation of process i. At the end of the inner loop op i should be decided before some op k in h • p i , otherwise, p i can make at least one more step during the inner loop. Thus, by Lemma 2 op i should be decided before op 4 , the first operation of p 4 . Let p 4 run pop operations until one of them returns ⊥, i.e., the stack is empty. Let this history be h .

By Lemma 9, op j is not decided before any operation of p 4 in h. Since Q is help-free and only p i and p 4 takes steps in h after h, op j cannot be decided before any operation of p 4 in h , and, consequently, operations of p 4 cannot pop an argument of op j . Since the operations of p 4 empty the stack, op j must be linearized after them. Thus, op 4 is decided before op j in h . By Transitivity Lemma 1, op i is decided before op j in h . Finally, since Q is help-free and only p 4 takes steps in h after h • p i , op i is decided before op j in h • p i . Lemma 13. Immediately before Line 16 the following holds:

1. The next primitive step by p i for 1 ≤ i ≤ 3 is to the same memory location. 2. The next primitive step by p i for 1 ≤ i ≤ 3 is fetch&add with a non-zero argument or compare&swap for which the expected value is the value that appears in the designated location and the new value is different from the expected one.

Proof. Suppose, that for some pair p i and p j the next steps are to different memory locations. We consider two histories

h = h • p i • p j • complete op i • complete op j and h = h•p j •p i •complete op i •complete op j .
By Lemma 12, after h , the two subsequent pop operations by p 4 should return first the argument of op j and then the argument of op i , while after h they should return the two values in the opposite order. This is impossible, since the local states of p 4 and the shared memory states after h and h are identical. The same argument will apply if the next steps of some pair of processes are read primitives. Suppose that the next primitive step of some p i is a write. We take any other process p j and build two histories:

h = h • p j • p i • complete op i and h = h•p i •complete op i .
As in the proof of Lemma 6, p i performs two pop operations (op i and op i ) and p j completes its operation after h : by Lemmas 1 and 12 op i and op i have to return the argument of op i and the argument of op j , respectively. The local states of p i and the shared memory states after h and h are identical, thus, op i and op i after h should return op i and op j . Hence, op j has to be decided before op i in h = h • perform op i • perform op i . By Lemma 2, op j is decided before any operation of p 4 in h. And, finally, since Q is help-free and p j does not take steps in h after h, op j has to be decided before any operation of p 4 in h, contradicting Lemma 9.

A similar argument applies to the case when the next primitive step of some p i is fetch&add with argument zero or compare&swap which expected value differs from the value in the designated location or the new value is equal to the expected. We take any other process p j (1 ≤ j ≤ 3) and build two histories h = h • p i • p j • complete p j and h = h • p j • complete p j . The proof for the previous case applies except that now the roles of p i and p j are swapped. Lemma 14. At most one out of p 1 and p 2 can have fetch&add as their next primitive step.

Proof. Suppose that p 1 and p 2 have fetch&add as their next primitive step. Consider two histories h = h • p 1 • p 2 and h = h • p 2 • p 1 . From Lemma 12 op 1 is decided before op 2 in h , thus, by Lemma 2 op 1 is decided before the first operation op 4 of p 4 . After h p 4 performs k pop operations until one of them returns ⊥, i.e., the stack is empty. One pop has to return 1, because if we now complete op 1 it has to be linearized before op 4 . The same with h : p 4 performs k pops until one of them returns ⊥. Since, the local states of p 4 and the shared memory states after h and h are the same: two pop operations pop 1 () and pop 2 () of k (= k ) operations of p 4 after h and h return 1 and 2. Now, we show that op 1 and op 2 are decided before op 3 in h . The same can be shown for h . Consider a history h: h continued with k pop operations by p 4 . By Lemma 12 op 1 is decided before op 3 in h . From Lemma 9 and two facts that Q is help-free and op 3 does not make any steps after h in h, it follows that op 3 cannot be decided before any operation of p 4 in h and, consequently, the operations of p 4 cannot pop an argument of op 3 . Since k pops of op 4 empty the stack, op 3 has to linearize after them, making operation pop 2 () to be decided before op 3 . Since pop 2 () returns 2 it has to be decided after op 2 . By Transitivity Lemma 1, op 2 is decided before op 3 in h. Q is help-free and only p 4 takes steps after h , thus, op 2 is decided before op 3 in h . Now consider two histories h • complete op 3 and h • complete op 3 . In both of these histories, op 1 and op 2 are decided before op 3 . After the first history let p 4 perform three pop operations and p 1 and p 2 complete push(1) and push(2): the three pops return id 3 , 2 and 1, respectively. Analougously, after the second history three pop return id 3 , 1 and 2. This is impossible, since the local states of p 4 and the memory states after these two histories are identical.

Observation 8 From the previous lemma we know that the next primitive step of at least one process p 1 or p 2 is compare&swap. Let it be process p k . By al-gorithm, p 3 takes a step at Line 16 changing the memory location either by fetch&add or by a successful compare&swap, thus, the next step of p k at Line 18 should be a failed compare&swap.

Observation 9 Immediately after Line 16, op 3 is decided before op 1 and op 2 .

Lemma 15. Immediately after Line 18, op 1 and op 2 are not decided before any operation of p 4 .

Proof. We prove the claim for op 1 , the case of op 2 is similar.

If p 2 took a step at Line 18, then by Lemma 9 and the fact that the steps by p 2 or p 3 cannot fix the order between op 1 and any operation of p 4 due to help-freedom, op 1 is not decided before any operation of p 4 .

If p 1 took a step at Line 18, then by Lemma 9 and the fact that the steps by p 3 cannot fix the order between op 1 and any operation of p 4 due to help-freedom, the only step that could fix the order is a step by p 1 at Line 18, i.e., a failed compare&swap. Suppose that op 1 is decided before some op 4 of p 4 after Line 18. We consider two histories h = h • p 3 • p 1 and h = h • p 3 . Let p 4 run solo after h until it completes op 4 , and then further until some of its pop operations returns ⊥, i.e., the stack becomes empty. Since op 1 is decided before op 4 , some completed operation op 4 of p 4 has to return 1: if we now complete op 1 it has to be linearized before op 4 . Now, let p 4 to run the same number of pop operations after h . Since the local states of p 4 and the shared memory states after h and h are identical, op 4 returns 1. Thus, op 1 is decided before op 4 in h . As Q is help-free and p 1 does not take steps after h in h , op 1 has to be decided before op 4 in h, contradicting Lemma 9.

Lemma 16. At the end of the outer loop (Line 21), the order between any two operations among op 1 , op 2 and the next op 3 = push(id 3 + 1) is not yet decided.

Proof. The operation op 3 is not yet started, thus, it cannot be decided before op i , i = 1, 2, by Observation 1 [START_REF] Afek | A completeness theorem for a class of synchronization objects[END_REF]. Suppose that op i , i = 1, 2, is decided before op j , then by Lemma 2 op i has to be decided before all operations of p 4 , contradicting Lemma 15.

We started with three invariants that hold before any iteration of the loop. By Observation 9 and Lemmas 15 and 16) the invariants hold after the iteration, and at least one of p 1 and p 2 made at least one primitive step.

This way we build a history in which one of op 1 and op 2 never completes its operation, even though it takes infinitely many steps. This contradicts the assumption that Q is wait-free. Theorem 3. In a system with at least four processes and primitives read, write, compare&swap and fetch&add, there does not exist a wait-free and help-free stack implementation.

Related work

Helping is often observed in wait-free (e.g., [START_REF] Fatourou | A highly-efficient wait-free universal construction[END_REF][START_REF] Timnat | Wait-free linked-lists[END_REF][START_REF] Feldman | A wait-free multi-word compare-and-swap operation[END_REF][START_REF] Peng | Fa-stack: A fast array-based stack with wait-free progress guarantee[END_REF]) and lock-free implementations (e.g., [START_REF] Arbel | Reuse, dont recycle: Transforming lock-free algorithms that throw away descriptors[END_REF][START_REF] Natarajan | Fast concurrent lock-free binary search trees[END_REF][START_REF] Shane | A non-blocking internal binary search tree[END_REF][START_REF] Maged | High performance dynamic lock-free hash tables and list-based sets[END_REF]): operations of a slow or crashed process may be finished by other processes. Typically, to benefit from helping, an operation should register a descriptor (either in a dedicated "announce" array or attached in the data items) that can be used by concurrent processes to help completing it.

We are aware of three alternative definitions of helping: (1) linearizationbased by Censor-Hillel et al. [START_REF] Censor-Hillel | Help! In PODC[END_REF] considered in this paper, (2) valency-based by Attiya et al. [START_REF] Attiya | Nontrivial and universal helping for wait-free queues and stacks[END_REF] and (3) universal by Attiya et al. [START_REF] Attiya | Nontrivial and universal helping for wait-free queues and stacks[END_REF].

Valency-based helping [START_REF] Attiya | Nontrivial and universal helping for wait-free queues and stacks[END_REF] captures helping through the values returned by the operations, which makes it quite restrictive. In particular, for stack, the definition cannot capture helping relations between two push operations. They distinguish trivial and non-trivial helping: for non-trivial helping, the operation that is being helped should return a data-structure-specific non-trivial (e.g., non-empty for stacks and queues) value. It is shown in [START_REF] Attiya | Nontrivial and universal helping for wait-free queues and stacks[END_REF] that any wait-free implementation of queue has non-trivial helping, while there exists a wait-free implementation of stack without non-trivial helping. This is an interesting result, given notorious attempts of showing that queue is in Common2 [START_REF] Afek | A completeness theorem for a class of synchronization objects[END_REF], i.e., that they can be implemented using reads, writes and 2-consensus objects, while stack has been shown to be in Common2 [START_REF] Afek | Common2 extended to stacks and unbounded concurrency[END_REF].

Attiya et al. [START_REF] Attiya | Nontrivial and universal helping for wait-free queues and stacks[END_REF] also introduce a very strong notion of helping -universal helping -which essentially boils down to requiring that every invoked operation eventually takes effect. This property is typically satisfied in universal constructions parameterized with object types. But most algorithms that involve helping in a more conventional (weaker) sense do not meet it, which makes the use of universal helping very limited.

Linearization-based helping [START_REF] Censor-Hillel | Help! In PODC[END_REF] considered in this paper is based on the order between two operations in a possible linearization. Compared to valency-based definitions, this notion of helping operates on the linearization order and, thus, can be applied to all operations, not only to those that return (non-trivial) values. By relating "helping" to fixing positions in the linearization, this definiton appears to be more intuitive: one process helps another make a "progress", i.e., linearize earlier. Censor-Hillel et al. [START_REF] Censor-Hillel | Help! In PODC[END_REF] also introduce two classes of data types: exact order types (queue as an example) and global view types (snapshot and counter as examples). They showed that no wait-free implementation of data types from these two classes can be help-free. By assuming stack to be exact order, they deduced that this kind of helping is required for wait-free stack implementations. In this paper, we show that stack is in fact not an exact order type, and give a direct proof of their claim.

Concluding remarks

In this paper, we give a direct proof that any wait-free implementation of stack in a system with read, write, comare&swap and fetch&add primitives is subject to linearization-based helping. This corrects a mistake in the indirect proof via exact order types in [START_REF] Censor-Hillel | Help! In PODC[END_REF].

Let us come back to the original intuition of helping as a process performing work on behalf of other processes. One may say that linearization-based helping introduced by Censor-Hillel et al. and used in our paper does not adequately capture this intuition. For example, by examining the wait-free stack implementation by Afek et al. [START_REF] Afek | Common2 extended to stacks and unbounded concurrency[END_REF], we find out that none of the processes explicitly performs work for the others: to perform pop() a process goes down the stack from the current top until it reaches some value or the bottom of the stack; while to perform push(x) a process simply increments the top of the stack and deposits x there. But we just showed that any wait-free stack implementation has linearization-based helping, and indeed this algorithm has it. So we might think that valency-based helping is superior to linearization-based one, since the algorithm by Afek et al. does not have non-trivial valency-based helping. Nevertheless, the aforementioned algorithm has trivial valency-based helping, and, thus, the (quite unnatural) distinction between trivial and non-trivial helping seems to be chosen specifically to allow the algorithm by Afek et al. to be help-free.

A very interesting challenge is therefore to find a definition of linearizationbased helping that would naturally reflect help-freedom of the algorithm by Afek et al., while queue does not have a wait-free and help-free implementation.

  element from the bottom of the stack. We extend W (n) • op in B with operations from R(m) until some operation op tries to pop the x-th element from the bottom. Note that all operations R(m) up to op (not including op ) return the same results in A and B. If such op does not exist then we are done. Otherwise, we insert W n+1 right before op , i.e., pop this element. Subsequent operations in R(m) are not affected, i.e., results of operations in R(m) are the same in A and B.op = pop, W n+1 = push(b). This case is symmetric to the previous one.op = push(a), W n+1 = push(b). For the first sequence, we take A = W (n + 1)•op•R(m). Now, we build the second sequence B from W (n)•op•(R(m)+ W n+1 ?). Let W n+1 push in A the x-th element from the bottom of the stack. Let us perform W (n) • op in B and start performing operations from R(m) until some operation op pops the x-th element (again, this should eventually happen, otherwise a contradiction is established). Note that all operations R(m) up to op (including op ) return the same results in A and B. If such op does not exist then we are done. Otherwise, right after op we perform W n+1 , i.e., push the element b in its proper position. Subsequent operations in R(m) are not affected and, thus, the results of all operations in R(m) are the same in A and B.

Lemma 9 .

 9 During (and right after) an execution of the inner loop (Lines 7-14) op 1 , op 2 and op 3 cannot be decided before any operation of p 4 .