Arthur Perais
email: arthur.perais@inria.fr

André Seznec
email: andre.seznec@inria.fr

Practical Data Value Speculation for Future High-end Processors

Dedicating more silicon area to single thread performance will necessarily be considered as worthwhile in future -potentially heterogeneous -multicores. In particular, Value prediction (VP) was proposed in the mid 90's to enhance the performance of high-end uniprocessors by breaking true data dependencies.

In this paper, we reconsider the concept of Value Prediction in the contemporary context and show its potential as a direction to improve current single thread performance. First, building on top of research carried out during the previous decade on confidence estimation, we show that every value predictor is amenable to very high prediction accuracy using very simple hardware. This clears the path to an implementation of VP without a complex selective reissue mechanism to absorb mispredictions. Prediction is performed in the in-order pipeline frond-end and validation is performed in the in-order pipeline back-end, while the outof-order engine is only marginally modified.

Second, when predicting back-to-back occurrences of the same instruction, previous context-based value predictors relying on local value history exhibit a complex critical loop that should ideally be implemented in a single cycle. To bypass this requirement, we introduce a new value predictor VTAGE harnessing the global branch history. VTAGE can seamlessly predict back-to-back occurrences, allowing predictions to span over several cycles. It achieves higher performance than previously proposed context-based predictors.

Specifically, using SPEC'00 and SPEC'06 benchmarks, our simulations show that combining VTAGE and a stridebased predictor yields up to 65% speedup on a fairly aggressive pipeline without support for selective reissue.

Introduction

Multicores have become ubiquitous. However, Amdahl's law [START_REF] Amdahl | Validity of the single processor approach to achieving large scale computing capabilities[END_REF] as well as the slow pace at which the software industry moves towards parallel applications advocates for dedicating more silicon to single-thread performance. This could be interesting for homogeneous general-purpose multicores as well as for heterogeneous multicores, as suggested by Hill and Marty in [START_REF] Hill | Amdahl's law the multicore era[END_REF]. In that context, archi-tectural techniques that were proposed in the late 90's could be worth revisiting; among these techniques is Value Prediction (VP) [START_REF] Gabbay | Using value prediction to increase the power of speculative execution hardware[END_REF][START_REF] Lipasti | Value locality and load value prediction[END_REF][START_REF] Mendelson | Speculative execution based on value prediction[END_REF].

Gabbay et al. [START_REF] Gabbay | Using value prediction to increase the power of speculative execution hardware[END_REF][START_REF] Mendelson | Speculative execution based on value prediction[END_REF] and Lipasti et al. [START_REF] Lipasti | Value locality and load value prediction[END_REF] independently proposed Value Prediction to speculatively ignore true data dependencies and therefore shorten critical paths in computations. Initial studies have led to moderately to highly accurate predictors [START_REF] Nakra | Global context-based value prediction[END_REF][START_REF] Sazeides | The predictability of data values[END_REF][START_REF] Wang | Highly accurate data value prediction using hybrid predictors[END_REF] while predictor accuracy has been shown to be critical due to the misprediction penalty [START_REF] Calder | Selective value prediction[END_REF][START_REF] Zhou | A study of value speculative execution and misspeculation recovery superscalar microprocessors[END_REF]. Said penalty can be as high as the cost of a branch misprediction, yet the benefit of an individual correct prediction is often very limited. As a consequence, high coverage is mostly irrelevant in the presence of low accuracy.

The contribution of this work is twofold: First, we present a simple yet efficient confidence estimation mechanism for value predictors. The Forward Probabilistic Counters (FPC) scheme yields value misprediction rates well under 1%, at the cost of reasonably decreasing predictor coverage. All classical predictors are amenable to this level of accuracy. FPC is very simple to implement and does not require substantial change in the counters update automaton. Our experiments show that when FPC is used, no complex repair mechanism such as selective reissue [START_REF] Tullsen | Storageless value prediction using prior register values[END_REF] is needed at execution time. Prediction validation can even be delayed until commit time and be done in-order: Complex and power hungry logic needed for execution time validation is not required anymore. As a result, prediction is performed in the in-order pipeline front-end, validation is performed in the in-order pipeline back-end while the out-of-order execution engine is only marginally modified.

Second, we introduce the Value TAGE predictor (VTAGE). This predictor is directly derived from research propositions on branch predictors [START_REF] Seznec | A case for (partially) TAgged GEometric history length branch prediction[END_REF] and more precisely from the indirect branch predictor ITTAGE. VTAGE is the first hardware value predictor to leverage a long global branch history and the path history. Like all other value predictors, VTAGE is amenable to very high accuracy thanks to the FPC scheme. VTAGE is shown to outperform previously proposed context-based predictors such as Finite Context Method [START_REF] Sazeides | The predictability of data values[END_REF] and complements stride-based predictors [START_REF] Eickemeyer | A load-instruction unit for pipelined processors[END_REF][START_REF] Gabbay | Using value prediction to increase the power of speculative execution hardware[END_REF].

Moreover, we point out that unlike two-level predictors (in particular, predictors based on local value histories), VTAGE can seamlessly predict back-to-back occurrences of instructions, that is, instructions inside tight loops. Practical implementations are then feasible. The remainder of this paper is organized as follows. Section 2 describes related work. Section 3 motivates the need to provide high accuracy as well as the interest of having a global history based predictor. Section 4 discusses the implications of VP validation at commit time on the outof-order engine. Section 5 describes the probabilistic confidence counter saturation mechanism that enables very high accuracy on all predictions used by the processor. In Section 6, we introduce VTAGE and describe the way it operates. Section 7 presents our evaluation methodology while Section 8 details the results of our experiments. Finally, Section 9 provides concluding remarks.

Related Work on Value Predictors

Lipasti et al. and Gabbay et al. independently introduce

Value Prediction [START_REF] Gabbay | Using value prediction to increase the power of speculative execution hardware[END_REF][START_REF] Lipasti | Value locality and load value prediction[END_REF][START_REF] Lipasti | Exceeding the dataflow limit via value prediction[END_REF][START_REF] Mendelson | Speculative execution based on value prediction[END_REF]. The Last Value Prediction scheme (LVP) was introduced in [START_REF] Lipasti | Value locality and load value prediction[END_REF][START_REF] Lipasti | Exceeding the dataflow limit via value prediction[END_REF] while [START_REF] Gabbay | Using value prediction to increase the power of speculative execution hardware[END_REF][START_REF] Mendelson | Speculative execution based on value prediction[END_REF] provides insights on the gains that can be obtained from Value Prediction.

Sazeides et al. refine the taxonomy of Value Prediction by categorizing predictors [START_REF] Sazeides | The predictability of data values[END_REF]. Specifically, they define two classes of value predictors: Computational and Context-based. These two families are complementary to some extent since they are expert at predicting distinct instructions. On the one hand, Computational predictors generate a prediction by applying a function to the value(s) produced by the previous instance(s) of the instruction. For instance, the Stride predictor [START_REF] Gabbay | Using value prediction to increase the power of speculative execution hardware[END_REF] and the 2-Delta Stride predictor [START_REF] Eickemeyer | A load-instruction unit for pipelined processors[END_REF] use the addition of a constant (stride).

On the other hand, Context-Based predictors rely on patterns in the value history of a given static instruction to generate predictions. The main representatives of this category are n th order Finite Context Method predictors (FCM) [START_REF] Sazeides | The predictability of data values[END_REF]. Such predictors are usually implemented as two-level structures. The first level (Value History Table or VHT) records a n-long value history -possibly compressed -and is accessed using the instruction address. The history is then hashed to form the index of the second level (Value Prediction Table or VPT), which contains the actual prediction. A confidence estimation mechanism is usually added in the form of saturating counters in either the first level table or the second level table [START_REF] Sazeides | Implementations of context based value predictors[END_REF].

Goeman et al. [START_REF] Goeman | Differential FCM: Increasing value prediction accuracy by improving table usage efficiency[END_REF] build on FCM by tracking differences between values in the local history and the VPT instead of values themselves. As such, the Differential FCM predictor is much more space efficient and combines the prediction method of FCM and Stride. D-FCM can be considered as a tightly-coupled hybrid.

Zhou et al. study value locality in the global value history and propose the gDiff predictor [START_REF] Zhou | Detecting global stride locality value streams[END_REF]. gDiff computes the difference existing between the result of an instruction and the results produced by the last n dynamic instructions. If a stable difference (stride) is found, then the instruction result can be predicted using the results of previous instructions. However, gDiff relies on another predictor to provide the speculative global value history at prediction time. As such, gDiff can be added on top of any other predictor, including the VTAGE predictor we propose in this paper or an hybrid predictor using VTAGE.

Similarly, Thomas et al. introduce a predictor that uses predicted dataflow information to predict values: DDISC [START_REF] Thomas | Using dataflow based context for accurate value prediction[END_REF]. As gDiff, DDISC can be combined to any other predictor. For an instruction that is not predictable but which operands are predictable, DDISC predicts the results through combining these predicted operands.

The VTAGE predictor we introduce in this work can be considered as a context-based predictor whose context consists of the global branch history and the path history. As such, it uses context that is usually already available in the processor -thanks to the branch predictor -while most predictors mainly focus on either local or global dataflow information, which is not as easily manageable.

Motivations

We identify two factors that will complicate the adaptation and implementation of value predictors in future processor cores. First, the misprediction recovery penalty and/or hardware complexity. Second the back-to-back predictions for two occurrences of the same instruction which can be very complex to implement while being required to predict tight loops.

Misprediction Recovery

Most of the initial studies on Value Prediction were assuming that the recovery on a value misprediction is immediate and induces -almost -no penalty [START_REF] Gabbay | Using value prediction to increase the power of speculative execution hardware[END_REF][START_REF] Lipasti | Value locality and load value prediction[END_REF][START_REF] Lipasti | Exceeding the dataflow limit via value prediction[END_REF][START_REF] Zhou | Detecting global stride locality value streams[END_REF] or simply focused on accuracy and coverage rather than actual speedup [START_REF] Goeman | Differential FCM: Increasing value prediction accuracy by improving table usage efficiency[END_REF][START_REF] Nakra | Global context-based value prediction[END_REF][START_REF] Rychlik | Efficient and accurate value prediction using dynamic classification[END_REF][START_REF] Sazeides | The predictability of data values[END_REF][START_REF] Thomas | Using dataflow based context for accurate value prediction[END_REF][START_REF] Wang | Highly accurate data value prediction using hybrid predictors[END_REF]. The latter studies were essentially ignoring the performance loss associated with misprediction recovery. Moreover, despite quite high coverage and reasonable accuracy, one observation that can be made from these early studies is that the average performance gain per correct prediction is rather small. Furthermore, Zhou et al. observed that to maximize the interest of VP, the total cost of recoveries should be as low as possible [START_REF] Zhou | A study of value speculative execution and misspeculation recovery superscalar microprocessors[END_REF]. To limit this total cost, one can leverage two factors: The average misprediction penalty P value and the absolute number of mispredictions N misp . A very simple modelization of the total misprediction penalty is T recov = P value * N misp .

Value Misprediction Scenarios

Two mechanisms already implemented in processors can be adapted to manage value misprediction recovery: Pipeline squashing and selective reissue. They induce very different average misprediction penalties, but are also very different from a hardware complexity standpoint.

Pipeline squashing is already implemented to recover from branch mispredictions. On a branch misprediction, all the subsequent instructions in the pipeline are flushed and instruction fetch is resumed at the branch target. This mechanism is also generally used on load/store dependency mispredictions. Using pipeline squashing on a value misprediction is straightforward, but costly as the minimum misprediction penalty is the same as the minimum branch misprediction penalty. However, to limit the number of squashes due to VP, squashing can be avoided if the predicted result has not been used yet, that is, if no dependent instruction has been issued.

Selective reissue is implemented in processors to recover in case where instructions have been executed with incorrect operands, in particular this is used to recover from L1 cache hit/miss mispredictions [START_REF] Kim | Understanding scheduling replay schemes[END_REF] (i.e. load-dependent instructions are issued after predicting a L1 hit, but finally the load results in a L1 miss). When the execution of an instruction with an incorrect operand is detected, the instruction as well as all its dependent chain of instructions are canceled then replayed.

Validation at Execution Time vs. Validation at Commit Time On the one hand, selective reissue must be implemented at execution time in order to limit the misprediction penalty. On the other hand, pipeline squashing can be implemented either at execution time or at commit time. Pipeline squashing at execution time results in a minimum misprediction penalty similar to the branch misprediction penalty. However, validating predictions at execution time necessitates to redesign the complete out-of-order engine: The predicted values must be propagated through all the out-of-execution engine stages and the predicted results must be validated as soon as they are produced in this outof-order execution engine. Moreover, the repair mechanism must be able to restore processor state for any predicted instruction. Prediction checking must also be implemented in the commit stage(s) since predictors have to be trained even when predictions were not used due to low confidence.

On the contrary, pipeline squashing at commit results in a quite high average misprediction penalty since it can delay prediction validation by a substantial number of cycles. Yet, it is much easier to implement for Value Prediction since it does not induce complex mechanisms in the out-of-order execution engine. It essentially restrains the Value Prediction related hardware to the in-order pipeline front-end (prediction) and the in-order pipeline back-end (validation and training). Moreover, it allows not to checkpoint the rename table since the committed rename map contains all the necessary mappings to restart execution in a correct fashion.

A Simple Synthetic Example Realistic estimations of the average misprediction penalty P value could be 5-7 cycles for selective reissue1 , 20-30 cycles for pipeline squashing at execution time and 40-50 cycles for pipeline squashing at commit.

For the sake of simplicity, we will respectively use 5, 20 and 40 cycles in the small example that follows. We assume an average benefit of 0.3 cycles per correctly predicted value (taking into account the number of unused predictions). With predictors achieving around 40% coverage and around 95% accuracy as often reported in the literature, 50% of predictions used before execution, the performance benefit when using selective reissue would be around 64 cycles per Kinstructions, a loss of around 86 cycles when using pipeline squashing at execution time and a loss of around 286 cycles when using pipeline squashing at commit time.

Our experiments in Section 8 confirm that when a value predictor exhibits a few percent misprediction rate on an application, it can induce significant performance loss when using pipeline squashing. Therefore, such a predictor should rather be used in conjunction with selective reissue.

Balancing Accuracy and Coverage

The total misprediction penalty T recov is roughly proportional to the number of mispredictions. Thus, if one drastically improves the accuracy at the cost of some coverage then, as long as the coverage of the predictor remains quite high, there might be a performance benefit brought by Value Prediction, even though the average value misprediction penalty is very high.

Using the same example as above, but sacrificing 25% of the coverage (now only 30%), and assuming 99.75% accuracy, the performance benefit would be around 88 cycles per Kinstructions cycles when using selective reissue, 83 cycles when using pipeline squashing at execution time and 76 cycles when using pipeline squashing at commit time.

In Section 8, we will show that the ranges of accuracy and coverage allowed by our FPC proposition are in the range of those used in this small example. As a consequence, it is not surprising that our experiments confirm that, using FPC, pipeline squashing at commit time achieves performance in the same range as an idealistic 0cycle selective reissue implementation.

Back-to-back prediction

Unlike a branch prediction, a value prediction is needed rather late in the pipeline (at dispatch time). Thus, at first glance, prediction latency does not seem to be a concern and long lookups in large tables and/or fairly complex computations could be tolerated. However, for most predictors, the outcomes of a few previous occurrences of the instruction are needed to perform a prediction for the current instance. Consequently, for those predictors, either the critical operation must be made short enough to allow for the prediction of close (possibly back-to-back) occurrences (e.g. by using small tables) or the prediction of tight loops must be given up. Unfortunately, tight loops with candidates for VP are quite abundant in existing programs. Experiments conducted with the methodology we will introduce in Section 7 suggest that for a subset of the SPEC'00/'06 benchmark suites, there can be as much as 15.3% (3.4% a-mean) fetched instructions eligible for VP and for which the previous occurrence was fetched in the previous cycle . We highlight such critical operations for each predictor in the subsequent paragraphs.

LVP Despite its name, LVP does not require the previous prediction to predict the current instance as long as the table is trained. Consequently, LVP uses only the program counter to generate a prediction. Thus, successive table lookups are independent and can last until Dispatch, meaning that large tables can be implemented. The top part of Fig. 1 describes such behavior. Similarly, the predictor we introduce in Section 6 only uses control-flow information to predict, allowing it to predict back-to-back occurrences. The same goes for the gDiff predictor itself [START_REF] Zhou | Detecting global stride locality value streams[END_REF] although a critical path may be introduced by the predictor providing speculative values for the global history.

Stride Prediction involves using the result of the previous occurrence of the instruction. Thus, tracking the result of only the last speculative occurrence of the instruction is sufficient.

The Stride value predictor acts in two pipeline steps, 1) retrieval of the stride and the last value 2) computation of the sum. The first step induces a difficulty when the last occurrence of the instruction has not committed or is not even executed. One has to track the last occurrence in the pipeline and use the speculative value predicted for this occurrence. This tracking can span over several cycles. The critical operation is introduced by the need to bypass the result of the second step directly to the adder in case of fetching the same instruction in two consecutive cycles (e.g. in a very tight loop), as illustrated by the central part of Fig. 1. However, a Stride value predictor supporting the prediction of two consecutive occurrences of the same instruction one cycle apart could reasonably be implemented since the second pipeline step is quite simple.

Finite Context Method

The local value history predictor (n th -order FCM) is a two-level structure. The first-level consists of a value history table accessed using the instruction address. This history is then hashed and used to index the second level table.

As for the Stride value predictor, the difficulty arises when several occurrences of the same instruction are fetched in a very short interval since the predictor is indexed through a hash of the last n values produced by the instruction. In many cases, the previous occurrences of the instruction have not been committed, or even executed. The logic is slightly more complex than for the Stride predictor since one has to track the last n values instead of a single one.

However, the critical delay is on the second step. The delay between the accesses to the second level table for two occurrences of the same instruction should be much shorter than the delay for computing the hash, reading the value table and then forward the predicted value to the second index hash/computation, as illustrated by the bottom part of Fig. 1. This implies that FCM must either use very small tables to reduce access time or give up predicting tight loops. Note that D-FCM [START_REF] Goeman | Differential FCM: Increasing value prediction accuracy by improving table usage efficiency[END_REF] and DDISC [START_REF] Thomas | Using dataflow based context for accurate value prediction[END_REF] also require two successive lookups. Consequently, these observations stand for those predictors.

In summary, a hardware implementation of a local history value predictor would be very complex since 1) it involves tracking the n last speculative occurrences of each fetched instruction 2) the predictor cannot predict instructions in successive iterations of a loop body if the body is fetched in a delay shorter than the delay for retrieving the prediction and forwarding it to the VPT index computation step.

Summary Table lookup time is not an issue as long as the prediction arrives before Dispatch for LVP and Stride. Therefore, large predictor tables can be considered for implementation. For stride-based value predictor, the main difficulty is that one has to track the last (possibly speculative) occurrence of each instruction.

For local value based predictors the same difficulty arises with the addition of tracking the n last occurrences. Moreover the critical operations (hash and the 2nd level table read) lead to either using small tables or not being able to timely predict back-to-back occurrences of the same instruction. Implementations of such predictors can only be justified if they bring significant performance benefit over alternative predictors.

The VTAGE predictor we introduce in this paper is able to seamlessly predict back-to-back occurrences of the same instruction, thus its access can span over several cycles. VTAGE does not require any complex tracking of the last occurrences of the instruction. Section 8 shows that VTAGE (resp. hybrid predictor using VTAGE) outperforms a local value based FCM predictor (resp. hybrid predictor using a local value based FCM predictor).

Commit Time Validation and Hardware

Implications on the Out-of-Order Engine

In the previous section, we have pointed out that the hardware modifications induced by pipeline squashing at commit time on the Out-of-Order engine are limited. In practice, the only major modification compared with a processor without Value Prediction is that the predicted values must be written in the physical registers before Dispatch.

At first glance, if every destination register has to be predicted for each fetch group, one would conclude that the number of write ports should double. In that case the overhead on the register file would be quite high. The area cost of a register file is approximately proportional to (R + W ) * (R + 2W ), R and W respectively being the number of read ports and the number of write ports [START_REF] Zyuban | The energy complexity of register files[END_REF]. Assuming R = 2W , the area cost without VP would be proportional to 12W 2 and the one with VP would be proportional to 24W 2 , i.e. the double. Energy consumed in the register file would also be increased by around 50% (using very simple Cacti 5.3 approximation).

For practical implementations, there exist several opportunities to limit this overhead. For instance one can limit the number of extra ports needed to write predictions. Each cycle, only a few predictions are used and the predictions can be known several cycles before Dispatch: One could limit the number of writes on each cycle to a certain limit, and buffer the extra writes, if there are any. Assuming only W 2 write ports for writing predicted values leads to a register file area of 35W 2 2 , saving half of the overhead of the naive solution. The same saving on energy is observed (Cacti 5.3 estimations). Another opportunity is to allocate physical registers for consecutive instructions in different register file banks, limiting the number of write ports on the individual banks. One can also prioritize the predictions according to the criticality of the instruction and only use the most critical one, leveraging the work on criticality estimation of Fields et al. [START_REF] Fields | Focusing processor policies via critical-path prediction[END_REF], Tune et al. [START_REF] Tune | Quantifying instruction criticality[END_REF] as well as Calder et al. [START_REF] Calder | Selective value prediction[END_REF].

Exploring the complete optimization to reduce the overhead on the register file design is out of the scope of this paper. It would depend on the precise micro-architecture of the processor, but we have clearly shown that this overhead in terms of energy and silicon area can be reduced to less than 25% and 50% respectively. Moreover, this overhead is restricted to the register file and does not impact the other components of the out-of-order engine. Similarly, thanks to commit time validation, the power overhead introduced by Value Prediction will essentially reside in the predictor table.

Maximizing Value Predictor Accuracy Through Confidence

As we already pointed out, the total misprediction recovery cost can be minimized through two vehicles: Minimizing the individual misprediction penalty and/or minimizing the total number of mispredictions.

When using the prediction is not mandatory (i.e. contrarily to branch predictions), an efficient way to minimize the number of mispredictions is to use saturating counter to estimate confidence and use the prediction only when the associated confidence is very high. For instance, for the value predictors considered in this study, a 3-bit confidence counter per entry that is reset on each misprediction leads to an accuracy in the 95-99% range if the prediction is used only when the counter is saturated. However this level of accuracy is still not sufficient to avoid performance loss in several cases unless idealistic selective reissue is used. To increase accuracy, Burtscher et al. proposed the SAg confidence estimation scheme to assign confidence to a history of outcomes rather than to a particular instruction [START_REF] Burtscher | Exploring last-n value prediction[END_REF]. However, this entails a second lookup in the counter table using the outcome history retrieved in the predictor table with the PC of the instruction. A way to maximize accuracy without increasing complexity and latency would be preferable.

We actually found that simply using wider counters (e.g. 6 or 7 bits) leads to much more accurate predictors while the prediction coverage is only reduced by a fraction. Prediction is only used on saturated confidence counters and counters are reset on each misprediction. Interestingly, probabilistic 3-bit counters such as defined by Riley et al. [START_REF] Riley | Probabilistic counter updates for predictor hysteresis and stratification[END_REF] augmented with reset on misprediction achieve the same accuracy for substantially less storage and a marginal increase in complexity.

We refer to these probabilistic counters as Forward Probabilistic Counters (FPC). In particular, each forward transition is only triggered with a certain probability. In this paper, we will consider 3-bit confidence counters using a probability vector v = {1, 1 16 , 1 16 , 1 16 , 1 16 , 1 32 , 1 32 } for pipeline squashing at commit and v = {1, 1 8 , 1 8 , 1 8 , 1 8 , 1 16 , 1 16 } for selective reissue, respectively mimicking 7-bit and 6-bit coun-ters. This generally prevents all the considered VP schemes to slow down execution while minimizing the loss of coverage (as opposed to using lower probabilities). The used pseudo-random generator is a simple Linear Feedback Shift Register.

Using FPC counters instead of full counters limits the overhead of confidence estimation. It also opens the opportunity to adapt the probabilities at run-time as suggested in [START_REF] Seznec | Storage free confidence estimation for the TAGE branch predictor[END_REF] and/or to individualize these probabilities depending on the criticality of the instructions.

The Value TAgged GEometric Predictor

Branch predictors exploiting correlations inside the global branch history have been shown to be efficient. Among these global history branch predictors, TAGE [START_REF] Seznec | A case for (partially) TAgged GEometric history length branch prediction[END_REF] is generally considered state-of-the-art. An indirect branch predictor ITTAGE [START_REF] Seznec | A case for (partially) TAgged GEometric history length branch prediction[END_REF] has been directly derived from TAGE. Since targets of indirect branches are register values, we have explored the possibility of adapting ITTAGE to Value Prediction. We refer to this modified ITTAGE as the Value TAgged GEometric history length predictor, VTAGE. To our knowledge, VTAGE is the first hardware value predictor to make extensive use of recent and less recent control-flow history. In particular, PS [START_REF] Nakra | Global context-based value prediction[END_REF] only uses a few bits of the global branch history.

As it uses branch history to predict, we expect VTAGE to perform much better than other predictors when instruction results are indeed depending on the control flow. Nonetheless, VTAGE is also able to capture control-flow independent patterns as long as they are short enough with regard to the maximum history length used by the predictor. In particular, it can still capture short strided patterns, although space efficiency is not optimal since each value of the pattern will reside in an entry (contrarily to the Stride predictor where one pattern can be represented by a single entry).

Fig. 2 describes a (1+N)-component VTAGE predictor.

The main idea of the VTAGE scheme (exactly like the IT-TAGE scheme) is to use several tables -components -storing predictions. Each table is indexed by a different number of bits of the global branch history, hashed with the PC of the instruction. The different lengths form a geometric series (i.e. VT1 is accessed with two bits of the history, VT2 with four, VT3 with eight and so on). These tables are backed up by a base predictor -a tagless LVP predictor -which is accessed using the instruction address only. In VTAGE, an entry of a tagged component consists of a partial tag, a 1-bit usefulness counter u used by the replacement policy, a full 64-bit value val, and a confidence/hysteresis counter c. An entry of the base predictor simply consists of the prediction and the confidence counter.

At prediction time, all components are searched in parallel to check for a tag match. The matching component accessed with the longest history is called the provider component as it will provide the prediction to the pipeline.

At update time, only the provider is updated. On either a correct or an incorrect prediction, c2 and u3 are updated. On a misprediction, val is replaced if c is equal to 0, and a new entry is allocated in a component using a longer history than the provider: All "upper" components are accessed to see if one of them has an entry that is not useful (u is 0). If none is found, the u counter of all matching entries in the upper components are reset, but no entry is allocated. Otherwise, a new entry is allocated in one of the components whose corresponding entry is not useful. The component is chosen randomly.

The main difference between VTAGE and ITTAGE is essentially the usage: The predicted value is used only if its confidence counter is saturated. We refer the reader to [START_REF] Seznec | A case for (partially) TAgged GEometric history length branch prediction[END_REF] for a detailed description of ITTAGE.

Lastly, as a prediction does not depend on previous values but only on previous control-flow, VTAGE can seamlessly predict instructions in tight loops and behaves like LVP in Fig. 1. However, due to index hash and multiplexing from multiple components, it is possible that its prediction latency will be higher, although this is unlikely to be an issue since prediction can span several cycles.

Evaluation Methodology

Value Predictors

Single Scheme Predictors

We study the behavior of several distinct value predictors in addition to VTAGE. Namely, LVP [START_REF] Lipasti | Exceeding the dataflow limit via value prediction[END_REF], the 2-delta Stride predictor (2D-Stride) [START_REF] Eickemeyer | A load-instruction unit for pipelined processors[END_REF] as a representative of the stride- .

based predictor family 4 and a generic order-4 FCM predictor (o4-FCM) [START_REF] Sazeides | The predictability of data values[END_REF].

One could argue that we disregard D-FCM while it is more efficient than FCM. This is because VTAGE can be enhanced in the same way as D-FCM and it would thus be more just to compare D-FCM against such a predictor rather than the baseline VTAGE. We leave such a comparison for future work.

All predictors use 3-bit saturating counters as confidence counters. The prediction is used only if the confidence counter is saturated. Baseline counters are incremented by one on a correct prediction and reset on a misprediction. The predictors were simulated with and without FPC (See Section 5). As the potential of VP has been covered extensively in previous work, we limit ourselves to reasonably sized predictors to gain more concrete insights. We start from a 128KB LVP (8K-entry) and derive the other predictors, each of them having 8K entries as we wish to gauge the prediction generation method, not space efficiency. Predictor parameters are illustrated in Table 1.

For VTAGE, we consider a predictor featuring 6 tables in addition to a base component. The base component is a tagless LVP predictor. We use a single useful bit per entry in the tagged components and a 3-bit hysteresis/confidence counter c per entry in every component. The tag of tagged components is 12+rank-bit long with rank varying between 1 and 6. The minimum and maximum history lengths are respectively 2 and 64 as we found that these values provided a good tradeoff in our experiments.

For o4-FCM, we use a hash function similar to those described in [START_REF] Sazeides | Implementations of context based value predictors[END_REF] and used in [START_REF] Goeman | Differential FCM: Increasing value prediction accuracy by improving table usage efficiency[END_REF]: For a n th order predictor, we fold (XOR) each 64-bit history value upon itself to obtain a 16-bit index. Then, we XOR the most recent one with the second most recent one left-shifted by one bit, and so on. Even if it goes against the spirit of FCM, we XOR the resulting index with the PC in order to break conflicts as we found that too many instructions were interfering with each other in the VPT. Similarly, we keep a 2-bit hysteresis 4 To save space, we do not illustrate the Per-Path Stride predictor [START_REF] Nakra | Global context-based value prediction[END_REF] that we initially included in the study. Performance were on-par with 2D-Str. counter in the VPT to further limit replacements (thus interference). This counter is incremented if the value matches the one already present at update time, and decremented if not. The value is replaced only if the counter is 0.

We consider that all predictors are able to predict instantaneously. As a consequence, they can seamlessly deliver their prediction before Dispatch. This also implies that o4-FCM is -unrealistically -able to deliver predictions for two occurrences of the same instruction fetched in two consecutive cycles. Hence, its performance is most likely to be overestimated.

Hybrid Predictors

We also report numbers for a simple combination of VTAGE/2D-Str and o4-FCM/2D-Str, using the predictors described in Table 1. To select the prediction, we use a very simple mechanism: If only one component predicts (i.e. has high confidence), its prediction is naturally selected. When both predictors predict and if they do not agree, no prediction is made. If they agree, the prediction proceeds. Our hybrids also use the prediction of a component as the speculative last occurrence used by another component to issue a prediction (e.g. use the last prediction of VTAGE as the next last value for 2D-Stride if VTAGE is confident). When a given instruction retires, all components are updated with the committed value. To obtain better space efficiency, one can use a dynamic selection scheme such as the one Rychlik et al. propose. They assign a prediction to one component at most [START_REF] Rychlik | Efficient and accurate value prediction using dynamic classification[END_REF].

For the sake of clarity, we do not study gDiff [START_REF] Zhou | Detecting global stride locality value streams[END_REF] and DDISC [START_REF] Thomas | Using dataflow based context for accurate value prediction[END_REF] but we point out that they can be added "on top" of any other predictor. In particular, a hybrid of VTAGE and Stride, which, contrarily to FCM or any hybrid featuring FCM, would be feasible.

Simulator

In our experiments, we use the gem5 cycle-accurate simulator (x86 ISA) [START_REF] Binkert | The gem5 simulator[END_REF]. We model a fairly aggressive pipeline: 4GHz, 8-wide superscalar, out-of-order processor with a la-tency of 19 cycles. We chose a slow front-end (15 cycles) coupled to a swift back-end (4 cycles) to obtain a realistic misprediction penalty. Table 2 describes the characteristics of the pipeline we use in more details. As µ-ops are known at Fetch in gem5, all the width given in Table 2 are in µ-ops, even for the fetch stage. Independent memory instructions (as predicted by the Store Set predictor [START_REF] Chrysos | Memory dependence prediction using store sets[END_REF]) are allowed to issue out-of-order. Entries in the IQ are released upon issue (except with selective reissue). Since accuracy is high, branches are resolved on data-speculative paths [START_REF] Sodani | Understanding the differences between value prediction and instruction reuse[END_REF].

The predictor makes a prediction at Fetch for every µop (we do not try to estimate criticality or focus only on load instructions) producing a register explicitly used by subsequent µ-ops. In particular, branches are not predicted with the value predictor but values feeding into branch instructions are. To index the predictors, we XOR the PC of the x86 instruction left-shifted by two with the µ-op number inside the x86 instruction to avoid all µ-ops mapping to the same entry. This mechanism ensures that most µops of a macro-op will generate a different predictor index and therefore have their own entry in the predictor. We assume that the predictor can deliver as many predictions as requested by the Fetch stage. A prediction is written into the register file and replaced by its non-speculative counterpart when it is computed. However, a real implementation of VP need not use this exact mechanism, as discussed in Section 4.

Misprediction Recovery

We illustrate two possible recovery scenarios, squashing at commit time and a very idealistic selective reissue. In both scenarios, recovery is unnecessary if the prediction of instruction I was wrong but no dependent instruction has been issued before the execution of I, since the prediction is replaced by the effective result at execution time. This removes useless squashes and is part of our implementation.

For selective reissue, we assume an idealistic mechanism where repair is immediate. All value speculatively issued instructions stay in the IQ until they become non speculative (causing more pressure on the IQ). When a value misprediction is found, the IQ and LSQ are searched for dependents to reissue. Ready instructions can be rescheduled in the same cycle with respect to the issue width.

Yet, even such an idealistic implementation of selective reissue does not only offer performance advantages. In particular, it can only inhibit an entry responsible for a wrong prediction at update time. Consequently, in the case of tight loops, several occurrences of the same instruction can be inflight, and a misprediction for the first occurrence will often result in mispredictions for subsequent occurrences, causing multiple reissues until the first misprediction retires.

In any case, the 0-cycle reissue mechanism is overly op- timistic because of the numerous and complex steps selective reissue implies. Our experiments should be considered as the illustration that even a perfect mechanism would not significantly improve performance compared to squashing at commit time as long as the predictor is very accurate.

Benchmark Suite

We use a subset of the the SPEC'00 and SPEC'06 suites to evaluate our contributions as we focus on single-thread performance. Specifically, we use 12 integer benchmarks and 7 floating-point programs 5 . Table 3 summarizes the benchmarks we use as well as their input, which are part of the reference inputs provided in the SPEC software packages. To get relevant numbers, we identify a region of interest in the benchmark using Simpoint 3.2. We simulate the resulting slice in two steps: 1) Warm up all structures (Caches, branch predictor and value predictor) for 50M instructions, then collect statistics (Speedup, coverage, accuracy) for 50M instructions.

Simulation Results

Potential benefits of Value Prediction

We first run simulations to assess maximum benefit that could be obtained by a perfect value predictor. That is, performance is limited only by fetch bandwidth, memory hierarchy behavior, branch prediction behavior and various structure sizes (ROB, IQ, LSQ). Fig. 3 shows that a perfect predictor would indeed increase performance by quite a significant factor (up to 3.3) in most benchmarks.

General Trends

Forward Probabilistic Counters

Fig. 4 illustrates speedup over baseline using squashing at commit to repair a misprediction. First, Fig. 4 (a) suggests that the simple 3-bit counter confidence estimation is not sufficient. Accuracy is generally comprised between 0.94 and almost 1.0, yet fairly important slowdowns can be observed. Much better accuracy is attained using FPC (above 0.997 in all cases), and translates to performance gain when using VP. Only milc is slightly slowed down, but this is considered acceptable as slowdown is smaller than 1%. This demonstrates that by pushing accuracy up, VP yields performance increase even with a pessimistic -but much simpler -recovery mechanism.

Prediction Coverage and Accuracy

Accuracy of predictions when using FPC is widely improved with accuracy being higher than 0.997 for every benchmark. This accuracy improvement comes at some reduction of the predictor coverage, especially for applications for which the accuracy of the baseline predictor was not that high. This is illustrated in Fig. 6 for VTAGE: The greatest losses of coverage correspond to the applications that have the lowest baseline accuracy, i.e. crafty, vortex, gamess, gobmk, sjeng. These applications are also those for which a performance loss was encountered for the baseline while no performance is lost with FPC, i.e. crafty, vortex, gobmk, sjeng. For applications already having high accuracy and showing performance increase with the baseline, coverage is also slightly decreased, but in a more moderate fashion. Similar behaviors are encountered for the other predictors.

Note that high coverage does not correlate with high performance, e.g. namd exhibits 90% coverage but marginal speedup since there does not exist potential to speedup the application slice through Value Prediction (see Fig. 3). On the other hand, a small coverage may lead to significant speed-up e.g. h264.

Prediction schemes

Fig. 4 (b) shows that from a performance standpoint, no single-scheme predictor plainly outperforms the others even though some benchmarks achieve higher performance with 2D-Stride (wupwise and bzip) or VTAGE (applu, gcc, gamess and h264). This advocates for hybridization. Nonetheless, if VTAGE is outperformed by computational predictors in some cases, it generally appears as a simpler and better context-based predictor than our implementation of o4-FCM. In our specific case, o4-FCM suffers mostly from a lack of coverage stemming from the use of a stricter confidence mechanism and from needing more time to learn patterns.

Pipeline Squashing vs. Selective Reissue

Fig. 5 illustrates experiments similar to those of Fig. 4 except selective reissue is used to repair value mispredictions. On the one hand, selective reissue significantly decreases the misprediction penalty, therefore, performance gain is generally obtained even without FPC because less coverage is lost due to the confidence estimation scheme. Yet, this result has to be pondered by the fact that our implementation of selective reissue is idealistic.

On the other hand, with FPC, we observe that the recovery mechanism has little impact since the speedups are very similar in Fig. 4 (b) and Fig. 5 (b). In other words, provided that a confidence scheme such as ours yields very high accuracy, even an optimistic implementation of a very complex recovery mechanism will not yield a significant performance increase. It is only if such confidence scheme is not available that selective reissue becomes interesting, although Zhou et al. state that even a single-cycle recovery penalty -which is more conservative than our implementation -can nullify speedup if accuracy is too low (under 85%) [START_REF] Zhou | A study of value speculative execution and misspeculation recovery superscalar microprocessors[END_REF]. Lastly, one can observe that performance with selective reissue is lower than with pipeline squashing at commit in some cases even with FPC (e.g. art with o4-FCM). This is due to consecutive mispredictions as discussed in Section 7.

Hybrid predictors

For the sake of readability, we only report results for the squashing recovery mechanism, but trends are similar for selective reissue.

Fig. 7 (a) illustrates speedups for a combination of VTAGE and 2D-Stride as well as o4-FCM and 2D-Stride. As expected, simple hybrids yield slightly higher performance than single predictor schemes, generally achieving performance at least on par with the best of the two predictors. However, improvement over this level is generally marginal. Also note that computational and context-based predictors (in particular, VTAGE and Stride) indeed predict different instructions since coverage is usually increased, as shown by Fig. 7 (b).

Nonetheless, VTAGE + 2D-Stride appears as a better combination than o4-FCM + 2D-Stride, in addition to being simpler to implement.

Conclusion

To our knowledge, Value Prediction has not been considered for current commercially-available microprocessors. However, as the number of cores in high-end processors has now reached the 8-16 range, there is a new call for increasing core performance rather than the number of cores. Given the availability of a large number of transistors, Value Prediction appears as a good candidate to do so. In this paper, we reconsidered Value Prediction in this new context. First, we have shown that the use of Value Prediction can be effective, even if prediction validation is performed at commit time. Using probabilistic saturating confidence counters with a low increment probability can greatly benefit any value predictor: A very high accuracy (> 99.5%) can be ensured for all existing value predictors at some cost in coverage, using very simple hardware. Very high accuracy is especially interesting because it allows to tolerate the high individual average misprediction cost associated with validation at commit time. In this context, complex recovery mechanisms such as selective reissue have very marginal performance interest. In other words, we claim that, granted a proper confidence estimation mechanism such as the FPC scheme, state-of-the-art value predictors can improve performance on a fairly wide and deep pipeline while the prediction validation is performed at commit time. In this case, the Value Prediction hardware is essentially restricted to the in-order front-end (prediction) and the in-order back-end (validation and training) and the modifications to the outof-order engine are very limited.

Second, we have introduced a new context-based value predictor, the Value TAGE predictor. We derived VTAGE from the ITTAGE predictor by leveraging similarities between Indirect Branch Target Prediction and Value Prediction. VTAGE uses the global branch history as well as the path history to predict values. We have shown that it outperforms previous generic context-based value predictors leveraging per-instruction value history (e.g. FCM). A major advantage of VTAGE is its tolerance to high latency which has to be contrasted with local value history based predictors as they suffer from long critical operation when predicting consecutive instances of the same instruction. They are highly sensitive to the prediction latency and cannot afford long lookup times, hence large tables. On the contrary, the access to VTAGE tables can span over several cycles (from Fetch to Dispatch) and VTAGE can be implemented using very large tables.

Through combining our two propositions, a practical hybrid value predictor can fairly improve performance while only requiring limited hardware modifications to the out-oforder execution engine. Our experiments show that while improvement might be limited in many applications -less than 5% on 10 out of 19 benchmarks -, encouraging performance gains are encountered in most applications: From 5% up to 65% on the remaining 9 benchmarks.

Figure 1 :

 1 Figure 1: Prediction flow and critical paths for different value predictors when two occurrences of an instruction are fetched in two consecutive cycles.

Figure 2 :

 2 Figure 2: (1+N)-component VTAGE predictor. Val is the prediction, c is the hysteresis counter acting as confidence counter, u is the useful bit used by the replacement policy.

Figure 3 :

 3 Figure 3: Speedup upper bound for the studied configurations. An oracle predicts all results.

4 :

 4 Speedup over baseline for different predictors using the squashing at commit mechanism to recover from a value misprediction.

FigureCoverageFigure

  Figure Speedup over baseline for different predictors using selective reissue recover from a value misprediction.

Figure 7 :

 7 Figure 7: Speedup over baseline and coverage of a 2-component symmetric hybrid made of 2D-Stride and VTAGE with FPC. Squashing at commit is the recovery mechanism.

Table 1 :

 1 Layout Summary. For VTAGE, rank is the position of the tagged component and varies from 1 to 6, 1 being the component using the shortest history length. History lengths are respectively 2, 4, 8, 16, 32 and 64.

	Predictor #Entries	Tag	Size (KB)
	LVP [13]	8192	Full (51)	120.8
	2D-Stride [6]	8192	Full (51)	251.9
	o4-FCM [18]	8192 (VHT) 8192 (VPT)	Full (51) -	120.8 67.6
	VTAGE	8192 (Base) 6 × 1024	-12 + rank	68.6 64.1

Table 2 :

 2 Simulator configuration overview. *not pipelined.

		L1I 4-way 32KB, Perfect TLB; 8-wide fetch (2 taken
	Front End	branch/cycle), decode, rename; TAGE 1+12 components [21] 15K-entry total, 20 cycles min. mis. penalty; 2-way 4K-entry
		BTB, 32-entry RAS;
		256-entry ROB, 128-entry IQ, 48/48-entry LQ/SQ, 256/256
	Execution	INT/FP registers; 1K-SSID/LFST Store Sets [5]; 8-issue, 8ALU(1c), 4MulDiv(3c/25c*), 8FP(3c), 4FPMulDiv(5c/10c*),
		4Ld/Str; Full bypass; 8-wide retire;
		L1D 4-way 32KB, 2 cycles, 64 MSHRs, 4 load ports; Unified L2
	Caches	16-way 2MB, 12 cycles, 64 MSHRs, no port constraints, Stride prefetcher, degree 8, distance 1; All caches have 64B lines and
		LRU replacement;
		Single channel DDR3-1600 (11-11-11), 2 ranks, 8 banks/rank,
	Memory	8K row-buffer, tREFI 7.8us; Across a 64B bus; Min. Read Lat.:
		75 cycles, Max. 185 cycles.

Table 3 :

 3 Benchmarks used for evaluation. Top: CPU2000, Bottom: CPU2006. INT: 12, FP: 7, Total: 19.

	Program	Input
	164.gzip (INT)	input.source 60
	168.wupwise (FP)	wupwise.in
	173.applu (FP)	applu.in
		net.in arch.in place.out dum.out -nodisp -
	175.vpr (INT)	place only -init t 5 -exit t 0.005 -alpha t 0.9412
		-inner num 2
		-scanfile c756hel.in -trainfile1 a10.img -trainfile2
	179.art (FP)	hc.img -stride 2 -startx 110 -starty 200 -endx 160
		-endy 240 -objects 10
	186.crafty (INT)	crafty.in
	197.parser (INT)	ref.in 2.1.dict -batch
	255.vortex (INT)	lendian1.raw	.
	401.bzip2 (INT)	input.source 280
	403.gcc (INT)	166.i
	416.gamess (FP)	cytosine.2.config
	429.mcf (INT)	inp.in
	433.milc (FP)	su3imp.in
	444.namd (FP)	namd.input
	445.gobmk (INT)	13x13.tst
	456.hmmer (INT)	nph3.hmm
	458.sjeng (INT)	ref.txt
	464.h264ref (INT)	foreman ref encoder baseline.cfg
	470.lbm (FP)	reference.dat
	3.5
	3.25
	3
	2.75
	2.5
	2.25
	2
	1.75
	1.5
	1.25
	1

Including tracking and canceling the complete chain of dependent instructions as well as the indirect sources of performance loss encountered such as resource contention due to reexecution, higher misprediction rate (e.g. a value predicted using wrong speculative value history) and lower prediction coverage

c++ if correct or c = 0 if incorrect. Saturating arithmetic.

u = correct

We do not use the whole suites due to some currently missing system calls in gem5-x86.

Acknowledgments

This work was partially supported by the European Research Council Advanced Grant DAL No. 267175


Nathalie Bertrand
email: nathalie.bertrand@inria.fr

Serge Haddad
email: serge.haddad@ens-cachan.fr

Engel Lefaucheux
email: engel.lefaucheux@ens-cachan.fr

Foundation of Diagnosis and Predictability in Probabilistic Systems *

In discrete event systems prone to unobservable faults, a diagnoser must eventually detect fault occurrences. The diagnosability problem consists in deciding whether such a diagnoser exists.

Here we investigate diagnosis for probabilistic systems modelled by partially observed Markov chains also called probabilistic labeled transition systems (pLTS). First we study different specifications of diagnosability and establish their relations both in finite and infinite pLTS. Then we analyze the complexity of the diagnosability problem for finite pLTS: we show that the polynomial time procedure earlier proposed is erroneous and that in fact for all considered specifications, the problem is PSPACE-complete. We also establish tight bounds for the size of diagnosers. Afterwards we consider the dual notion of predictability which consists in predicting that in a safe run, a fault will eventually occur. Predictability is an easier problem than diagnosability: it is NLOGSPACE-complete. Yet the predictor synthesis is as hard as the diagnoser synthesis. Finally we introduce and study the more flexible notion of prediagnosability that generalizes predictability and diagnosability.

Introduction

Diagnosis. In computer science, diagnosis may refer to different kinds of activities. For instance, in artificial intelligence it can describe the process of identifying a disease from its symptoms, as performed by the expert system MYCIN [START_REF] Buchanan | Rule Based Expert Systems: The MYCIN Experiments of the Stanford Heuristic Programming Project[END_REF]. In this work, we concentrate on diagnosis as studied in control theory, where it is applied to partially observable systems prone to faults. A sequence of observations of such a system is said to be surely correct (respectively surely faulty) if all possible runs corresponding to this sequence are correct (respectively faulty); otherwise the observed sequence is ambiguous. While monitoring the system, the diagnoser should rule out ambiguities, and in particular detect that a fault occurred; and the problem of existence of such a diagnoser is refered to as diagnosability [START_REF] Sampath | Diagnosability of discrete-event systems[END_REF].

In order to anticipate problems triggered by fault occurrences, one can also be interested in predictors that detect that a fault will eventually occur, and the predictability problem [START_REF] Genc | Predictability of event occurrences in partially-observed discreteevent systems[END_REF] is concerned with the existence of a predictor. Diagnosis of discrete event systems. Diagnosability and predictability were first defined and studied in the framework of finite discrete event systems modelled by labeled transition systems (LTS), and the problems were shown to be solvable in PTIME (see [START_REF] Jiang | A polynomial algorithm for testing diagnosability of discrete-event systems[END_REF] and [START_REF] Genc | Predictability of event occurrences in partially-observed discreteevent systems[END_REF], respectively). Despite the polynomial time complexity of the decision problems, for diagnosable (respectively predictable) LTS, the size of the diagnoser (respectively predictor) constructed by the algorithms may be exponential. Diagnosers as well as predictors must ensure two requirements: correctness, meaning that the information provided by the diagnoser/predictor is accurate, and reactivity, ensuring that a fault will eventually be detected.

Diagnosis of probabilistic systems. Building on the work for LTS, the notion of diagnosability was later extended to Markov chains with labels on transitions, also called probabilitic labeled transition systems (pLTS) [START_REF] Thorsley | Diagnosability of stochastic discrete-event systems[END_REF]. In a probabilistic context, the reactivity requirement now asks that faults will be almost surely eventually detected. Regarding correctness, two specifications have been proposed: either one sticks to the original definition and requires that the provided information is accurate, defining A-diagnosability; or one weakens the correctness by admitting errors in the provided information that should, however, have an arbitrary small probability when the delay before the diagnostic is long enough, defining AA-diagnosability. From a computational viewpoint, PTIME algorithms have been proposed to solve these two specifications of probabilistic diagnosability [START_REF] Chen | Polynomial test for stochastic diagnosability of discrete-event systems[END_REF]. Predictability in pLTS with arbitrary small probability of erroneous information has also been studied in [START_REF] Chen | Failure prognosability of stochastic discrete event systems[END_REF].

In case a system is not diagnosable, one may be able to control it, by forbidding some controllable actions, so that is becomes diagnosable. This property of active diagnosability has been studied for probabilistic systems in [START_REF] Bertrand | Active diagnosis for probabilistic systems[END_REF] pursuing the work of [START_REF] Sampath | Active diagnosis of discrete-event systems[END_REF][START_REF] Haar | Optimal constructions for active diagnosis[END_REF] for discrete-event systems. Decidability and complexity issues are considered and optimal size diagnosers are synthesized. Interestingly, the diagnosability notion from [START_REF] Bertrand | Active diagnosis for probabilistic systems[END_REF] slightly differs from the original one in [START_REF] Thorsley | Diagnosability of stochastic discrete-event systems[END_REF].

Remaining issues. Some issues remained untouched in the above line of work. First, diagnosability was only considered w.r.t. finite faulty runs. It seems as important to consider diagnosability of correct runs, and ambiguity can also be defined for infinite computations. Second, in most work, the complexity of the varied diagnosability problems and of the diagnosers synthesis were left open. Moreover, optimizing the delay between the fault occurrence and its detection is an important issue. Yet the search for diagnosers (or predictors) with optimal reactivity was not even considered. Last predictability and diagnosability were independently studied while combining them is obviously a fruitful direction.

Contributions.

In this paper, we address the above mentioned gaps, and revisit diagnosability and predictability for probabilistic systems, from a semantical as well as a computational perspectives.

In constrast to existing work, we define diagnosability directly on the ambiguity triggered by the behaviours of the system, and then establish that it is equivalent to the existence of a diagnoser.

In order to give a firm semantical classification of diagnosability notions, we define criteria for diagnosability in probabilistic systems, depending on (1) whether the ambiguity is related to faulty runs only or to all runs and, (2) whether ambiguity is defined at the level of infinite runs, or for longer and longer finite subruns. A priori these two dimensions yield four specifications. We prove that two of them coincide leading to three main specifications: FF-diagnosability, IA-diagnosability used in [START_REF] Bertrand | Active diagnosis for probabilistic systems[END_REF] and FA-diagnosability, and we establish the connections between them. In addition we show that FF-diagnosability is equivalent to the A-diagnosability of [START_REF] Thorsley | Diagnosability of stochastic discrete-event systems[END_REF] for finite pLTS and that this hypothesis is necessary.

For finite state probabilistic systems, we show that these three notions of diagnosability can be characterized based on deterministic (finite or Büchi) automata acting as monitors, and synchronized with the pLTS. We further prove that the diagnosability problem (for all three specifications) is PSPACE-complete, contradicting the polynomial time result for FF-diagnosability [START_REF] Chen | Polynomial test for stochastic diagnosability of discrete-event systems[END_REF], and identify the error in their algorithm. Afterwards, we design algorithms for the synthesis of finite-memory diagnosers and prove that their size 2 Θ(n) (where n is the number of states of the pLTS model) is optimal. Since predictability is an interesting alternative to diagnosability, we introduce two possible specifications for predictability in probabilistic systems, and show that in both cases the predictability problem is NLOGSPACE-complete. Yet, as for diagnosers, the optimal size of predictors is in 2 Θ(n) . Last, we introduce and study prediagnosability that combines the benefits of predictability and diagnosability: depending on the observations, a prediagnoser behaves as a diagnoser or a predictor. Prediagnosability is of interest since predictability is more difficult to achieve than diagnosability, also prediagnosers can be seen as "as soon as possible" diagnosers. For the varied notions of prediagnosability, we establish that the prediagnosability problem is PSPACE-complete and design prediagnosers with optimal size. Summarizing we provide a full picture of the hierarchy for the different notions and the frontier between NLOGSPACE and PSPACE-complete problems. Organization. In Section 2, we introduce probabilistic LTS, define the possible diagnosability specifications, establish their connection. In Section 3, we provide characterizations for diagnosability of finite pLTS and we determine the exact complexity of the diagnosability problems. In Section 4, we design algorithms for synthesis of diagnosers with optimal size. In Section 5, we study predictability and prediagnosis, and focus on optimal diagnosers. All the proofs and additional results can be found in the companion research report [START_REF] Bertrand | Foundation of diagnosis and predictability in probabilistic systems[END_REF].

Diagnosability specification

In the context of stochastic discrete event systems diagnosis, systems are often modeled using labeled transition systems.

◮ Definition 1. A probabilistic labeled transition system (pLTS) is a tuple A = Q, q 0 , Σ, T, P where: Q is a set of states with q 0 ∈ Q the initial state; Σ is a finite set of events; T ⊆ Q × Σ × Q is a set of transitions; P : T → Q >0 is the probabilistic transition function fulfilling for all q ∈ Q:

(q,a,q ′ )∈T P(q, a, q ′ ) = 1.

Observe that a pLTS is a labeled transition system (LTS) equipped with transition probabilities. The transition relation of the underlying LTS is defined by: q a -→ q ′ for (q, a, q ′ ) ∈ T ; this transition is then said to be enabled in q. A pLTS is said to be live if in every state q of the pLTS, a transition is enabled. We assume the pLTS we consider are countably branching, i.e., in every state q, only countably many transitions are enabled, so that the summation (q,a,q ′ )∈T P(q, a, q ′ ) is well-defined.

Let us now introduce some important notions and notations that will be used throughout the paper. A run ρ of a pLTS A is a (finite or infinite) sequence ρ = q 0 a 0 q 1 . . . such that for all i, q i ∈ Q, a i ∈ Σ and when q i+1 is defined, q i ai -→ q i+1 . The notion of run can be generalized, starting from an arbitrary state q. We write Ω for the set of all infinite runs of A starting from q 0 , assuming the pLTS is clear from context. When it is finite, ρ ends in a state q and its length, denoted |ρ|, is the number of actions occurring in it. Given a finite run ρ = q 0 a 0 q 1 . . . q n and a (finite or infinite) run ρ ′ = q n a n q n+1 . . ., we call concatenation of ρ and ρ ′ and we write ρρ ′ the run q 0 a 0 q 1 . . . q n a n q n+1 . . .; the run ρ is then a prefix of ρρ ′ , which we denote ρ ρρ ′ . The cylinder defined by a finite run ρ is the set of all infinite runs that extend ρ: C(ρ) = {ρ ′ ∈ Ω | ρ ρ ′ }. The sequence associated with ρ = qa 0 q 1 . . . is the word σ ρ = a 0 a 1 . . ., and we write equally q ρ = ⇒ or q σρ = ⇒ (resp. q ρ = ⇒ q ′ or q σρ = ⇒ q ′ ) for an infinite (resp. finite) run ρ. A state q is reachable (from q 0 ) if there exists a run such that q 0 ρ = ⇒ q, which we alternatively write q 0 = ⇒ q. The language of pLTS A consists of all infinite words that label runs of A and is formally defined as

L ω (A) = { σ ∈ Σ ω | q 0 σ = ⇒ }.
Forgetting the labels and merging (and summing the probabilities of) the transitions with same source and target, a pLTS yields a discrete time Markov chain (DTMC). As usual for DTMC, the set of infinite runs of A is the support of a probability measure defined by Caratheodory's extension theorem from the probabilities of the cylinders:

P(C(q 0 a 0 q 1 . . . q n )) = P(q 0 , a 1 , q 1 ) • • • P(q n-1 , a n-1 , q n ) .
In order to formalize problems related to fault diagnosis, we partition the event set Σ into two disjoint sets Σ o and Σ u , the sets of observable and of unobservable events, respectively. Moreover, we distinguish a special fault event f ∈ Σ u . Let σ ∈ Σ * be a finite word; its length is denoted |σ|. The projection of σ onto Σ o is defined inductively by: P(ε) = ε; for a ∈ Σ o , P(σa) = P(σ)a; and P(σa

) = P(σ) for a / ∈ Σ o . Write |σ| o for |P(σ)|.
When σ is an infinite word, its projection is the limit of the projections of its finite prefixes. This projection is applicable to runs via their associated sequence; it can be either finite or infinite. As usual the projection is extended to languages. With respect to the partition of Σ = Σ o ⊎ Σ u , a pLTS A is convergent if there is no infinite sequence of unobservable events from any reachable state:

L ω (A) ∩ Σ * Σ ω u = ∅. When A is convergent, for every σ ∈ L ω (A), P(σ) ∈ Σ ω o .
In the rest of the paper we assume that pLTS are convergent. We will refer to a sequence for a finite or infinite word over Σ, and an observed sequence for a finite or infinite sequence over Σ o . Clearly, the projection onto Σ o of a sequence yields an observed sequence.

The observable length of a run ρ denoted |ρ| o ∈ N ∪ {∞}, is the number of observable actions that occur in it:

|ρ| o = |σ ρ | o .
A signalling run is a finite run whose last action is observable. Signalling runs are precisely the relevant runs w.r.t. partial observation issues since each observable event provides an additional information about the execution to an external observer. In the sequel, SR denotes the set of signalling runs, and SR n the set of signalling runs of observable length n. Since we assume that the pLTS are convergent, for all n > 0, SR n is equipped with a probability distribution defined by assigning measure P(ρ) = P(C(ρ)) to each ρ ∈ SR n . Given ρ a finite or infinite run, and n ≤ |ρ| o , ρ ↓n denotes the signalling subrun of ρ of observable length n. For convenience, we consider the empty run q 0 to be the single signalling run, of null length.

Let A be a pLTS. A run ρ is faulty if σ ρ contains f , otherwise it is correct. W.l.o.g., by considering two copies of each state, we assume that the states of A are partitioned into correct states and faulty states:

Q = Q f ⊎ Q c where Q f are
σ ∈ Σ ω o is surely correct if P -1 (σ) ∩ L ω (A) ⊆ (Σ \ f ) ω ; it is surely faulty if P -1 (σ) ∩ L ω (A) ⊆ Σ * f Σ ω ;
otherwise, it is ambiguous. For finite sequences, we need to rely on signalling runs: a finite observed sequence σ ∈ Σ * o is surely faulty (resp. surely correct) if for every signalling run ρ with P(σ ρ ) = σ, ρ is faulty (resp. correct); otherwise it is ambiguous. A (finite signalling or infinite) run ρ is surely faulty (resp. surely correct, ambiguous) if P(ρ) is surely faulty (resp. surely correct, ambiguous).

In order to introduce diagnosability, we define different subsets of infinite runs.

◮ Definition 2 (Ambiguous runs). Let A be a pLTS and n ∈ N with n ≥ 1. Then: FAmb ∞ is the set of infinite faulty ambiguous runs of A;

CAmb ∞ is the set of infinite correct ambiguous runs of A; FAmb n is the set of infinite runs of A whose signalling subrun of observable length n is faulty and ambiguous; CAmb n is the set of infinite runs of A whose signalling subrun of observable length n is correct and ambiguous.

We propose four possible specifications of diagnosability for probabilistic systems. There are two discriminating criteria: whether the non ambiguity requirement holds for faulty runs only (_F) or for all runs (_A), and whether ambiguity is defined at the infinite run level (I_) or for longer and longer finite signalling subruns (F_).

◮ Definition 3 (Diagnosability specifications). Let A be a pLTS. Then:

A pLTS A is IF-diagnosable if P(FAmb ∞ ) = 0. A pLTS A is IA-diagnosable if P(FAmb ∞ ⊎ CAmb ∞ ) = 0. A pLTS A is FF-diagnosable if lim sup n→∞ P(FAmb n ) = 0. A pLTS A is FA-diagnosable if lim sup n→∞ P(FAmb n ⊎ CAmb n ) = 0.
Let us illustrate these specifications on the two pLTS of Figure 1 where {u, f } is the set of unobservable events, represented by dashed arrows. Here and later on, unless mentioned, the transitions outgoing a state are uniformly distributed. On the left, a faulty run will almost surely produce a b-event that cannot be mimicked by the single correct run. Thus this pLTS is IF-diagnosable. The unique correct run ρ = q 0 uq 1 (aq 1 ) ω has probability 1 2 and its corresponding observed sequence a ω is ambiguous. Thus this pLTS is not IA-diagnosable. On the right, any infinite faulty run will contain a b-event, and cannot be mimicked by a correct run, therefore FAmb ∞ = ∅. The two infinite correct runs have a ω as observed sequence, and cannot be mimicked by a faulty run, thus CAmb ∞ = ∅. As a consequence, this pLTS is IA-diagnosable. Consider now the infinite correct run ρ = q 0 uq 1 (aq 1 ) ω . It has probability 1 2 , and all its finite signalling subruns are ambiguous since their observed sequence is a n , for some n ∈ N. Thus for all n ≥ 1, P(CAmb n ) ≥ 1 2 , so that this pLTS is not FA-diagnosable.

q 0 f 1 f 2 q 1 f a u a b a q 0 q 2 f 1 f 2 q 1 u f a u a b b a Figure 1 Left: a pLTS that is IF-diagnosable but not IA-diagnosable. Right: a pLTS that is IA-diagnosable but not FA-diagnosable.
The next theorem establishes the connections between these definitions.

◮ Theorem 4. The different diagnosability notions for pLTS relate according to the table below. Moreover, all implications hold for infinite-state pLTS, and non implications already hold for finite-state pLTS. (The implication marked with * requires finitely branching pLTS.)

Diagnosability All runs Faulty runs

Signalling runs

FA ⇒ ⇐ FF ⇓ ⇑ ⇓⇑ * Infinite runs IA ⇒ ⇐ IF
To conclude this section, we compare IF-diagnosability with A-diagnosability from [START_REF] Thorsley | Diagnosability of stochastic discrete-event systems[END_REF].

◮ Theorem 5. A finite pLTS A is IF-diagnosable if and only if it is A-diagnosable, that is:

∀ε > 0, ∃N ε ∈ N, for every faulty signalling run ρ and every n ≥ N ε , P({ρ ′ ∈ FAmb n+|ρ|o | ρ ρ ′ }) < εP(ρ). This condition is only sufficient for finitely branching infinite pLTS.

Complexity of diagnosability

In this section, we establish the complexity of diagnosability stated in the next theorem.

◮ Theorem 6. The IF-diagnosability, IA-diagnosability, and FA-diagnosability problems for finite pLTS are PSPACE-complete.

To prove membership in PSPACE, we provide characterizations of the different diagnosability notions we introduced. For each notion of diagnosability, we proceed similarly. First, given a pLTS A we design a deterministic automaton that accepts some (finite or infinite) observed sequences of A. Then we build the synchronized product of this automaton with A, to obtain another pLTS with the same stochastic behaviour as A but augmented with additional information about the current run, that will be useful for diagnosability. Finally, we characterize diagnosability by graph properties on the synchronized product.

Here we only detail the procedure for IA-diagnosability. Its automaton IA(A) is the deterministic Büchi automaton introduced in [START_REF] Haar | Optimal constructions for active diagnosis[END_REF]. Its states are triples of disjoint subsets of states (U, V, W ) where given some observed sequence, U is the set of possible correct states and V and W are possible faulty states. The decomposition between V and W reflects the fact that the IA-automaton tries to resolve the ambiguity between U and W (when both are non empty), while V corresponds to a waiting room of states reached by faulty runs that will be examined when the current ambiguity is resolved. The set F of accepting states consists of all triples (U, V, W ) with U = ∅ or W = ∅. When U = ∅, the current signalling run is surely faulty. When W = ∅ the current signalling run may be ambiguous (if V = ∅) but the "oldest" possible faulty runs have been discarded. Hence, any infinite observed sequence of A passing infinitely often through F is not ambiguous (ambiguities are resolved one after another). Figure 2 shows the IA-automaton of the pLTS depicted on the right of Figure 1. Observe that, despite the fact that all observed sequences a n are ambiguous as witnessed by the possible faulty state f 2 , a ω , which is indeed unambiguous, is accepted by the IA-automaton since its execution infinitely often visits state ({q 1 , q 2 }, {f 2 }, ∅).

{q 0 }, ∅, ∅ s 0 {q 1 , q 2 }, ∅, {f 2 } s 1 {q 1 , q 2 }, {f 2 }, ∅ s ′ 1 ∅, {f 1 }, {f 2 } s 2 ∅, ∅, {f 1 , f 2 } s ′ 2 ∅, ∅, {f 1 } s 3 ∅, ∅, {f 2 } s 4 ∅, {f 2 }, ∅ s ′
To come up with a characterization, one builds A IA = A × IA(A), the product of A and IA(A) synchronized over observed events.

◮ Proposition 7. A finite pLTS A is IA-diagnosable if and only if A IA has no bottom strongly connected component (BSCC) such that:

either, all its states (q, U, V, W ) fulfill q ∈ Q f and U = ∅; or all its states (q, U, V, W ) fulfill q ∈ Q c and W = ∅.

The decision algorithm for IA-diagnosability checks whether the above characterization is satisfied by looking for a state that violates the disjunction and then checking that it belongs to a BSCC. This can be done in polynomial space without explicitly building A IA , and relying on Savitch's theorem.

In order to establish a lower bound for the complexity of IA-diagnosability, we introduce a variant of language universality. A language L over an alphabet Σ is said eventually universal if there exists a word v ∈ Σ * such that v -1 L = Σ * , where v -1 L denotes the left quotient of

L by v: v -1 L = {v ′ | vv ′ ∈ L}.
Recently, several variants of the universality problem were shown to be PSPACE-complete [START_REF] Rampersad | The computational complexity of universality problems for prefixes, suffixes, factors, and subwords of regular languages[END_REF] but, to the best of our knowledge, eventual universality has not yet been considered.

Because of our diagnosis framework, we focus on live non deterministic finite automata (NFA). Similarly to pLTS, an NFA is live if from every state there is at least one outgoing transition. The language of an NFA A, denoted L(A), is defined as the set of finite words that are accepted by A. We reduce the universality problem for NFA, which is known to be PSPACE-complete [START_REF] Meyer | The equivalence problem for regular expressions with squaring requires exponential space[END_REF] to the eventual universality problem to obtain the following result.

◮ Proposition 8. Let A be a live NFA where all states are terminal. Then deciding whether L(A) is eventually universal is PSPACE-hard.

Let us sketch how we reduce this problem to IA-diagnosability. Given a live NFA A over Σ where all states are terminal, one builds the pLTS of Figure 3 where Σ ∪ {♯} are observable. Since a correct run almost surely "outputs" a ♯, ambiguity may only occur with faulty runs. Since after the fault one observes Σ * , using the characterization in Proposition 7 one concludes that the pLTS is not IA-diagnosable if and only if A is eventually universal.

q ′ 0 f 0 q 0 q q ♯ f Σ u ♯ ♯ ♯ A Figure 3 A reduction for PSPACE-hardness of IA-diagnosability.
Theorem 6 seems to contradict the PTIME decision procedure from [START_REF] Chen | Polynomial test for stochastic diagnosability of discrete-event systems[END_REF] for A-diagnosability (or, equivalently IF-diagnosability). However, we establish that: ◮ Fact 9. The PTIME algorithm of [START_REF] Chen | Polynomial test for stochastic diagnosability of discrete-event systems[END_REF] for A-diagnosability is erroneous.

Diagnoser construction

In this section, we focus on the construction of diagnosers. A diagnoser is a function D : Σ * o → {?, ⊤, ⊥} assigning to every finite observation sequence a verdict. Informally when a diagnoser outputs ? it does not provide any information, while ⊤ ensures that a fault is certain and ⊥ that some information about correctness has been provided. We consider the natural partial order ≺ on these values defined by ? ≺ ⊤ and ? ≺ ⊥.

A finite memory diagnoser is given by a tuple (M, Σ o , m 0 , up, D fm ) where M is a finite set of memory states, m 0 ∈ M is the initial memory state, up : M × Σ o → M is a memory update function, and finally D fm : M → {?, ⊤, ⊥} is a diagnoser function. The mapping up is extended into a function up : M × Σ * o → M defined inductively by up(m, ε) = m and up(m, wa) = up(up(m, w), a). A finite memory diagnoser is not a diagnoser as defined above, yet it induces the diagnoser defined by D(w) = D fm (up(m 0 , w)).

Diagnosers we define in the sequel will have two important properties: soundness and reactivity. Soundness ensures that the information provided is accurate and reactivity specifies which pieces of information the diagnoser must provide. The precise soundness and reactivity requirements depend on the diagnosability notion of interest. Moreover, we restrict to diagnosers that, once they output ⊤, never change their verdict in the future. Note that any sound diagnoser can be turned into one that is sound and satisfies this commitment property. In this short version, we only introduce IA-diagnosers (the synthesis of FA-diagnosers and IF-diagnosers is similar and even simpler). Intuitively, IA-diagnosers may resolve an ambiguity late, while another one has already been produced.

◮ Definition 10. An IA-diagnoser for A is a function D : Σ * o → {⊤, ⊥, ?} such that soundness For all w ∈ Σ * o if D(w) = ⊤, then w is surely faulty; if D(w) = ⊥, letting |D(w)| ⊥ = |{0 < n ≤ |w| | D(w ≤n ) = ⊥}|, then for all signalling run ρ such that P(ρ) = w, ρ ↓|D(w)| ⊥ is correct. reactivity P({ρ ∈ Ω | D sup (P(ρ)) =?}) = 0 where for w ∈ Σ ω o , D sup (w) = lim sup n→∞ D(w ≤n ).
(D sup is well-defined since once the diagnoser outputs ⊤, it always sticks to this verdict.)

The reactivity condition requires that almost surely the diagnoser detects a fault or guarantees that longer and longer subruns of the current run are correct. Soundness of ⊤ verdict implies that indeed the run is faulty. The interpretation of D(w) = ⊥ is that the diagnoser ensures that any signalling subrun of length |D(w)| ⊥ ≤ |w| of a signalling run for w is correct. Of course it may deduce this information from the last |w| -|D(w)| ⊥ observations. This is illustrated on the example of Figure 4 for which we describe an IA-diagnoser. After observing any sequence wbaa, with w ∈ {a, b} * , the diagnoser knows a posteriori that two steps before, that is after the observation of wb, the run was necessarily correct. Indeed, observing the suffix aa is not possible after a fault, yet wba is not surely correct. The function D defined by: for w ∈ {a, b} * (ab + aa), D(w) = ⊥, for w ∈ {a, b, c} * c, D(w) = ⊤ and otherwise D(w) =?, is an IA-diagnoser.

q 0 f 1 f 2 f a b c a, b Figure 4 A pLTS which is IA-diagnosable.
The next proposition establishes that this definition of diagnosers is appropriate for IA-diagnosability. Furthermore it provides tight lower and upper bounds for the size of IA-diagnosers. The pLTS of Figure 5 is used to prove the lower bound. Intuitively, every IA-diagnoser for this pLTS must decide, on observing a c, whether the run is faulty or correct. To do so, it must remember whether, n observations earlier, the event was a or b. Due to the self-loop on q 0 , it cannot know when a c will occur, and must remenber the n last observations. This requires at least 2 n memory states.

◮ Proposition 11. A finite pLTS A is IA-diagnosable if and only if it admits an IA-diagnoser.

For every pLTS A with n c correct states and n f faulty states which is IA-diagnosable, one can build an IA-diagnoser with at most 2 nc 3 n f states. There is a family {A n } n∈N of IAdiagnosable pLTS such that A n has 2n + 2 states and it admits no IA-diagnoser with less than 2 n memory states.

A n q 0 l 0 l 1 l 2 . . . l n r 1 r 2 . . . r n f a a, b a, b a, b b a, b a, b a, b a, b c c Figure 5
Example of an IA-diagnosable pLTS requiring an IA-diagnoser with exponential size.

Predictability and prediagnosis

Predictability. Fault predictability has been first introduced for LTS in [START_REF] Genc | Predictability of event occurrences in partially-observed discreteevent systems[END_REF]: in words, an LTS predictable (resp. k-predictable) if a fault can be predicted (resp. at least before k observations) whatever the future behavior of the LTS. There are two possible adaptations for pLTS: (1) either one sticks to the original definition and requires that the fault surely occurs or, (2) one relaxes it and only requires that the fault almost surely occurs.

In order to reason about predictability, we introduce some particular prefixes of a run. For a finite run ρ, and k ∈ N, we define pre k (ρ), the k-past of ρ, by pre k (ρ) = ρ ↓|ρ|o-min(k,|ρ|o) . For example, in the pLTS of Figure 6, pre 0 (q 0 bq 1 f q 2 ) = q 0 bq 1 as f is unobservable and pre 1 (q 0 bq 1 f q 2 ) = q 0 . In fact for k ≥ 1, pre k (q 0 bq 1 f q 2 ) = q 0 .

q 0 q 1 q 2 q 3 f 1 b c a f c a b
Figure 6 A 0-surely predictable and 1-predictable pLTS.

We also introduce sets of observed sequences defined on their possible future behaviors. In words, an observed sequence σ forbids prediction of a fault when there is still either a correct infinite run where σ is a prefix of its observed sequence (UPC) or a set of positive measure of such runs (UPSC). Thus in order to be k-predictable, k observations before a possible fault the observed sequence should not belong to these sets (see Definition 13).

◮ Definition 12 (ultimately possibly (significantly) correct). Let σ be a finite observed sequence of a pLTS A. Then:

σ is ultimately possibly correct if {ρ ′ ∈ Ω | σ P(ρ ′ )} ∩ C ∞ = ∅.
The set of ultimately possibly correct observed sequences is denoted UPC. σ is ultimately possibly significantly correct if P({ρ

′ ∈ Ω | σ P(ρ ′ )} ∩ C ∞ ) > 0.
The set of ultimately possibly significantly correct observed sequences is denoted UPSC.

◮ Definition 13 ((sure) predictability). Let k ∈ N.

A pLTS A is k-surely predictable if for every run ρf q of A, P(pre k (ρ)) / ∈ UPC;

A pLTS A is k-predictable if for every run ρf q of A, P(pre k (ρ)) / ∈ UPSC.

Observe that in the previous definition, one can safely restrict to check the condition on correct runs ρ by considering the first occurrence of a fault in the run ρf q. For example, the pLTS of Figure 6 is 0-surely predictable. Every correct run ρ that is followed by f is such that P(ρ) = b n c for some n ≥ 1. As it is the unique signalling run with such an observed sequence, the fault can be predicted. It is not 1-surely predictable as the 1-past of ρ = q 0 bq 1 cq 2 f f 1 is pre 1 (ρ) = q 0 bq 1 and the infinite run ρ ′ = q 0 (bq 1 ) ω is correct. However it is 1-predictable as for every signalling run with observed sequence b n for some n ≥ 1 (thus ending in q 1 ) a fault eventually almost surely occurs. Finally it is not 2-predictable since the 2-past of ρ = q 0 bq 1 cq 2 f f 1 is q 0 and the infinite correct run ρ = q 0 (aq 3 ) ω has probability 1 2 . We have established all the relations between the different notions of diagnosability and predicatibility (see Figure 8 in the conclusion). The main result about predicatibility is given in the next theorem, and highlights the complexity gap between predictability and diagnosability for probabilistic systems (recall that their complexity coincide for LTS). Despite this difference, the size of optimal predictors is comparable to the one of optimal diagnosers (see details in our research report [START_REF] Bertrand | Foundation of diagnosis and predictability in probabilistic systems[END_REF]).

◮ Theorem 14. Deciding, given A a pLTS and k ∈ N, whether A is k-predictable (resp. surely k-predictable) is an NLOGSPACE-complete problem. Moreover, the same complexity applies assuming k is fixed (rather than given as input).

Prediagnosis. On the one hand, diagnosis is concerned with detection of faults that have occurred: given a sequence of observations a diagnoser tries to detect that a fault has occurred in the past of all consistent behaviors. On the other hand, prediction is concerned with anticipation of faults: given a sequence of observations a predictor tries to detect that a fault will eventually occur in the future of all consistent behaviors. The notion we introduce now, prediagnosis, concerns detection of faults both in the past and in the future.

Let us start by introducing two sets of infinite faulty runs that make prediagnosis impossible. FUPC ∞ is the set of faulty runs that admit for all their finite prefixes a compatible infinite correct run. The condition is strengthened for FUPSC ∞ which gathers the faulty runs that admit for all their finite prefixes, a positive measure of compatible infinite correct runs.

◮ Definition 15. Let A be a pLTS. Then: FUPC ∞ , the set of faulty, ultimately possibly correct runs is defined by: FUPC ∞ = {ρ ∈ Ω | ρ faulty and ∀i ∈ N, P(ρ ↓i ) ∈ UPC} FUPSC ∞ , the set of faulty, ultimately possibly significantly correct runs is defined by: FUPSC ∞ = {ρ ∈ Ω | ρ faulty and ∀i ∈ N, P(ρ ↓i ) ∈ UPSC}

The reactivity requirement for prediagnosers will impose that these sets are negligible. The difference between these two sets impacts correctness: relying on FUPC ∞ provides a sure correctness while relying on FUPSC ∞ only provides an almost sure correctness.

◮ Definition 16 ((Sure) Prediagnosability). Let A be a pLTS. Then:

A is surely prediagnosable if P(FUPC ∞ )=0; A is prediagnosable if P(FUPSC ∞ )=0.
Surprisingly, sure prediagnosability lies strictly between FF-diagnosability and IF-diagnosability with equivalence for finitely branching pLTS. Also (sure) 0-predictability implies (sure) prediagnosability. As expected, the less demanding specification is prediagnosability. All the relations that we have established between the different notions of diagnosability, predictability and prediagnosability are described by Figure 8 in the conclusion. From a complexity point of view, prediagnosability is equivalent to diagnosability: ◮ Theorem 17. The (sure) prediagnosability problem is PSPACE-complete.

In the research report [START_REF] Bertrand | Foundation of diagnosis and predictability in probabilistic systems[END_REF], we formally define and study the notion of prediagnosers. Here we informally discuss the interest of prediagnosers. While sure prediagnosability and IF-diagnosability are equivalent for finitely branching pLTS, there are differences between sure prediagnosers and IF-diagnosers. An IF-diagnoser is a sure prediagnoser, but a sure prediagnoser may output a verdict ⊤ even before a fault. This phenomenon occurs even if the pLTS is non predictable. The non predictable pLTS of Figure 7 points out this difference. A diagnoser may output ⊤ only after observing two a's, since then, surely a fault occurred. In contrast, a sure prediagnoser can already output ⊤ after observing the first a. In fact this pLTS is FA-diagnosable since after an occurrence of b, the run is surely correct. Prediagnosers, can be thought of as monitors that emit verdicts as soon as possible, while preserving soundness. In the proof that prediagnosability is equivalent to the existence of a prediagnoser, the prediagnosers we construct are indeed optimal in that sense.

q 0 f 1 q 1 q 2 f a f b a b
Figure 7 A non-predictable pLTS, for which a sure prediagnoser is quicker than all diagnosers. In this work, we settled the foundations of diagnosability and predictability for partially observed stochastic systems. In particular, we investigated semantical issues and provided several meaningful definitions for diagnosability and predictability in a probabilistic context. We also introduced prediagnosability, that combines the advantages of diagnosability and predictability. Beyond providing relations between these notions, we obtained tight complexity bounds using graph-based characterizations on the product of the system under scrutiny and an appropriate monitor. The complexity ranges from NLOGSPACE-completeness for predictability to PSPACE-completeness for diagnosability and prediagnosability, as summarized on Figure 8. Last, we proved exponential almost matching lower and upper bounds for the diagnosers, predictors, and prediagnosers synthesis problems.

The present contribution opens several interesting research perspectives. First of all, the decidability status (and in the positive case, the precise complexity) of the approximate diagnosability (AA-diagnosability) introduced in [START_REF] Thorsley | Diagnosability of stochastic discrete-event systems[END_REF] is still open since we only proved the algorithm from [START_REF] Chen | Polynomial test for stochastic diagnosability of discrete-event systems[END_REF] to be erroneous (see [START_REF] Bertrand | Foundation of diagnosis and predictability in probabilistic systems[END_REF]). Second, beyond diagnosability and its variants (predictability and prediagnosability), we wish to conduct a systematic study of other paradigms related to partial observability, such as opacity or detectability, in a probabilistic context. Last, we plan to move to more quantitative versions of diagnosis including optimization issues. The objective would be to minimize the observational capacities of the monitor, either spatially or timely by restricting either the observable actions, or the observation time instants, while preserving diagnosability.

Figure 2

 2 Figure 2The IA-automaton of pLTS depicted on the right of Figure1.

Figure 8

 8 Figure 8 Summarizing relations between specifications, and associated complexities.

  faulty states, and Q c correct states. Faulty (resp. correct) states are only reachable by faulty (resp. correct) runs. An observed sequence

* This work has been supported by project ImpRo ANR-2010-BLAN-0317 and the European Union Seventh Framework Programme [FP7/2007-2013] under grant agreement 257462 HYCON2 NOE. © Nathalie Bertrand, Serge Haddad, Engel Lefaucheux;