Cyril Six
email: csix@kalrayinc.com

Kalray S A Montbonnot

Léo Gourdin
email: leo.gourdin@univ-grenoble-alpes.fr

Sylvain Boulmé
email: sylvain.boulme@univ-grenoble-alpes.fr

David Monniaux
email: david.monniaux@univ-grenoble-alpes.fr

Justus Fasse
email: justus.fasse@kuleuven.be

Nicolas Nardino
email: nicolas.nardino@ens-lyon.fr

Formally Verified Superblock Scheduling

Keywords: CCS Concepts:, Software and its engineering → Formal software verification, Retargetable compilers, • Theory of computation → Scheduling algorithms, • General and reference → Performance, • Computer systems organization → Superscalar architectures, Very long instruction word Translation validation, Symbolic execution, the Coq proof assistant, Instruction-level parallelism

On in-order processors, without dynamic instruction scheduling, program running times may be significantly reduced by compile-time instruction scheduling. We present here the first effective certified instruction scheduler that operates over superblocks (it may move instructions across branches), along with its performance evaluation. It is integrated within the CompCert C compiler, providing a complete machinechecked proof of semantic preservation from C to assembly.

Our optimizer composes several passes designed by translation validation: program transformations are proposed by untrusted oracles, which are then validated by certified and scalable checkers. Our main checker is an architectureindependent simulation-test over superblocks modulo register liveness, which relies on hash-consed symbolic execution.

Introduction

In-order processor cores execute assembly instructions in their syntactic order. If one instruction computes a register and the next instruction uses this register, then the core stalls until the value computed becomes available, which may take several clock cycles. An optimizing compiler thus reorders instructions to minimize stalling. 1 CompCert 2 [Leroy 2009a,b] is a compiler for the C programming language with a machine-checked proof of correctness: if compilation succeeds, then the semantics of the assembly code matches that of the source: an execution of the C program without undefined behaviors translates into an assembly execution with the same sequence of observable events (calls to external functions, accesses to volatile variables. . . ). CompCert does not reschedule instructions, thus producing suboptimal assembly code for in-order cores.

Motivations. [START_REF] Six | Certified and efficient instruction scheduling: application to interlocked VLIW processors[END_REF] added instruction scheduling and some peephole optimizations to CompCert (thus creating CompCertSched) at the assembly level, in postpass (after register allocation and final transformations, Fig. 1 and2). One of their goals was to form instruction "bundles", to be executed in parallel, for the Kalray KVX, a VLIW (Very Long Instruction Word) processor. However, due to that late position within compilation, they were limited to scheduling inside basic blocks (instruction sequences with one single entry point and one single exit point). Dependencies induced by register reuse may thus prevent finding good schedules. Moreover, the porting effort of their approach is rather high for every architecture. 1 The alternative is an out-of-order core, dynamically reordering instructions.

Their complexity and lower predictability (e.g., for bounding worst-case execution time), excludes them from some safety-critical systems. Scheduling over superblocks (where instructions may move across branches) is desirable because such blocks are often larger than basic blocks, thus with more opportunities to reorder instructions. Reordering before register allocation, at the RTL level 3 , is also desirable as it can take advantage of the infinite number of pseudo-registers, in contrast to postpass scheduling which works with a limited number of registers, some of them having already been spilled. While postpass scheduling (anyway necessary for generating bundles on VLIW processors) benefits from the precise view of the final assembly code, e.g., with register-spilling instructions, prepass scheduling greatly leverages various heuristics that increases semantic parallelism, such as renaming with fresh pseudo-registers after loop unrolling. RTL also provides a representation generic over all processor architectures, thus with a reduced per-architecture development effort.

Contributions and structure of the paper. Section 2 recalls the approach of [START_REF] Six | Certified and efficient instruction scheduling: application to interlocked VLIW processors[END_REF] and how, as a secondary contribution, we have ported their postpass instruction scheduler to the AArch64 architecture. This demonstrates which parts of their postpass are generic, and which need to be ported. Our postpass scheduler, like theirs, also performs a peephole optimization just before scheduling 3 RTL, or "Register Transfer Language", is the intermediate representation on which most optimizations take place within CompCert. Optimizing from RTL to RTL facilitates compatibility, so our work can be easily slotted into other CompCert-related projects.

(in the scheduler's front-end). But, ours is slightly more advanced (for leveraging AArch64 features). Here, our main result is that we have simply reused their translation validation procedure: this strengthens the case for this approach to verification, which still works after tweaks to heuristics whereas a direct proof would surely require much reengineering.

Our main contribution is a portable verified instruction scheduler, working on a portable intermediate representation (RTL, see Figure 2). It operates over superblocks: a generalization of basic blocks, such that each instruction of a given block has still at most one successor in this block, but may also branch to another superblock [START_REF] Hwu | The Superblock: An Effective Technique for VLIW and Superscalar Compilation[END_REF][START_REF] Lee | Software pipelining and superblock scheduling: compilation techniques for VLIW machines[END_REF]]. The semantics of the scheduled superblock must preserve the observable outputs on live registers of the nontrapping executions of the original superblock. Undefined behaviors (e.g., traps such as division by zero or incorrect memory accesses) may be preserved or replaced by defined behaviors. For example, the scheduler may move instructions across some internal conditional branches as long as this is not observable by other superblocks; it may also introduce fresh registers (e.g., local renamings), or replace some instructions by equivalent combinations. Section 3 recalls the specificities of superblock (vs basic-block) scheduling.

In addition, we provide a certified checker for path duplications, which we use to prove tail duplication and loop unrolling optimizations. These optimizations increase scheduling opportunities (at the price of code size increase). Our checker of path duplications illustrates the interest of translation validation designs: a simple formally verified checker enables to certify the correctness of an important class of transformations, modulo small hints provided by oracles. This checker and the heuristics and methods for selecting relevant superblocks are explained in Section 4.

Next, Section 5 summarizes the several preprocessing transformations that are applied on selected superblocks to increase scheduling opportunities. As our prepass scheduling operates on RTL, the pass is technically available for every architecture. However, the scheduling process itself is only useful on in-order cores and needs to be parametrized by a description of the micro-architecture. Thus, our scheduling oracle is decomposed into a front-end that is specific to the architecture, and a generic backend (similarly to [START_REF] Six | Certified and efficient instruction scheduling: application to interlocked VLIW processors[END_REF]). Our verifier is completely generic, but parametrized by rules specific to the target backend. This allows validating some target-specific rewritings in the scheduler's front-end (e.g., the RISC-V expansion of Section 5.2). Hence, similar rewritings could be easily set up for another target.

Section 6 details the implementation of our prepass scheduler's backend. Finally, Section 7 describes how we formally verify both instruction schedulings and rewritings, with a single simulation checker. Because our checker is significantly more powerful than the one of [START_REF] Six | Certified and efficient instruction scheduling: application to interlocked VLIW processors[END_REF] (support of superblocks, rewritings during symbolic execution, simulation modulo register liveness), it is an important step forward for certifying compilers from symbolic executions. Lastly, Section 8 provides a thorough experimental evaluation of our optimizations, and Section 9 concludes with related works.

Six's PhD [START_REF] Six | Optimized and formally-verified compilation for a VLIW processor[END_REF]] details more in depth many parts of this paper. We use "CompCert" to denote official releases, and CompCertSched for our version of CompCert with scheduling. Our source code is available on our gitlab server, in the CPP22_main branch (a release consistent with this paper): gricad-gitlab.univ-grenoble-alpes.fr/certicompil/compcert-kvx/-/tree/CPP22_main 2 Postpass Scheduler for AArch64 [START_REF] Six | Certified and efficient instruction scheduling: application to interlocked VLIW processors[END_REF] created CompCertSched, a postpass (post register allocation) scheduler and peephole optimizer for Comp-Cert, operating on basic blocks (one entry point, one exit point) in KVX assembly code. First, their peephole optimizer rewrites the assembly code to merge loads (resp., stores) to consecutive locations into double or quadruple loads (resp., stores). Then, a dependency analysis is performed and a scheduler, chosen by a command-line option among several available ones, computes a reordering of instructions. Lastly, the previous transformations being performed by untrusted oracles, the final transformed code is validated against the original one by a certified checker. This checker performs a symbolic execution of both codes, that computes the final contents of registers and of the memory as symbolic expressions over their initial contents. The two codes are considered equivalent if these expressions are structurally equal. For compilation efficiency, structural equivalence of expressions is reduced to pointer equality through hash-consing (i.e. memoizing expressions such that two structurally equal expressions are uniquely allocated in each compiler run). 4Since certain processor operations may trap (e.g., reading from invalid memory locations), the symbolic execution engine also checks that the set of possibly invalid expressions of the original code includes that of the transformed code.

Example 2.1 (Simulation on symbolic states). Consider two basic blocks 𝐵 1 and 𝐵 2 :

(𝐵 1 ) 𝑟 1 𝑟 1 + 𝑟 2 ; 𝑟 3 load[𝑚, 𝑟 1 ]; 𝑟 3 𝑟 1 ; 𝑟 1 𝑟 1 + 𝑟 3 (𝐵 2 ) 𝑟 3 𝑟 1 + 𝑟 2 ; 𝑟 1 𝑟 3 + 𝑟 3
Both 𝐵 1 and 𝐵 2 lead to the same parallel assignment:

𝑟 1 (𝑟 1 + 𝑟 2 ) + (𝑟 1 + 𝑟 2 ) ∥ 𝑟 3 𝑟 1 + 𝑟 2 . But, 𝐵 1 is preconditioned by "load[𝑚, 𝑟 1 +𝑟 2 ]
has not trapped", whereas the precondition of 𝐵 2 is trivially true. Hence, 𝐵 2 simulates 𝐵 1 , but the converse is false. [START_REF] Six | Certified and efficient instruction scheduling: application to interlocked VLIW processors[END_REF] encodes such a precondition as a list of potentially trapping terms, hence relaxing the implication of preconditions as a list inclusion. ical (or pointer) equality, bound to the OCaml == operator, that compares these expressions by their allocation address in the compiler run; second, the structural one, corresponding to the OCaml = operator and the Coq definitional equality, that recursively compares their abstract syntax. CompCert provides a backend for the AArch64 architecture (non-VLIW processors) and thus provides us the "Machto-Asm" pass of Figure 2. We have replaced this pass by the "Mach-to-Asm" passes resulting from the composition of the "Mach-to-Machblock" of [START_REF] Six | Certified and efficient instruction scheduling: application to interlocked VLIW processors[END_REF] with the passes of "Machblock-to-Asm" of Figure 3. The overall implementation of our formally verified postpass scheduler on AArch64 represents a bit more than three person•months of development. This port for a single architecture represents about 7000 LOC of Coq, with many bureaucratic proofs.

In contrast to the peephole optimizer of [START_REF] Six | Certified and efficient instruction scheduling: application to interlocked VLIW processors[END_REF]], ours, also applied in the scheduler's front-end, can merge non-consecutive loads or stores within the original basic block, as long as they respect the semantic dependencies and offset constraints on double load/store specific to the AArch64 ISA. Figure 4 illustrates four situations found by our peephole, now described from top to bottom. (i) Backward load pairing, with increasing offset (the offset of the second load is greater than that of the first one): the pairing must happen backward because, we need to preserve the write into w4 on line 1, before its read on line 2. (ii) Forward load pairing, with increasing offset: the pairing must happen forward because, we need to preserve the read into w7 before its write. (iii) Consecutive load pairing, with decreasing offset (the offset of the second load is lower than that of the first one). (iv) Forward store pairing, with increasing offset.

Like [START_REF] Six | Certified and efficient instruction scheduling: application to interlocked VLIW processors[END_REF], our formally verified simulation test validates these rewritings by performing the reverse rewriting (i.e. from double loads/stores to pairs of simple loads/stores) in the Asmblock-to-AbstractBasicBlock pass (see Fig. 3). Currently, the main benefit of our peephole optimizations for AArch64 is code size reduction: it reduces the number of generated memory transfer instructions by about 10%, approximately 3% of the total code length (on average across all our benchmarks). This optimization opens the door for future similar replacements: e.g., selection of ands or the bics instructions 5 .

Our experimental evaluation (see Sect. 8) shows that prepass and postpass schedulings of CompCertSched are complementary, both on KVX and on AArch64.

Superblock vs Basic-Block Scheduling

A major improvement of our prepass scheduling over the basic-block scheduling of [START_REF] Six | Certified and efficient instruction scheduling: application to interlocked VLIW processors[END_REF] is that it operates on superblocks (one entry point, possibly several exit points).

The scheduled superblock must simulate the original superblock. We check this simulation property with a formally proved simulation test summarized in Section 7. Similar to the postpass verifier of [START_REF] Six | Certified and efficient instruction scheduling: application to interlocked VLIW processors[END_REF], this test is based on symbolic execution with formally verified hash-consing. Additionally, our symbolic execution normalizes symbolic values in order to validate some rewritings of instructions applied in the scheduler's front-end. And, the simulation between superblocks is proved modulo register liveness: instead of comparing the symbolic values of all assigned registers, we only compare, for a given exit, those which are live at this exit (i.e. only those read by any execution starting at this exit). Simulation modulo liveness is both more expressive (since assignments of non-live registers are ignored) and more efficient (since we only compare a small subset of assigned registers).

Prior to scheduling, a preliminary phase selects a superblock structure for each function [START_REF] Hwu | The Superblock: An Effective Technique for VLIW and Superscalar Compilation[END_REF][START_REF] Lee | Software pipelining and superblock scheduling: compilation techniques for VLIW machines[END_REF]]. Here, many choices are possible as there are several possible partitions of a given function into superblocks: in particular, on each conditional branch, we may choose to extend the current superblock to one of the successors, or to end it when there is no clearly better choice. Moreover, during the selection of superblocks, we may duplicate some instructions (tail duplication, several variations of loop unrolling) in order to create new opportunities of superblock partitioning with larger superblocks at the end.

This selection pass has a deep impact on the overall performance, since intra-superblock scheduling amounts to optimizing some execution path at the expense of other execution paths. For example, moving the lws instruction above the loop exit toward label .L101 in Figure 8 eliminates a stall at each loop iteration, but slows down the path toward .L101. Currently, our superblocks are selected to be the "most likely path" inside the code, and instruction duplications are controlled through compiler options. This is detailed in Section 4.

5 Specific versions of the corresponding arithmetic instructions update the condition flags while writing the result. We describe here how we transform each function into a carefully chosen partition of superblocks. The first step to form superblocks is to identify "CFG paths"-called traces6 by [START_REF] Fisher | Trace scheduling: A technique for global microcode compaction[END_REF]-likely to be executed. Depending on the accuracy of this static branch prediction, our optimizations may result in a performance gain or loss.

Then, based on this prediction, we may duplicate some paths of the CFG in order to increase the size of superblocks, and thus the scope of our superblock scheduling. Finally, the selection of our superblocks for scheduling combines branch predictions (presented in Sections 4.1 and 4.2) and these path duplications (see Sect. 4.3).

Principles of our Static Branch Prediction

We optionally attach one Boolean prediction per conditional branch: if present it indicates the truth value for the condition that we consider the most likely, and thus the next step in the superblock; if absent, it indicates no prediction at this branch, and thus the end of the superblock.

4.1.1 Detecting Innermost Loops. Fig. 5 depicts a program consisting of two nested loops. The innermost, starting at test "D?", is the one of interest: this is usually where most of the computation time lies. Ideally, our static branch prediction should favor the path staying within the innermost loops, instead of the one going out: "F?" should be predicted as branching on "G", in order to enable loop unrolling, which builds a big superblock by duplication of this loop body.

However, there are other examples where both successors of a given test remain within the loop. In such a case, without additional profiling information, we end the superblock at that test. A wrongly predicted branch can be harmful to overall performance. In contrast, an unpredicted branch that could have been predicted will just result in a missed opportunity for optimization: it will not decrease performance compared to the original code.

Acquiring Prediction Information

Prediction information can be acquired by user annotations, profiling (Sect. 4.2.1) or by static analysis (Sect. 4.2.2). Annotations use __builtin_expect, as in GCC and LLVM. Profiling consists in instrumenting the code to record execution statistics into a file. Then, that file is used on subsequent compilations to guide branch prediction. Absent annotations and profiling information, we exploit certain patterns in the program in order to guess the most likely direction of many branches. In particular, innermost loops as well as their exit branches are detected by static prediction.

Prediction by

Profiling. We developed a profiling system in CompCertSched. Classically, our profiling system is used in two steps. First, the program is compiled with special instrumentation: (i) counters are inserted into each object file as local data blocks; the link between the counter and the instruction in the program is given by a hash code depending on the function being compiled and the location within the function, so that counters can be retrieved during recompilation; (ii) right after each branch, a special Com-pCert builtin is inserted, which increments the appropriate counter; (iii) at program exit, counters are written to a file, through special linker sections added to each compiled object file. The program is then run on representative input, and branch counts are accumulated in a log file.

After profiling information has been recorded, the software is recompiled. The compiler loads the logging file and the profiler-based heuristic consists in assigning the prediction to the branch more taken if the relative difference between the two branches counts exceeds a given threshold. 7 4.2.2 Prediction by Heuristics. When no profiling is available, our heuristics-mostly inspired by [START_REF] Ball | Branch prediction for free[END_REF]-perform an educated guess of the privileged direction. Heuristics are run sequentially, until one of them decides a prediction, otherwise preserving the default "None" prediction. (i) In a conditional branch, a comparison such as (𝑥 < 0)? is likely to be an error-code check, so we predict that the check succeeds (that is, the condition is not taken). Similarly, float equality checks are predicted to be false. (ii) If a given branch leads to a return, then that branch is unlikely to be taken. (iii) If a branch leads away from a loop (the destination is not in the loop body) while the other stays in the loop, we predict the looping branch. This heuristic is very important for later identifying the superblock following that innermost loop. (iv) Finally, if one branch leads to a call instruction and the other does not, privilege the latter. Experimentally, these heuristics seem to detect most branches of interest, though there are a few slightly disappointing corner cases, in particular for heuristic (i) on conditions.

Path Duplication and Selection from Predictions

After branch prediction, we apply path duplications while selecting superblocks: (i) tail duplication consists in duplicating a path after a join point (i.e. a new superblock entry), 7 Right now, the threshold is 1: if the execution count of the "if" branch is strictly greater than that of the "else" branch, then the "if" branch is privileged. It would be interesting in the future to change it to a relative threshold instead (e.g., privileging a branch if at least 70% of the executions pass through it).

in order to move that join point further and hence, extends the superblock ending on this join point (see Fig. 6); (ii) loop body unrolling consists in unrolling a whole innermost loop in order to make its unrolled loop body a big superblock, and thus enable scheduling across the original loop iterations; (iii) first iteration peeling, essentially consisting in replacing while(e) {b} by if (e) {b; while(e) {b}}; (iv) loop rotation consists in turning "while-do" loops into "if-do-while", by duplicating the exit-condition and its context: this enables scheduling the context of the exit-condition within the loop body and removes a "goto" from the loop.

In addition to these selections with duplications, path selection is performed in two other passes of the compiler: (i) for superblock scheduling, the pass "RTL-to-RTLpath" of Fig. 11 involves a superblock selection, which partitions each function into superblocks; (ii) the linearization pass, "LTL-to-Linear" in Fig. 2, also partitions functions into superblocks: it lays out basic blocks that are likely to flow from one to the next in consecutive memory locations, which typically benefits code fetch in processors.

Among these path selection phases, tail duplication is the most complex, and the one that ends up defining which parts of the code will be optimized. We mostly use the algorithm from [START_REF] Chang | Trace Selection for Compiling Large C Application Programs to Microcode[END_REF], which consists in selecting a node that has the largest execution count, then growing a path forward (by going through the "best successors" in regard to execution count), and then growing it backward (through the "best predecessors"). Then, the path stops, and the next unvisited node is selected to grow a new path. Here are key differences between our implementation and their algorithm. (i) They have access to precise execution counts for each node. We do not. We follow instead the branch prediction information, stopping the path when that information is None. (ii) Their algorithm was not designed for superblocks: it allows node sharing between paths. In contrast, we enforce paths without intersection, by ending paths before such node sharing.

Formally Verified Checker of Path Duplications

All the duplications of Sect.4.3 are path duplications: they duplicate paths in the CFG, while preserving syntactically the CFG structure modulo renaming of nodes. In our compiler, these duplications are perfomed by dedicated untrusted oracles followed by a common certified checker. The latter can check in a single run any combination of these transformations. Moreover, it is both simple and small (only 650 lines of Coq, including its correctness proof).

Each oracle is expected to return: (i) the resulting CFG; (ii) the new entrypoint in this new CFG; (iii) a mapping from nodes of the new CFG to nodes of the original CFG, that we call the duplicate mapping, noted 𝜙 in Fig. 6. Fig. 6 illustrates path duplication: the original is on the left; the transformed code is on the right; and the duplicate mapping 𝜙, in red, indicates which node originated where. A new node 4, named 4 ′ , is introduced: it is a duplicate of node 4, denoted (4 ′ ↦ → 4) ∈ 𝜙. Node 3 is then modified so that its successor becomes 4 ′ . Thanks to the duplicate mapping 𝜙, it is very simple to check that any execution step of the function 𝑓 1 associated to the original CFG is simulated by the new function 𝑓 2 , for a lockstep simulation (Fig. 7). Informally, 𝑆 1 ∼ 𝑆 2 means that the current program counters 𝑛 1 of state 𝑆 1 in 𝑓 1 and 𝑛 2 of state 𝑆 2 in 𝑓 2 satisfy (𝑛 2 ↦ → 𝑛 1 ) ∈ 𝜙 (and that return addresses of the respective stacks also match for duplicate mappings of caller functions).

𝑆 1 𝑆 2 𝑆 ′ 1 𝑆 ′ 2 ∼ 𝑡 𝑡 ∼ Figure 7. Lockstep First, our checker verifies that the entrypoint 𝑒 2 of 𝑓 2 maps the entrypoint 𝑒 1 of 𝑓 1 through 𝜙, ie (𝑒 2 ↦ → 𝑒 1 ) ∈ 𝜙.
Then, for any pair (𝑛 2 ↦ → 𝑛 1 ) in 𝜙, we check that, if 𝑛 1 is a node in 𝑓 1 's CFG, then 𝑛 2 is also a node in 𝑓 2 's CFG such that: (i) the instruction at node 𝑛 1 in 𝑓 1 's CFG syntactically matches the instruction at node 𝑛 2 in 𝑓 2 's CFG (e.g., if the instruction at 𝑛 1 performs assignment "𝑟 ′ 𝑟 1 +𝑟 2 ", then the instruction at 𝑛 2 performs exactly the same assignment); (ii) 𝑛 1 (in 𝑓 1 's CFG) and 𝑛 2 (in 𝑓 2 's CFG) have the same number of successors; (iii) for any

𝑖-th successor 𝑛 ′ 1 of 𝑛 1 (in 𝑓 1 's CFG), the 𝑖-th successor 𝑛 ′ 2 of 𝑛 2 (in 𝑓 2 's CFG) must satisfy (𝑛 ′ 2 ↦ → 𝑛 ′ 1 ) ∈ 𝜙.
Hence, any step from 𝑛 1 can be simulated by a step from 𝑛 2 while preserving the simulation relation ∼ of Fig. 7.

This checker also accepts oracles that prune unreachable parts of the CFG (from 𝑒 1 ), as long as these pruned nodes do not appear in 𝜙, and oracles that negate conditions of conditional branches: in this case, the two successors must also be exchanged. This is useful on architectures such as the KVX where branching costs more than not branching.

Finally, the same checker could also be applied to check code factorizations, because intuitively, it ensures a bisimulation. However, we have not yet formally proved the reverse simulation, nor yet designed a pass leveraging this feature.

Rewriting for Better Scheduling

In order to remove some semantic constraints on instruction reorderings, our scheduler's front-end sometimes rewrites instructions into other instructions, which possibly introduces "fresh" registers. The verifier (detailed in Sect. 7) thus checks the simulation by normalizing symbolic expressions and by reasoning modulo register liveness.

KVX Speculative Loads

In addition to normal load instructions that trap (usually aborting the program) if an unmapped address is accessed, the Kalray KVX provides special load instructions known as "speculative", "dismissible" or "non-trapping", which instead return a default value. In our semantics, these loads return the "undefined" (Vundef) value when accessing an incorrect location.8 Speculative loads can be freely moved before a conditional branch, whereas a normal load cannot unless one can prove that it cannot trap; they are thus very interesting for superblock scheduling.

It would be correct to compile C programs entirely using speculative loads: access to incorrect addresses is undefined behavior, and returning a default value is a legal way of implementing undefined behavior. Yet, this would hinder debugging and detection of abnormal behavior. We opted to generate speculative loads only as needed by the schedule.

Consider for instance the superblock starting at label .L100 of Figure 8: it is the body of a loop exiting on label .L101 that computes in $r0 the sum of the $r1 integer array for index variable $r4 (bounded by $r2). On the left, the superblock has been scheduled and bundled with the postpass scheduler of [START_REF] Six | Certified and efficient instruction scheduling: application to interlocked VLIW processors[END_REF]. On the right, our prepass scheduler has moved sxwd (originally on line 6) and lws.xs (originally on line 9) above the conditional exit originally on line 4. The effect of these moves is to gain one bundle and to remove one pipeline stall on the update of $r0. 9 The gain is of 2𝑛 -1 cycles where 𝑛 is the number of loop iterations (there is a 1 cycle loss if there is no iteration, because the two moved instructions have been executed while being useless; sxwd has been executed in parallel of compw.ge, thus its useless execution does not lose a cycle). For this simple loop, this is a gain of almost 25%.

Note that, for [START_REF] Six | Certified and efficient instruction scheduling: application to interlocked VLIW processors[END_REF], these moves were impossible because the original superblock is made of two basic blocks, the first one ended on the conditional exit of line 4. In order to prove that the second superblock simulates the first one, we need to check that the assignment of $r5 and $r3 involved in these moved instructions have no effect on the code after the loop exit (at label .L101). Fortunately, they are not in the live registers of .L101 (they are "local" to the loop body). Moreover, we need to check that these moved instructions do not introduce any undefined behavior should label .L101 be taken. This is the case, because the scheduler's front-end an arbitrary value if that memory location is accessible to the CPU, regardless of what was in that location. This is a valid refinement of "undefined". 9 Only one stall remains in the improved scheduling, because loads have a latency of 3 cycles on the KVX. But, they are only selected on KVX (i.e. except for KVX, the compiler will fail to produce assembly code, if an intermediate pass selects them).

Expanding Operations on RISC-V

Figure 9 presents a fragment of C code and the resulting RISC-V superblock, both for CompCert and for CompCert-Sched. Registers x10, x11 and x12 respectively correspond to variables x, y and t of the input program. CompCert does not attempt to minimize pipeline stalls: on line 1, the lw instruction dereferencing x12 in x7 may induce pipeline stalls at line 3, where x7 is added to x10, with the result written to x6. Moreover, CompCert expands the comparison with immediate only in the "Mach-to-Asm" pass (Figure 2): the immediate (here 7) is stored in the scratch register x31 (in RISC-V, x0 is a read-only register equal to 0). Additionally, CompCert does not attempt to remember that from line 4, register x31 has value 7: thus it reloads 7 in x31 a second time on line 6.

On RISC-V, our prepass scheduler's front-end performs an expansion of comparisons with immediate (branching or not), and of some other instructions (arithmetic operations on immediates, casts, loads of constants, and length conversions). Intermediate values generated by expansions are stored into fresh pseudo-registers (before register allocation), and the untrusted preprocessor uses a dynamic value numbering system to avoid redundant instructions (a Common-Subexpression Elimination limited to the superblock, operating on every instruction in the path). Fortunately, in Figure 9, the fresh pseudo-register assigned to immediate 7, has been allocated (after the prepass scheduling) into x12 (register reuse). In the general case, because the scope of our preprocessing is limited to a superblock, this memoization of immediates should only have a limited impact on register pressure. Performing these expansions within the scheduler's frontend increases scheduling opportunities. Here, the assignment of x12 to 7 is interleaved by the scheduler between the load of 0(x12) into x7, and the addition of x7 to x10: this potentially saves one cycle.

Our formally verified simulation test must check that the expansions performed by the untrusted scheduling preprocessor simulate the original RTL superblock. This is achieved by applying rewriting rules mimicking those of the preprocessor within the symbolic execution and formally proving that these rewritings preserve the semantics of symbolic values. It would be difficult to directly prove the memoization mechanism within the preprocessor, whereas it is proved "for free" by our simulation test with symbolic execution. Even without memoization, verifying these rewriting rules on symbolic values is much easier than verifying them directly on the RTL code. Indeed, symbolic values are directly expression trees, whereas the RTL code is a CFG of register assignments. In particular, the rewriting rules on symbolic values do not involve registers (and substitution of registers). For example, let us consider the following rewriting on RTL conditional branch instructions (written in pseudocode):

𝐿 1 : if (GEs 7) [𝑟 1 ] goto 𝐿 2 else goto 𝐿 3 → 𝐿 1 : 𝑟 2 (ADDiwx0 7); goto 𝐿 4 𝐿 4 : if GE[𝑟 1 , 𝑟 2 ] goto 𝐿 2 else goto 𝐿 3
where 𝑟 2 is a fresh pseudo-register and 𝐿 4 is a fresh node. This rewriting is simply expressed in the symbolic representation by the rule

(GEs 7) [𝑣] → GE[𝑣, ( ADDiwx0 7)
] where 𝑣 is the symbolic value of 𝑟 1 .

Moreover, verifying that rewritings of the untrusted preprocessor correctly deal with "fresh" registers is just a particular case of the simulation test modulo liveness: the expansion on the right-hand side of Figure 9 is correct because x12 is not live at label .L10. Hence, embedding the rewriting rules within the symbolic execution allows the proof of these rewrite rules to ignore liveness issues. In contrast, expressed in a preprocessing of the simulation test (like in the postpass of [START_REF] Six | Certified and efficient instruction scheduling: application to interlocked VLIW processors[END_REF]), rewriting rules would be required to satisfy a bisimulation modulo register liveness.

Register Renaming

Register allocation may introduce a lot of name dependencies (e.g., write-after-write and write-after-read) by reusing the same register for previously independent pseudo-registers. This may reduce the number of possible schedules. On the contrary, before register allocation name dependencies are rare because "fresh" registers can be generated at any time. This is a big advantage of pre-over postpass scheduling.

However, the path duplications of Section 4.4 may induce name dependencies. In particular, as illustrated on the lefthand side of Fig. 10, loop unrolling produces two almost exact copies of the loop body (shown here in assembly instead of RTL), thus leading to name dependencies between instructions of the original and duplicated loop body. These name dependencies are due to the reuse of register names (e.g., d1 and d2 in Fig. 10) and can be removed by renamings with "fresh" names (resp. d4 and d3). We implemented an oracle providing such renamings, and we check the correctness of its results with our certified simulation test modulo liveness over superblocks. Therefore, renamed registers must either not be visible outside the superblock (this is the case in Fig. 10), or else the expected data flow be restored by assigning the correct value to the expected name before exits, at the price of extra-moves.

The result is a superblock-local register renaming pass, which allows for greater scheduling flexibility within the superblock while preserving the expected data flow with respect to the successor superblocks. Note that CompCert's register allocator [START_REF] Rideau | Validating register allocation and spilling[END_REF], with coalescing and live-range splitting, eliminates most of the extra-moves created by renaming.

If-Lifting: Moving Up Side Exits in Superblocks

For architectures such as AArch64 which do not provide speculative loads, load instructions cannot move above side-exits without adding a potential trap (which is incorrect). Even after the register renaming on the left-hand side of Fig. 10, this "trap-after-exit" dependency between lines 9 and 7 prevents the desired interleaving of the two occurrences of the initial loop body. A workaround (Fig. 10, right) is to "lift" the side-exit of line 7 above the two arithmetic operations of lines 5 and 6. Interleaving these operations with those of the second body is now possible. On ARM Cortex A53 (dual issue, where each of these operations takes 6 cycles), this reduces the initial makespan from 25 to 21 cycles (a gain of 16%). The price to pay is the compensation code at the "fresh" label .L102 which duplicates these two arithmetic operations for when the side-exit is taken. The correctness of this transformation is verified by combining existing verifiers of CompCertSched (modulo minor extensions). 10 See [Justus Fasse 2021] for details.

Oracle of the Superblock Scheduler

After superblock selection, each superblock is scheduled separately. Our superblock scheduling oracle, after preprocessing the superblock according to Section 5, schedules the transformed superblock by extending the principles of [START_REF] Six | Certified and efficient instruction scheduling: application to interlocked VLIW processors[END_REF] for basic block scheduling. The scheduling problem of a given superblock is expressed through a system of constraints, where each instruction 𝑗, including exit branches, is associated to a time-slot 𝑡 ( 𝑗) expressing the number of clock cycles at which it is estimated that this instruction is executed. Constraints on 𝑡 ( 𝑗) are of two kinds: resource constraints (i.e. feasible allocations of pipeline units) and latency constraints (i.e. semantic and time dependencies between instructions). In order to find schedules that preserve the semantics in presence of side-exits, we need to extend the latency constraints of [START_REF] Six | Certified and efficient instruction scheduling: application to interlocked VLIW processors[END_REF], with latency constraints specific to branching instructions: (i) we represent live variables at side exits, by extra reads of the branch instruction; (ii) we forbid trapping instructions to move above side-exit, by making each trapping instruction 10 However, it is currently implemented through an intricate combination of passes: it is thus not yet integrated in our mainline CompCertSched. Its code is in the CPP22_if_lifting branch gricad-gitlab.univ-grenoble-alpes.fr/certicompil/compcert-kvx/-/tree/CPP22_if_lifting depend on the preceding side-exit with a latency of 1 cycle; (iii) similarly, we forbid side-exits to be reordered, through a latency of 1 between successive side-exits.

Compared to postpass scheduling [START_REF] Six | Certified and efficient instruction scheduling: application to interlocked VLIW processors[END_REF], our prepass scheduler reasons at a higher level of abstraction: not only do we have an unbounded amount of registers, but also certain pseudo-instructions have not yet been expanded into sequences of elementary assembly instructions. We, however, still have to assign latencies and resource usage to instructions. On the Kalray KVX, we generate the assembly instruction sequence, and then call the functions of the postpass scheduler that give latency and resource usage. On AArch64 and RISC-V, for a limited number of cores (Cortex-A53, Cortex-A35; Rocket, SweRV EH1, SiFive U74), we implemented these functions directly, with numbers from the available documentation or from relevant scheduling parameters in the LLVM compiler.

One difficulty is that the format of latency and resource constraints, originally from [START_REF] Six | Certified and efficient instruction scheduling: application to interlocked VLIW processors[END_REF], was designed for fully pipelined processors: processors in which there are resource constraints on which instructions can be issued at the same clock cycle, but no constraints across different clock cycles. That is, on a fully pipelined processor, such as the KVX, if a multiplication was issued at a cycle 𝑡, then it does not prevent another multiplication from being issued at cycle 𝑡 + 1. In many processors, some units, especially dividers, are not pipelined: an instruction entering the unit monopolizes it until completion. A general solution would be to introduce multiple-cycle resource reservations. We are waiting to have more core descriptions to introduce a more general format (with added functionality, such as operand reads at different cycles). Meanwhile, we handle this by adding a constraint 𝑡 ( 𝑗 ′ ) -𝑡 ( 𝑗) ≥ 𝛿 when 𝑗 and 𝑗 ′ are two successive uses of the same non-pipelined unit, where 𝛿 is an estimated number of cycles of use. 11 A drawback is that this does not allow reordering operations using the same non-pipelined unit with respect to one another.

Postpass optimization within a basic block [START_REF] Six | Certified and efficient instruction scheduling: application to interlocked VLIW processors[END_REF]] has a single objective, reducing the makespan: the time when the last value produced by the basic block is available. In contrast, superblock prepass optimization has multiple, conflicting objectives: (i) reducing the makespan (with respect to the final exit); (ii) reducing register pressure (the number of physical registers needed), or, as a proxy, the live ranges of values; (iii) pushing side-exits as early as possible.

For solving the constraint system, we reuse two algorithms of [START_REF] Six | Certified and efficient instruction scheduling: application to interlocked VLIW processors[END_REF]]. (i) Forward list scheduling: time slots are greedily filled by increasing time (clock cycle), adding instructions to each slot as long as they respect the resource and latency constraints, with a priority for instructions that start the longest path in the latency graph. Forward scheduling tends to place exit points as soon as possible, but may 11 The cycle count for division often depends on the quotient bit-length.

increase the live ranges of variables. (ii) Backward list scheduling: time slots are greedily filled by decreasing time, with a priority for instructions that end the longest path in the latency graph.

A difficulty not present in postpass scheduling is that scheduling some instructions early, whereas their result is not used soon, increases the number of live pseudo-registers; the risk is that a superblock that originally used less pseudoregisters than the number of physical registers in the processor could, after scheduling, use more, resulting in costly spill code (loads and stores to stack slots) being inserted by the register allocation pass. The risk of exceedingly early scheduling is higher with the forward list scheduler than with the backward scheduler, thus we originally favored the latter for prepass scheduling. In addition, we introduced: (iii) Zigzag scheduling: forward scheduling is used to place exit points, and then backward scheduling places other instructions. (iv) Register-pressure-aware scheduling: the forward list scheduler is made aware, at each allocation step, of the number of live pseudo-registers in each register class (e.g., integer vs floating-point registers). When this number becomes close (e.g., the difference is less than three) to the number of physical registers in the processor, the strategy is modified: the scheduler favors instructions which decrease the number of live registers in that class, and chooses the one which decreases it the most. If no instruction decreases register pressure, we favor instructions which do not increase the number of live registers of the given class, with long paths to the exit in the latency graph. Finally, if all possible instructions increase the number of live registers, we wait for an instruction that does not, and if none becomes available after 5 cycles, we schedule the next instruction with the normal list scheduling strategy (priority for instructions that finish the longest path in the latency graph). When the number of live registers drops below the threshold, the normal list scheduling strategy applies again. See [START_REF] Nardino | Register-Pressure-Aware Prepass-Scheduling for Com-pCert[END_REF] for details.

Formally Verified Superblock Scheduler

We now describe how our superblock scheduler is formally verified. For the sake of concision, this description remains informal, and in particular, without Coq definition. Full details are given in [Six 2021, Chap. 5&7] and in our Coq code (see the URL given on page 3).

Figure 11 sketches the design of our formally verified RTL superblock scheduler. RTLpath is a new IR which annotates RTL programs with information about superblocks: entrypoints, exit-points and register liveness. It also represents the execution of a whole superblock in a single step.

Hence, our formally verified superblock scheduler requires that its input RTL program has been previously rewritten, as described in Section 4, in order to exhibit "relevant" superblocks in each function. Then, the untrusted scheduler

𝑆 1 𝑆 2 𝑆 ′ 1 ∼ 𝜖 ∼ RTL RTLpath 𝑆 1 𝑆 2 𝑆 ′ 1 𝑆 ′ 2 ∼ 𝑡 𝑡 ∼ 𝑆 ′ 1 in the path & |𝑆 ′ 1 | < |𝑆 1 | 𝑆 ′ 1 out of the path

Definition of the RTLpath IR

RTLpath extends the RTL CFG of instructions, with a super CFG-structure of paths, where such a path represents a superblock. But, for the formal proofs, the path-structure does not need to partition the CFG into superblocks: two distinct paths are not required to be disjoint. Our notion of CFG path is more like the usual notion of trace in "trace-scheduling". To each instruction we assign an optional default successor. Instructions with a default successor are either basic instructions, or conditional branches. 12 A CFG path connects a sequence of instructions to their default successors; the final instruction of a path has no default successor. The whole execution of a path of length 𝑝 emits at most one observational event, in the CompCert semantic sense (call to an external function, access to a volatile variable): at its final node (this is important for forward simulation proofs). In fact, all functions calls are restricted to be at the final node. Note that one given CFG path represents several execution paths: the execution may exit early from the CFG path through an intermediate conditional branch.

RTLpath comes with a semantics: one step of RTLpath execution runs all RTL instructions from path entry to path exit. States are the same as for RTL, but store as well that all caller functions are well-formed RTLpath functions.

12 For conditional branches, the default successor is the one that "continues the sequence" (i.e. the "else" branch). Indeed, it has the smallest latency in usual pipelines. It also corresponds to the one predicted in Sect. 4: conditions have been negated if necessary, as explained at the end of Sect. 4.4.

Bisimulation of RTLpath and RTL Executions

RTLpath RTL

𝑆 1 𝑆 2 𝑆 ′ 1 𝑆 ′ 2 ∼ 𝑡 𝑡 + ∼ Figure 13. Back to RTL
With these definitions, the forward simulation of RTLpath by RTL is reduced to a simple "Plus-simulation" (Fig. 13): an RTLpath step runs at least one RTL instruction, but at most 𝑝 + 1 where 𝑝 is the size of the executed path.

The reverse simulation, of RTL by RTLpath, is less trivial. In an RTLpath execution, successive states necessarily correspond to entry paths. In particular, each return address stored in the stack is itself an entry path of the return function (recall that a call instruction must be last in a path, so its return location is at the start of another path). Relation ∼ matching RTL states with RTLpath states encodes these invariants. More generally, 𝑆 1 ∼ 𝑆 2 relates an RTL state 𝑆 1 with an RTLpath state 𝑆 2 that is the entry point of a CFG path containing 𝑆 1 . As pictured in Figure 12, one RTL step is simulated by one RTLpath step on path exits. Otherwise, the RTLpath execution stutters. To prevent silent infinite loops from being simulated by any program, CompCert forward simulations require proving that the number of successive stuttering steps is finite: here, this number is bounded by the size of the current CFG path.

Path-Executions Equivalence Modulo Liveness

Given the original RTL program, the oracle pictured in pass (1) of Figure 11 produces an RTLpath program, annotated with a set of "input" (i.e. live) registers on each path entry. The wellformedness of this RTLpath program is checked by a certified simple forward analysis, that simultaneously checks the correctness of liveness information: the set of input registers given on each path entry must include the sets of registers actually read in all executions starting from this path entry.

For RTLpath programs with correct liveness information, we prove a "lockstep" simulation (see Fig. 7) of RTLpath execution modulo liveness: here, 𝑆 1 ∼ 𝑆 2 means that RTLpath states 𝑆 1 and 𝑆 2 only match on live registers, including those that have been stored in the stack during function calls. Since RTLpath states (like RTL ones) comprise a well-formed list of stack frames modeling the call stack, it is easy to define this simulation relation that both involves registers and memory.

Design of the Certified RTLpath Scheduler

The scheduling oracle takes as input an RTLpath function, computes a schedule for each superblock (each path), and returns a tuple (𝑐, 𝑒, 𝑝𝑚, dm) where 𝑐 is the scheduled RTL CFG, 𝑒 is its main entry-point, 𝑝𝑚 is its associated pathmap, and dm is the reverse mapping from entry paths of the scheduled CFG to the original CFG (like the duplicate mapping 𝜙 in Sect. 4.4). Given an original RTLpath function f1, our Figure 14. Comparing Symbolic States of the KVX Superblocks given in Figure 8. certified pass turns the (𝑐, 𝑒, 𝑝𝑚) returned by the oracle into an RTLpath function f2, after verifying the well-formedness conditions (like in Sect. 7.3). Then, thanks to the dm mapping, it checks that f2 "matches" f1: (i) dm is a mapping from path entries of f2 to path entries of f1; (ii) for each path entry pc2 of f2, given pc1 its matching path entry in f1, the symbolic execution of the f2 path starting at pc2 simulates the symbolic execution of the f1 path starting at pc1 modulo live registers of f1 (with the simulation checker detailed in Sect. 7.5). Formally, the forward simulation proof of our scheduler also corresponds to a lockstep simulation, similar to the one of Sect. 7.3.

Certifying the RTLpath Simulation Test

Fig. 14 illustrates the comparison of symbolic states for validating the transformation of Fig. 8. Each symbolic state is a sequence of conditional exits followed by a final one. The state of memory and registers on each exit is represented by a preconditioned parallel assignment (following the terminology of Example 2.1), where the precondition is a list of possibly trapping expressions, within the "ok" keyword in Fig. 14. Our simulation test checks the implication of preconditions on each exit by testing list inclusion: here, the lists of the right-hand side on both exits are implicitly empty. And the simulation test compares the symbolic values of live registers on each exit: here, only r0 is live at exit .L101, whereas only r0, r1, r2, and r4 are live at exit .L100. 13 Our formal development follows the general lines of that of [START_REF] Six | Certified and efficient instruction scheduling: application to interlocked VLIW processors[END_REF]]: we define an abstract model of symbolic execution, allowing for a definition of a specification for the simulation test in this symbolic semantics, then we refine this model into an efficient implementation that uses their formally verified hash-consing technique, extended with our rewriting engine.

We retain their approach of modeling the impure computations involved in hash consing in a monad of "impure" computations [START_REF] Boulmé | Formally Verified Defensive Programming (efficient Coq-verified computations from untrusted ML oracles[END_REF]]. The core of our simulation test is implemented in this monad and proved correct by a lemma, expressing that when the test normally terminates 13 Superblock of Fig. 8 is a loop of entry .L100 and exit .L101, where r0 is the result of the loop, r4 is the loop counter, and where r1 and r2 are parameters.

then property (ii) of Section 7.4 holds. The primary goal of their refinement technique is to circumscribe the reasoning on impure computations as much as possible.

However, our abstract model of the simulation test is more complex than the one of [START_REF] Six | Certified and efficient instruction scheduling: application to interlocked VLIW processors[END_REF]] on several points. (i) We consider superblocks: the symbolic state thus must represent several execution paths (where [START_REF] Six | Certified and efficient instruction scheduling: application to interlocked VLIW processors[END_REF]] only deal with a single execution path). (ii) Our simulation test compares symbolic states on each path exit modulo liveness. (iii) Our notion of RTL/RTLpath state is richer than their notion of Asm/Asmblock state. Note that, since call instructions are always at the end of a path, return addresses in the call stack must always point to the start of a path. (iv) In Comp-Cert's memory model, a pointer comparison fails when these pointers are allocated in distinct memory blocks. 14 Hence, arithmetic operators that may compare pointers (comparisons of integers of the same size as the pointers) contain a read dependency on memory, which may lead a naive implementation of the simulation test to reject some desirable schedules. The solution of [START_REF] Six | Certified and efficient instruction scheduling: application to interlocked VLIW processors[END_REF] to this technical issue works on the last IR of CompCert (assembly), but not in an intermediate IR such as RTLpath. Alternatively, we solved this issue by proving that the memory within a path execution is only modified by store instructions, which do not change the results of pointer comparisons: thus, all pointer comparisons do not really depend on the current memory, but only on the initial memory of the path execution.

Verified Rewritings during Symbolic Execution

In contrast to rewriting rules of [START_REF] Six | Certified and efficient instruction scheduling: application to interlocked VLIW processors[END_REF], which happens during the "Asmblock-to-AbstractBasicBlock" compilation, ours are directly integrated in the symbolic execution engine. As explained in Section 5.2, our approach gives simpler proofs about these rewriting rules, but makes the symbolic execution implementation a little trickier. In particular, we have to integrate them within the hash-consing mechanism.

Our rewriting rules are always applied at the top of hashconsed terms (like a smart constructor). The rewritten terms 14 Comparison of pointers pointing to different blocks has undefined behavior according to the C standard [ISO 2011, §6.5.8p5].

are then turned into proper hash-consed terms by a dedicated (impure) function that only transforms their top nodes. In other words, the management of hash-consing during rewriting is delegated to this dedicated function: this both simplifies the implementation of rewriting rules and its formal proof.

Formally, a rewriting rule must turn a term 𝑡 1 into a term 𝑡 2 such that for all register and memory states, if evaluation of 𝑡 1 does not fail, then 𝑡 2 evaluates to the same value as 𝑡 1 . This allows us to rewrite 𝑡 1 as 𝑡 2 in parallel assignments but not in preconditions. For example, as illustrated in Fig. 14, rewriting lws.ws operation into lws.s.ws suffices for our certified simulation test to validate the transformation in Fig. 8.

As explained in Section 5.2, on the RISC-V backend, we succeeded to move most of the assembly expansions expressed at the "Mach-to-Asm" pass in CompCert (see Fig. 2) as rewriting rules on RTLpath. This required us to overcome a little issue: while the forward simulation proof of "Machto-Asm" supports that expansions replace the Vundef value by any other value, this is not supported in the proof of our rewriting rules. In CompCert, Vundef represents a potential undefined behavior that has not yet been observed (e.g., read into an uninitialized register): it is a poison value which does not abort computation until it becomes observable. In our case, Vundef may appear when evaluating some RISC-V macro-operations on unexpected immediate arguments (e.g., the shrximm macro-operation used to model division by a power of two, expansed into a sequence of right shifts and additions). The "Mach-to-Asm" expansion typically replaces Vundef by a silent arithmetic overflow.

Our simple workaround is to introduce within rewriting rules some dedicated pseudo-instructions able to generate the necessary Vundef (hence, acting like defensive tests): these extra pseudo-instructions are further removed in the "Machto-Asm" pass. Note that these extra pseudo-instructions do not disturb the scheduling because they are assigned 0 latency and 0 resource.

On complex ISAs, such as AArch64, many expansions of "Mach-to-Asm" pass cannot be expressed at RTL level. This is due to limitations of RTL, which does not support arithmetic instructions modifying several pseudo-registers in parallel, such as instructions with side effects on flags. Even on RISC-V, expansions that involve stack-accessing instructions cannot really be expressed at RTL level, because the layout of stack frames is not yet defined at this level (see Fig. 2): stack accesses are only handled very abstractly.

Experimental Evaluation

Tables 1 to 3 summarize our experiments on several architectures: AArch64 is an ARM Cortex A53 (AArch64) in a Raspberry Pi 3 running Ubuntu 18.04.5 LTS;15 KVX a Kalray KV3 "Coolidge" core; RISC-V a SiFive U74 RISC-V dual-issue, in-order core in a HiFive Unmatched board. In each case, we tie the process to one core of the machine, and measure clock cycles using hardware counters. We run different suites: the benchmarks of [START_REF] Six | Certified and efficient instruction scheduling: application to interlocked VLIW processors[END_REF], the computational oriented Polybench [START_REF] Pouchet | the Polyhedral Benchmark suite[END_REF]], and the embedded systems oriented TACLeBench [START_REF] Falk | TACLeBench: A Benchmark Collection to Support Worst-Case Execution Time Research[END_REF].

First, Table 1 measures the cumulative impact of each gradually introduced optimization compared to CompCert 3.8. 16Note that postpass scheduling and peephole optimizations apply only to AArch64 and KVX, and RTL expansion only applies to RISC-V. The postpass scheduling for KVX is the one of [START_REF] Six | Certified and efficient instruction scheduling: application to interlocked VLIW processors[END_REF]; LICM (Loop Invariant Code Motion) is the one of [START_REF] Monniaux | Simple, light, yet formally verified, global common subexpression elimination and loop-invariant code motion[END_REF]. The Q1, Med and Q3 values respectively denote the first quartile, the median, and the third quartile on the entirety of our benches. Here are a few conclusions. (i) For both the AArch64 and KVX cores, postpass scheduling has a significant impact. For the KVX, this impact is bigger, as expected on a VLIW architecture. (ii) LICM is another meaningful optimization, producing a gain of 20% on some benchmarks. (iii) Prepass scheduling (without any loop unrolling) also helps, increasing by 5-10% for the AArch64 and RISC-V cores. This is mostly due to removing the false dependencies (compared to the postpass scheduling). In contrast, the KVX core, with 64 user registers, is barely affected (in absence of optimizations for building large superblocks such as loop unrolling). Using both prepass and postpass scheduling together on AArch64 is the best setting, mainly because the latter fine-tunes the placement of spills and other instructions that have been expanded between RTL and Asm. (iv) Tail duplication and loop unrolling, combined with prepass scheduling, increase performance by about 5% on KVX. Those are also useful on specific benches thanks to their ability to enlarge the size of superblocks. (v) Loop rotation used alone has a small impact on RISC-V, but the postpass (on AArch64) benefits from it as the rotation may provide more scheduling opportunities. It shines mostly for the KVX architecture, since it results in a more efficient bundling of the loop header in postpass. (vi) RTL expansions (RISC-V only) have no significant impact on average (for all benchmarks) but they can, on some programs, result in a large performance gain when combined with prepass scheduling. We observe an improvement of 4% on the third quartile.

We also compared our best version of CompCertSched to GCC. Table 2 shows the gain (can be negative) of using GCC with the given optimization flag, versus our best version of CompCertSched, for the three suites. We are getting closer to GCC -O2 with our optimizations on AArch64 and KVX, and we are better than GCC -O1 in most cases on KVX. On RISC-V, we still have a margin of progression: we suspect the lack of postpass scheduling and of strength reduction. RISC-V needs several instructions for operations, such as accesses to consecutive indices in an array, feasible in one instruction on KVX or AArch64 and also strength-reducible, thus the lack of strength reduction is more evident on a RISC-V core than on architectures with more powerful individual instructions. More generally, less work went into the RISC-V backend.

Another experiment, in Table 3, shows that the prepass scheduling algorithms of Section 6 produce almost equivalently efficient code. List scheduling seems generally a little better than its variants for KVX, but not for AArch64 and RISC-V where register-pressure-aware and backward (respectively) seems to give better results.

We measured on KVX that branch prediction from profiling information, instead of our static heuristics, gives only negligible benefit (+1% on Q3, 0% on Q1 and Median). To evaluate the impact more finely, we first profiled all our benchmarks, then we modified the compiler code to count the number of times that our heuristics gave a wrong prediction. Out of the 17816 branches that could be profiled, only 5% of them were wrongly predicted, and 14% of them had a pattern not caught by our used heuristics. 17 This gives us confidence in our static branch prediction.

We also measured that the preprocessing pass exploiting non-trapping loads on KVX yields an average gain of about +1.5% on benchmarks where replacements are made. 17 That's only half of the branches encountered: this is because our benchmarks do not have a 100% code coverage, only a part of each benchmark code is actually executed. This score would possibly be higher if followed by an ifconversion pass.

Finally, we have also measured the effect of our experimental "if-lifting" optimization of Section 5.4 (together with register renaming) on AArch64. On most benches, it has little effect with only a few percent of performance gain or loss when added to "Best". Nonetheless, on some, we observe a marked improvement of more than five percent, for a code size increase below 5%. Interestingly, the efficiency gain on TACLeBench's Susan exceeds 30%.

Our verified checkers ensure that if code compiles successfully, then it is compiled correctly. However, there is the possibility that the scheduler, peephole optimizer, expander. . . are incorrect and code is rejected by the checker. We thus test CompCertSched on benchmarks, applications, as well as hundreds of random programs generated by compiler fuzzers, such as CSmith18 [START_REF] Yang | Finding and understanding bugs in C compilers[END_REF]] and Yarp-Gen19 [START_REF] Livinskii | Random testing for C and C++ compilers with YARPGen[END_REF]]. CSmith found one bug in the AArch64 peephole optimizer, which produced an incorrect replacement which was refused by the verified checker; the bug case was reduced using CReduce20 [START_REF] Regehr | Test-case reduction for C compiler bugs[END_REF]] and then fixed.

Related Works and Conclusions

Remarks on heuristics within compilers. We implement a variant of [START_REF] Ball | Branch prediction for free[END_REF]'s static branch predictor, as do GCC (citing [START_REF] Wu | Static branch frequency and program profile analysis[END_REF]) and LLVM [START_REF] Alovisi | Static Branch Prediction through Representation Learning[END_REF]. Profile-guided scheduling, the "ground truth", performs better only on a small minority of examples, thus we do not expect that more advanced static prediction [START_REF] Deitrich | Improving Static Branch Prediction in a Compiler[END_REF]] would improve the situation. From our experiments, nonprediction is preferable to misprediction: this is why we do not use some of Ball and Larus's heuristics. Similarly, we use heuristics to solve the instruction scheduling optimization problems. [START_REF] Six | Certified and efficient instruction scheduling: application to interlocked VLIW processors[END_REF] observed that, for postpass scheduling, their optimal and costly algorithm based on integer linear programming yields a better makespan than heuristics only in a very small fraction of the cases, and the makespan is then only marginally improved. [START_REF] Shobaki | Preallocation Instruction Scheduling with Register Pressure Minimization Using a Combinatorial Optimization Approach[END_REF] propose an optimal scheduling algorithm in the presence of register pressure, with high cost. As they rightly point out, optimality when solving the combinatorial optimization problem does not necessarily translate into optimal runtime behavior, because the latter depends on other compiler phases and microarchitectural aspects that are not reflected in the model in which optimization is performed.

State of the art on unverified compilers. As of version 11.1.0, GCC optionally has postpass superblock scheduling (-fsched2-use-superblocks) and can enlarge superblocks by tail duplications (-ftracer), as CompCertSched. Superblock scheduling was introduced in GCC 3.4 but is still described as "experimental"; it is not active at -O3, one has to pass the specific option. An option for trace scheduling (-fsched2-use-traces) exists but seems to be a dummy (trace scheduling is not in the list of active passes listed by -fverbose-asm); it appears to have been introduced in GCC 3.4 and deactivated later. GCC has an "interblock" prepass scheduler based on region scheduling [START_REF] Gupta | Region Scheduling: An Approach for Detecting and Redistributing Parallelism[END_REF].

As of LLVM version 12.0.0, MachineScheduler and Machine-Pipeliner operate on basic blocks only. Swing modulo scheduling, a software pipelining technique, and an extension to superblocks were implemented for LLVM in 2005 [START_REF] Lattner | An Implementation of Swing Modulo Scheduling with Extensions for Superblocks[END_REF]] but this work was not integrated into official releases. Recently, [START_REF] Rangasamy | Superblock Scheduler for Code-Size Sensitive Applications[END_REF]] proposed a superblock scheduler for LLVM. They neither aim at supporting code motion below side exits with compensation code, nor do they currently take liveness into account in checking if code motion is valid without compensation code.

Trace vs. Superblock scheduling. Trace scheduling, as introduced by [START_REF] Fisher | Trace scheduling: A technique for global microcode compaction[END_REF], is more general than superblock scheduling: it allows for side entrances in addition to side exits. Instruction may then be moved above and below both side entrances and exits. Generating the necessary compensation code, especially when branches are moved across each other, is however complex.

Superblock scheduling [START_REF] Hwu | The Superblock: An Effective Technique for VLIW and Superscalar Compilation[END_REF][START_REF] Lee | Software pipelining and superblock scheduling: compilation techniques for VLIW machines[END_REF]] is presented as a simpler alternative. By disallowing sideentrances, and movements of branches across one another, only the comparatively simple compensation code for moving instructions below side exits (e.g., "if-lifting" of Sect. 5.4) is necessary [START_REF] Gregg | Comparing Tail Duplication with Compensation Code in Single Path Global Instruction Scheduling[END_REF]]. Moreover, the loss of side entrances may be compensated by tail duplication. [START_REF] Gregg | Comparing Tail Duplication with Compensation Code in Single Path Global Instruction Scheduling[END_REF] actually argues that superblock scheduling gives comparable results to full trace scheduling while being much simpler to implement. We add that superblocks, in contrast to general traces, allows for a compositional reasoning on scheduling correctness, which makes formal proofs much easier.

Comparison with verified compilers. [START_REF] Tristan | Formal Verification of Translation Validators: a Case Study on Instruction Scheduling Optimizations[END_REF] certified a simplified postpass trace scheduling within CompCert (at the Mach level): they disallow moves of branches across each other and, because they do not consider register liveness, they systematically duplicate instructions (without register renaming). Moreover, their implementation suffered from exponential complexity [Tristan 2009, §6.7.1][Tristan andLeroy 2008, §7], and was never integrated into official releases of CompCert.

In contrast, our certified superblock scheduling leverages most of the power of superblock scheduling while remaining efficient even for large superblocks. Moreoever, it composes with existing RTL-level optimizations. We thus apply Comp-Cert optimizations such as CSE3,21 constant propagation or deadcode elimination, between our code duplications and the actual scheduling. We intend to extend our approach to certify more complex optimizations.

Apart from CompCert, the only other real-scale verified compiler backend is CakeML, which does not include an instruction scheduler. An alternative is to use a normal compiler and apply post-hoc translation validation. For example, [START_REF] Necula | Translation validation for an optimizing compiler[END_REF] and [START_REF] Tristan | Evaluating value-graph translation validation for LLVM[END_REF] previously established that symbolic simulation is effective to validate state-of-theart compilers. However, it seems difficult to turn their powerful debuggers into formally verified checkers. Alternatively, a translation validation approach by SMT-solving, applied from source to object code without modification to the compiler, was used for the seL4 secure operating system kernel [START_REF] Arthur | Translation validation for a verified OS kernel[END_REF], with the GCC compiler and the ARM architecture, with some restrictions as to the form of the C programs to be compiled and the level of optimization. The fact that this approach was only used for one specific program seems to indicate that there are difficulties in applying it more widely.

Figure 1 .Figure 2 .

 12 Figure1. The KVX backend of[START_REF] Six | Certified and efficient instruction scheduling: application to interlocked VLIW processors[END_REF]

Figure 4 .

 4 Figure 4. Examples of Load/Store Compactions on AArch64

Figure 5 .

 5 Figure 5. Innermost loop within a superblock

Figure 6 .

 6 Figure 6. Example of Path Duplication

Figure 9 .

 9 Figure9. On the left: the RISC-V assembly produced by CompCert (3.8). On the right: the RISC-V assembly produced with our prepass' front-end (one addiw & one potential lw stall have been gained, resulting in a potential gain of two cycles).

Figure 10 .

 10 Figure 10. Interleaving of unrolled loop-bodies on AArch64.

Figure 12 .

 12 Figure 12. RTL to RTLpath

  We have thus slightly extended RTL to support trapping load instructions. Formally, CompCertSched intermediate representations model these instructions for all architectures.

	Formally Verified Superblock Scheduling
		int sum ( int *t , int n ) {
		int s =0; for ( int i =0; i < n ; i ++) s += t [ i ];
		return s;
		}
	Sequence of bundles as	Effect of our prepass
	emitted by Six et al. [2020]	scheduler in between
	(makespan of 8 cycles)	(makespan of 6 cycles)
	1	L100 :	. L100 :
	2	compw . ge $r32 = $r4 , $r2	sxwd $r5 = $r4
	3 ;;	compw . ge $r32 = $r4 , $r2
	4	cb . wnez $r32 ? . L101	;;
	5 ;;	lws.s.xs $r3 = $r5 [ $r1 ]
	6	sxwd $r5 = $r4	;;
	7	addw $r4 = $r4 , 1	cb . wnez $r32 ? . L101
	8 ;;	;; // 1 STALL
	9	lws.xs $r3 = $r5 [ $r1 ]	addw $r0 = $r0 , $r3
	10 ;; // 2 STALLS	addw $r4 = $r4 , 1
	11	addw $r0 = $r0 , $r3	goto . L100
	12	goto . L100

Figure 8. Scheduling and bundling a loop body on the KVX has rewritten the trapping load lws.xs into a non-trapping (speculative) load lws.s.xs.

Thus, Six et al. [2020] distinguishes two notions of equality: first, the phys-

CompCert already defines a trace as a sequence of observational events. Instead, we use "CFG path", where CFG stands for "Control-Flow Graph".

Reading from an incorrect location w.r.t CompCert semantics may return

This dual-issue, in-order core was chosen because it is similar to other in-order ARM cores used in embedded systems; also it is used as little core in "big.LITTLE" settings.

For the KVX target, not available in CompCert, we use the one from[START_REF] Six | Certified and efficient instruction scheduling: application to interlocked VLIW processors[END_REF] without postpass scheduling (nor bundling).

https://github.com/csmith-project/csmith

https://github.com/intel/yarpgen

https://embed.cs.utah.edu/creduce/

CSE3 is a common subexpression elimination that analyzes across branches[START_REF] Monniaux | Simple, light, yet formally verified, global common subexpression elimination and loop-invariant code motion[END_REF]].

Acknowledgments

This work has been partially supported by the LabEx PER-SYVAL-Lab (ANR-11-LABX-0025-01) and the IRT Nanoelec (ANR-10-AIRT-05), funded by the French national program "Investissement d'Avenir".

We also wish to thank Delphine Demange, Benoît Dupont de Dinechin, Frédéric Pétrot, Xavier Leroy, and anonymous referees for their helpful advices.


Rahma Boujelbane
email: rahma.boujelbane@gmail.com

Inès Zribi
email: ineszribi@gmail.com

Syrine Kharroubi
email: syrinekharroubi@gmail.com

Mariem Ellouze
email: mariem.ellouze@planet.tn

An Automatic Process for Tunisian Arabic Orthography Normalization

Keywords: Tunisian Arabic, normalization, CODA

. We show that rule-based and statistical methods can reduce the transcription errors by 77.73% over this baseline on an unseen test set.

Introduction

Arabic dialects or vernaculars are the mother tongues of Arabic speakers. They are the daily languages used in interviews and informal conversations. With the emergence of the Internet and social media, Tunisian Arabic (TA) and other Arabic dialects have become the language of informal online communication such as emails, blogs, discussion forums, SMS, etc. Most Arabic natural language processing tools and resources were developed specially to treat Modern Standard Arabic (MSA).

Corresponding tools processing TA are not as matured and sophisticated as those developed for the MSA. This is due to the recent involvement of works on TA and the limited quantity of corpora necessary for the efficient development of TA processing applications.

In fact, as there is no Automatic Speech Recognition (ASR) system, TA suffers from the lack of written corpus causing a bottleneck mainly for systems based on statistical learning technique.

In this study, we investigate how to remedy this situation and how easy it is to convert automatically spontaneous orthography written with Arabic script into CODA-TA orthography [START_REF] Zribi | A Conventional Orthography for Tunisian Arabic[END_REF]. Our proposed approach is close to the approach proposed by [START_REF] Eskander | Processing Spontaneous Orthography[END_REF]. We built an automatic normalization system of spelled TA using a hybrid method that combines rule-based methods and statistical methods.

This paper is structured as follows. After reviewing relevant linguistic facts for TA in section 2, we review related works in section 3. We present, in section 4, the conventionalized CODA-TA orthography [START_REF] Zribi | A Conventional Orthography for Tunisian Arabic[END_REF] that we use in this paper. We expose, in section 5, the main orthographic errors that often occur in TA. We detail the different steps of our approach in section 6. In section 7, we report our experiments and evaluation. We conclude with a discussion of future work

Linguistic Facts of Tunisian Arabic

Tunisian Arabic is a dialect of the Arabic language spoken in Tunisia. It is an underresourced language. It has neither a standard orthography nor large collections of written texts and dictionaries. Actually, there is no strict separation between MSA (the official language of the government and the education) and TA, which begins to seep progressively and deeply in the Tunisian media and different social networks.

The two languages exist on a continuum dominated by a mixed form. This leads to several word categories in the TA. Indeed, the use of the TA lexicon in conjunction with the MSA lexicon causes several orthographic ambiguities. This duality affects strongly the agglutination phenomenon, which is a characteristic of the Arabic language. As a consequence, new type of words appears to involve ambiguities in their writing. For example, the word 'these pictures' in TA may be written in three different manners: هتصاور htSAwr, التصاور ه h AltSAwr or هالتصاور hAltSAwr. The variations of the orthographic forms are the result of the agglutination of the particle /هh ('this' or 'these') to a noun. We note that the three orthographic forms have the same pronunciation.

Furthermore, TA marks the appearance of the multiple pronunciation phenomenon. Some consonants in a same word may be pronounced differently from a native speaker to another which leads to two different forms. For instance, the word 'there is' has two pronunciations /fama/ or /θama/. So, it can be written as ثمة θamaħ or فمة famaħ.

On the other hand, the Tunisian lexicon is rich with words through lexical borrowing. The intermingling of many civilizations throughout centuries made traces of their languages in the TA. Therefore, one of the most notable differences between the TA and the MSA is the presence of borrowed words from several other languages such as Italian, French, Spanish, Berber and Turkish. Given the absence of orthographic rules and dictionaries, TA borrowed words have multiple variations in their writing. For example, the word 'boat' /ba:bu:r/ in TA may be written in two different ways بابور bAbuwr and ببور babuwr.

Related Works

Several Arabic dialects have been the focus for developing orthographic rules for dialectal Arabic. Indeed, Zawaydeh et al. [START_REF] Zawaydeh | Guidelines for Transcribing Arabic Dialects[END_REF] and Maamouri et al. [START_REF] Maamouri | Dialectal Arabic Telephone Speech Corpus : Principles, Tool design, and Transcription Conventions[END_REF] developed a set of rules for orthographic transcription and annotation of Levantine dialects in order to create a Levantine Arabic corpus. Similarly, Habash et al. [START_REF] Habash | Conventional Orthography for Dialectal Arabic[END_REF] have proposed the convention CODA for transcribing Arabic dialects. This convention has been also proposed to some dialects such as Egyptian Arabic [START_REF] Habash | Conventional Orthography for Dialectal Arabic[END_REF], Tunisian Arabic [START_REF] Zribi | A Conventional Orthography for Tunisian Arabic[END_REF], Palestinian Levantine Arabic [START_REF] Jarrar | Building a Corpus for Palestinian Arabic : a Preliminary Study[END_REF], and Algerian Arabic [START_REF] Saadane | A Conventional Orthography for Algerian Arabic[END_REF].

Another efforts on modernizing TA orthography was proposed by Zribi et al. [START_REF] Zribi | Orthographic Transcription for Spoken Tunisian Arabic[END_REF] in which the authors presented OTTA: the Orthographic Transcription for Tunisian Arabic convention. This convention proposed the use of some rules based on MSA conventions and defined another set of rules, which preserved the phonetic particularities of TUN.

Contrariwise, research in automatic normalization of Arabic dialects has been recently raised. For TA, Masmoudi et al. [START_REF] Masmoudi | Arabic Transliteration of Romanized Tunisian Dialect Text: A Preliminary Investigation[END_REF] presented an effort to create a transliteration tool for the spontaneous Romanization of Tunisian dialect (Tunisian Arabizi) following the CODA-TA convention introduced by [START_REF] Zribi | A Conventional Orthography for Tunisian Arabic[END_REF]. Likewise, Eskander et al. [START_REF] Eskander | Processing Spontaneous Orthography[END_REF] benefited from the CODA convention [START_REF] Habash | Conventional Orthography for Dialectal Arabic[END_REF] to define an automatic normalization system for Egyptian dialect. Thus, given the presence of CODA-TA, we got the idea to create a similar system for TA.

CODA-TA: practical considerations

CODA is a conventionalized orthography for Dialectal Arabic [START_REF] Habash | Conventional Orthography for Dialectal Arabic[END_REF]. It was designed as a unified framework for writing all Arabic dialects. It aims to find an optimal balance between maintaining a level of dialectical unity and establish agreements based on MSA-DA similarities thus leading to the improvement of computational approaches.

In this paper, we only discuss the instantiation of CODA for defining normalization rules to TA ambiguous words. We list in the following some features of CODA-TA relevant to this paper. Arabic script. CODA uses only the characters of the Arabic language, including diacritics used for writing MSA. CODA allows writing without diacritics as the MSA.

Morphology. There are many morphological differences between Arabic dialects and MSA. CODA preserves in general the TA morphology except word having cognate in standard Arabic.

Phonetic. CODA generally keeps the phonological form of TA words given the phonological rules and the limits of the Arabic script. The dialectal words are generally written as they are pronounced except in some cases where we mark multiple pronunciations for the same word. In this case, CODA proposes the use of the MSA cognate rules if an MSA cognate exists. For example, long vowels, which are shortened in certain cases (such as when they attached to clitics), are written in its long form as in MSA. In addition, CODA requires Arabic letters to transcribe foreign phonemes. For example, the foreign letter ڤ G in the dialectal word 'garage' ڤراج garage is transcribed using the Arabic letter ق q.

Tunisian Orthographic Errors

The main idea of this work consists on projecting CODA-TA rules on TA orthographic errors that often occur in texts. We considered a sample of one hour of transcriptions in TA carried out by three native speakers. From transcriptions made by these transcribers, we highlighted the orthographic errors according to the CODA-TA convention.

Indeed, we distinguished two categories of errors. The first relates to grammatical errors that occur when transcribing MSA words such as the transformation of the final ي y to ى ý. The second concerns the errors associated with the lack of orthographic rules for the TA. We found multiple orthographic forms for the same word.

MSA Spelling Errors

Alif maqsura ى ý vs. Final Ya' ي y. The letter ى ý is often used in Tunisian spontaneous orthography to write word-final ي y and vice versa. In CODA-TA, all rules for using Alif maqsura ى ý and the final ي y are the same as in MSA. For example, the word 'Tunisian' in TA spontaneous orthography can be written as تونسى tuwnsý or تونسي tuwnsy. However, the last orthographic form is the correct form in CODA-TA. Likewise, the word 'candy' has two spontaneous orthographic forms حلوى Hlwý (the correct form according to CODA-TA) and حلو ي Hlwy.

Simple Alif ا A vs. Alif maqsura ى ý. The letter ى ý is often incorrectly used in TA (and in MSA) to write word-final Alif and vice versa. In CODA-TA, all rules for using Alif maqsura are the same as in MSA. For instance, TA spontaneous orthographic form of the verb 'he eat' is كلى klý, but in CODA-TA, it should be written as كال klA.

Ta-Marbuta ة ħ vs. hāʾ ه h vs. Simple Alif ا A. As in MSA, the TA-Marbuta ة ħ is incorrectly transformed into ه h or into simple Alif ا A. The transcription error is caused by the non-pronunciation of the Ta-Marbuta ة ħ in TA and often in MSA. For example, the noun 'four', pronounced as /arbςa/, has two spontaneous orthographic forms اربعه Arbςh and اربعا ArbςA. According to CODA-TA, this noun should be finished by Ta-Marbuta ة ħ .Therefore, the correct form is اربعة Arbςħ.

Space Absence. The error according to the addition of the space between the coordination conjunction و w and the following word is frequently made in TA spontaneous orthography. CODA-TA requires the deletion of the space after the coordination conjunction و w.

5.2

Specific Spelling errors in TA.

Question particle اش Aš. The question particle اش Aš 'what' is generally attached to the following word in TA spontaneous orthography. In CODA-TA, the question particle is written as a separate word. For example, the phrase 'what did he say?' قال اش Aš qAl in the correct form. It can be written as اشقال AšqAl in spontaneous orthography.

Negation particle ما mA. CODA-TA requires the separation between the negation particle ما mA and the verb that is agglutinated to the TA negative particle ش š. In spontaneous TA, the negation particle is, sometimes, attached to the verb.

Future particle باش bAš. CODA-TA requires separation between the future particle باش bAš and the following verb. For example, 'he will leave' باش يمشي bAš ymšy is the correct form. It can be written as بش يمشي bšymšy in spontaneous orthography.

The vocative particle.

In spontaneous spelling, the space between the vocative particle يا yA and a proper noun is deleted.

The third person singular pronoun. The third person singular pronoun ه h is pronounced as /w/ when it is attached to a consonant. In this case, TA spontaneous orthography uses the و w letter for marking the third person pronoun. As an example, the noun 'his government' is generally written as حكومتو Hkwmtw. Although, the correct form according CODA-TA is حكومته Hkwmth.

Indirect object enclitic.

The indirect object enclitic in TA is generally attached to the verb preceding the enclitic while the CODA-TA convention requires the separation between the verb and the enclitic. For example, 'he told them' لهم قال qAl lhm is the correct form of the TA spontaneous spelling قاللهم qAllhm.

Waw of Plurality.

The silent Alif at the end of the third person plural affix is often neglected in spontaneous spelling. The letter و w is often used in TA to write the third person plural affix وا wA, e.g. 'they went out' خرجو xrjw is the wrong form of خرجوا xrjwA.

Attached Clitics. TA defines some attached clitics. The non-conventionalized transcription writes them as separated clitics.

Etymologically Spelled Consonants. TA has many consonants with multiple pronunciations such as س s, ص S, ث θ, ف f and ج j. For example, the consonant س s is pronounced /s/ or /S/. So, the word 'prophet' رسول rswl can be written as رصول rSwl in spontaneous orthography. Likewise, the consonant ق q has two possible pronuncia-tions /q/ and /G/. The CODA-TA convention proposes to write the word as it is defined in MSA.

The Hamza letter. Many words in TA whose MSA cognates had the Hamza phoneme (glottal stop, ء ') lost that phoneme. In many cases, the glottal stop becomes a long vowel or disappears altogether.

N of Number Construct. The phoneme ن n that is added after some numerals in construct cases is generally omitted in some non-conventional transcription.

CODA-TA word list. CODA-TA guidelines include a word list specifying ad hoc spellings of TA words that may be inconsistent with the default mapping outlined above. As an example, we find as both مش mš موش and mwš. The CODA-TA spelling is موش mwš.

Tunisian Arabic Normalization Process

Our challenge consists on the manner of projecting the normalization rules defined in CODA-TA on the errors presented in the previous section. Therefore, by studying different kind of errors, we defined the number of spelling variation of a word as a criterion for classifying them. So words having more than one variation will be normalized using a statistical model, otherwise, they will be normalized with a specific lexicon lookup.

Statistical Models

Data collection. In this work, we have artificially built a training corpus based on lexicon collection, to overcome the problem of a lack of corpus. So, we used 1,030 nouns from a manually annotated TA corpus [START_REF] Boujelbane | Traitements linguistiques pour la reconnaissance automatique de la parole appliquée à la langue arabe : de l'arabe standard vers l'arabe dialectal[END_REF], 5,674 verbs extracted from the TA lexicon developed by [START_REF] Boujelbane | Mapping Rules for Building a Tunisian Dialect Lexicon and Generating Corpora[END_REF] and 111 tool words from various sources (internet, transcriptions and from the dialect form of the Tunisian constitution).

Data preparation. We proposed to each correct form (CODA form) of the lexicon the different variations that a word can have in a non-normalized corpus. For example, the word 'This health' هالصحة hAlSHħ (CODA form) can take these nonconventionalized orthographic forms: الصحة ها hA AlSHħ or الصحة ه h AlSHħ or هل الصحة hl AlSHħ or الصحة هالhAl AlSHħ or صحة هل hl SHħ or هلصحة hlSHħ or صحة هال hAl SHħ. These errors are due to the TA particle ه h that has no spelling rules and which can be attached to any noun. Thus, we assigned such forms to each word of the TA lexicon and we defined a class for each nominal form. Table 1 shows defined classes for the ه h particle. The same principle have been used for the ع ς, م m and ك k particles. Training the classifiers. For each attached TA particle, we train a separate classifier.

The classifiers are trained on our training corpus using the k-nearest neighbor algorithm (k-NN) [START_REF] Wang | Solving Multiple-Instance Problem: A Lazy Learning Approach[END_REF] included in the WEKA machine learning tool [START_REF] Hall | The WEKA Data Mining Software: An Update[END_REF], which is a method for classifying objects based on the closest training examples in the feature space [START_REF] Eskander | Processing Spontaneous Orthography[END_REF]. In the training process, a set of ten static features is applied. We exploited the same features proposed by [START_REF] Eskander | Processing Spontaneous Orthography[END_REF] for the automatic normalization of spontaneous Egyptian spelling. The features are the character that is queried for the transformation with its two preceding and three following characters along with the first two and the last two characters in the underlying word. In this model, each data point is a character, where a classifier determines, depending on the class predicted, whether a character should receive a substitution, deletion, or addition of another character.

Linguistics techniques

Lexicon lookup.

For each error form, we built a specific lexicon. If a corresponding error is detected, it we will be substituted from the corresponding lexicon by the correct form, based on the criteria of orthographic similarity. For example, we have extracted from the lexicon described in the previous section a sub-lexicon containing 2,808 words ending with ي y dedicated to the correction of the MSA spelling error "Alif maqsura ى ý vs. Final Ya' ي y". Thus, the wrong form of the word 'Tunisian' تونسى tuwnsý will be replaced by the CODA form تونسي tuwnsy. Spelling errors go beyond words to detect phrases. Indeed, several nominal and verbal phrases were affected by agglutination thus requiring specific patterns for the separation. For example, the word 'He did not tell him' ماقاللوش mAqAllwš should be replaced by the phrase لوش قال ما mA qAl lwš.

So, we defined patterns for each agglutinative forms and we projected them on the corresponding non-CODA word. For example, we defined the pattern [Negation particle ما mA+stem+verb] to correct the agglutinative form: Negation particle ما mA+verbal stem. We detect the verbal stem form by referring to the TA lexicon.

Table 3 lists the different agglutinative forms and the corresponding pattern of normalization.

Evaluation

The Tunisian Arabic Normalization Process gave rise to an automatic normalisation system for Tunisian Arabic that we baptized COTA orthography (COnventionalized Tunisian Arabic orthography). It has been tested against a part from the nonconventionalized version of the STAC corpus [START_REF] Zribi | Spoken Tunisian Arabic Corpus "STAC ": Transcription and Annotation[END_REF]. It contains 10,236 words and we detected manually 2,640 non-coda words.

The evaluation metric that we use is a word accuracy metric, i.e., we evaluate how well we can correctly predict the CODA-TA form of the input spontaneous orthography. Results show that a "do nothing" baseline achieves a normalization performance of 74.2%, and our normalization process achieves a performance of 86.6%, an error reduction of 77.73% over this baseline on an unseen test set. Table 4 lists the accuracy of each rule on the test set. This is to show the potential of the method lexicon based method and by consequent lexical coverage.

Conclusion

In order to enhance the quality of TA resources, we presented in this paper an effort for transforming spontaneous orthography of the Tunisian Arabic dialect into a conventionalized form, CODA-TA. Our normalization process relies on a hybrid technique based on a TA lexicon and a KNN statistical model. The resulting system achieves satisfactory results. In future work, we plan to extend our approach to handle TA content in social media, which contain more orthographic errors than transcriptions. Since the lexical coverage can never be complete, we will also study a statistical method that can replace the used Lexicon lookup method.

Table 1 .

 1 Defined classes for ه h particle

	Word forms	Class
	hA + space+Al+noun	DeleteAlif_DeleteSpace
	h + space +Al+noun	DeleteSpace
	hl +space+Al+noun	DeleteLam_DeleteSpace
	hl+noun	AddAlif
	hAl+space+Al+noun	DeleteSpace_DeleteAlif_DeleteLam
	hAl+space+noun	DeleteSpace
	hl+space+noun	DeleteSpace_AddAlif

Table 2 .

 2 The sub lexicon size for each spelling errors corrected by lexicon lookup step.

	Spelling errors	Lexicon size
	Alif maqsura ى ý vs. Final Ya' ي y	2,808
	Etymologically Spelled Consonants	1,632
	Ta-Marbuta ة ħ vs. hāʾ ه h vs. Simple Alif ا A	3,255
	CODA-TA word list	111
	The third person singular pronoun	1,066
	Waw of Plurality	5,674
	Pre-defined Patterns for normalization.

Table 3 .

 3 List of CODA-TA normalization patterns.

	Spelling errors forms	CODA normalization pattern
	Question particle اش Aš/ش š+verbal	Question particle اش Aš+space+verbal stem
	stem
	Negation particle ما mA+verb	Negation particle ما mA+space+verb
	Verbal stem+Indirect object enclitic.	Verbal stem+Space+ Indirect object enclitic
	Future particle باش bAš/بش bš + verb	Future particle باش bAš +space+ verb
	Vocative particle+proper noun	Vocative particle+space+proper noun
	Number+space+n+space+noun	Number+n+space+noun

Table 4 .

 4 The accurancy of each spelling errors. Marbuta ة ħ vs. hāʾ ه h vs. Simple Alif ا A.

	Orthographic errors	Frequency	Accuracy
	Alif maqsura ى ý vs. Final Ya' ي y.	173	98,2%
	Simple Alif ا A vs. Alif maqsura ى ý	2	100%
	Etymologically Spelled Consonants.	25	48%
	Ta-78	97,4%
	Question particle اش Aš.	23	60.8%
	Negation particle ما mA.	97	80.4%
	Indirect object enclitic.	50	60%
	The third person singular pronoun.	95	81.1%
	Waw of Plurality.	356	90.7%
	Future particle باش bAš.	6	100%
	Space Absence	338	100%
	Attached Clitics.	110	51.8%
	The hamza letter.	657	100%
	The vocative particle.	2	100%
	N of Number Construct.	118	95.7%
	CODA-TA word list	694	96.4%
	Total	2,640	86.6%