Angela Felisia

Chiarello

Paola Goatin

Non-local multi-class traffic flow models

We prove the existence for small times of weak solutions for a class of non-local systems in one space dimension, arising in traffic modeling. We approximate the problem by a Godunov type numerical scheme and we provide uniform L ∞ and BV estimates for the sequence of approximate solutions. We finally present some numerical simulations illustrating the behavior of different classes of vehicles and we analyze two cost functionals measuring the dependence of congestion on traffic composition.

Introduction

We consider the following class of non-local systems of M conservation laws in one space dimension:

∂ t ρ i (t, x) + ∂ x ρ i (t, x)v i ((r * ω i )(t, x)) = 0, i = 1, ..., M,

where

r(t, x) := M i=1 ρ i (t, x), (1.2)
v i (ξ) := v max i ψ(ξ), (1.3)
(r * ω i )(t, x) :=

x+η i x r(t, y)ω i (y -x) dy , (1.4)
and we assume:

(H1) The convolution kernels ω i ∈ C1 ([0, η i ]; R + ), η i > 0, are non-increasing functions such that η i 0 ω i (y) dy = J i . We set W 0 := max i=1,...,M ω i (0). (H3) ψ : R + → R + is a smooth non-increasing function such that ψ(0) = 1 and ψ(r) = 0 for r ≥ 1 (for simplicity, we can consider the function ψ(r) = max{1 -r, 0}).

We couple (1.1) with an initial datum ρ i (0, x) = ρ 0 i (x), i = 1, . . . , M.

(1.5)

Model (1.1) is obtained generalizing the n-populations model for traffic flow described in [START_REF] Benzoni-Gavage | An n-populations model for traffic flow[END_REF] and it is a multi-class version of the one dimensional scalar conservation law with non-local flux proposed in [START_REF] Blandin | Well-posedness of a conservation law with non-local flux arising in traffic flow modeling[END_REF], where ρ i is the density of vehicles belonging to the i-th class, η i is proportional to the look-ahead distance and J i is the interaction strength. In our setting, the non-local dependence of the speed functions v i describes the reaction of drivers that adapt their velocity to the downstream traffic, assigning greater importance to closer vehicles, see also [START_REF] Chiarello | Global entropy weak solutions for general non-local traffic flow models with anisotropic kernel[END_REF][START_REF] Goatin | Well-posedness and finite volume approximations of the LWR traffic flow model with non-local velocity[END_REF]. We consider different anisotropic discontinuous kernels for each equation of the system, therefore the results in [START_REF] Aggarwal | Nonlocal systems of conservation laws in several space dimensions[END_REF] cannot be applied. The model takes into account the distribution of heterogeneous drivers and vehicles characterized by their maximal speeds and look-ahead visibility in a traffic stream. One of the limitations of the standard LWR traffic flow model [START_REF] Lighthill | On kinematic waves. II. A theory of traffic flow on long crowded roads[END_REF][START_REF] Richards | Shock waves on the highway[END_REF] is the first in first out rule, conversely in multi-class dynamic faster vehicles can overtake slower ones and slower vehicles slow down the faster ones.

Due to the possible presence of jump discontinuities, solutions to (1.1), (1.5) are intended in the following weak sense.

Definition 1. A function ρ = (ρ 1 , . . . , ρ M ) ∈ (L 1 ∩ L ∞ )([0, T [ ×R; R M ), T > 0, is a weak solution of (1.1), (1.5) if T 0 ∞ -∞ ρ i ∂ t ϕ + ρ i v i (r * ω i )∂ x ϕ (t, x) dx dt + ∞ -∞ ρ 0 i (x)ϕ(0, x) dx = 0 for all ϕ ∈ C 1 c (] -∞, T [ ×R; R), i = 1, . . . , M .
The main result of this paper is the proof of existence of weak solutions to (1.1), (1.5), locally in time.

Theorem 1. Let ρ 0 i (x) ∈ (BV ∩ L ∞ ) (R; R + ), for i = 1, . . . , M , and assumptions (H1) -(H3) hold. Then the Cauchy problem (1.1), (1.5) admits a weak solution on [0, T [ ×R, for some T > 0 sufficiently small.

The paper is organized as follows. Section 2 is devoted to prove uniform L ∞ and BV estimates on the approximate solutions obtained through an approximation argument based on a Godunov type numerical scheme, see [START_REF] Friedrich | A Godunov type scheme for a class of scalar conservation laws with non-local flux[END_REF]. We have to point out that these estimates heavily rely on the monotonicity properties of the kernel functions ω i . In Section 3 we prove the existence in finite time of weak solutions applying Helly's theorem and a Lax-Wendroff type argument, see [START_REF] Leveque | Finite volume methods for hyperbolic problems[END_REF]. In Section 4 we present some numerical simulations for M = 2. In particular, we consider the case of a mixed flow of cars and trucks on a stretch of road, and the flow of mixed autonomous and non-autonomous vehicles on a circular road. In this latter case, we analyze two cost functionals measuring the traffic congestion, depending on the penetration ratio of autonomous vehicles. The final Appendix contains an alternative proof of Theorem 1, based on approximate solutions constructed via a Lax-Friedrichs type scheme, which is commonly used in the framework of non-local equations, see [START_REF] Aggarwal | Nonlocal systems of conservation laws in several space dimensions[END_REF][START_REF] Amorim | On the numerical integration of scalar nonlocal conservation laws[END_REF][START_REF] Blandin | Well-posedness of a conservation law with non-local flux arising in traffic flow modeling[END_REF].

Godunov type approximate solutions

First of all, we extend ω i (x) = 0 for x > η i . For j ∈ Z and n ∈ N, let x j+1/2 = j∆x be the cells interfaces, x j = (j -1/2)∆x the cells centers and t n = n∆t the time mesh.

We aim at constructing a finite volume approximate solution ρ ∆x = ρ ∆x 1 , . . . , ρ ∆x M , with

ρ ∆x i (t, x) = ρ n i,j for (t, x) ∈ C n j = [t n , t n+1 [×]x j-1/2 , x j+1/2
] and i = 1, ..., M. To this end, we approximate the initial datum ρ 0 i for i = 1, ..., M with a piecewise constant function ρ 0 i,j = 1 ∆x

x j+1/2 x j-1/2 ρ 0 i (x) dx , j ∈ Z.
Similarly, for the kernel, we set

ω k i := 1 ∆x x j+1/2 x j-1/2 ω 0 i (x) dx , k ∈ N, so that ∆x +∞ k=0 ω k i = η i 0 ω i (x) dx = J i (the sum is indeed finite since ω k i = 0 for k ≥ N i sufficiently large). Moreover, we set r n j+k = M i=1
ρ n i,j+k for k ∈ N and

V n i,j := v max i ψ   ∆x +∞ k=0 ω k i r n j+k   , i = 1, . . . , M, j ∈ Z. (2.1)
We consider the following Godunov-type scheme adapted to (1.1), which was introduced in [START_REF] Friedrich | A Godunov type scheme for a class of scalar conservation laws with non-local flux[END_REF] in the scalar case:

ρ n+1 i,j = ρ n i,j -λ ρ n i,j V n i,j+1 -ρ n i,j-1 V n i,j (2.2)
where we have set λ = ∆t ∆x .

Compactness estimates

We provide here the necessary estimates to prove the convergence of the sequence of approximate solutions constructed via the Godunov scheme (2.2).

Lemma 1. (Positivity) For any T > 0, under the CFL condition

λ ≤ 1 v max M ψ ∞ , (2.3)
the scheme (2.2) is positivity preserving on [0, T ] × R.

Proof. Let us assume that ρ n i,j ≥ 0 for all j ∈ Z and i ∈ 1, ..., M . It suffices to prove that ρ n+1 i,j in (2.2) is non-negative. We compute

ρ n+1 i,j = ρ n i,j 1 -λV n i,j+1 + λ ρ n i,j-1 V n i,j ≥ 0 (2.4)
under assumption (2.3).

Corollary 2. (L 1 -bound) For any n ∈ N, under the CFL condition (2.3) the approximate solutions constructed via the scheme (2.2) satisfy

ρ n i 1 = ρ 0 i 1 , i = 1, . . . , M, (2.5)
where ρ n i 1 := ∆x j ρ n i,j denotes the L 1 norm of the i-th component of ρ ∆x .

Proof. Thanks to Lemma 1, for all i ∈ {1, ..., M } we have

ρ n+1 i 1 = ∆x j ρ n+1 i,j = ∆x j ρ n i,j -λρ n i,j V n i,j+1 + λ ρ n i,j-1 V n i,j = ∆x j ρ n i,j , proving (2.5).
Lemma 2. (L ∞ -bound) If ρ 0 i,j ≥ 0 for all j ∈ Z and i = 1, ..., M , and (2.3) holds, then the approximate solution ρ ∆x constructed by the algorithm (2.2) is uniformly bounded on [0, T ]×R for any T such that

T < M ρ 0 ∞ v max M ψ ∞ W 0 -1 . Proof. Let ρ = max{ρ n i,j-1 , ρ n i,j }. Then we get ρ n+1 i,j = ρ n i,j 1 -λV n i,j+1 + λ ρ n i,j-1 V n i,j ≤ ρ 1 + λ V n i,j -V n i,j+1 (2.6)
and

V n i,j -V n i,j+1 = v max i ψ   ∆x +∞ k=0 ω k i r n j+k   -ψ   ∆x +∞ k=0 ω k i r n j+k+1   ≤ v max i ψ ∞ ∆x +∞ k=0 ω k i (r n j+k+1 -r n j+k ) = v max i ψ ∞ ∆x -ω 0 i r n j + +∞ k=1 (ω k-1 i -ω k i )r n j+k ≤ v max i ψ ∞ ∆xM ρ n ∞ ω i (0) (2.7)
where

ρ ∞ = (ρ 1 , . . . , ρ M ) ∞ = max i,j ρ i,j . So, until ρ n ∞ ≤ K, for some K ≥ ρ 0 ∞ , we get ρ n+1 ∞ ≤ ρ n ∞ 1 + M Kv max M ψ ∞ W 0 ∆t , which implies ρ n ∞ ≤ ρ 0 ∞ e Cn∆t , with C = M Kv max M ψ ∞ W 0 . Therefore we get that ρ(t, •) ∞ ≤ K for t ≤ 1 M Kv max M ψ ∞ W 0 ln K ρ 0 ∞ ≤ 1 M e ρ 0 ∞ v max M ψ ∞ W 0 ,
where the maximum is attained for K = e ρ 0 ∞ . Iterating the procedure, at time t m , m ≥ 1 we set K = e m ρ 0 ∞ and we get that the solution is bounded by K until t m+1 such that

t m+1 ≤ t m + m M e m ρ 0 ∞ v max M ψ ∞ W 0 .
Therefore, the approximate solution remains bounded, uniformly in ∆x, at least for t ≤ T with

T ≤ 1 M ρ 0 ∞ v max M ψ ∞ W 0 +∞ m=1 m e m ≤ 1 M ρ 0 ∞ v max M ψ ∞ W 0 .
Remark 1. Unlike the classical multi-population model [START_REF] Benzoni-Gavage | An n-populations model for traffic flow[END_REF], the simplex

S :=    ρ ∈ R M : M i=1 ρ i ≤ 1, ρ i ≥ 0 for i = 1, . . . , M   
is not an invariant domain for (1.1), see Figure 1 for a numerical example. Indeed, let us consider the system

∂ t ρ i (t, x) + ∂ x ρ i (t, x)v i (r(t, x)) = 0, i = 1, ..., M, (2.8)
where r and v i are as in (1.2) and (1.3), respectively. We have the following:

Lemma 3. Under the CFL condition λ ≤ 1 v max M ψ ∞ + ψ ∞ ,
for any initial datum ρ 0 ∈ S the approximate solutions to (2.8) computed by the upwind scheme

ρ n+1 j = ρ n j -λ F(ρ n j , ρ n j+1 ) -F(ρ n j-1 , ρ n j ) , (2.9)
with F(ρ n j , ρ n j+1 ) = ρ n j ψ(r n j+1 ), satisfy the following uniform bounds:

ρ n j ∈ S ∀j ∈ Z, n ∈ N.
Proof. Assuming that ρ n j ∈ S for all j ∈ Z, we want to prove that ρ n+1 j ∈ S. Rewriting (2.9), we get

ρ n+1 i,j = ρ n i,j -λ v max i ρ n i,j ψ(r n j+1 ) -v max i ρ n i,j-1 ψ(r n j ) .
Summing on the index i = 1, . . . , M , gives (c)

r n+1 j = M i=1 ρ n+1 i,j = M i=1 ρ n i,j -λ M i=1 v max i ρ n i,j ψ(r n j+1 ) -v max i ρ n i,j-1 ψ(r n j ) = r n j + λψ(r n j ) M i=1 v max i ρ n i,j-1 -λψ(r n j+1 ) M i=1 v max i ρ n i,j .
0 0.5 1 1.5 2 2.5 3 1 1.05 1.1 1.15 1.2 1.25 (d)
Figure 1: Numerical simulation illustrating that the simplex S is not an invariant domain for (1.1). We take M = 2 and we consider the initial conditions ρ 1 (0, x) = 0.9χ [-0.5,-0.3] and ρ 2 (0, x) = 0.1χ ]-∞,0] + χ ]0,+∞[ depicted in (a), the constant kernels ω 1 (x) = ω 2 (x) = 1/η, η = 0.5, and the speed functions given by v max

1 = 0.2, v max 2 = 1, ψ(ξ) = max{1 -ξ, 0}
for ξ ≥ 0. The space and time discretization steps are ∆x = 0.001 and ∆t = 0.4∆x. Plots (b) and (c) show the density profiles of ρ 1 , ρ 2 and their sum r at times t = 1.8, 2.8. The function max x∈R r(t, x) is plotted in (d), showing that r can take values greater than 1, even if r(0, x) = ρ 1 (0, x) + ρ 2 (0, x) ≤ 1.

Defining the following function of ρ

n j Φ(ρ n 1,j , . . . , ρ n M,j ) = r n j + λψ(r n j ) M i=1 v max i ρ n i,j-1 -λψ(r n j+1 ) M i=1 v max i ρ n i,j , we observe that Φ(0, . . . , 0) = λψ(0) M i v max i ρ n i,j-1 ≤ λ ψ ∞ v max M ≤ 1 if λ ≤ 1/v max M ψ ∞ and Φ(ρ n 1,j , ..., ρ n M,j ) = 1 -λψ(r n j+1 ) M i=1 v max i ρ n i,j ≤ 1 for ρ n j ∈ S such that r n j = M i=1 ρ n i,j = 1. Moreover ∂Φ ∂ρ n i,j (ρ n j ) = 1 + λψ (r n j ) M i=1 v max i ρ n i,j-1 -λψ(r n j+1 )v max i ≥ 0 if λ ≤ 1/v max M ψ ∞ + ψ ∞ .
This proves that r n+1 j ≤ 1. To prove the positivity of (2.9), we observe that

ρ n+1 i,j = ρ n i,j 1 -λv max i ψ(r n j+1 ) + λv max i ρ n i,j-1 ψ(r n j ) ≥ 0 if λ ≤ 1/v max M ψ ∞ . Lemma 4. (Spatial BV-bound) Let ρ 0 i ∈ (BV ∩ L ∞ ) (R, R + ) for all i = 1, ..., M. If (2.
3) holds, then the approximate solution ρ ∆x (t, •) constructed by the algorithm (2.2) has uniformly bounded total variation for t ∈ [0, T ], for any T such that

T ≤ min i=1,...,M 1 H TV (ρ 0 i ) + 1 , (2.10)
where

H = ρ ∞ v max M W 0 M 6M J 0 ρ ∞ ψ ∞ + ψ ∞ .
Proof. Subtracting the identities

ρ n+1 i,j+1 = ρ n i,j+1 -λ ρ n i,j+1 V n i,j+2 -ρ n i,j V n i,j+1 , (2.11)
ρ n+1 i,j = ρ n i,j -λ ρ n i,j V n i,j+1 -ρ n i,j-1 V n i,j , (2.12)
and setting ∆ n i,j+1/2 = ρ n i,j+1 -ρ n i,j , we get

∆ n+1 i,j+1/2 = ∆ n i,j+1/2 -λ ρ n i,j+1 V n i,j+2 -2 ρ n i,j V n i,j+1 + ρ n i,j-1 V n i,j .
Now, we can write

∆ n+1 i,j+1/2 = 1 -λV n i,j+2 ∆ n i,j+1 (2.13)
+ λV n i,j ∆ n i,j-1/2 -λρ n i,j V n i,j+2 -2V n i,j+1 + V n i,j . (2.14)
Observe that assumption (2.3) guarantees the positivity of (2.13). The term (2.14) can be estimated as

V n i,j+2 -2V n i,j+1 + V n i,j = = v max i   ψ   ∆x +∞ k=0 ω k i r n j+k+2   -2 ψ   ∆x +∞ k=0 ω k i r n j+k+1   + ψ   ∆x +∞ k=0 ω k i r n j+k      = v max i ψ (ξ j+1 )∆x   +∞ k=0 ω k i r n j+k+2 - +∞ k=0 ω k i r n j+k+1   + v max i ψ (ξ j )∆x   +∞ k=0 ω k i r n j+k - +∞ k=0 ω k i r n j+k+1   = v max i ψ (ξ j+1 )∆x   +∞ k=1 (ω k-1 i -ω k i )r n j+k+1 -ω 0 i r n j+1   + v max i ψ (ξ j )∆x   +∞ k=1 (ω k i -ω k-1 i )r n j+k + ω 0 i r n j   = v max i (ψ (ξ j+1 ) -ψ (ξ j ))∆x   +∞ k=1 (ω k-1 i -ω k i )r n j+k+1 -ω 0 i r n j+1   + v max i ψ (ξ j )∆x   +∞ k=1 (ω k-1 i -ω k i )(r n j+k+1 -r n j+k ) + ω 0 i (r n j -r n j+1 )   = v max i ψ ( ξj+1/2 )(ξ j+1 -ξ j )∆x   +∞ k=1 M β=1 ω k i ∆ n β,j+k+3/2   + v max i ψ (ξ j )∆x   M β=1 N -1 k=1 (ω k-1 i -ω k i )∆ n β,j+k+1/2 -ω 0 i ∆ n β,j+1/2   ,
with ξ j ∈ I ∆x +∞ k=0 ω k i r n j+k , ∆x +∞ k=0 ω k i r n j+k+1 and ξj+1/2 ∈ I ξ j , ξ j+1 , where we set I(a, b) = min{a, b}, max{a, b} . For some ϑ, µ ∈ [0, 1], we compute

ξ j+1 -ξ j = ϑ∆x +∞ k=0 ω k i M β=1 ρ n β,j+k+2 + (1 -ϑ)∆x +∞ k=0 ω k i M β=1 ρ n β,j+k+1 -µ∆x +∞ k=0 ω k i M β=1 ρ n β,j+k+1 -(1 -µ)∆x +∞ k=0 ω k i M β=1 ρ n β,j+k = ϑ∆x +∞ k=1 ω k-1 i M β=1 ρ n β,j+k+1 + (1 -ϑ)∆x +∞ k=0 ω k i M β=1 ρ n β,j+k+1 -µ∆x +∞ k=0 ω k i M β=1 ρ n β,j+k+1 -(1 -µ)∆x +∞ k=-1 ω k+1 i M β=1 ρ n β,j+k+1 = ∆x +∞ k=1 ϑω k-1 i + (1 -ϑ)ω k i -µω k i -(1 -µ)ω k+1 i M β=1 ρ n β,j+k+1 + (1 -ϑ)∆xω 0 i M β=1 ρ n β,j-1 -µ∆xω 0 i M β=1 ρ n β,j+1 -(1 -µ)∆x   ω 0 i M β=1 ρ n β,j + ω 1 i M β=1 ρ n β,j+1   .
By monotonicity of ω i we have

ϑω k-1 i + (1 -ϑ)ω k i -µω k i -(1 -µ)ω k+1 i ≥ 0 .
Taking the absolute values we get

ξ j+1 -ξ j ≤ ∆x    +∞ k=2 ϑω k-1 i + (1 -ϑ)ω k i -µω k i -(1 -µ)ω k+1 i + 4ω 0 i    M ρ n ∞ ≤ ∆x    +∞ k=2 ω k-1 i -ω k+1 i + 4ω 0 i    M ρ n ∞ ≤ ∆x 6 W 0 M ρ n ∞ .
Until j ∆ n β,j ≤ K 1 for β = 1, . . . , M for some K 1 ≥ j ∆ 0 β,j , taking the absolute values and rearranging the indexes, we have

j ∆ n+1 i,j+1/2 ≤ j ∆ n i,j+1/2 1 -λ V n i,j+2 -V n i,j+1 + ∆t HK 1 ,
where

H = ρ ∞ v max M W 0 M 6M J 0 ρ ∞ ψ ∞ + ψ ∞ . Therefore, by (2.7) we get j ∆ n+1 i,j+1/2 ≤ j ∆ n i,j+1/2 (1 + ∆t G) + ∆t HK 1 , with G = v max M ψ ∞ W 0 M ρ ∞ . We thus obtain j ∆ n i,j+1/2 ≤ e Gn∆t j ∆ 0 i,j+1/2 + e HK 1 n∆t -1,
that we can rewrite as

TV (ρ ∆x i )(n∆t, •) ≤ e Gn∆t TV (ρ 0 i ) + e HK 1 n∆t -1 ≤ e HK 1 n∆t TV (ρ 0 i ) + 1 -1 ,
since H ≥ G and it is not restrictive to assume K 1 ≥ 1. Therefore, we have that TV (

ρ ∆x i ) ≤ K 1 for t ≤ 1 HK 1 ln K 1 + 1 TV (ρ 0 i ) + 1
, where the maximum is attained for some K 1 < e TV (ρ 0

i ) + 1 -1 such that ln K 1 + 1 TV (ρ 0 i ) + 1 = K 1 K 1 + 1 .
Therefore the total variation is uniformly bounded for

t ≤ 1 He TV (ρ 0 i ) + 1
.

Iterating the procedure, at time t m , m ≥ 1 we set K 1 = e m TV (ρ 0 i ) + 1 -1 and we get that the solution is bounded by K 1 until t m+1 such that

t m+1 ≤ t m + m He m TV (ρ 0 i ) + 1 . (2.15)
Therefore, the approximate solution has bounded total variation for t ≤ T with

T ≤ 1 H TV (ρ 0 i ) + 1 . Corollary 3. Let ρ 0 i ∈ (BV ∩ L ∞ ) (R; R + ). If (2.
3) holds, then the approximate solution ρ ∆x constructed by the algorithm (2.2) has uniformly bounded total variation on [0, T ] × R, for any T satisfying (2.10).

Proof. If T ≤ ∆t, then TV (ρ ∆x i ; [0, T ] × R) ≤ T TV (ρ 0 i ). Let us assume now that T > ∆t. Let n T ∈ N\{0} such that n T ∆t < T ≤ (n T + 1)∆t. Then

TV (ρ ∆x i ; [0, T ] × R) = n T -1 n=0 j∈Z ∆t ρ n i,j+1 -ρ n i,j + (T -n T ∆t) j∈Z ρ n T i,j+1 -ρ n T i,j ≤ T sup t∈[0,T ] TV(ρ ∆x i )(t,•) + n T -1 n=0 j∈Z ∆x ρ n+1 i,j -ρ n i,j .
We then need to bound the term

n T -1 n=0 j∈Z ∆x ρ n+1 i,j -ρ n i,j .
From the definition of the numerical scheme (2.2), we obtain

ρ n+1 i,j -ρ n i,j = λ ρ n i,j-1 V n i,j -ρ n i,j V n i,j+1 = λ ρ n i,j-1 V n i,j -V n i,j+1 + V n i,j+1 ρ n i,j-1 -ρ n i,j
.

Taking the absolute values and using (2.7) we obtain

ρ n+1 i,j -ρ n i,j ≤ λ v max i ψ ∞ M ρ n ∞ ω i (0)∆x ρ n i,j-1 + v max i ψ ∞ ρ n i,j-1 -ρ n i,j
.

Summing on j, we get

j∈Z ∆x ρ n+1 i,j -ρ n i,j = v max i ψ ∞ M ρ n ∞ ω i (0) ∆t j∈Z ∆x ρ n i,j-1 + v max i ψ ∞ ∆t j∈Z ρ n i,j-1 -ρ n i,j , which yields n T -1 n=0 j∈Z ∆x ρ n+1 i,j -ρ n i,j ≤ v max M ψ ∞ T sup t∈[0,T ] TV (ρ ∆x i )(t, •) + v max M ψ ∞ M W 0 T sup t∈[0,T ] ρ ∆x i (t, •) 1 ρ ∆x i (t, •)
∞ that is bounded by Corollary 2, Lemma 2 and Lemma 4.

Proof of Theorem 1

To complete the proof of the existence of solutions to the problem (1.1), (1.5), we follow a Lax-Wendroff type argument as in [START_REF] Blandin | Well-posedness of a conservation law with non-local flux arising in traffic flow modeling[END_REF], see also [START_REF] Leveque | Finite volume methods for hyperbolic problems[END_REF], to show that the approximate solutions constructed by scheme (2.2) converge to a weak solution of (1.1). By Lemma 2, Lemma 4 and Corollary 3, we can apply Helly's theorem, stating that for i = 1, . . . , M , there exists a subsequence, still denoted by ρ ∆x i , which converges to some

ρ i ∈ (L 1 ∩ BV)([0, T ] × R; R + ) in the L 1 loc -norm. Let us fix i ∈ {1, . . . , M }. Let ϕ ∈ C 1 c ([0, T [ ×R)
and multiply (2.2) by ϕ(t n , x j ). Summing over j ∈ Z and n ∈ {0, . . . , n T } we get

n T -1 n=0 j ϕ(t n , x j ) ρ n+1 i,j -ρ n i,j = -λ n T -1 n=0 j ϕ(t n , x j ) ρ n i,j V n i,j+1 -ρ n i,j-1 V n i,j .
Summing by parts we obtain

- j ϕ((n T -1)∆t, x j )ρ n T i,j + j ϕ(0, x j )ρ 0 i,j + n T -1 n=1 j ϕ(t n , x j ) -ϕ(t n-1 , x j ) ρ n i,j + λ n T -1 n=0 j ϕ(t n , x j+1 ) -ϕ(t n , x j ) V n i,j+1 ρ n i,j = 0. (3.1)
Multiplying by ∆x we get

-∆x j ϕ((n T -1)∆t, x j )ρ n T i,j + ∆x j ϕ(0, x j )ρ 0 i,j (3.2)
+ ∆x∆t

n T -1 n=1 j ϕ(t n , x j ) -ϕ(t n-1 , x j ) ∆t ρ n i,j (3.3)
+ ∆x∆t n T -1 n=0 j ϕ(t n , x j+1 ) -ϕ(t n , x j ) ∆x V n i,j+1 ρ n i,j = 0. (3.4) By L 1 loc convergence of ρ ∆x i → ρ i , it is straightforward to see that the terms in (3.2), (3.3) converge to R ρ 0 i (x)ϕ(0, x) -ρ i (T, x)ϕ(T, x) dx + T 0 R ρ i (t, x)∂ t ϕ(t, x) dx dt , (3.5)
as ∆x → 0. Concerning the last term (3.4), we can rewrite

∆x∆t n T -1 n=0 j ϕ(t n , x j+1 ) -ϕ(t n , x j ) ∆x V n i,j+1 ρ n i,j = ∆x∆t n T -1 n=0 j ϕ(t n , x j+1 ) -ϕ(t n , x j ) ∆x ρ n i,j V n i,j+1 -ρ n i,j V n i,j (3.6)
+ ∆x∆t

n T -1 n=0 j ϕ(t n , x j+1 ) -ϕ(t n , x j ) ∆x ρ n i,j V n i,j .
By (2.7) we get the estimate

ρ n i,j V n i,j+1 -ρ n i,j V n i,j ≤ v max i ψ ∞ ∆xM ρ 2 ∞ ω i (0).
Set R > 0 such that ϕ(t, x) = 0 for |x| > R and j 0 , j

1 ∈ Z such that -R ∈ ]x j 0 -1 2 , x j 0 + 1 2 ] and R ∈ ]x j 1 -1 2 , x j 1 + 1 2 ], then ∆x∆t n T n=0 j ϕ(t n , x j+1 ) -ϕ(t n , x j ) ∆x (ρ n i,j V n i,j+1 -ρ n i,j V n i,j ) ≤ ∆x∆t ∂ x ϕ ∞ n T n=0 j 1 j=j 0 v max i ψ ∞ M ρ 2 ∞ ω i (0) ∆x ≤ ∂ x ϕ ∞ v max i ψ ∞ M ρ 2 ∞ ω i (0) ∆x 2 R T ,
which goes to zero as ∆x → 0. Finally, again by the L 1 loc convergence of ρ ∆x i → ρ i , we have that

∆x∆t n T -1 n=0 j ϕ(t n , x j+1 ) -ϕ(t n , x j ) ∆x ρ n i,j V n i,j-1 2 → T 0 R ∂ x ϕ(t, x)ρ i (t, x)v i (r * ω i ) dx dt .

Numerical tests

In this section we perform some numerical simulations to illustrate the behaviour of solutions to (1.1) for M = 2 modeling two different scenarios. In the following, the space mesh is set to ∆x = 0.001.

Cars and trucks mixed traffic

In this example, we consider a stretch of road populated by cars and trucks. The space domain is given by the interval [-2, 3] and we impose absorbing conditions at the boundaries, adding N 1 = η 1 /∆x ghost cells for the first population and N 2 = η 2 /∆x for the second one at the right boundary, and just one ghost cell for both populations at the left boundary, where we extend the solution constantly equal to the last value inside the domain. The dynamics is described by the following 2 × 2 system

∂ t ρ 1 (t, x) + ∂ x ρ 1 (t, x)v max 1 ψ((r * ω 1 )(t, x)) = 0, ∂ t ρ 2 (t, x) + ∂ x ρ 2 (t, x)v max 2 ψ((r * ω 2 )(t, x)) = 0, ( 4.1)
with

ω 1 (x) = 2 η 1 1 - x η 1 , η 1 = 0.3, ω 2 (x) = 2 η 2 1 - x η 2 , η 2 = 0.1, ψ(ξ) = max {1 -ξ, 0} , ξ ≥ 0, v max 1 = 0.8, v max 2 = 1.3.
In this setting, ρ 1 represents the density of trucks and ρ 2 is the density of cars on the road. Trucks moves at lower maximal speed than cars and have grater view horizon, but of the same order of magnitude. Figure 2 describes the evolution in time of the two population densities, correspondent to the initial configuration

ρ 1 (0, x) = 0.5χ [-1.1,-1.6] , ρ 2 (0, x) = 0.5χ [-1.6,-1.9] ,
in which a platoon of trucks precedes a group of cars. Due to their higher speed, cars overtake trucks, in accordance with what observed in the local case [START_REF] Benzoni-Gavage | An n-populations model for traffic flow[END_REF].

Impact of connected autonomous vehicles

The aim of this test is to study the possible impact of the presence of Connected Autonomous Vehicles (CAVs) on road traffic performances. Let us consider a circular road modeled by the space interval [-1, 1] with periodic boundary conditions at x = ±1. In this case, we assume that autonomous and non-autonomous vehicles have the same maximal speed, but the interaction radius of CAVs is two orders of magnitude grater than the one of human-driven cars. Moreover, we assume CAVs have constant convolution kernel, modeling the fact that they have the same degree of accuracy on information about surrounding traffic, independent from the distance. In this case, model (1.1) reads with

           ∂ t ρ 1 (t, x) + ∂ x ρ 1 (t, x)v max 1 ψ((r * ω 1 )(t, x)) = 0, i = 1, ..., M, ∂ t ρ 2 (t, x) + ∂ x ρ 2 (t, x)v max 2 ψ((r * ω 2 )(t, x)) = 0, ρ 1 (0, x) = β (0.5 + 0.3 sin(5πx)), ρ 2 (0, x) = (1 -β) (0.5 + 0.3 sin(5πx)),
ω 1 (x) = 1 η 1 , η 1 = 1, ω 2 (x) = 2 η 2 1 - x η 2 , η 2 = 0.01, ψ(ξ) = max {1 -ξ, 0} , ξ ≥ 0, v max 1 = v max 2 = 1.
Above ρ 1 represents the density of autonomous vehicles, ρ 2 the density of non-autonomous vehicles and β ∈ [0, 1] is the penetration rate of autonomous vehicle. Figure 3 displays the traffic dynamics in the case β = 0.9. As a metric of traffic congestion, given a time horizon T > 0, we consider the two following functionals:

J(β) = T 0 d| ∂ x r| dt , (4.3)
Ψ(β) = T 0 ρ 1 (t, x)v max 1 ψ((r * ω 1 )(t, x)) + ρ 2 (t, x)v max 2 ψ((r * ω 2 )(t, x)) dt , (4.4)
where x = x 0 ≈ 0. The functional J measures the integral with respect to time of the spatial total variation of the total traffic density, see [START_REF] Colombo | Minimising stop and go waves to optimise traffic flow[END_REF]. Instead, the functional Ψ measures the integral with respect to time of the traffic flow at a given point x, corresponding to the number of cars that have passe through x in the studied time interval. Figure 4 displays the values of the functionals J and Ψ for different values of β = 0, 0.1, 0.2, . . . , 1. We can notice that the functionals are not monotone and present minimum and maximum values.

The traffic evolution patterns corresponding these stationary velues are reported in Figure 5, showing the (t, x)-plots of the total traffic density r(t, x) corresponding to these values of β. Proof. Let us assume that ρ n i,j ≥ 0 for all j ∈ Z and i ∈ 1, ..., M . It suffices to prove that ρ n+1 i,j in (A.1) is non-negative. Compute

ρ n+1 i,j = ρ n i,j + λ 2 α(ρ n i,j+1 -2ρ n i,j + ρ n i,j-1 ) + λ 2 ρ n i,j-1 V n i,j-1 -ρ n i,j+1 V n i,j+1 (A.5) = ρ n i,j-1 λ 2 α + V n i,j-1 + ρ n i,j (1 -λα) + ρ n i,j+1 λ 2 α -V n i,j+1 , (A.6)
under assumptions (A.3) and (A.4), we obtain that ρ n+1 i,j is positive. Proof. See proof of Corollary 2.

Lemma 6. (L ∞ -bound) If ρ 0 i,j ≥ 0 for all j ∈ Z and i = 1, ..., M , and the CFL conditions (A.3)-(A.4) hold, the approximate solution ρ ∆x constructed by the algorithm (A.2)-(A.1) is uniformly bounded on [0, T ] × R for any T such that

T < M ρ 0 ∞ v max M ψ ∞ W 0 -1 . (A.7)
Proof. From (A.6) we can define

ρ n+1 i,j = λ 2 ρ n i,j-1 α + V n i,j-1 + (1 -λα)ρ n i,j + λ 2 ρ n i,j+1 α -V n i,j+1
Let ρ = max ρ n i,j-1 , ρ n i,j , ρ n i,j+1 . Then we get

ρ n+1 i,j ≤ ρ 1 + λ 2 V n i,j-1 -V n i,j+1
and by (2.7)

V n i,j-1 -V n i,j+1 ≤ 2v max M ψ ∞ ∆x ω i (0)M ρ ∞ . (A.8) Therefore, until ρ n ∞ ≤ K, for some K ≥ ρ 0 ∞ , we get ρ n+1 ∞ ≤ ρ n ∞ 1 + M Kv max M ψ ∞ W 0 ∆t ,
and we can reason as in the proof of Lemma 2.

Lemma 7. (BV estimates)

Let ρ 0 i ∈ (BV ∩ L ∞ ) (R, R + ) for all i = 1, ..., M . If (A.4) holds and ∆t ≤ 2 2α + ∆x ψ ∞ W 0 v max M ρ ∞ ∆x, (A.9)
then the solution constructed by the algorithm (A.2)-(A.1) has uniformly bounded total variation for any T such that

T ≤ min i=1,...,M 1 D TV (ρ 0 i ) + 1 , (A.10) where D = ρ ∞ v max M W 0 M 3M J 0 ρ ∞ ψ ∞ + 2 ψ ∞ .
Proof. Subtracting the following expressions

ρ n+1 i,j+1 = ρ n i,j+1 + λ 2 α(ρ n i,j -2ρ n i,j+1 + ρ n i,j+2 ) + λ 2 ρ n i,j V n i,j -ρ n i,j+2 V n i,j+2 , ρ n+1 i,j = ρ n i,j + λ 2 α(ρ n i,j-1 -2ρ n i,j + ρ n i,j+1 ) + λ 2 ρ n i,j-1 V n i,j-1 -ρ n i,j+1 V n i,j+1 ,
we get

∆ n+1 i,j+1/2 = λ 2 α∆ n+1 i,j-1/2 + (1 -λα)∆ n i,j+1/2 + λ 2 α∆ n+1 i,j+3/2 + λ 2 V n i,j ∆ n i,j-1/2 + ρ n i,j-1 V n i,j -V n i,j-1 -V n i,j+2 ∆ i,j+3/2 + ρ i,j+1 V n i,j+1 -V n i,j+2
. Now, we can write

V n i,j -V n i,j-1 = v max i ψ (ξ j-1/2 )∆x +∞ k=0 ω k i M β=1 ρ n β,j+k -ρ n β,j+k-1 = v max i ψ (ξ j-1/2 )∆x +∞ k=0 ω k i M β=1 ∆ n β,j+k-1/2 = v max i ψ (ξ j-1/2 )∆x   M β=1 +∞ k=0 (ω k i -ω k+1 i )ρ β,j+k -ω 0 i ρ β,j-1   , and
V n i,j+2 -V n i,j+1 = v max i ψ (ξ j+3/2 )∆x +∞ k=0 ω k i M β=1 ρ n β,j+k+2 -ρ n β,j+k+1 = v max i ψ (ξ j+3/2 )∆x +∞ k=0 ω k i M β=1 ∆ n β,j+k+3/2 = v max i ψ (ξ j+3/2 )∆x   M β=1 +∞ k=1 (ω k-1 i -ω k i )ρ β,j+k+1 -ω 0 η ρ β,j+1   .
We get

∆ n+1 i,j+1/2 = = λ 2 α + V n i,j ∆ n i,j-1/2 + (1 -λα) ∆ n i,j+1/2 + λ 2 α -V n i,j+2 ∆ n i,j+3/2 + λ 2 ρ n i,j-1   v max i ψ (ξ j-1/2 )∆x   M β=1 +∞ k=0 (ω k i -ω k+1 η )ρ n β,j+k -ω 0 η ρ n β,j-1      - λ 2 ρ n i,j+1   v max i ψ (ξ j+3/2 )∆x   M β=1 +∞ k=1 (ω k-1 i -ω k i )ρ n β,j+k+1 -ω 0 i ρ n β,j+1      = λ 2 α + V n i,j ∆ n i,j-1/2 + (1 -λα) ∆ n i,j+1/2 + λ 2 α -V n i,j+2 ∆ n i,j+3/2 + λ 2 (ρ n i,j-1 -ρ n i,j+1 ) V n i,j -V n i,j-1 + λ 2 ρ n i,j+1   v max i ψ (ξ j-1/2 )∆x   M β=1 +∞ k=0 (ω k i -ω k+1 i )ρ n β,j+k -ω 0 η ρ n β,j-1   ± v max i ψ (ξ j+3/2 )∆x   M β=1 +∞ k=0 (ω k i -ω k+1 i )ρ n β,j+k -ω 0 i ρ n β,j-1   -v max i ψ (ξ j+3/2 )∆x   M β=1 +∞ k=1 (ω k-1 i -ω k i )ρ n β,j+k+1 -ω 0 i ρ n β,j+1      = λ 2 α + V n i,j ∆ n i,j-1/2 + (1 -λα) ∆ n i,j+1/2 + λ 2 α -V n i,j+2 ∆ n i,j+3/2 - λ 2 V n i,j -V n i,j-1 ∆ n i,j-1/2 + ∆ n i,j+1/2 + λ 2 ρ n i,j+1   v max i ψ (ξ j+1 )(ξ j-1/2 -ξ j+3/2 )∆x   M β=1 +∞ k=0 (ω k i -ω k+1 i )ρ n β,j+k -ω 0 η ρ n β,j-1   + v max i ψ (ξ j+3/2 )∆x   M β=1 +∞ k=0 (ω k i -ω k+1 i )(ρ n β,j+k -ρ n β,j+k+2 ) -ω 0 i (ρ n β,j-1 -ρ n β,j+1 ) = λ 2 α + V n i,j-1 ∆ n i,j-1/2 (A.11) + 1 -λα - λ 2 V n i,j -V n i,j-1 ∆ n i,j+1/2 (A.12) + λ 2 α -V n i,j+2 ∆ n i,j+3/2 (A.13) + λ 2 ρ n i,j+1   v max i ψ ( ξj+1 )(ξ j-1/2 -ξ j+3/2 )∆x   +∞ k=0 ω k i M β=1 ∆ n β,j+k-1/2   + v max i ψ (ξ j+3/2 )∆x   +∞ k=0 (ω k+1 i -ω k i ) M β=1 ∆ n β,j+k+1/2 + ∆ n β,j+k+3/2 +ω 0 i M β=1 ∆ n β,j-1/2 + ∆ n β,j+1/2      .
where ξj+1 ∈ I(ξ j+1/2 , ξ j+3/2 ). For some ϑ, µ ∈ [0, 1], we compute

ξ j-1/2 -ξ j+3/2 = ϑ∆x +∞ k=0 ω k i M β=1 ρ n β,j+k + (1 -ϑ)∆x +∞ k=0 ω k i M β=1 ρ n β,j+k-1 -µ∆x +∞ k=0 ω k i M β=1 ρ n β,j+k+2 -(1 -µ)∆x +∞ k=0 ω k i M β=1 ρ n β,j+k+1 = ϑ∆x +∞ k=0 ω k i M β=1 ρ n β,j+k + (1 -ϑ)∆x +∞ k=-1 ω k+1 i M β=1 ρ n β,j+k -µ∆x +∞ k=2 ω k-2 i M β=1 ρ n β,j+k -(1 -µ)∆x +∞ k=1 ω k-1 i M β=1 ρ n β,j+k = ∆x +∞ k=2 ϑω k i + (1 -ϑ)ω k+1 i -µω k-2 i -(1 -µ)ω k-1 i M β=1 ρ n β,j+k + ϑ∆x   ω 0 i M β=1 ρ n β,j + ω 1 i M β=1 ρ n β,j+1   + (1 -ϑ)∆x   ω 0 i M β=1 ρ n β,j-1 + ω 1 i M β=1 ρ n β,j + ω 2 i M β=1 ρ n β,j+1   -(1 -µ)∆x   ω 0 i M β=1 ρ n β,j+1   .
By monotonicity of ω η we have

ϑω k i + (1 -ϑ)ω k+1 i -µω k-2 i -(1 -µ)ω k-1 i ≤ 0.
Taking the absolute values we get

ξ j-1/2 -ξ j+3/2 ≤ ∆x    +∞ k=2 µω k-2 i + (1 -µ)ω k-1 i -ϑω k i -(1 -ϑ)ω k+1 i + 3ω i (0)    M ρ n ∞ ≤ ∆x    N -2 k=2 ω k-2 i -ω k+1 i + 3ω i (0)    M ρ n ∞ ≤ ∆x 6 ω i (0)M ρ n ∞ .
Observe that assumption (A.4) guarantees the positivity of (A.11) and (A.13). Similarly, (A.9) ensures the positivity of (A.12). Until j ∆ n β,j ≤ K 1 for β = 1, ..., M for some K 1 ≥ j ∆ 0 β,j , taking the absolute values and rearranging the indexes, we have

j ∆ n+1 i,j+1/2 ≤ j ∆ n i,j+1/2 1 + λ 2 V i,j-1 -V i,j+1 + ∆t DK 1 where D = ρ ∞ v max M W 0 M 3M J 0 ρ ∞ ψ ∞ + 2 ψ ∞ . Therefore, by (A.8) we get j ∆ n+1 i,j+1/2 ≤ j ∆ n i,j+1/2 (1 + ∆t C) + ∆t DK 1 with C = v max M ψ ∞ W 0 M ρ ∞ .
In this way we obtain

j ∆ n+1 i,j+1/2 ≤ e Cn∆t j ∆ 0 i,j+1/2 + e DK 1 n∆t -1,
that we can rewrite as

TV (ρ i,∆x )(n∆t, •) ≤ e Cn∆t TV (ρ 0 i ) + e DK 1 n∆t -1 ≤ e DK 1 n∆t TV (ρ 0 i ) + 1 -1, (A.14) since D ≥ 2C and it is not restrictive to assume K 1 ≥ 1 2 . Therefore we have that TV (ρ i,∆x ) ≤ K 1 for t ≤ 1 DK 1 ln K 1 + 1 TV (ρ 0 i ) + 1
, where the maximum is attained for some K 1 ≤ e TV (ρ 0

i ) + 1 -1 such that ln K 1 + 1 T V (ρ 0 i ) + 1 = K 1 K 1 + 1 .
Therefore the total variation is uniformly bounded for

t ≤ 1 De TV (ρ 0 i ) + 1 .
Iterating the procedure, at time t m , m ≥ 1 we set K 1 = e m TV (ρ 0 i ) + 1 -1 and we get that the solution is bounded by K 1 until t m+1 such that

t m+1 ≤ t m + m De m TV (ρ 0 i ) + 1 . (A.15)
Therefore, the approximate solution satisfies the bound (A.14) for t ≤ T with Let us make use of the definition of the numerical scheme (A.2)-(A.1), we obtain ρ n+1 i,j -ρ n i,j = λ 2 α + V i,j+1 (ρ i,j-1 -ρ i,j ) -λ 2 α -V i,j+1 (ρ i,j -ρ i,j+1 ) + λ 2 ρ i,j-1 V i,j-1 -V i,j+1 .

T ≤ 1 D TV (ρ 0 i ) + 1 . Corollary 5. Let ρ 0 i ∈ BV(R; [0, 1]). If (A.
If (A.4) holds, we can take the absolute value

ρ n+1 i,j -ρ n i,j = λ 2 α + V i,j+1 ρ i,j-1 -ρ i,j - λ 2 α -V i,j+1 ρ i,j -ρ i,j+1 + λ 2 ρ i,j-1 V i,j-1 -V i,j+1 .
Summing on j and rearranging the indexes we get j∈Z ∆x ρ n+1 i,j -ρ n i,j = ∆t 2 j∈Z ρ i,j+1 -ρ i,j 2α + V i,j+2 -V i,j+1

+ ∆t 2 j∈Z ρ i,j-1 V i,j-1 -V i,j+1 = ∆t 2 j∈Z ρ i,j+1 -ρ i,j 2α + v max M ψ ∞ ∆x ω η (0)M ρ ∞
as ∆x → 0. Concerning the last term, we can observe that g(ρ n i,j , ..., ρ n i,j+N ) -ρ n i,j V n i,j ≤ α 2 ρ n i,j+1 -ρ n i,j + 1 2 (ρ n i,j+1 -ρ n i,j )V n i,j+1 + ρ n i,j V n i,j+1 -V n i,j

≤ α + v max M ψ ∞ 2 ρ n i,j+1 -ρ n i,j + 1 2 W 0 ∆x TV (ρ i,∆x (t n , •))v max M ψ ∞ ≤ α + v max M ψ ∞ 2
ρ n i,j+1 -ρ n i,j + J ∆x.

where J = ϕ(t n , x j+1 ) -ϕ(t n , x j ) ∆x (g(ρ n i,j , ..., ρ n i,j+N ) -ρ n j V n i,j ).

By L 1 loc convergence of ρ i,∆x → ρ i and boundedness of ω i , the first term in the above decomposition converges to T 0 R ρ i (t, x)v(r * ω η )∂ x ϕ(t, x) dx dt .

Set R > 0 such that ϕ(t, x) = 0 for |x| > R and j 0 , j 1 ∈ Z such that -R ∈]x j 0 -1/2 , x j 0 +1/2 [ and R ∈]x j 1 -1/2 , x j 1 +1/2 [, then ∆x∆t n T -1 n=0 j ϕ(t n , x j+1 ) -ϕ(t n , x j ) ∆x (g(ρ n i,j , ..., ρ n i,j+N ) -ρ n i,j V n i,j )

≤ ∆x∆t ∂ x ϕ ∞ n T -1 n=0 j 1 j=j 0 α + v max M ψ ∞ 2 ρ n i,j+1 -ρ n i,j + J ∆x = α + v max M ψ ∞ 2 ∂ x ϕ ∞ ∆x∆t n T -1 n=0 j 1 j=j 0 ρ n i,j+1 -ρ n i,j + ∂ x ϕ ∞ J ∆x 2 R τ ≤ α + v max M ψ ∞ 2 ∂ x ϕ ∞ TV (ρ i,∆x (T, •))∆x + ∂ x ϕ ∞ J ∆x 2 R τ
which goes to zero when ∆x → 0. Finally, again by the L 1 loc convergence of ρ ∆x i → ρ i , we have that ∆x∆t n T -1 n=0 j ϕ(t n , x j+1 ) -ϕ(t n , x j ) ∆x ρ n i,j V n i,j → T 0 R ∂ x ϕ(t, x)ρ i (t, x)v i (r * ω i ) dx dt .

(H2) v max i are the maximal velocities, with 0 < v max 1 ≤ v max 2 ≤

 12 . . . ≤ v max M .

Figure 2 :

 2 Figure 2: Density profiles of cars and trucks at increasing times corresponding to the non-local model (4.1).

Figure 3 :Figure 4 : 9 Figure 5 :

 3495 Figure 3: Density profiles corresponding to the non-local problem (4.2) with β = 0.9 at different times.

Corollary 4 .

 4 (L 1 bound) For any T > 0, under the CFL conditions (A.3)-(A.4) the scheme (A.2)-(A.1) preserves the L 1 norm of the i-th component of ρ ∆x .

  3)-(A.4) holds, then the approximate solution ρ ∆x constructed by the algorithm (A.2)-(A.1) has uniformly bounded total variation on [0, T ] × R, for any T satisfying (A.10).Proof. Let us fix T ∈ R + such that (A.10) and (A.7) hold. If T ≤ ∆t, then TV (ρ i,∆x ; R × [0, T ]) ≤ T TV (ρ i,0 ). Let us assume now that T ≥ ∆t. Let M ∈ N\{0} such that n T ∆t < T ≤ (n T + 1)∆t. ThenTV (ρ i,∆x ; R × [0, T ]) -ρ n i,j + (T -n T ∆t) j∈Z ρ n T i,j+1 -ρ n T i,j ≤T sup t∈[0,T ] TV(ρ ∆x i )(t,•) then need to bound the term n T -1 n=0 j∈Z ∆x ρ n+1 i,j -ρ n i,j . (A.18)

  1 2 v max M ψ ∞ W 0 TV (ρ i,∆x (T, •)).Therefore, the last term in (A.22) can be rewrit-

	ten as
	∆x∆t	n T -1 n=0 j	ϕ(t n , x j+1 ) -ϕ(t n , x j ) ∆x	g(ρ n i,j , ..., ρ n i,j+N )
	= ∆x∆t	n T -1 n=0 j	ϕ(t n , x j+1 ) -ϕ(t n , x j ) ∆x	ρ n i,j V n i,j
			n T -1
	+ ∆x∆t
			n=0 j

Inria Sophia Antipolis -Méditerranée, Université Côte d'Azur, Inria, CNRS, LJAD,

route des Lucioles -BP 93, 06902 Sophia Antipolis Cedex, France. E-mail: {felisia.chiarello, paola.goatin}@inria.fr

Acknowledgements

The authors are grateful to Luis M. Villada for suggesting the non-local multi-class traffic model studied in this paper.

Appendix A Lax-Friedrichs numerical scheme

We provide here an alternative existence proof for (1.1), based on approximate solutions constructed via the following adapted Lax-Friedrichs scheme:

where α ≥ 1 is the viscosity coefficient and λ = ∆t ∆x . Lemma 5. For any T > 0, under the CFL conditions λα < 1, (A.3)

.

and multiply (A.1) by ϕ(t n , x j ). Summing over j ∈ Z and n ∈ {0, 1, ..., n T } we get

ϕ(t n , x j ) g(ρ n i,j , ..., ρ n i,j+N ) -g(ρ n i,j-1 , ..., ρ n i,j+N -1 ) .

Summing by parts we obtain

Multiplying by ∆x

By L 1 loc convergence of ρ i,∆x → ρ i , it is straightforward to see that the first two terms in (A.23) converge to R (ρ 0 i (x)ϕ(0, x) -ρ i (T, x)ϕ(T, x)) dx + T 0 R ρ i (t, x)∂ t ϕ(t, x) dx dt (A.25)


Julia Lawall

Gilles Muller

Coccinelle: 10 Years of Automated Evolution in the Linux Kernel

The Coccinelle C-program matching and transformation tool was first released in 2008 to facilitate specification and automation in the evolution of Linux kernel code. The novel contribution of Coccinelle was that it allows software developers to write code manipulation rules in terms of the code structure itself, via a generalization of the patch syntax. Over the years, Coccinelle has been extensively used in Linux kernel development, resulting in over 6000 commits to the Linux kernel, and has found its place as part of the Linux kernel development process. This paper studies the impact of Coccinelle on Linux kernel development and the features of Coccinelle that have made it possible. It provides guidance on how other research-based tools can achieve practical impact in the open-source development community.

Introduction

Today, everyone uses the Linux kernel, whether on a mobile phone (86% of the smartphones sold in the first quarter of 2017 were running Android [22]), in the cloud (at the end of 2016, 92% of virtual machine instances on Amazon's Elastic Compute Cloud (EC2) were running Linux), or on a supercomputer (at the end of 2017, all of the top 500 supercomputers were running Linux [START_REF] Vaughan-Nichols | Linux totally dominates supercomputers[END_REF]). To support these diverse computing environments, the size of the Linux kernel has been steadily growing, reaching 16.5 million lines of code in the recently released version 4.15 (Jan. 2018). Furthermore, the existing source code of the Linux kernel is continually changing, with around 13,000 commits per release recently, to improve security, performance or maintainability, as well as to provide support for new services such as new kinds of devices, file systems, or hardware architectures.

A stumbling block in this continual revision of the Linux kernel is that ultimately some developer has to modify the source code. Developers have limited time, may not fully understand what a given change entails, and are prone to making mistakes, particularly when changes affect many code sites, pervasively, across multiple kernel subsystems. These problems are further compounded by the fact that the Linux kernel has a widely dispersed and very diverse set of developers, ranging from core maintainers, with many years of experience, to occasional contributors, to developers of outof-tree code who do not participate in the Linux kernel developer community. Indeed, while over 1700 developers have contributed to each recent release, in each case a third or more of these developers have contributed only a single patch to that release. A potential solution is to formally specify changes and automate them. To be used in practice, such an approach must fit with the background and habits of the developers themselves.

The Coccinelle C-program matching and transformation tool was first released in 2008 to facilitate specification and automation of the evolution of Linux kernel code [START_REF] Padioleau | Documenting and automating collateral evolutions in Linux device drivers[END_REF]. Coccinelle was built around the observation that Linux kernel developers already have a precise notation for describing changes with which they are very familiar, the patch [START_REF] Mackenzie | Comparing and Merging Files With Gnu Diff and Patch[END_REF]. A patch is an extract of source code in which some lines are annotated withor + indicating that the line should be removed or added, respectively. All contributions to the Linux kernel pass in the form of patches through mailing lists where they are commented on by other developers, and thus developers are used to seeing and understanding them. Exploiting this background of kernel developers, Coccinelle is designed around a domain-specific language (DSL), SmPL (Semantic Patch Language), for expressing changes in terms of an abstracted form of patch, referred to as a semantic patch. Unlike a patch, which is tied to specific lines and files in the source code, a single semantic patch can update all relevant locations in the entire code base.

Today, Coccinelle has been under development for 12 years. 59 semantic patches are part of the Linux kernel source tree, and over 6000 Linux kernel commits, includ-ing 900 from Linux kernel maintainers, use Coccinelle. Coccinelle retains as a guiding principle the notion of an abstracted patch. Nevertheless, it has grown, both in terms of expressiveness and to improve performance, based on lessons learned from the experiences of Linux developers and other users. At the same time, it has successfully integrated into the Linux kernel community.

Coccinelle has been used in previous research [START_REF] Lawall | Fast and precise retrieval of forward and back porting information for Linux device drivers[END_REF][START_REF] Lawall | WYSIWIB: exploiting fine-grained program structure in a scriptable API-usage protocol-finding process[END_REF][START_REF] Lozi | Fast and portable locking for multicore architectures[END_REF][START_REF] Palix | Faults in Linux 2.6[END_REF]. This paper instead focuses on its evolution and impact. We examine its initial design (Sec. 2), and how that design has been refined in response to experience with the tool and feedback from users (Sec. 3). We then evaluate performance (Sec. 4) and the benefit of our expressivity extensions (Sec. 5), quantify the impact of Coccinelle in the Linux community (Sec. 6), and give an overview of its wider use (Sec. 7). Finally, we present some related work (Sec. 8) and conclude (Sec. 9), with lessons learned about dissemination of a research tool.

Initial Design of Coccinelle

Coccinelle development began in 2006. It was first made publicly available in binary in 2007 and in open source in 2008. We first review the original design decisions for Coccinelle, in terms of goals, expressivity, performance, correctness guarantees, and dissemination.

Goals

Coccinelle was initially designed to solve a specific problem, that of porting Linux device drivers from Linux 2.4, a previous stable version, to stable version Linux 2.6, which had been released shortly before the start of the project. The initial design was motivated by an earlier paper on collateral evolutions in the Linux kernel [START_REF] Padioleau | Understanding collateral evolution in Linux device drivers[END_REF], i.e., evolutions needed in API clients in response to changes in the API interface. The examples from that paper showed that to automate Linux kernel collateral evolutions it would be necessary to support transformations on scattered parts of the source code with various kinds of connections between them, including intraprocedural control-flow paths with specific properties. As a small research project could not encode the entire porting activity, these kinds of connections, derived from programanalysis concepts, would need to be expressed in a way that would be accessible to Linux driver developers, who could carry on the work. Targeting driver developers furthermore implied that Coccinelle would have to allow the user to reason about the code as it is shown to him, without simplification to an internal representation, and that it would have to treat a very large subset of C constructs, including various gcc extensions, according to the needs of arbitrary Linux kernel device driver code. Finally, the generated code would have to retain the structure of 1 @ rule1 @ 2 identifier fn, irq, dev_id; 3 typedef irqreturn_t; 4 @@ 5 static irqreturn_t 6 fn(int irq, void *dev_id) 7 { ... } 8 @@ 9 identifier rule1.fn; 10 expression E1, E2, E3; 11 @@ 12 fn(E1, E2 13 -,E3

14

)

Figure 1: The first semantic patch submitted to Linux the original source code, including comments and whitespace, to ensure the code's continuing maintainability.

Design decisions affecting expressivity

Coccinelle provides a transformation language SmPL (Semantic Patch Language) and an engine for applying SmPL semantic patches to C code. SmPL was conceived as a code pattern-matching language, mimicking the patch syntax. A SmPL semantic patch consists of a series of rules, analogous to patch hunks, each providing a code pattern to match or transform. Patterns are comprised of concrete syntax, ". . . ", and metavariables. Concrete syntax matches itself, ". . . " matches a possibly empty sequence of arbitrary terms, e.g., the list of statements between two other statements, and metavariables match arbitrary terms of a particular type. Metavariables are declared in a rule header and are used as ordinary variables in the pattern, to make the patterns close to the source code. Ideally, a Linux kernel developer should be able to copy a typical code example and add metavariable declarations, ". . . ", andand + annotations, to obtain a transformation rule with minimal effort. The semantic patch in Figure 1 illustrates the various features of SmPL. This semantic patch completes an evolution and associated collateral evolutions that had been initiated by a Linux developer. The evolution changed the type of a callback function, by removing its third parameter. This required additionally removing the third argument from direct calls to this function. This change is challenging because the names of the affected functions are all different, implying that grep may not be sufficient to find all occurrences. A common strategy is to identify code to fix by compiler errors, iterating until the kernel compiles successfully. In this case, some of the direct calls had been overlooked due to being under ifdefs or in the support for obscure architectures.

The semantic patch consists of two rules, on lines 1-7 and lines 8-14, respectively. The first rule, named rule1, declares three identifier metavariables fn, irq and dev id, representing the name of the function to match and the names of its two parameters, respectively. The rest of the first rule is a pattern that matches a function definition, in which the parameters and return value are indicated to have specific types (lines 5-6) and the body is allowed to be an arbitrary sequence of statements (line 7). The second rule, which has no name, declares four metavariables: the function name fn, whose value is explicitly inherited from the previous rule (line 9), and three expression metavariables, E1, E2, and E3, representing arbitrary argument expressions (line 10). The rest of this rule matches a call to the function that was identified in the first rule. In this call, the third argument is indicated to be removed (line 13). A wider variety of semantic patches is illustrated in various publications [START_REF] Lawall | WYSIWIB: exploiting fine-grained program structure in a scriptable API-usage protocol-finding process[END_REF][START_REF] Padioleau | Semantic patches for collateral evolutions in device drivers[END_REF][START_REF] Rodriguez | Increasing automation in the backporting of Linux drivers using Coccinelle[END_REF] and at the Coccinelle website [START_REF]Coccinelle website[END_REF][START_REF]Coccinellery[END_REF].

To apply a semantic patch to a code base, Coccinelle processes the C source code files one at a time. On each file, it applies the first rule of the semantic patch to each function or other top-level declaration, then applies the second rule to the code resulting from the first rule application, etc. Based on the needs observed in the prior collateral evolution study, the processing of a function is based on its intraprocedural control-flow graph. Thus, at the statement level, e.g., line 7 of Figure 1, ". . . " follows intraprocedural control-flow paths, using a semantics based on a variant of CTL model checking [START_REF] Brunel | A foundation for flow-based program matching: using temporal logic and model checking[END_REF]. By default, a pattern must match all control-flow paths starting from the control-flow graph node matching the beginning of the pattern, to ensure that the semantic patch describes a consistent view of the program behavior. For example, when a pattern such as A(); ... B(); matches code including a conditional, B(); must be reachable from A(); via both branches of the conditional. Alternatively, a rule or an individual instance of ". . . " can be annotated with exists to indicate that only the existence of a matching path is required. By default, ". . . " cannot contain any code that is matched by the code pattern immediately preceding or following it, e.g., to allow matching a call to a locking function and to the unlocking call closest to it, as needed due to the fine-grained locking found in the Linux kernel. Finally, a metavariable must match identical terms within a single control-flow path, but may match different terms in different control-flow paths, e.g., different conditional branches [START_REF] Brunel | A foundation for flow-based program matching: using temporal logic and model checking[END_REF].

Design decisions affecting performance

Coccinelle is intended to be used by a Linux developer in the course of his ordinary work, whenever a recurring transformation is needed. Accordingly, it must be usable on a standard laptop without much disruption. A number of the initial design decisions were guided by this goal.

The Linux kernel is very large, and indeed has more than tripled in size between Feb. 2007 (version 2.6.20, 5M LOC) and Jan. 2018 (version 4.15, 16.5M LOC). Processing the entire code base and achieving reasonable performance on a developer's laptop, thus requires making some tradeoffs. To reduce running time, Coc-cinelle focuses on regions of code that are most likely to be relevant for collateral evolutions, at the expense of the rest. A key observation is that an individual Linux kernel file typically addresses a problem at a given level of abstraction, while references to other files, via #include or function calls, typically move to a lower level of abstraction. Thus, the contents of header files and called functions may be less relevant for collateral evolutions.

Based on the above observation, by default, Coccinelle processes only .c files, includes only header files that are located in the same directory as the .c file or that have the same name as the .c file, and does not perform interprocedural analysis. Command-line options are provided to additionally process header files, independently of any files into which they may be included, and to include header files directly referenced in a .c file or all header files referenced recursively. The latter options, however, increase the amount of code processed, and thus the processing time. The use of these strategies is thus left up to the user, who is expected to know whether such information is relevant to the desired evolution. Finally, interprocedural analysis within a single file can be encoded up to a finite depth using a series of SmPL rules, each of which matches the definition of a function for which a function call was identified by a previous rule. More general interprocedural analysis originally required the use of external scripts to collect the names of called functions and to restart Coccinelle to process their definitions.

The only program analysis performed by Coccinelle is type inference. This analysis is best-effort, as noninclusion of header files means that type information may be unavailable. Although the type information is incomplete, the inclusion of type information makes Coccinelle very useful for tasks such as finding where a field of a particular type of structure is referenced, without knowing the name of the variable pointing to that structure. Coccinelle performs no alias analysis or other form of dataflow analysis. Semantic patches that require control over aliases have to implement it explicitly, e.g., by declaring that the code region matched by ". . . " cannot store the address of a given variable. This approach saves execution time, as the analysis is only performed if and to the extent that it is expected to be useful, and improves the predictability of the tool, as the semantic patch writer knows the strengths and limitations of the analysis.

Design decisions affecting correctness guarantees

Automatic program transformation has the potential to update code at a large scale reliably and efficiently, but it can also introduce pervasive bugs across a code base, if the transformation rules are incorrect or are implemented incorrectly by the transformation engine. Coc-cinelle only checks that a rule preserves the structural well formedness of the code, e.g., ensuring that a statement is replaced by a statement, an expression by an expression, etc. It does not check for semantic correctness. This enables encoding bug fixes, which are intrinsically not semantics preserving. Furthermore, it enables efficiently applying rules, without complicated, typically interprocedural, analysis to show correctness. The goal of Coccinelle is to allow the user to express his knowledge about the software and the required changes, in terms of code fragments that resemble the affected code and that can be easily checked to conform to the user's intent.

Dissemination strategy

Reaching potential users is always a challenge for research projects. An open-source development context provides a diverse audience, which increases the chance that individual users will pick up new approaches, but makes it harder to impose a new approach on the entire developer base than in a monolithic industry setting. This is particularly the case of the Linux kernel developer community, which puts few restrictions on the tools used by developers to create and manage code.

To validate the utility of Coccinelle and to encourage its use by Linux developers, the Coccinelle developers took the strategy of showing by example. The first submitted patches (e.g., 632155e65944 on June 1, 2007 [START_REF] Torvalds | Linux kernel source tree[END_REF]) exploited only the Coccinelle parser [START_REF] Padioleau | Parsing C/C++ code without pre-processing[END_REF]. Indeed, as Coccinelle does not expand macros or reduce ifdefs, its parser can find errors that are overlooked in typical compile testing. The first submitted patch generated by a semantic patch was 0da2f0f164f0 (July 5, 2007). This patch was created using the semantic patch of Figure 1, and included the semantic patch in the commit log. It updated five files in the net, atm, and usb directories.

The next patch dd00cc486ab1 based on a semantic patch was submitted on July 6, 2007, changing a call to the memory allocator kmalloc followed by a memset to clear the memory into a single call to the function kzalloc, added in 2005. This patch affected 166 calls distributed over 146 files. The semantic patch in the log message received the comment "Cool!" from a developer, 1 but the patch ran afoul of the Linux kernel requirement that patches on different parts of the kernel be submitted separately to the relevant maintainers. Indeed, Coccinelle had shifted the burden from performing the change, which was now fully automated, to routing the individual changes to the proper maintainers, for which no automatic support was then available.

The first patches explicitly mentioning "Coccinelle" were submitted in December 2007, fixing various missing resource-release errors (76832d841643, etc.). These 1 https://lkml.org/lkml/2007/7/7/98 attempted to set a precedent for how the tool should be used, by including the URL of the tool, as well as the XML-like tags <smpl> and </smpl> around the semantic patch, to ease the tracking of the use of the tool. The first commits from outside the group of Coccinelle developers, 77bbadd5ea89 and 52fd8ca6ad41, came in July 2008, from the developer of the kernel-level memory checker kmemcheck. These patches corrected the type of a flag passed to various lock-related function calls. Coccinelle was released as open source in October 2008.

Evolutions in the Coccinelle Design

In retrospect, the design decisions presented in the previous section reflect a number of fundamental hypotheses about how to design a program transformation system that will be useful to and used by kernel developers:

Expressivity: Linux kernel developers will find it easy and convenient to describe needed code changes in terms of fragments of removed and added code. Performance: Many interesting Linux kernel evolutions can be implemented reliably without incurring the cost of collecting and correlating information in multiple C files. Indeed, Linux kernel development relies on humans, who typically focus on one file at a time, and thus all relevant information should be directly apparent in a single C file. Correctness: Proving correctness is not necessary because Linux kernel developers can easily incorporate their knowledge of kernel invariants into a semantic patch. Giving the developer control over the rules implies that the developer can control the rate of false positives, and can easily check for them in the results. Dissemination: It is effective to show how a tool can be useful, rather than attempting to impose its use.

While Coccinelle still builds on these hypotheses, experience in using the tool and feedback from Linux kernel developers have provided lessons that have motivated various evolutions. We highlight those that have had the greatest impact on the use and usability of the tool.

Expressivity evolutions

Many changes, both simple and complex (e.g., Figure 1), can be expressed purely in terms of code structure. Some kinds of changes, however, require more semantic information. Two evolutions that have greatly enhanced the expressivity of Coccinelle have been the introduction of position variables and scripting rules.

Position variables. A position variable is a Coccinelle metavariable that matches the position where a term occurs in a file. Position variables allow rematching the 1 @ rule1 @ 2 expression t, f, e; 3 position p1, p2; 4 @@ 5 init_timer@p1(&t); 6 ... when != f = e 7 t.function =@p2 f; 8 9 @ rule2 @ 10 expression rule1.t, d, e; 11 position rule1.p1, p3; 12 @@ 13 init_timer@p1(&t); 14 ... when != d = e 15 t.data =@p3 d; Figure 2: init timer conversion same code in a later rule, as well as ensuring that a match in one rule is different than a match in an earlier rule.

Figure 2 illustrates the use of position variables to convert calls to init timer to setup timer when the init timer call is followed by initializations of the timer data and function fields. The first two rules (lines 1-15) identify instances of the same init timer call with two different properties (the when annotations in lines 6 and 14 indicate assignments that should not occur in the matched region). The last rule (lines 16-29) transforms init timer calls that satisfy both properties. This rule includes a disjunction, such that all of the relevant code fragments can be transformed at once, wherever they occur, as once a transformation takes place, all previously bound position variables are invalidated.

Scripting language interface. The scripting language interface was initially motivated by the goal of using Coccinelle for bug finding [START_REF] Stuart | Towards easing the diagnosis of bugs in OS code[END_REF]. While bugs that mainly depend on the code structure, such as use after free, could be found, the pattern-matching features of Coccinelle were not sufficient to detect bugs such as buffer overflows that require reasoning about variable values.

To allow reasoning about arbitrary information, support was added in 2008 for scripting-language rules. The first language supported was Python, which was expected to be familiar to Linux developers. Coccinelle is implemented in OCaml, and OCaml scripting was added in 2010, for the convenience of the Coccinelle developers. Scripts were originally designed to filter sets of metavariable bindings established by previous rules. Figure 3 shows an example, which drops a semicolon after an if header if the subsequent statement is indented, suggesting that the latter statement is intended to be the if branch. A script rule compares the indentation of the two statements (line 11) and discards metavariable binding environments (line 12) in which the conditional is aligned with or to the right of the subsequent statement.

Ultimately, the original motivation for scripting, i.e., finding bugs such as buffer overflows, was not success-1 @r@ 2 expression E; statement S; 3 position p1,p2; 4 @@ 5 if@p1 (E); 6 S@p2 7 8 @script:python@ 9 p1 << r.p1; p2 << r.p2;

10 @@ 11 if (p1[0].col >= p2[0].col): 12 cocci.include_match(False)
14 @@ 15 expression E; statement S; 16 position r.p1; 17 @@ 18 if@p1 (E) 19 -; 20 S Figure 3: Drop spurious semicolon after if header ful. The code patterns were small and generic, and the scripts implementing the required analyses were complex. Still, scripting has been a major leap forward for the expressiveness of Coccinelle, and new scripting functionalities have been added as new needs have emerged. Early on, libraries were added for generating formatted error messages. In 2009, initialize and finalize scripts were introduced to allow defining state global to the processing of all files, to facilitate the collection of statistics. In 2010, scripts became able to create new code fragments to be stored in metavariables and inherited by subsequent rules. In 2016, to improve performance and reduce semantic patch size, it became possible to add script code to metavariable declarations, to define predicates that would discard metavariable bindings early in the matching process. Finally, scripting enables iteration, which allows a semantic patch to submit new "jobs" to the Coccinelle engine, in order to perform analysis across multiple files.

Performance evolutions

While avoiding including header files reduces the volume of code to process, the Linux kernel remains a large and growing code base. Furthermore, parsing the code without relevant macro definitions from header files involves using heuristics, which can increase the parsing time. Thus, further optimizations were needed.

Indexing. An early observation was that performance could be improved by not parsing files that could not be matched by the semantic patch. Indeed, many semantic patches contain keywords such as the names of API functions that must be present for the semantic patch to match and that occur only a moderate number of times in the Linux kernel. Coccinelle initially used the Unix command grep to find the files containing these keywords, but this was still slow, given the large code size.

A second approach was to use glimpse [START_REF]Glimpse[END_REF] to prepare an index in advance, and then to only process the files indicated by the index. As the index is smaller than the kernel source code and is organized efficiently, the use of glimpse substantially improves performance, particularly for semantic patches that involve kernel API functions. Nevertheless, glimpse was originally only freely available to academic users, had to be manually installed, and creating an index on each kernel update is time-consuming. In 2010, this was complemented by support for id-utils, which is part of many Linux distributions and for which index creation is much faster. In 2013, the support for users who do not have an index available was rewritten to essentially reimplement the grep operation in OCaml, reducing system calls and better taking into account the specific needs of Coccinelle.

Parallelism. By default Coccinelle works on each .c file independently, and thus is ripe for parallelism. Nevertheless, when Coccinelle was first developed, there was no convenient support for parallelism in OCaml. Instead, the Coccinelle distribution included a shell script to launch multiple Coccinelle instances in parallel, each covering a different part of the code base. Users, however, were uneasy about using Coccinelle via an external script. Furthermore, processing different files can require very different amounts of time, and the lack of load balancing in this static solution meant that many cores could end up idle. Meanwhile, the Parmap OCaml parallelization library [START_REF] Danelutto | minimal disruption" skeleton experiment: seamless map & reduce embedding in OCaml[END_REF] became available, and between 2015 and 2017 increasing support was provided for parallelism, still at the .c file level, within Coccinelle itself.

Supporting finer grained parallelism, at the function level, was also considered. Initial experiments, however, suggested that the cost of passing around the state built up within the matching of a given file outweighed the benefits of parallelism. In contrast, Coccinelle treats each file independently, so the amount of state that needs to be passed between processes is minimal.

Correctness guarantee evolutions

Unlike the other cases, there have been no major evolutions in the view of transformation correctness. After having created over 450 semantic patches that have led to kernel patches, the Coccinelle developers have found that the original hypothesis that giving the developer control over the rules enables them to easily check the results is mostly sufficient. The few errors, e.g., [START_REF] Shevchenko | make 'bt sfi data' const[END_REF], have come from misunderstanding of kernel invariants that would require a prohibitively complex and time consuming semantic analysis to infer and check. Kernel maintainers have indeed concluded in some cases that it was the original code that was written in an error prone way [START_REF] Molnar | Revert "make 'bt sfi data' const[END_REF].

Dissemination strategy evolutions

Showing the value and capabilities of Coccinelle by the example of submitted patches generated initial interest in the tool. As the expressivity of Coccinelle evolved to permit the specification of more complex changes, it became apparent that it would also be beneficial to more directly teach developers how to use Coccinelle, and to enable Coccinelle users to interact with each other.

Four workshops were organized on the use of Coccinelle and advertised on the Coccinelle mailing list, attracting industry participants. The Coccinelle developers also presented the tool and offered tutorials in a variety of developer conferences, including those targeting opensource enthusiasts (e.g., FOSDEM) and those specifically targeting Linux kernel developers (e.g., Linux Plumbers). These presentations focused on the uservisible aspects of Coccinelle, such as how to write semantic patches and what results could be achieved, rather than the details of the internal design of the system, which were presented in research venues [START_REF] Brunel | A foundation for flow-based program matching: using temporal logic and model checking[END_REF].

The work on Coccinelle was also picked up by the Linux Weekly News (LWN), which is the standard reference for issues around the development of the Linux kernel and other open-source software. Tutorial articles on Coccinelle appeared in 2009 [START_REF] Henson | Semantic patching with Coccinelle[END_REF] and 2010 [START_REF] Sang | Evolutionary development of a semantic patch using Coccinelle[END_REF], authored not by the Coccinelle developers, but by wellknown kernel developers. LWN has also reported on various talks about Coccinelle [START_REF] Corbet | Lightning talks[END_REF][START_REF] Edge | Inside the mind of a Coccinelle programmer[END_REF].

Performance Evaluation

Coccinelle is intended to be used by a kernel developer as part of the normal development process, on a standard professional laptop. Accordingly, Coccinelle's performance should be acceptable in this setting. We illustrate the performance on a Lenovo Thinkpad T460s with two hyperthreaded 2.30GHz cores (Intel(R) Core(TM) i5-6200U CPU), a 3M cache, and 12G RAM. Our experiments focus on the 59 semantic patches found in the Linux 4.15 kernel, using the report mode, which is supported by all these semantic patches. 2 Times are based on a single run, with a timeout of 30 seconds per file. We use id-utils indexing. Figure 4 presents the elapsed time when running the semantic patches on the Thinkpad laptop, using both cores, with hyperthreading. The semantic patches are sorted in order of increasing running time.

For the Linux kernel, there is a precise performance point of reference that is familiar to the kernel developer; the time to perform a complete compile of the Linux kernel itself. The elapsed time for full kernel compilation on the Thinkpad laptop with 4 threads (hyperthreading) with make clean; make allyesconfig; make, is 54 minutes. Based on the results shown in Figure 4, all but one of the semantic patches complete within this time. The remaining semantic patch requires 75 minutes.

The timeout per file affects performance. In our experiment, Coccinelle timed out on 52 files, of 705,179 files considered, giving a timeout rate of 0.007%. Typically files on which timeouts occur contain complex code such as long sequences of loops and conditionals. These files can be analyzed separately, when more time is available.

Figure 5 shows the impact of indexing using id-utils on the number of files considered. The largest number of files considered is 46,336, in 10 cases, where no keywords are inferred from the semantic patch. These are associated with larger, but not the largest, execution times. At the far right of the graph, between 5000 and 26,000 files are considered, but the cost of tracing through all possible intraprocedural execution paths overwhelms the savings obtained by processing fewer files.

In terms of header files, 43 of the semantic patches specify that no include files should be considered. 11 specify to use the default (local and same-named files), and 1 specifies that all explicitly included should be taken into account. To assess the cost and benefit of including header files, we take the 44 semantic patches from the Linux kernel that complete in our test configuration in under 10 minutes and test them with options forcing the inclusion of no header files, the default, and all explicitly included header files. As compared to inclusion of no header files, the default increases the run time by up to 90% and the inclusion of all explicitly included header files increases the run time by up to 10x. The number of reports ranges from 1631 for no headers to 1691 for all headers, with most of the few differences on .h files.

The performance studied here is only relevant when scanning the entire kernel. When checking a single modified file, the time should rarely exceed a few seconds per semantic patch. Indexing may identify some semantic patches as irrelevant, reducing the execution time.

Expressivity Extension Evaluation

The position variable and scripting extensions increase the expressivity of SmPL, but add concepts that are not found in C code and thus are not already familiar to Linux developers. We thus assess the degree to which these features are used in practice. We note, however, that our only source of information about semantic patches is from those found in the Linux kernel and from those included in commit messages. This information may be incomplete, because developers can omit or simplify semantic patches in the commit message All of the semantic patches found in the Linux kernel use positions and scripts in order to generate output in the report mode. 20 semantic patches were contributed by developers from outside the Coccinelle team. 3325 commits up through Linux 4.15 contain semantic patches in the commit message. Of these 586 (18%) contain position variables and 165 (5%) contain scripts. 43% of the latter commits come from outside the Coccinelle team.

Impact on Linux

Over the past 10 years, Coccinelle has been increasingly applied to the Linux kernel, by both Coccinelle developers and Linux kernel developers. As of Linux 4.15, over 6000 commits in the Linux kernel are based on the use of Coccinelle. In this section, we give an overview of the impact of Coccinelle on the Linux kernel. Graphs by subsystem reflect commits up through the release of Linux 4.15 (Jan. 2018). Graphs by year end with 2017.

Changed lines per subsystem

Figure 6 shows the number of lines removed and added by commits using Coccinelle in various kernel subsystems. The most affected is drivers, with 57,882 removed lines and 77,306 added lines, followed by arch, fs, net, sound, and include, all of which are affected by thousands of removed or added lines. The predominance of drivers is not surprising, given that drivers makes up 67% of the Linux 4.15 kernel source code. drivers has also been a target for other bug finding and code reliability tools [START_REF] Machiry | CHECKER: A soundy analysis for Linux kernel drivers[END_REF][START_REF] Érillon | Devil: An IDL for hardware programming[END_REF][START_REF] Renzelmann | Testing drivers without devices[END_REF][START_REF] Ryzhyk | Improved device driver reliability through hardware verification reuse[END_REF][START_REF] Swift | Recovering device drivers[END_REF].

Figure 7 compares the numbers of removed and added lines to the number of code lines (non-blank, noncomment, measured using SLOCCount [START_REF]SLOCCount[END_REF]

Categories of users over time

A variety of kinds of developers contribute to the Linux kernel, by submitting patches. Among those who mention Coccinelle in their commit logs, we distinguish six categories of Coccinelle users:

Coccinelle developers. These are members of the Coccinelle development team, and persons employed by the team to disseminate Coccinelle.

Outreachy interns. The Linux kernel participates in the Outreachy internship program [START_REF] Outreachy | [END_REF] and interns may use Coccinelle in the application process or the internship. Dedicated user. This is a single developer who uses Coccinelle in the kernel for a small collection of widely relevant simple changes. 0-day. This is an automated testing service at Intel that builds and boots the Linux kernel for multiple kernel configurations, on each commit to hundreds of git trees.

The service also runs a number of static analysis tools, including Coccinelle, on the result of each commit. Kernel maintainers. These are kernel developers who receive and commit patches, and are generally responsible for some subsystem's continued well being. We identify maintainers as developers who are named in the Others. These are other Linux kernel contributors. These contributors may be frequent or occasional.

The top of Figure 8 shows the number of commits per year using Coccinelle from various kinds of Coccinelle users, while the bottom shows the number of Coccinelle users involved in each category. The first commits (2007) were from the Coccinelle development team. Use from maintainers and other kernel contributors started in the two years afterwards. The number of commits from maintainers has grown steadily, except for a major peak in 2015, when several maintainers undertook cross-tree refactoring projects using Coccinelle. The number of other kernel contributors has gone up and down, but shows an upward trend. These numbers may be underestimated, however, as some developers have revealed when asked that they used Coccinelle for repetitive changes, but did not mention it in the commit. 3The Linux developers who are most likely to have need for Coccinelle are those who perform large scale changes across the code base. To approximate this set of developers, we consider those who have at least one commit that touches at least 100 files, since Linux 3.0 (July 2011), i.e., the period in which Coccinelle was becoming more established. There are 88 such developers, of which 67 (76%) are maintainers. All but two of the others are in the Other category. 39 (44%) of these develop-ers overall and 31 (46%) of these maintainers have commits using Coccinelle. Of the 88 developers, 27 (31%) have 1-5 commits using Coccinelle, 9 (10%) have 6-100 such commits, and 3 (3%) have more than 100. Among the 67 maintainers, 21 (31%) have 1-5 commits using Coccinelle, 8 (12%) have 6-100 such commits, and 2 (3%) have more than 100. These numbers suggest that Coccinelle is well known among the Linux kernel developers and maintainers who can benefit from it most.

Finally, we consider the most established kernel contributors. We collect the set of maintainers from the Linux 4.15 MAINTAINERS file and the set of developers who have committed at least one patch between Linux 3.0 and Linux 4.15. 45 have at least 10 years of experience as committers and 117 have committed at least 1000 patches. 29% and 32% of these, respectively, have created at least one patch that uses Coccinelle. These numbers reflect the knowledge of Coccinelle at the core of the Linux kernel developer community.

Changes performed using Coccinelle

Coccinelle facilitates performing changes across the kernel, that may cover code managed by multiple maintainers. Some examples are as follows:

TTY. Remove an unused function argument. One commit (429b474990cb) in 2015, affecting 11 TTY driver files. The author is not a maintainer, but has over 350 commits in the Linux kernel, since 2013. IIO. Add missing devinit and devexit annotations. One commit (8e8287526844) in 2012 affecting 28 new IIO driver files. The author is an IIO maintainer. DRM. Eliminate a redundant field in a data structure. One commit (438b74a5497c) in 2016 affecting 54 direct rendering manager (DRM) files. The author is a maintainer, but not for the affected files. Interrupts. Prepare to remove the irq argument from interrupt handlers, and then remove that argument. 40 commits (e.g. f4acd122a738) in 2015, affecting 188 files (mostly drivers, arch). The author is a core Linux developer with over 3500 commits in the Linux kernel since the start of the Linux kernel's usage of git (2005).

More generally, Figure 9 characterizes as cleanups or bug fixes the complete set of patches that use Coccinelle from maintainers. Typical cleanups address generic C issues, such as useless double semicolons, as well as introductions of new APIs and refactorings in preparation for the introduction of new APIs. Commonly identified bugs include memory leaks, allocation of a memory region of the size of a pointer rather than the size of the referenced structure, and storing a potentially negative value in a variable of type unsigned int and then checking whether the value is less than zero. As noted in Section 2.5, Coccinelle facilitates making changes that affect the entire Linux kernel source tree, and in particular subsystems managed by different maintainers. While the initial problem of knowing who maintains which part of the kernel was resolved in 2009 by the introduction of the get maintainer.pl script, it is not always clear who should actually commit the changes, particularly when there are dependencies between the resulting patches. The problem of managing cross-tree changes was a proposed topic at the 2017 Linux Kernel Maintainers Summit. Preliminary discussions included proposing the use of Coccinelle for refreshing cross-tree changes when patch sets are incompletely applied [START_REF] Bottomley | Maintainer's summit agenda planning[END_REF].

Semantic patches in the Linux kernel

Since 2010, the Linux kernel has hosted a set of semantic patches in its scripts/coccinelle directory. Semantic patches are categorized as being related to APIs [START_REF] Engler | Checking system rules using system-specific, programmerwritten compiler extensions[END_REF], resource release [START_REF]Clang vs other open source compilers[END_REF], iteration [START_REF] Brunel | A foundation for flow-based program matching: using temporal logic and model checking[END_REF], locking (4), NULL values (4), test expressions (4) and others (18). The kernel Makefile contains a coccicheck target that runs one or all of these semantic patches on the entire kernel or some portion thereof. Kernel developers may thus easily use Coccinelle to check their work, without learning SmPL. Such use, however, is not visible in the kernel history.

As of Linux v4.15, there are 59 semantic patches in the Linux kernel. Figure 10 shows the number of commits including new semantic patches per year, as contributed by various categories of users. Semantic patches were initially contributed by the Coccinelle developers. Recently, 2-3 have been contributed each year, and a few more requested, by the wider kernel community.

0-day build testing service

Intel's 0-day testing service [START_REF] Kerrisk | Kernel build/boot testing[END_REF][START_REF]The kbuild-all archives[END_REF] runs a number of static analyses on commits to hundreds of Linux kernel git trees, both public and private. Kernel developers may check their changes themselves on only one configuration and then rely on the 0-day service for the rest. Coccinelle-based reports generated by the 0-day build testing service come in two forms. If the semantic patch producing the report is able to propose a fix for the identified problem, then the report contains this patch. The remaining Coccinelle-based reports contain a textual error or warning message, accompanied by a code extract highlighting the relevant lines, as indicated by the semantic patch. Figure 11 shows the number of public reports that mention Coccinelle in various categories, distinguishing between those that include a patch or only a message. Figure 12 likewise shows the percentage of all public reports mentioning Coccinelle. The most common type of report including a patch removes a field initialization in drivers that is redundant with respect to the driver core (244 patches). The most common type of report including only a message detects missing unlocks (68 reports). The latter reports are manually checked by a Coccinelle developer and have few false positives. Both semantic patches involve kernel-specific features.

The Coccinelle Community

A measure of the long term potential impact of a project is the willingness and ability of external developers to contribute to the project's development and maintenance. Today Coccinelle amounts to over 84,000 lines of OCaml code. 25 developers have contributed to Coccinelle, with over 3000 commits over 12 years for one developer, almost 1000 in the first few years for another developer, and 200-300 commits in the last few years for several others. All of the contributors with more than 5 commits have been somehow affiliated with the core development team, as either an employee or a guest. These numbers are likely related to the fact that the implementation language of Coccinelle, OCaml, is not widely used in the target developer community, and to the interdisciplinary nature of Coccinelle, which builds on programming-language concepts but targets the systems developer community. The small number of contributions by external developers may be a source of long term fragility. Nevertheless, the fact that several developers have joined the project in recent years and each made around 200 or more commits suggests that the code is accessible to developers who did not initiate the project.

Coccinelle is packaged with a number of Linux distributions, such as Ubuntu [62], Debian [15], Fedora [18], Gentoo [23], and Archlinux [START_REF]Archlinux[END_REF]. It is also available for FreeBSD [21] and NetBSD [40]. The full commit history is available at Github [START_REF]Coccinelle github repository[END_REF]. Although Coccinelle is developed using OCaml, there has been an effort to limit the amount of dependence on the traditional OCaml culture and infrastructure. Some needed OCaml libraries are bundled with the Coccinelle distribution, in case they are not available on the local machine. Once Coccinelle is installed, it is fully usable, via the C-like SmPL language and Python scripting, without knowing OCaml.

Although Coccinelle is mainly used on the Linux kernel, it is also used on other software projects. RIOT [START_REF]Riot[END_REF], qemu [47] and systemd [START_REF]Systemd[END_REF] include semantic patches in their source code distributions. Patches mentioning Coccinelle are also found in the commit histories of systems software projects such as cpython (d1302c01544 and 228b12edcce) [13], wine (f6ced24999f etc.) [START_REF] Wine | [END_REF], and even one in Firefox (ab4e3a0d4213) [19]. The latter used Coccinelle's rudimentary support for C++.

Related Work

Academic software development tools. Other academic software development tools that have had an impact on industry practice include CIL [START_REF] Necula | CIL: Intermediate language and tools for analysis and transformation of C programs[END_REF], LLVM [START_REF] Lattner | LLVM: A compilation framework for lifelong program analysis & transformation[END_REF], and Metal [START_REF] Engler | Checking system rules using system-specific, programmerwritten compiler extensions[END_REF]. CIL provides basic parsing and visitor infrastructure for processing C code, and is used for rapid prototyping as well as being at the base of mature tools such as Frama-C [START_REF][END_REF]. LLVM is a compiler infrastructure that originally targeted providing good support for static, link-time, and run-time optimization, and has evolved into a common alternative to gcc, due to its cus-tomizability, speed and space efficiency, and permissive license [START_REF]Clang vs other open source compilers[END_REF]. Neither has specifically targeted the Linux kernel and its particular coding style. Indeed, LLVM still does not fully support Linux kernel code, despite a long refactoring effort [START_REF]LLVM[END_REF]. Both tools have furthermore focused on building a user community rather than taking on the challenge of integrating into an existing one.

Metal is an automata-based tool for scanning large systems source code bases for faults such as use after free and inconsistent locking. It was never made publicly available. Instead, it was the foundation of the highly successful static analysis tool Coverity [START_REF] Bessey | A few billion lines of code later: using static analysis to find bugs in the real world[END_REF]. Coverity has been used on the Linux kernel more or less over the years, depending on the degree to which its results have been made freely available. Nevertheless, the freely available results address generic C issues, rather than Linux specific properties.

Development tool impact analysis. Koyuncu et al. [START_REF] Koyuncu | Impact of tool support in patch construction[END_REF] compare properties of Linux kernel patches that are entirely manually generated, manually generated in response to a tool report, and tool generated according to a manually written transformation rule. The patches in the third category are primarily generated by Coccinelle. They find that manually generated patches are accepted more quickly than tool-supported patches, but that the acceptance rate of the latter is increasing. Other tools used on the Linux kernel. Checkpatch is a regular-expression based style checker, whose use is required by the Linux kernel patch submission checklist [32]. It does not have a global view of the code, so it cannot detect inconsistencies that involve multiple code fragments, such as a variable declaration and its use.

Sparse [START_REF] Brown | Sparse: a look under the hood[END_REF] was an effort by Linus Torvalds to develop an open source static checker for the Linux kernel, in response to Metal. Sparse processes developer-provided annotations, enabling it to, e.g., detect endianness issues. Smatch [55] grew out of sparse as a more flexible bug finding tool. Like Coccinelle, Smatch is scriptable, but rules are expressed at the abstract-syntax tree level rather than at the source code level. Thus, the user needs to know about internal representations. Smatch also does only bug finding, not transformation. On the other hand, Smatch tracks variable values, while Coccinelle reasons only in terms of code structure. Thus, smatch can find bugs such as off-by-one errors that are difficult to find using Coccinelle. Thousands of commits in the Linux kernel are derived from the use of smatch, but the creation of new rules is mostly limited to the tool author.

Another academic effort on improving Linux kernel code is the Linux Driver Verification project [START_REF] Khoroshilov | Configurable toolset for static verification of operating systems kernel modules[END_REF]. It centers around developing infrastructure and rule sets making it possible to apply verification tools such as CPAchecker and BLAST to the Linux kernel. A few hundred commits in the Linux kernel are based on its results. The Undertaker project [6,[START_REF] Tartler | Revealing and repairing configuration inconsistencies in large-scale system software[END_REF], in contrast to the other tools, finds bug in the use of configuration variables.

Lessons Learned

In this paper, we have reviewed the evolution of the program transformation tool Coccinelle and its impact on the Linux kernel. The experience of Coccinelle can help guide other projects that want to have an impact on an open source systems developer community.

First, visibility is necessary. The Coccinelle developers taught by example, by using Coccinelle to make a sustained contribution to the Linux kernel. At the same time, they organized workshops on the use of Coccinelle and presented Coccinelle in a variety of developer conferences, both focusing on the user-visible aspects of Coccinelle, to make the tool accessible to developers.

Second, the tool must be easy to install and freely available. Coccinelle is implemented in OCaml, but targets C developers. There has been a concerted effort to minimize reliance on OCaml infrastructure. The cost is a complex build system, but it reduces the chance that users will immediately abandon Coccinelle because it is difficult to install. Likewise, Coccinelle is freely available (GPLv2), with no registration requirement.

Third, the tool must be easy to use and robust, with support to quickly address problems encountered by users. While many research prototypes are only robust enough to complete an evaluation for a paper submission, users will try it on all kinds of code, and use it in unanticipated ways. A strength of Coccinelle is its lax C parser, motivated by the need to parse code without reliance on header files. This has the side effect of allowing it to adapt to C variants used by different projects. On the other hand, many users have mentioned that the documentation, consisting mainly of a BNF, some examples and some tutorial presentations, is hard to understand. Nevertheless, Coccinelle has an active mailing list [START_REF]Coccinelle mailing list[END_REF] on which user problems are quickly addressed. Fixes are made available quickly via Github [START_REF]Coccinelle github repository[END_REF].

Finally, in a research setting, there is a constant temptation to make a tool do more, until the resulting complexity causes the tool to collapse under its own weight. While new features have been added to Coccinelle, the tool has remained within the scope of pattern matchingbased transformation of C code. This focus has allowed it to grow and achieve practical success in this area.

Availability. http://coccinelle.lip6.fr. This work was supported in part by ANR-NRF ITrans.

Figure 4 :Figure 5 :

 45 Figure 4: Elapsed time per semantic patch in the Linux 4.15 kernel on the Thinkpad laptop

Figure 7 :

 7 Figure 7: Lines removed and added by commits using Coccinelle per Linux 4.15 line of code, by subsystem

Figure 8 :

 8 Figure 8: Number of commits using Coccinelle from various categories of Coccinelle users (top) and number of Coccinelle users in various categories having at least one commit using Coccinelle (bottom)

Figure 9 :

 9 Figure 9: Cleanup vs. bug fix changes among maintainer patches using Coccinelle

Figure 10 :Figure 12 :

 1012 Figure 10: Number of commits adding a semantic patch to the Linux kernel source tree per year

  In contrast, we study what kinds of Linux kernel developers use Coccinelle, for what purpose, and what features of Coccinelle have led to its acceptance.

  ) found in Linux 4.15. The rate of Coccinelle-motivated changed

	lines of code (log scale)	10 1 10 3 10 5	arch	block	crypto	drivers Removed lines fs include init ipc kernel	lib	mm	net Added lines samples security sound	tools	virt
	Figure 6: Number of lines removed and added by com-
	mits using Coccinelle, by subsystem
						Removed lines			Added lines
	line change per LOC	0.0000 0.0020 0.0040 0.0060 0.0080	arch	block	crypto	drivers	fs	include	init	ipc	kernel	lib	mm	net	samples	security	sound	tools	virt

The semantic patches and Coccinelle version used contain some performance improvements that will appear in Linux 4.18 and Coccinelle 1.0.7, respectively.

https://marc.info/?l=kernel-janitors&m=150403263119030&w=2