- 20 Nov, 2020 1 commit
-
-
Denis Merigoux authored
-
- 12 Nov, 2020 5 commits
-
-
Raphaël Monat authored
Fuzzer-generated tests * [x] Improve fuzzing harness by making input more compact (using `uint16_t`) * [x] Changed `2018_6_7.mpp` file to simplify `compute_benefits` functions * [x] Added a set of tests generated by fuzzing, that enjoys a better value coverage than private DGFiP tests and randomized tests * [x] Made fuzzing tests the default test suite * [x] Fixed interpreter on `floor` * [x] Debug the backend on the new fuzzer tests See merge request !20
-
Denis Merigoux authored
-
Denis Merigoux authored
-
Denis Merigoux authored
-
Denis Merigoux authored
-
- 11 Nov, 2020 6 commits
-
-
Denis Merigoux authored
-
Denis Merigoux authored
-
Denis Merigoux authored
-
Denis Merigoux authored
-
Denis Merigoux authored
-
Denis Merigoux authored
-
- 10 Nov, 2020 9 commits
-
-
Denis Merigoux authored
-
Denis Merigoux authored
-
Raphaël Monat authored
Coq update to match the paper See merge request !19
-
Denis Merigoux authored
-
Denis Merigoux authored
-
Raphaël Monat authored
-
Denis Merigoux authored
-
Raphaël Monat authored
-
Denis Merigoux authored
-
- 09 Nov, 2020 19 commits
-
-
Denis Merigoux authored
Optimizations: add --fast-math option, for optimizations that do not preserve IEEE-754 semantics See merge request !18
-
Denis Merigoux authored
-
Denis Merigoux authored
-
Denis Merigoux authored
-
Raphaël Monat authored
M++ paper-related updates - Check if clean semantics for M calls is possible + Clean unnecessary M variables once a call is finished (this introduces 598023 new instructions) + Check that inputs from the M++ environment are not modified + ~~Local dependency analysis to avoid inlining + cleaning too many variables?~~ - Change syntax of the call - Prefix local M++ variables by `mpp_` to avoid conflicts in the backend See merge request !16
-
Denis Merigoux authored
-
Raphaël Monat authored
-
Raphaël Monat authored
Switched C backend to use variable array The current extraction scheme to C involves one main function that contains the requested computation. Inside that function, there is one local variable per `Mir.Variable.t` involved, so the function has thousands of local variables. Moreover, the uses and defs of these local variables are very intricated, making it hard for C compilers to produce an efficient register allocation in the generated binary object. Actually, the number of variables spilled on the stack is so big that running the programs required raising `ulimit -s`, else it raises a segmentation fault. This overspilling on the stack is responsible for a number of unnecessary shuffle of the variables during the computation, which reduces performance. Using `-O0`, we estimate a typical computation requiring ~2ms, compared to ~1ms for the DGFiP's code. The solution to this problem actually comes from the DGFiP. Looking at their code, we figured out that the variables of M are not represented as local variables, but rather in a big, heap-allocated array of variables called TGV. It turns out that this memory layout, although less sophisticated that what an efficient register allocation can achieve, yields better performance results for the generated code. We suspect that this better performance is related to the fit of the TGV inside the processor cache. Indeed, the TGV is typically a few dozens of kilo-octets. The processor cache can thus hold the TGV in its entirety, making TGV accesses faster than accesses to a local variable spilled randomly on a stack location determined by the C compiler. This unintuitive result is surprising and show a very happy technical choice by the DGFiP, which is robust enough to survive our modernization effort. This PR thus replicates the TGV in our C backend. In terms of performance, the switch to TGV enabled a big performance gain. Compiled using `-O0`, our generated C code takes ~1ms per computation, same as the DGFiP. However, compiling with `-O1` yields even better performance, around ~0.5ms per computation! We attribute that to the optimizations performed directly in Mlang, which reduce a lot the number of statements generated in the C compared to what the DGFiP does. See merge request !17
-
Denis Merigoux authored
-
Raphaël Monat authored
-
Denis Merigoux authored
-
Raphaël Monat authored
-
Raphaël Monat authored
-
Raphaël Monat authored
-
Raphaël Monat authored
-
Raphaël Monat authored
-
Denis Merigoux authored
-
Raphaël Monat authored
-
Raphaël Monat authored
-