Quentin L Meunier
email: quentin.meunier@lip6.fr

FastCPA: Efficient Correlation Power Analysis Computation with a Large Number of Traces

Keywords: Correlation Power Analysis, Side-Channel Attacks, Performance, Efficient Computation ACM Reference Format: Correlation Power Analysis Computation

Cryptographic algorithm implementations need to be secured against side-channel attacks. Correlation Power Analysis (CPA) is an efficient technique for recovering secret key bytes of a cryptographic algorithm implementation by analyzing the power traces of its execution. Although CPA usually does not require a lot of traces to recover secret key bytes, it is no longer true in a noisy environment, for which the required number of traces can be very high. Computation time can then become a major concern for performing this attack and assessing the robustness of an implementation against it. This article introduces FastCPA, which is a correlation computation targeting the same goal as regular CPA, but based on power consumption vectors indexed by plaintext values. The main advantage of FastCPA is its fast execution time compared to the regular CPA computation, especially when the number of traces is high: for 100,000 traces, the speedup factor varies from 70 to almost 200 depending on the number of samples.

An analysis of FastCPA accuracy is made, based on the number of correct key bytes found with an increasing noise. This analysis shows that FastCPA performs similarly as the regular CPA for a high number of traces. The minimum required number of traces to get the correct key guess is also computed for 100,000 noisy traces and shows that FastCPA obtains similar results to those of regular CPA. Finally, although FastCPA is more sensitive to plaintext values than the regular CPA, it is shown that this aspect can be neglected for a high number of traces.

INTRODUCTION

Cryptographic algorithm implementations need to be secured against side-channel attacks. Since the first differential power analysis (DPA) on the DES by Kocher et. al [START_REF] Kocher | Differential power analysis[END_REF], a lot of techniques based on side-channels information have been developed and enhanced for recovering secrets or assessing security against leakage: multi-bit DPA [START_REF] Bevan | Ways to enhance differential power analysis[END_REF][START_REF] Thomas S Messerges | Examining smart-card security under the threat of power analysis attacks[END_REF], correlation power analysis (CPA) [START_REF] Brier | Correlation power analysis with a leakage model[END_REF][START_REF] Mayer-Sommer | Smartly analyzing the simplicity and the power of simple power analysis on smartcards[END_REF], partitioning power analysis [START_REF] Le | A proposition for correlation power analysis enhancement[END_REF], mutual information analysis [START_REF] Gierlichs | Mutual information analysis[END_REF][START_REF] Prouff | Theoretical and practical aspects of mutual information based side channel analysis[END_REF] and statistical tests, especially specific and non specific Welch's T-Tests [START_REF] Coron | Statistics and secret leakage[END_REF][START_REF] Schneider | Leakage assessment methodology[END_REF]. These attacks and measures are carefully taken into account by system designers, especially for embedded systems, for which an attacker can measure the power consumption and the electromagnetic emanations, which are two of the main physical quantities used for non invasive attacks.

This article focuses on CPA, as it is an efficient technique for recovering a key given a simple power consumption model, and it usually requires a number of traces smaller by an order of magnitude than a DPA for recovering a key byte. If for an unprotected implementation running on a device without noise, a hundred of traces are usually sufficient to recover the key, protected implementations can require a huge amount of traces to assess their protection w.r.t. a type of attacks. Besides, real world devices usually contain much noise, and an attack may work only if the number of traces is very large. Finally, to assess the protection of a secure device against certain types of attacks, the designers need to consider a large amount of traces, since it corresponds to the worst case scenario, and resisting to an attack using 1,000 traces does not mean resisting to an attack using 100,000 traces. For these reasons, some works now consider the resistance of devices against up to a million of traces or more [START_REF] Schneider | Leakage assessment methodology[END_REF]. Therefore, having an efficient way for evaluating all types of attacks and tests is critical, as illustrated in [START_REF] Schneider | Robust and One-Pass Parallel Computation of Correlation-Based Attacks at Arbitrary Order -Extended Version[END_REF], which highlights the high computational demand of the CPA and proposes a parallel implementation for a CPA at any order. Besides, several works have brought significant improvements in the T-Test computation complexity [START_REF] Adam Ding | Simpler, faster, and more robust t-test based leakage detection[END_REF][START_REF] Reparaz | Fast Leakage Assessment[END_REF][START_REF] Schneider | Leakage assessment methodology[END_REF].

The basics of CPA are described in Section 2, and related work is discussed in section 3. We then introduce FastCPA, which is an efficient correlation coefficient computation allowing to recover secret key bytes, and describe the approach in Section 4. We show that FastCPA allows to significantly reduce the computation time of the CPA, especially when the number of traces is large (typically more than 1,000) in Section 5. We also show that this modification gives similar results in terms of detection accuracy. Finally, we conclude in Section 6.

CPA BASICS

CPA was first introduced by Brier et. al in [START_REF] Brier | Correlation power analysis with a leakage model[END_REF]. It is based on a power consumption model of the running device at some point in time, which must depend on certain secret bits, and on some input bits which change for each trace (namely the plaintext). For the AES, the time instant mostly used for performing the attack is after the first SBox, because it is the place where the linearity between the plaintext and the key is broken and with the finest granularity, i.e. where key bytes are not yet mixed together, allowing for few key values hypotheses. Similarly, the attack can be performed before the last SBox and target the last round key. The most widely used consumption models are the Hamming distance between two relevant values (e.g. stored consecutively in the same register), or simply the Hamming weight of a particular value. Then, this model is correlated with actual power consumption measures using the empirical Pearson's correlation coefficient. This empirical correlation coefficient between two samples x i and

y i (1 ≤ i ≤ n) is given by: r = σX,Y σX σY (1) with σX,Y = 1 N N i=1 (x i -x )(y i -y) (2) σX = 1 N N i=1 (x i -x ) 2 , σY = 1 N N i=1 (y i -y) 2 (3)
where x and y are the empirical means of x i and y i .

In the following, we focus on one key byte as the attack to recover key bytes independently. More specifically, given N power traces of length L, we note by t n,i the consumption value of point i in trace n (with 1 ≤ n ≤ N , 1 ≤ i ≤ L). For K possible subkeys (typically K = 256), we note h n,k the power estimation in trace n (depending on the plaintext), assuming the subkey is k (0 ≤ k < K). With these data, we can see how well our model and measurements match for each guess k at each time instant i, by calculating:

r k,i = N n=1 (h n,k -h k )(t n,i -t i ) N n=1 (h n,k -h k ) 2 N n=1 (t n,i -t i ) 2 (4)
in which h k and t i are respectively the average values of the modeled power consumption and the measured power consumption at instant i.

We can show that r i,k can be equivalently computed with the following formula, which is more efficient because it allows for online computation (i.e. the data set needs to be traversed only once):

r k,i = N N n=1 h n,k t n,i -( N n=1 h n,k )( N n=1 t n,i ) (( N n=1 h n,k ) 2 -N N n=1 h 2 n,k )(( N n=1 t n,i ) 2 -N N n=1 t 2 n,i ) (5)
Then, by taking the maximum of the r k,i over all the values for i and k, we can deduce which key hypothesis is the most probable (the maximum over i is required since we do not know a priori at which instant in the trace our power model applies).

An algorithm for computing such a correlation coefficient based on Equation 5 is shown in Algorithm 1. In particular, we can note that the complexity of this algorithm is proportional to N × K × L, what can be somewhat prohibitive: an AES round typically is 6,000 samples (using 4 samples per cycle), what makes more than 153 billions iterations of the innermost loop for 100,000 traces! Algorithm 1 Algorithm for computing the correlation coefficient Require: N traces with L points of measure, a power model h n,k

for each key hypothesis k and trace n Ensure: The key byte value with highest correlation w.r.t. the power consumption model is returned

for all i ∈ [1; L] do sum_t i ← 0 sum_t 2 i ← 0 end for for all k ∈ [0; K -1] do sum_h k ← 0 sum_h 2 k ← 0 for all i ∈ [1; L] do sum_ht k,i ← 0 end for end for for all n ∈ [1; N ] do for all i ∈ [1; L] do sum_t i ← sum_t i + t n,i sum_t 2 i ← sum_t 2 i + t 2 n,i end for for all k ∈ [0; K -1] do sum_h k ← sum_h k + h n,k sum_h 2 k ← sum_h 2 k + h 2 n,k for all i ∈ [1; L] do sum_ht k,i ← sum_ht k,i + t n,i • h n,k end for end for end for MaxCorrCoeff ← 0 MaxKHyp ← 0 for all i ∈ [1; L] do for all k ∈ [0; K -1] do CorrCoeff ← N •sum_ht k, i -sum_h k •sum_t i ((sum_h k ) 2 -N •sum_h 2 k )((sum_t i ) 2 -N •sum_t 2 i ) if |CorrCoeff| >MaxCorrCoeff then MaxCorrCoeff ← |CorrCoeff| MaxKHyp ← k end if end for end for return MaxKHyp
In opposition, the method proposed in this article requires less than 1 billion iterations of the innermost loop for the same configuration.

RELATED WORKS

Since the first works on CPA, the focus has first been on the method accuracy, and recently moved on the computation effectiveness.

In [START_REF] Le | A proposition for correlation power analysis enhancement[END_REF], the authors try to unify the concepts of DPA, multi-bit DPA and CPA via the concept of Partitioning Power Analysis (PPA). The article defines classes in which all the traces are partitioned, depending on their Hamming weight at a given moment in the computation. The correlation is then computed on the classes using different weights for the different classes. The authors show that CPA is a particular case PPA. Although the work presented in this article uses the same principle of classes as well, it is not a particular case of PPA since the classes are not based on Hamming weights but directly on values. Besides, [START_REF] Le | A proposition for correlation power analysis enhancement[END_REF] focuses on key recovery accuracy and does not consider computation time.

The work described in [START_REF] Kim | Biasing power traces to improve correlation power analysis attacks[END_REF] presents an improvement of CPA which consists in selecting a biased subset of the power traces containing more information than the average traces. The selection process tries to maximize the signal to noise ratio, by selecting the traces which are located at the extremities of the empirical probability density function. This article does not focus on execution time, and in particular does not present a computational analysis in terms of execution time: overhead linked to the selection process, and time saved thanks to the reduction of traces.

More recently, [START_REF] Schneider | Leakage assessment methodology[END_REF] presented a very effective way to compute the T-Test requiring only a single pass on the set of traces, allowing to compute regularly the T-Test value and to potentially stop before all the traces have been processed. The method uses the higher order central moments and is stable at least up to the fifth order. However, the proposed method is not applicable to CPA.

The method presented in [START_REF] Reparaz | Fast Leakage Assessment[END_REF] also targets an effective computation of the T-Test by representing the set of traces at each instant by a vector containing, for each possible measured value, the number of times that the corresponding value has been measured. This technique allows to decouple the estimation of measurements distributions and the computation of the statistical moments, which thus becomes independent from the number of traces. The work presented in this article also uses the idea to gather values in a vector, this time not indexed by the measured value, but by the plaintext value. To the best of our knowledge, the method proposed in this article has not been proposed in prior works.

FASTCPA

This Section first presents our proposed algorithm for performing the correlation power analysis, and then we expose the rationale of the proposed approach compared to the original CPA.

Algorithm

Similarly to the original CPA, our proposed method for performing the correlation power analysis on an attacked key byte targets an intermediate value in the computation. The method is based on the idea to create, at each point in time, a vector of consumption values indexed by the plaintext byte value. The i t h element of such a vector thus represents the average measured consumption for all runs where the plaintext value was i at a given point in time. During the first phase of the algorithm, these vectors are created in a single pass, requiring N × L iterations.

In a second part, these vectors are correlated, for each point in time, with vectors of identical length containing a consumption model, for all key hypotheses. These consumption model vectors are also indexed by the plaintext value, and contain typically the Hamming weight of the targeted internal value. This second phase takes L × K 2 iterations.

The proposed algorithm is shown in Algorithm 2. In this algorithm, the CompCC function calculates the correlation coefficient between the two vectors and is given in Algorithm 3.

Algorithm 2 Proposed FastCPA algorithm

Require: N traces with L measure points, a pre-computed vector of the power consumption model h k for each key hypothesis k, with the associated means and variances. We typically have

h k [pt] = h k,pt = HW(SBox[k ⊕pt]

Rationale

Compared to the original correlation coefficient computation, this method puts the same weight on each of the plaintext possible value in the correlation computation, and correlates only K points. For example, if we consider a 2-bit plaintext for simplicity and if we have 1,000 traces for plaintext value "0", 100 for plaintext values "1"

Algorithm 3 Function CompCC

Require: u and v two vectors of K values, with their respective means µ 0 , µ 1 and their respective variances σ 2 0 , σ 2 1 Ensure: The empirical correlation coefficient between the two vectors is returned

µ 01 ← 0 for all k ∈ [0; K -1] do µ 01 ← µ 01 + u[k ]v[k ]-µ 01 k +1
end for return

µ 01 -µ 0 µ 1 σ 2 0 σ 2 1
and "2", and only 5 for plaintext value "3", all four plaintext values consumptions are weighted the same and count as much the proposed correlation computation. Indeed, it is not obvious that each of the 1,000 power consumption values for the plaintext value "0" should count as much as each of the 5 values for plaintext value "3": intuitively, we feel that this 5 values contain more information than 1/200 of all measured values. Yet, putting the same weight is still not ideal because of the variability -having less values means less confidence in the average -but we can see that the question of the best way of computing the correlation is not trivial. We can also notice that the quantities computed in the case where the number of traces is identical for each plaintext value are different from those of the original CPA. This shows the need to assess experimentally the efficiency of the proposed computation compared to the original one.

More formally, if we define T i the set of measures at instant i, T v i the restriction of T i for traces in which the plaintext value is v, and η k,v the power consumption model for key guess k and plaintext value v, the formula for the computed correlation coefficient is (assuming plaintext values are in [0; K -1]):

r k,i = K -1 v=0 (η k,v -η k )(τ i,v -τ i ) K -1 v=0 η k,v -η k 2 K -1 v=0 τ i,v -τ i 2 (6)
with:

τ i,v = 1 |T v i | t ∈T v i t, τ i = 1 K K -1 v=0 τ i,v , η k = 1 K K -1 v=0 η k,v (7)
We can note that τ i is not the average power consumption measured at instant i, but the average of the averages for all plaintext values.

EXPERIMENTAL EVALUATION

This Section evaluates FastCPA on a standard AES implementation compared to the traditional correlation coefficient used for CPA (Ref. CPA) w.r.t. two criteria: the execution time, and the accuracy of both methods for several configurations. For all experiments and configurations, the traces were recorded by the ChipWhispererPro (R) platform [START_REF]ChipWhisperer Pro Platform[END_REF] with an Xmega target board.

Execution Time

We measured the execution times of both methods for a CPA targeting a key byte after the first SBox, for the configurations listed in Table 1. The computations, implemented as a single-threaded program, were run on an Intel (R) Xeon E5-2637 v2 processor at 3.50 GHz, and the code for both versions has been compiled with gcc 4.8 and optimisation level O2. The results are shown in Figure 1. We can see that the FastCPA computation method is way faster than the original CPA computation, achieving speedup factors from ×2 (2,000 traces of 1,000 samples) to ×191 (100,000 traces of 10,000 samples).

To allow for more readable results of FastCPA, we provide Table 2 which contains the execution times of this proposed method.

As expected, the larger the configuration is in terms of number of samples and traces, the greater speedup FastCPA exhibits compared to the reference CPA. We can note the that FastCPA computation time seems less sensitive to the number of traces than to the number of samples: when the former is multiplied by 10, the execution time is roughly multiplied by 2, whereas when the latter is multiplied by 10, the execution time is roughly multiplied by 10 as well.

Method Accuracy

To evaluate the method accuracy w.r.t. the reference CPA, we cannot just compare the values of the correlation coefficients of both methods, as the coefficients will be higher with FastCPA due to the fact that the number of points is to correlate is smaller (256 vs. number of traces). Thus, we compare the number of correct key guesses as the noise increases, for a recorded set of traces and for both methods. The noise added is a centered gaussian noise. Two configurations are considered for this experiment:

• Configuration 1: 5,000 traces comprising 3,000 samples, with a Gaussian noise added ranging from σ = 0 (16 correct key bytes for both methods) to σ = 0.2 (16 incorrect key bytes for both methods), with steps of 0.01; • Configuration 2: 100,000 traces comprising 3,000 samples, with a Gaussian noise added ranging from σ = 0.3 (16 correct key bytes for both methods) to σ = 0.90 (16 incorrect key bytes for both methods), with steps of 0.01;

The values of σ should be considered knowing that all the recorded samples values are in the interval [-0.7; 0.1].

The goal of configuration 1 is to assess that even with a relatively low number of traces, the proposed method performs decently. At the opposite, configuration 2 corresponds to the case where more traces are required to perform an attack because of the presence of noise, and therefore where more computation is required.

The results for configuration 1 are presented in Figure 2(a). We can see that for 5,000 traces, the reference CPA seems to perform a little better, since the drop in the number of key bytes correctly found happens for a slightly higher noise.

However, the results for configuration 2 with 100,000 traces indicate that while being a lot faster, the precision of FastCPA is very similar to the reference CPA, as shown on Figure 2(b). We believe that this experimentation illustrates the situations where FastCPA shows all of its usefulness.

To strengthen the confidence in FastCPA accuracy, we also measured for each byte the minimum number of traces required to get the correct key value (for any higher number of traces), and compared it for both methods. Obviously, for non noisy traces, the regular CPA performs better since it can get the correct key in 30 to 100 traces, whereas a minimum number of traces is required for FastCPA to get it (see section 5.3). Thus, we performed this measure for an arbitrary standard deviation noise value of 0.3, since all key bytes are still correctly found for both methods for such a noise. The results are shown in Figure 3. We can see that the results for both methods do not differ significantly, except for key byte 12 for which FastCPA requires almost 90K traces, while the reference CPA only requires 68K traces.

Plain Text Sensitivity

The proposed approach is more sensitive to the plaintext values in the sense that the correlation given by the function CompCC will be low until all (or almost) of the plaintext possible values have been reached by at least one run. This effect is visible on the Figure 4 which shows the correlation coefficients obtained for one key byte 1 for a number of traces varying between 1 and 5,000. There are several ways to take this drawback into account. First, the traces can be ordered so that plain values do not appear twice as long as all of them have not been encountered. Second, the CompCC function can be adapted to only consider the points of the vector for which at least one run had the corresponding plaintext. This allows to suppress this effect and gives the curve a similar aspect to the one of the original correlation. However, this is not necessarily desirable since this lengthen the compute time of the function, and after a sufficient number of traces, the corresponding code modification becomes useless. Finally, table 3 shows the probability to not have reached all plaintext values, supposing uniformly and independent plaintexts, after some number of traces for 256 possible plaintext values. We can see that after 4,000 runs, the probability of not reaching all plaintext possible values is less than 0.005 %, suggesting that we can neglect this aspect for a high number of traces. 1 The curves shapes are representative of all other key bytes

CONCLUSION

In this article, we proposed a new method, called FastCPA to perform a correlation power analysis in order to recover secret key bytes. This method consists in gathering measures by plaintext values and build a profile vector indexed by plaintext values, which is then correlated to a power consumption model vector. The proposed method achieves up to ×200 speedups compared to the original CPA computation, and is particularly efficient when the number of traces is high. The proposed method's accuracy to recover secret key bytes is comparable to the original CPA for two different metrics, namely the number of correct key bytes found for an increasing gaussian noise added to the traces, and the minimum number of traces required to get the correct key guess.

Future work includes the study of combining FastCPA with existing techniques for reducing the number of traces or for improving its accuracy. We also intend to adapt the correlation computation by giving different weights to the vector elemnts depending on the number of corresponding samples. Finally, we intend to make experiments with up to one million traces for both methods to assess the scalability of the proposed approach.

Figure 1 :

 1 Figure 1: Execution time results for both methods, for traces containing 1,000 samples (a), 3,000 samples (b), 6,000 samples (c), 10,000 samples (d), for a varying number of traces.

Figure 2 :

 2 Figure 2: Number of correct key bytes for both methods, with a varying gaussian noise added, for configurations 1 (a) and 2 (b)

Figure 3 :

 3 Figure 3: Minimum number of traces required for getting the correct key guess for any greater number of traces, for a gaussian noise with standard deviation σ = 0.3. The lower the better.

Figure 4 :

 4 Figure 4: Plain Text Sensitivity: correlations obtained for one key byte for both methods for each key guess, for a number of traces varying between 1 and 5,000. The red line corresponds to the correct key guess, the blue lines to bad key guesses.

  ). Ensure: The key byte value with highest correlation w.r.t. the power consumption model is returned ComputeMeanAndVar(MeanPower i ) for all k ∈ [0; K -1] do ▷ µ 1 and σ 2 1 are pre-computed values corresponding ▷ respectively to the mean and the variance of h k ▷ The function CompCC computes the correlation coef-▷ ficient between the two vectors MeanPower i and h k CorrCoeff ← CompCC(MeanPower i , µ 0 , σ 2 0 , h k , µ 1 , σ 2

	end for
	end for
	MaxCorrCoeff ← 0
	MaxKHyp ← 0
	for all i ∈ [1; L] do
	µ 0 , σ 2 0 ← 1 ) if |CorrCoeff| >MaxCorrCoeff then
	MaxCorrCoeff ← |CorrCoeff|
	MaxKHyp ← k
	end if
	end for
	end for
	return MaxKHyp

for all pt ∈ [0; K -1] do for all i ∈ [1; L] do MeanPower i,pt = 0; NumValues i,pt = 0; end for end for for all n ∈ [1; N ] do pt ← plaintext[n]; for all i ∈ [1; L] do NumValues i,pt ← NumValues i,pt + 1 MeanPower i,pt ← MeanPower i,pt + t n,i -MeanPower i,pt NumValues i,pt

Table 1 :

 1 Parameters of the CPA attack on an AES key byte for execution time measurements

	Number of samples (L)	{ 1,000; 3,000; 6,000; 10,000 }
	Number of traces (N)	{ 2,000; 5,000; 10,000; 20,000;
		50,000; 100,000 }
	Number of key values (K) { 256 }

Table 2 :

 2 FastCPA Execution Time (in seconds)

			# Traces
	# Samples	1,000	3,000	6,000	10,000
	2,000	0.49	1.48	3.16	5.32
	5,000	0.50	1.52	3.16	5.29
	10,000	0.51	1.58	3.48	5.62
	20,000	0.57	1.70	3.50
	50,000	0.72	2.29	4.16	7.54
	100,000	0.90	2.72	5.48	10.23

Table 3 :

 3 Probability of not reaching all 256 plaintext values after a varying number of traces

	# Traces	500	1,000 2,000 3,000 4,000
	Probability 100 % 99.5 % 9.7 % 0.2 % 0.004 %


Aymen Sendi

Pierre Fau

Myrtil L Kahn

Katia Fajerwerg

Vincent Bley

Chaabane Talhi

Frederic Blanc

Philippe Menini

PERFORMANCE OF MOX GAS SENSORS OBTAINED BY MIXING P-TYPE AND N-TYPE METAL OXIDES FOR RELIABLE INDOOR AIR QUALITY MONITORING

Novelty

In this work, we study the effect of n-p heterojunctions in metal oxides (MOX) gas sensors, and particularly on their gas sensitivity and relative humidity dependence for indoor air quality applications. This effect depends on the relative proportion of MOX in the mixture. This study was achieved in order to build a MOX gas sensor that overcomes the effects of humidity variations and to improve the overall sensitivity of MOS gas sensors.

Background

Indoor air quality is major health concern in our societies but European recommendations (directive 2008/50/EC) will be still difficult to fulfill without the help of simple and efficient air quality monitoring systems. MOX gas sensors have proven their interest for the air quality monitoring in open air or indoor areas [START_REF] Jońca | Organometallic Synthesis of CuO Nanoparticles: Application in Low-Temperature CO Detection[END_REF]. The main drawback of theses sensors concerns their stability over time and lack of selectivity among mixtures of gases as well as in variable humidity environment. While a great attention has been focused on n-type semiconducting oxides, few studies have been devoted to the p-type gas sensors. Among p-type oxide semiconductors, single phase, or CuO as part of heterojunction sensors, have demonstrated considerable potential for detection of gases such C 2H5OH, NO2, H2S, H2, CO and NH 3 [START_REF] Chen | A CuO-ZnO nanostructured p-n junction sensor for enhanced N-butanol detection[END_REF]. Some of these sensors exhibited interesting selectivity properties towards investigated gases.

Description of the New Method

In order to increase the sensitivity and the selectivity of semi-conducting gas sensors, SnO 2, WO 3, CuO and ZnO nanopowders of this study have been synthesized by a metalorganic approach and mixed in binary or ternary blends in order to prepare efficient sensitive layers integrated on silicon substrates. The mixture of n-type and p-type metal oxides have been used to modify the response gas sensor [START_REF] Sendi | Effect of Nanostructured octahedral SnO2 added with a binary mixture P-type and N-type metal oxide on CO detection[END_REF], but there is still a lack of knowledge about the role of n-p heterojunction to overcome the effect of the hygrometry changes. In this work, the optimum blending of different metal oxides (n-type and p-type) is achieved by mixing and grinding the nanoparticles previously suspended in an organic solvent. Then the mixed metal oxides have been prepared in the form of a screen-printing paste in order to facilitate their deposition on silicon micro hotplates [START_REF] Dufour | Technological improvements of a metal oxide gas multi-sensor based on a micro-hotplate structure and inkjet deposition for an automotive air quality sensor application[END_REF]. Gas sensors have been realized with nanostructured SnO 2 (Fig. 1) and a blend (Fig. 2) composed by 75% in volume of CuO and 25% of ZnO (Table 1). With an experimental set-up, we applied a gas injection protocol (Fig. 3). All injections with the reactive gas concentrations are summarized in Table 2. Another preparation mixture was set up where WO 3 particles (fig. 4) mixed with various amounts of nanosized SnO2 or CuO were used. The performances (sensitivity, stability) of the gas sensors are presented and compared with simple MOX sensors.

Experimental Results

In Figure 5 we present the result of SnO 2. The sensor sensitivity decreases in dry air, and the resistance baseline is different between dry and humid air. This suggests that the humidity influence is prominent for a single metal oxide composition as SnO 2.

In Figure 6 we show the effect of mixing 25% mass of SnO 2 with 75% mass of a binary CuO/ZnO blend. The sensor response sensitivity is lowered in dry and humid air but the baseline has only slightly changed. In Figure 7 we present the result of the ternary mixture made of SnO 2 (50%) and CuO/ZnO (50%). The resistance baseline remains unchanged between dry and humid air conditions, so that it overcomes the effect of humidity, and thus improves the gas sensitivity in humid air conditions (30% RH). The interest of p-n junctions in gas sensing sensitivity and humidity variation for indoor air quality are discussed and justified.

Word Count: 600

Figure 2 :Figure 3 :

 23 Figure 2: TEM image of CuO 75%/ZnO 25% blend -100nm

Figure 4 :

 4 Figure 4: SEM image of WO3 sensitive layer

Figure 6 :

 6 Figure 6: Responses of gas sensor at 500°C for the ternary mixture 25% SnO2 and 75% of CuO/ZnO in dry and humid air.

Figure 7 :Figure 1 :

 71 Figure 7: Responses of gas sensor at 500°C for the

Table 1 :

 1 The different sensors and their composition

	Sensors	Type	MOX Blend (% masse)
	Sensor 1	Single	SnO2 100%
	Sensor 2	Ternary	25% SnO2 and 75% of
		mixture	CuO/ZnO
	Sensor 3	Ternary	50% SnO2 and 50% of
		mixture	CuO/ZnO
		Table 2: Injected gas concentrations
		Gas	Concentrations
		Acetaldehyde	500 ppb
			300 ppb
	Carbon Monoxide	20 ppm
			50 ppm
			100 ppm


Quentin L Meunier
email: quentin.meunier@lip6.fryann.thierry-mieg@lip6.fremmanuelle.encrenaz@lip6.fr

Yann Thierry-Mieg

Emmanuelle Encrenaz

Modeling a Cache Coherence Protocol with the Guarded Action Language

We present a formal model built for verification of the hardware Tera-Scale ARchitecture (TSAR), focusing on its Distributed Hybrid Cache Coherence Protocol (DHCCP). This protocol is by nature asynchronous, concurrent and distributed, which makes classical validation of the design (e.g. through testing) difficult. We therefore applied formal methods to prove essential properties of the protocol, such as absence of deadlocks, eventual consensus, and fairness.

Introduction

Testing and simulation are unfortunately not sufficient to provide strong correctness guarantees expected from hardware designs, where patching is not an option. However, proving a design correct is a difficult process despite the improvement of verification tools, as complexity of hardware designs has also grown along with Moore's law.

The TSAR (Tera-Scale ARchitecture) shared memory architecture [1] studied in this paper is a general-purpose multicore architecture, in which cache-coherence is entirely supported by the hardware. The main technical challenge of this architecture is scalability, as it is intended to integrate up to 1024 cores. Its embedded cache-coherence protocol is a key architectural point, and has been designed scale well when the number of cores grows.

To formally prove properties of the designed protocol, named Distributed Hybrid Cache Coherence Protocol (DHCCP), we built several formal models over a number of student internships, designed to investigate how different model-checking tools could address our need. This case study is the result of a collaboration between the experts in systems-on-chip design that developed TSAR, and experts in formal verification that provide model-checking tools.

We first present the DHCCP protocol and the relevant characteristics of the hardware that must be captured by the semantics of the model. We then present the formal models that we built over time in Promela, Divine and GAL, together with the results we were able to obtain.

All these models are made available as part of this submission process and will be accessible in the MARS repository as well as on github 1 .

TSAR Hardware Architecture and Coherence Protocol

. Each cluster typically contains 4 processor cores with their L1 caches, a local interconnect, one L2-cache bank, and some peripherals.

The set of all L2-cache banks form a distributed L2 cache: the physical address space is statically split into fixed-size segments, and each L2 cache is responsible for one segment, defined by the physical address MSB bits. As such, the L2 cache is logically shared and physically distributed, making the architecture NUCA (Non Uniform Cache Access): all processors can access all L2-cache banks, but the access time and power consumption depend on the distance between the processor and the cache bank. For L1-L2 communication, TSAR uses a L1-L2 Interconnect composed of two hierarchical levels: a Local Interconnect for intra-cluster communication, and a Global Interconnect for inter-cluster communication, implemented as a network-on-chip with a 2D-mesh topology. For a L1 cache, accessing a L2 located in another local interconnect results in a longer latency, but both levels implement a logically flat address space. The L1-L2 interconnect provides a built-in broadcast service used by the coherence protocol to efficiently broadcast invalidation messages and contains five independent networks.

Hardware Coherence Mechanism. For scalability purpose, TSAR implements a directory-based cache-coherence policy. From a conceptual point of view, the coherence protocol is supported by a global directory located in the L2 controller: this global directory stores the status of each cache line replicated in at least one L1 cache of the architecture. The policy between L1 and L2 caches is writethrough, meaning that the L2 cache always contains the most recent value of a cache line, and there is no exclusive ownership state for a L1 cache. This global directory is physically distributed in the corresponding L2 banks.

The basic coherence mechanism is the following: when the L2 controller receives a WRITE request for a given cache line, it sends an UPDATE or INVAL request to all L1 caches containing a copy except the writer. The write request is acknowledged only when all UPDATE or INVAL transactions are completed.

The L2 cache is inclusive: a cache line present in at least one L1 cache must be present in the L2 cache. Thus for any evicted line, the corresponding copies must be invalidated. When a shared piece of data is modified, the DHCCP protocol uses two different strategies depending on the number of copies:

• MULTICASTUPDATE: when the number of copies is smaller than a certain threshold, called DHCCP threshold, the L2-cache controller registers the locations of all the copies and sends an UPDATE request to each concerned L1 cache.

• BROADCASTINVAL: when the number of copies is larger than the DHCCP threshold or if there is no room left to register the copies locations, the L2-cache controller registers only the number of copies without their location, and sends an INVAL request to all L1 caches. Only the L1 caches which own a copy of the line must respond to this request, thus reducing the traffic.

The list of sharers of a given cache line is stored in the L2 directory with a per bank hardware heap shared between lines. A counter of sharers is also maintained in the directory entry. When the threshold of copies is exceeded or when the heap is full, the sharers list is freed and only the counter of copies is used. In this case, broadcast invalidates are used to maintain cache-coherence.

Types of Transactions. Two types of transactions are defined for L1-L2 communication: Direct transactions, containing the messages read, write, ll (Load-Linked), sc (Store Conditional), cas (Compare-and-Swap), along with their responses. These transactions use two separated networks for commands and responses. They are initiated by L1-cache controllers. For these transactions, the target can be any L2-cache controller.

Coherence transactions, containing the messages cleanup (eviction from L1 or invalidation acknowledgement), clack (CLeanup ACK), multicast_update, multicast_inval, broadcast_inval, and multi_ack. There are four types of coherence transactions, each requiring two or three steps. Coherence Transactions.

• A local cleanup is a two step transaction initiated by a L1-cache controller when it makes a cache line replacement, usually following a miss. The L1 cache sends a cleanup request indicating it is invalidating the cache line, and the L2-cache controller returns a clack response to acknowledge the line invalidation.

• A multicast update is a two step transaction initiated by the L2-cache controller when it receives a write request to a replicated cache line, for which the number of copies does not exceed the DHCCP threshold. It sends as many multi_updt requests as the number of registered copies, but the writer. The expected response is a multi_ack sent by each involved L1 cache. The L2cache controller counts the number of responses to detect the completion of the multicast update transaction.

• A multicast invalidate transaction is a three step transaction initiated by a L2-cache controller when it makes a cache line replacement (following a miss) and the victim line has a number of copies smaller than the DHCCP threshold. It sends as many multi_inval requests as the number of registered copies; each L1 cache returns a cleanup response, and the L2 cache acknowledges the invalidation with a clack. The L2-cache controller counts the number of responses to detect the completion of the multicast invalidate transaction.

• A broadcast invalidate is a three step transaction initiated by a L2-cache controller when it either replaces a line, or receives a Write request to a replicated cache line, and this cache line has a number of copies larger than the DHCCP threshold. The L2 cache sends a single message broadcast_inval, which is dynamically replicated by the network to all L1 caches. L1 caches which have a copy must respond by a cleanup message. All these cleanup responses are counted by the L2 cache to detect the completion of the transaction. Finally, the L2-cache controller acknowledges each invalidation with a clack.

The multi_updt, multi_inval, broadcast_inval and clack messages use the direction L2 → L1 Cache, while the cleanup and multi_ack messages use the direction L1 → L2 Cache.

A L1-cache controller must be sure that a sent cleanup request has arrived to the L2 cache before sending a read request for the same line; otherwise, there would be a risk of inconsistency if the latter request passes the cleanup. To enforce this, L2 caches must respond to each cleanup message with a clack. In order to avoid deadlocks, clack responses must use a physically separated network. Therefore, the coherence transactions require three separated networks:

• cleanup and multi_ack share the first network.

• multi_updt, multi_inval and broadcast_inval share the second network.

• clack are conveyed by the third network.

Direct transactions use two further networks: one for requests and one for responses, for a total of five independent networks.

Modeled Architecture

Verification Objectives. If intensive testing is mandatory, formal verification can help detect subtle bugs due to some uncommon interleavings of messages on the different networks. In our case, one of the main challenges in the DHCCP protocol consists in counting the correct number of responses for each coherence transaction, since an incorrect count will eventually result in a deadlock.

Our goals were first to model formally the DHCCP protocol so as to prove the absence of deadlocks. We also wanted to prove simple functional properties, such as every request receives a response, or a shared copy modification eventually leads to an invalidation or an update of the other copies. Proving these properties would greatly strengthen our confidence in the protocol.

We did not expect verification to scale up to the full 1024 core design, but that is not truly necessary due to the symmetry of DHCCP. Our main goal was then to target a platform configuration that would exhibit all the characteristics of DHCCP by working up progressively from smaller configurations. To exhibit all relevant properties we determined that we needed a threshold for DHCCP that is strictly less than the number of possible copies of a data, so all types of coherence transactions can occur, so we need to scale to a design with at least three processors. Another parameter we identified is that at least two addresses should be represented to show that no problem arises from the sharing of the channels between the different L1 caches and L2 banks.

Architecture Parameters. In order to be able to verify properties, the components in the architecture need to be abstracted, and some restrictions have to be made. The modeled components are processor, L1 cache, L2 cache, memory and interconnect channels. All of these components except channels are modeled as reactive communicating automata, they have a control location or state that defines which messages they can send or receive.

As seen in the section on the interconnect, the topology is logically "flat" , and is modeled as such. Channels have the capability to serialize requests coming from different sources, and to route a request to different destinations.

The architecture parameters are the following:

• Number of processors and their L1 caches: NB_PROC.

• Number of cache lines in the L2 cache: NB_L2. Each L2-cache bank contains only one line in the model, and thus several cache lines translate into several L2-cache banks.

• DHCCP threshold: CACHE_TH.

This parametrized description should be preserved during the modelling to be able to easily consider configurations of increasing complexity.

There are three significant restrictions in the models we built: 1. the single line L2-cache bank, 2. the assumption that the L2 is large enough to contain all memory lines, and 3. the absence of data modelling.

The first restriction prevents a L2-cache bank from receiving on its port requests at different addresses. This is a reasonable simplification, as there is globally not much interaction between requests targeting different cache lines in the L2 cache. The second restriction prevents several memory addresses from being in the same L2 bank; lifting this restriction would require to modify the L2 state machine and add several variables into it (thus yielding even quicker combinatorial explosion). The third restriction means that we only model the control part of the protocol, and abstract away the content of the data in the lines of cache. Adding data is easy from a modelling point of view, and would enable verification of some coherency properties but these data values do not impact correctness of the protocol (e.g. deadlock freedom) and they would participate in state space explosion.

Table 1 describes the variables we considered relevant inside each component. The processor model is very simple and sends random read or write requests at a random address. The L1 cache contains only one line, and the line validity is defined by the cache state. Each L1 cache is defined with a unique identifier. Each L2 cache contains the line address it can hold, along with arrays for the explicit list of copies, and a variable to store the copies count. A channel interconnects two components and is modeled as a one-place buffer. There is one channel per network, i.e. 5 between L1 caches and L2 banks for the case of DHCCP.

Figure 2 shows a system instance with NB_PROC = 2, NB_L2 = 2, and CACHE_TH = 2, and with some of the components variables values. Appendices A and B show the finite state machines for the L1 and L2 caches. All states are represented, but some transition actions are omitted for clarity. Appendice C describes the different messages modeled and the channels on which they are conveyed. These messages types are directly obtained from the DHCCP description in section 2. Figure 3 shows the dynamics, through a sequence diagram describing a cache miss. (1) The processor connected to the L1 cache sends a read request (message DT_RD) for the line with address 0 (PL1DTREQ channel).

(2) The L1 cache does not own a valid copy of the line and sends a RD message for the line at address 0 (L1L2DTREQ channel).

(3) The L2 cache in charge of address 0 receives the request and, as it misses, sends a GET message for address 0 to the memory (L2MEMDTREQ channel).

(4) The memory responds with a RSP_GET message to the requesting L2 (MEML2DTRSP channel).

(5) The L2 cache updates it state for the line and responds to the L1 with a RSP_RD message (L2L1DTRSP channel).

(6) Upon receiving the response, the L1 cache updates its state and responds to the processor with a RSP_DT_RD message (L1PDTRSP channel).

Modeling using Communicating Process

Promela Models. To model DHCCP we first used the Promela language and its supporting tool Spin [START_REF]Spin model checker home page[END_REF]. It offers as modeling framework asynchronous process communicating over channels. The language itself is relatively comfortable, each component is described using code-like control structures (case, loop). The tool can exhibit traces as sequence diagrams, which are particularly valuable to develop and debug the model. We first built [START_REF] Najem | Modélisation et Analyse du protocole de cohérence de caches de la machine multiprocesseur TSAR[END_REF] up automata of the behavior of the L1 cache and the memory controller, and abstracted the activity of processors to arbitrary read and write requests. These automata were then encoded into Promela using labels and goto.

To validate the models, we used properties encoded into "observation" automata, synchronized with the system. In some cases, adding these automata proved to be a problem, as they can incorrectly block the system if not well designed. Also, to observe channels we had to duplicate channels and messages (one for the true channel, one for the observer) which is quite intrusive. Overall, this observation mechanism was quite cumbersome, and participated in state space explosion.

We separately analyzed the components in simple configurations before assembling them. The simple configurations helped validate that the Promela code correctly reflected the automata. Full modelchecking was however only possible on the simplest instances, with a single processor and two addresses. For the full system, we were only able to use simulation and bounded model-checking (up to roughly 10 8 states).

This Promela model was then extended and refined with the same goals in mind [START_REF] Mansour | Modélisation et Analyse du protocole de cohérence de caches de la machine multiprocesseur TSAR : Absence de deadlocks[END_REF]. We simplified and abstracted the data manipulation, and removed the observers. We were still unable to explore the full state space for three processors, reaching 270 steps in depth for 10 9 states. We explored instead two configurations with two processors, while varying the threshold variable. We were also able to include the LL/SC (Load-link/Store-conditional) support in the TSAR architecture, leading unfortunately to much more complex automata, as more control messages were introduced.

While partial-order reduction was activated, we could not activate d step as every set of actions contains at least one channel interaction. The channels themselves are shared for both writing and reading (precluding use of xr/xs keywords) since it models a bus.

In conclusion, despite some aggressive simplifications (e.g. full data abstraction), we were unable to fully verify deadlock freedom for Promela models for even the smallest truly relevant configuration, i.e. at least three processors, two addresses, and a threshold at 2 so that both multicasts and broadcasts can occur. The language and simulator were however quite comfortable to use. Divine Models. We then built a second set of models [START_REF] Gharbi | Vérification compositionnelle du Protocole de Cohérence de Cache de la Machine Multiprocesseur TSAR[END_REF], but this time using the Divine [START_REF] Barnat | DiVinE 2.0: High-Performance Model Checking[END_REF] language. Similarly to Promela, Divine is a language to express systems as (asynchronous) processes communicating over channels. However, it is a much simpler language with less features. Each process is described using an automaton with "local" variables ; transitions have a source and target state, a guard or enabling condition over variables, may send or receive messages from channels and update variables.

We chose to use Divine mostly because we wanted to try other tools than Spin. Thanks to having a relatively simple syntax and semantics, and also due to the existence of a nice set of benchmark models [START_REF] Pelánek | BEEM: Benchmarks for Explicit Model Checkers[END_REF], several tools provided support for the language. The Divine tool coming with the language handled LTL in multi-core and distributed settings, LTSmin [START_REF] Blom | LTSmin: Distributed and symbolic reachability[END_REF] offered support for both explicit and symbolic exploration, and building upon new results [START_REF] Colange | Towards Distributed Software Model-Checking using Decision Diagrams[END_REF], a prototype path to input Divine models to our symbolic model-checker ITS-Tools had been recently built.

Building the model in Divine was harder than in Promela however. On the positive side, we have good control over the atomicity of statements; in the Promela models, due to interaction of send/receive actions with the atomic keyword, some interleavings of independent progression of different process were still observable. For instance, a (passive) component that consumes a message and immediately sends an answer on a different channel could not be modeled without the state between receive and send being materialized.

On the other hand, we fell into some difficulties to model channels; Promela let us peek at the content of a channel without consuming it, enabling a routing mechanism where an entity only consumes messages which are addressed to it. Without this mechanism, we were in fact unable to model the semantics we needed; we had to resort to explicit modeling of the channel as shared global variables, and simulating read and write operations with instructions. Divine's support for parametric modeling was also poor, since it basically recommends the use of the macro expansion tool m4, which is not comfortable.

During this internship, we again built separate components, then progressively assembled them to build more complex configurations. We used LTL (instead of observation automata) to express expected properties of the system, under fairness constraints that force all of the processes to progress. Without fairness, most of the properties were not valid, which was expected, but unfortunately fairness is not supported by all the tools.

With these models, we were able to reproduce a real deadlock found on a previous version of the DHCCP protocol. On the configuration with two processors, two addresses and a threshold set at 1, the scenario exhibited by the sequence diagram in Figure 4 could occur. It leads to an incorrect counter value, that ultimately leads to a deadlock by propagation as the head message in the FIFO channel cannot be consumed and communications lock down.

This bug was detected in the cycle-accurate TSAR prototype by its designers, using testing and simulation, but it took one year to detect this issue and correctly diagnose it. Building a solution to correct the problem was non trivial, and took another six months. In contrast, once the formal models were built, detecting it was easy, even for a relatively non expert Master 2 student, and model-checking could exhibit readable diagnostic traces. We were then able to modify our model to match the next (correct) version of the DHCCP protocol described in section 2, and we checked that the deadlock issue was indeed resolved.

However, we were still unable to fully verify larger configurations with three or more processors. The use of ITS-tools was possible only for deadlock detection, as fairness constraints were unavailable to check the more complex LTL properties. The input from Divine to ITS-tools also involves several automated transformation steps, that yielded a relatively complex model due in part to channel communications modeled as shared variables, and to the loss of structural information in the transformation (i.e. from a set of processes to a single large specification). Experimentation with LTSmin was not extensive, but we measured performance similar to that of the Divine tool; again chains of transformations and relatively poor tool integration made this path less comfortable than just using Divine natively.

In conclusion, using Divine models, we were able to successfully reproduce a critical bug in the TSAR coherence protocol, and to prove that the patch did solve the problem. However, we were still unable to perform verification for larger instances with three or more processors.

Modeling with GAL

The third set of models were built using the Guarded Action Language (GAL) [START_REF]ITS-tools model checker and GAL language home page[END_REF] during a Master Thesis [START_REF] Zhao | Vérification de protocole de cohérence de cache hybride multicast/broadcast avec les techniques de model-checking[END_REF]. GAL is a language offering very fine control over the expression of concurrent semantics, with no assumptions on the existence of higher level constructs such as processes or channels and very few keywords.

Guarded Action Language. GAL is a formalism supporting hierarchical descriptions of components; terminal or leaf components are specified as GAL type declarations, while composite type definitions allow to instantiate existing types (of GAL or composite nature) and synchronize these instances. A GAL specification is then composed of a set of type declarations, and a specific instance main which is designated as the full system. These characteristics of the language, borrowed from architectural description languages, help reuse model elements in various configurations easily.

A GAL type declaration defines a set of integer variables and fixed-size arrays of integers as variables. A state of a GAL is then a complete assignment of an integer value to each of these variables. Transitions Messages can be received out of order due to the existence of several channels between the memory controller and the L1 cache. The RSP_B_INV message was exclusive to that version of DHCCP. At the end of the sequence, the line count in the L2 is one whereas there are no copies left.

are defined as a triplet g, l, a , where g is a boolean enabling condition or guard, l is a label chosen from a finite set, and a is a sequence of statements or actions that must be executed atomically. A statement can be an assignment to a variable of an expression computed over variables, or a call to a label. The call statement is resolved by finding a transition bearing the target label, whose guard is enabled, and executing it.

A composite type declaration defines a set of instances and fixed-size arrays of instances as variables. A state of a composite is then a complete assignment of a subcomponent state to each of these instances. Synchronizations are defined as a pair l, a , where l is a label chosen from a finite set, and a is a sequence of call statements that must be executed atomically. A call statement has a target, which can be either the enclosing instance itself, or any nested instance. The target of the call must then evolve through a transition (or synchronization in composite case) that bears the target label.

GAL also offers parametric modeling features, in the form of parameters defined over a discrete range of values2 . These parameters let us define parametric transitions, that correspond to a set of non parametric transitions, one per possible value of the parameters. Parameters can be used to define parametric labels, in order to model communications over discrete data types as calls to labels.

GAL is mostly designed to be the target in a model transformation process, where the specification is typically expressed using a domain specific notation such as Promela or Divine, and automatically translated to GAL for analysis purposes. Going for direct modeling in GAL however, gives us proximity to the symbolic solution engine, enabling the use of advanced features that are not built into the general purpose transformation, e.g. from Divine.

In particular, the automatic transformation loses structural information, yielding a single GAL com- ponent instead of a composition of process. The encoding of channels as global variables also prevents the transformation from automatically building a representation using synchronizations on labels.

Elementary Components. We separately developed the models of the communication channels and of the various components. For normal components, we model automata by defining a state variable, then adding a GAL transition for every transition of the automata.

For channels, we built a GAL with enough variables to store the message, and a boolean flag to test if the channel is full. For each possible message going through the channel (which must be a finite domain) we generate two transitions read and write with a distinct label for each of them. In this example (see Figure 5) the channel messages carry a target address (among possible memory slots) and a message type (among 20 possible values, e.g. update request). The read operation also flushes the state of the channel, to prevent this unreadable state information from participating in the state space explosion.

The processor is modeled as a three state automaton, alternating between an idle state and a state where a read (resp. write) request is sent to the L1 cache on an arbitrary address. Then, it awaits the reply to go back to idle. The Memory cells are even simpler: since data values have been abstracted away, they feature a single state and two transitions that simply acknowledge and reply appropriately to PUT and GET requests.

The L1 and L2 cache are much larger with respectively 14 and 16 states. They also feature variables that increase the state space size significantly. When transitions of an automaton read or write on channels, we add labels to those actions, indicating which channel is used. The message data is filtered by specifying values in the target label. For instance, the transition from EMPTY to WRITE_WAIT_EMPTY shown in Figure 5 reads a DT_WR request from the channel PL1DTREQ and writes a WR to the channel L1L2DTREQ. Some components such as the L1 cache have a set identifier defined at initialization, that is used to tag outgoing messages, or to filter messages according to their target address. Transitions without communications on channels are left unlabeled, and can thus occur at any time.

Assembling a Configuration. From these models of channels and components we hierarchically build a representation of the full system. A first composite type CompositeCacheL1 is defined containing an instance of a Processor, an instance of a L1 cache, and two instances of channels connecting them together.

Channels are connected to appropriate endpoints using synchronizations. Unlabeled synchronizations are used to label local communications within the composite. The synchronization s_write_-PL1DTREQ shown in Figure 6 is an example of this, and models the processor p sending a write request. The contents of the message (address and type) could be anything at this synchronization level. The labels that correspond to communications between the L1 cache and the L2 cache are however reexposed as labels of the composite, which simply forwards the request to the L1 cache instance.

We then build a top level composite acting as main that contains an array of instances of CompositeCacheL1, an array of instances of L2 caches and all the channel instances connecting them. The whole description is parametric and controlled by the three parameters set at the top of the file. Several other configurations were built to test each component in isolation.

Experiments and Measurements. On these models we were able to prove absence of deadlock and some logical properties expressed in CTL. Overall we considered all configurations with up to NB_PROC = 6 processors, up to NB_L2 = 3 L2 addresses, and a CACHE_TH between 1 and 3. For each configuration, we ran the verification on an Intel Xeon 2.6 GHz machine with a limit set to 8 hours to complete the simulation, and a maximum of 192 GB of memory. Table 2 reports on the experiments that finished within the time and memory constraints, and gives their time, the number of accessible states and the memory used.

The state space size is relatively modest, compared to the models crafted in other languages, thanks to the fine control over the atomicity of steps offered in GAL. We were indeed able to scale up to the configurations of interest, i.e. 3 processors, 2 L2 cache, and a threshold of 2.

A set of 16 properties were expressed in CTL, covering request response scenarios such as "any time two processors share an address and one writes on it, the other one eventually gets an invalidate request."

Conclusion

We presented a case-study focusing on the modeling of a cache-coherence protocol in GAL, and discussed previous implementations using other languages and tools for the same protocol. We noticed a certain difficulty, for the students who worked on the subject, to assimilate the underlying formalism of each tool. We also noticed how small changes in the language semantics can result in big changes, either in the model description or in the state space size. In particular, the communication and synchronisation primitives offered by a language are of high importance for getting clean and efficient models. The parametric and compositional features of GAL proved adequate to write models directly by hand. The parametric features are useful both for writing a model with several instances of a same module (e.g. cache) and for exploiting internally the similarities between these modules to improve verification efficiency.

Overall, this case study showed that model-checking tools could highlight real bugs and could run on problems of substantial size, provided appropriate formal models can be built accurately.

A L1 Cache Finite State Machine

Figure 1 :

 1 Figure 1: Tsar Architecture Overview: Mesh Topology and Cluster Details

Figure 2 :Figure 3 :

 23 Figure 2: Example of an architectural state modelisation, in which the line with address 1 has a copy in both L1 caches

Figure 4 :

 4 Figure 4: Part of a deadlock sequence in a previous version of the DHCCP protocol. Blue arrows represent direct messages while red arrows represent coherence messages.Messages can be received out of order due to the existence of several channels between the memory controller and the L1 cache. The RSP_B_INV message was exclusive to that version of DHCCP. At the end of the sequence, the line count in the L2 is one whereas there are no copies left.

1 typedef 4 5 gal ChannelAddrType { 6 i n t i s F u l l = 0 ; 7 i n t addr = 0 ; 8 i n t t y p e = 0 ; 9 t r a n s i t i o n read 10 (t r a n s i t i o n w r i t e 19 (

 1467891019 a d d r t = 0 . . $NB L2 -1 ; 2 typedef t y p e t = 0 . . 19 ; 3 typedef i d t = 0 . . $NB PROC -1 ; a d d r t $addr , t y p e t $rtype ) 11 [ i s F u l l == 1 && addr == $addr 12 && t y p e == $rtype ] 13 l a b e l " read " ( $addr , $rtype ) a d d r t $addr , t y p e t $wtype ) 20 [ i s F u l l == 0 ] 21 l a b e l " w r i t e " ( $addr , $wtype ) { 22 i s F u l l = 1 ; 23 addr = $addr ; 24 t y p e = $wtype ;

43 l a b

  e l " read PL1DTREQ write L1L2DTREQ " 44 ( $id , $addr , $DT WR, $WR) { 45 s t a t e = $L1 WRITE WAIT EMPTY ; 46 addr save = $addr ;

Figure 5 :

 5 Figure 5: GAL encoding of a channel carrying messages (5-26) featuring a type (8) and an address field (7). Part of the GAL modeling the L1 cache (27-46).

10 } 11 /

 1011 e l " i n i t " ( $id ) { 9 c . " i n i t " ( $id ) ; / l o c a l communications are u n l a b e l e d 12 synchronization s write PL1DTREQ 13 ( a d d r t $addr , t y p e t $type ) { 14 p . " write PL1DTREQ " ( $addr , $type ) ; 15 chan PL1DTREQ . " w r i t e " ( $addr , $type ) ; 16 } 17 / / exposing t h e p o r t s o f t h e L1 cache 18 synchronization s read L2L1CPREQ 19 ( i d t $id , a d d r t $addr , t y p e t $type ) 20 l a b e l " c read L2L1CPREQ " ( $id , $addr , $type ) { 21 c . " read L2L1CPREQ " ( $id , $addr , $type ) ;

Figure 6 :

 6 Figure 6: Composite encoding a component nesting a Processor, a L1 cache and two channels.

Figure 7 :

 7 Figure7: L1 cache finite state machine. '?' denotes the reception of a message; '!' denotes the sending of a message; → denotes actions associated to a guard. Some actions are omitted for readability.

Figure 8 :

 8 Figure8: L2 cache finite state machine. '?' denotes the reception of a message; '!' denotes the sending of a message; → denotes actions associated to a guard. Some actions are omitted for readability.

Table 1 :

 1 Components modeled with their variables true if the line has been modified w.r.t. the memory src_save and src_save_clnup: used to save a request source id when a coherence request is needed cpt, cpt_clnup and rsp_cpt: counters used for the sending of multicast or broadcast requests v_c_id[] and c_id[]: arrays of size CACHE TH storing the explicit list of copies; if v_c_id[i]== 1, then entry i in c_id is valid and c_id[i] contains the corresponding cache identifier.

	Processor	Channel
	state FSM state	address:
		request type
	L1 cache
	state	FSM state
	id:	identifier of the cache (different for all caches)
	v_addr:	address contained in the cache when it is valid
		(validity is encoded in the sate)
	addr_save:	address of the last request sent
	L2 cache
	state	FSM state
	line_addr:	address of the line mapped in this L2-cache bank
	n_copies:	number of copies for this line
	dirty:

target address of the request addr: address of the last id (optional): identifier of the request sender request emitted type:

Table 2 :

 2 Runtime (in seconds) and memory (in MB) required for the configurations of the parameters NB_PROC,NB_L2,CACHE_TH which could be explored.

	PROC 1 1 1 1 1 1 1 1 1 2 2 2 2 2 2 2	L2 1 1 1 2 2 2 3 3 3 1 1 1 2 2 2 3	TH 1 2 3 1 2 3 1 2 3 1 2 3 1 2 3 1	States 51 52 53 555 565 575 4503 4572 4641 7070 1892 2160 681471 68401 77449 2.76e+07	Time 0.05 0.05 0.06 0.13 0.12 0.18 0.47 0.52 0.44 0.54 0.46 0.47 14 5 6 640.14	Mem 5 5 5 7 7 8 15 15 15 14 15 15 232 98 99 3482	PROC 2 2 3 3 3 3 3 3 3 4 4 4 4 5 5 6 6	L2 3 3 1 1 1 2 2 2 3 1 1 1 2 1 1 1 1	TH 2 3 1 2 3 1 2 3 3 1 2 3 2 1 2 1 2	States 1.13e+06 1.27e+06 175234 226329 130450 4.32e+07 6.77e+07 1.54e+07 5.14e+08 3.36e+06 5.53e+06 1.04e+07 4.49e+09 6.06e+07 1.08e+08 1.05e+09 1.87e+09	Time 44 46 3 35 51 860.58 3692 1396 18759 44 184 574 149471 254 9315 831 12324	Mem 568 599 57 326 625 3871 7547 6315 66733 662 1645 3285 171457 1389 9439 3710 23118

https://github.com/lip6/TSAR-DHCCP

In the syntax, parameters are distinguished from variables by a $ sign.

Acknowledgements

This work would not have been possible without the contributions of the students working on the project Mohamad Najem, Akli Mansour, Zahia Gharbi and Di Zhao.

C Types of Messages and Associated Channels