aboutsummaryrefslogtreecommitdiffstats
path: root/backend
Commit message (Collapse)AuthorAgeFilesLines
* Merge branch 'kvx-work' of ↵David Monniaux2021-09-013-5/+107
|\ | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into kvx-work
| * cleanupLéo Gourdin2021-09-011-9/+0
| |
| * Merge remote-tracking branch 'origin/kvx-work' into kvx-workLéo Gourdin2021-09-015-89/+24
| |\
| * \ [MERGE] BTL into kvx-work (replacing RTLpath)Léo Gourdin2021-09-013-5/+116
| |\ \
| | * \ Merge branch 'kvx-work' into BTLLéo Gourdin2021-06-1038-738/+774
| | |\ \
| | * | | [disabled checker] BTL Scheduling and Renumbering OK!Léo Gourdin2021-05-271-0/+1
| | | | |
| | * | | Moving common tools, adding liveness input/output information to BTL ↵Léo Gourdin2021-05-243-2/+39
| | | | | | | | | | | | | | | | | | | | generation oracle
| | * | | Changing to an opaq record in BTL info, this is a broken commitLéo Gourdin2021-05-201-0/+52
| | | | |
| | * | | Grouping common RTL functions, printer improvementLéo Gourdin2021-05-192-5/+2
| | | | |
* | | | | Merge remote-tracking branch 'origin/parameterized-cse3' into kvx-workDavid Monniaux2021-09-014-61/+79
|\ \ \ \ \ | |_|_|_|/ |/| | | |
| * | | | more parameterizationDavid Monniaux2021-07-161-2/+0
| | | | |
| * | | | make operations cse3 parametricDavid Monniaux2021-07-162-6/+10
| | | | |
| * | | | make trivial ops parametricDavid Monniaux2021-07-162-6/+7
| | | | |
| * | | | make conditions a parameter in CSE3David Monniaux2021-07-162-3/+12
| | | | |
| * | | | rename parameterized versionsDavid Monniaux2021-07-162-38/+38
| | | | |
| * | | | make CSE3 condition parametricDavid Monniaux2021-07-162-29/+42
| | | | |
| * | | | rm condition parametrization in CSE3analysisDavid Monniaux2021-07-162-13/+6
| | | | |
* | | | | RTLTunneling: fix comments and authors informationSylvain Boulmé2021-08-245-89/+24
| |/ / / |/| | |
* | | | remove default_notrap_load_valueSylvain Boulmé2021-07-241-1/+1
| | | |
* | | | Merge branch 'kvx-work' into rtl-tunnelingSylvain Boulmé2021-07-2413-25/+18
|\| | |
| * | | Replacing default notrap load value by Vundef everywherecsix-PhDCyril SIX2021-06-1813-25/+18
| | |/ | |/|
* | | Change "Tunneling" to "LTLTunneling" everywherePierre Goutagny2021-06-175-5/+5
| | | | | | | | | | | | To respect the symmetry between RTL- and LTL-Tunneling
* | | Use Tunnelinglibs in TunnelingauxPierre Goutagny2021-06-171-256/+81
| | |
* | | Simplify tunneling factorisationPierre Goutagny2021-06-172-168/+173
| | | | | | | | | | | | | | | The recursive module definitions required unnecessarily long expicit signatures for little added legibility.
* | | Use Tunnelinglibs in RTLTunnelingauxPierre Goutagny2021-06-162-265/+123
| | |
* | | Add Tunneling factorisation modulePierre Goutagny2021-06-161-0/+237
| | |
* | | Add RTL Tunneling as a passPierre Goutagny2021-06-142-0/+6
| | |
* | | Add the RTLTunneling oraclePierre Goutagny2021-06-141-0/+284
| | |
* | | Complete RTLTunnelingproofPierre Goutagny2021-06-111-16/+66
| | | | | | | | | | | | There is still some refactoring to do, though
* | | Complete `tunnel_step_correct` proof up to IjumptablePierre Goutagny2021-06-101-9/+227
| | | | | | | | | | | | Excluding Icond
* | | Starts proof for `tunnel_step_correct`Pierre Goutagny2021-06-091-15/+120
| | |
* | | Monday's work on RTLTunnelingproofPierre Goutagny2021-06-071-31/+153
| | |
* | | Add RTLTunnelingproof.vPierre Goutagny2021-06-041-0/+170
| | |
* | | Fix check_instr Icond target conditionsPierre Goutagny2021-06-041-2/+2
| | |
* | | Write RTLTunneling.vPierre Goutagny2021-06-031-0/+125
| | |
* | | Add RTLTunneling.vPierre Goutagny2021-06-031-0/+0
|/ /
* | Merge remote-tracking branch 'verimag/manuscript' into kvx-workCyril SIX2021-06-011-13/+11
|\ \
| * | Do not rotate if the CB was already at the end.Cyril SIX2021-04-281-1/+5
| | |
| * | Heuristic counter updateCyril SIX2021-04-281-12/+6
| |/
* | Merge remote-tracking branch 'origin/kvx-work' into merge_master_8.13.1Cyril SIX2021-06-014-545/+286
|\|
| * Merge remote-tracking branch 'origin/manuscript' into kvx-worksubmission_OOPSLA2021_AARCH64_KVXCyril SIX2021-04-133-511/+129
| |\
| | * CleaningCyril SIX2021-04-021-2/+1
| | |
| | * More efficientCyril SIX2021-04-021-8/+12
| | |
| | * Outermost loop detection worksCyril SIX2021-04-021-9/+10
| | |
| | * Getting all loop bodiesCyril SIX2021-04-021-2/+36
| | |
| | * get_loop_headers simplification (using the new get_loop_backedges)Cyril SIX2021-04-021-39/+7
| | |
| | * Simple backedge detection (modified code from get_loop_headers)Cyril SIX2021-04-022-0/+43
| | |
| | * Big simplification of get_loop_infoCyril SIX2021-03-311-111/+16
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Another remnant of trying to devise a complicated algorithm for a problem that was, in fact, very simple: I just had to check whether the branch was within the loop body. I tested it functionally on the benchmarks: only heapsort is changed, in slightly worst (4-5%), because the old get_loop_info had done a buggy guess that proved to be lucky for that particular case. The other benchmarks are unchanged: the predictions stay the exact same. The get_loop_info could potentially be improved by having a natural loop detection that extends to outer loops (not just inner loops), though I expect the performance improvements would be very small.
| | * Simplification of the Linearize heuristic (same result functionally)Cyril SIX2021-03-301-216/+6
| | |
| | * Simplifications on Linearize - details belowCyril SIX2021-03-291-205/+79
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | While I was developing the new trace linearize, I started off with implementing a big algorithm reasoning on dependencies etc.., but I realized later that it was giving a too different performance (sometimes better, sometimes worst) than the original CompCert. So I stripped it off gradually until its performance (on regular code with just branch prediction) was on par with the base Linearize of CompCert. I was aiming here for something that is either equal, or better, in terms of performance. My (then and current) theory is that I have stripped it out so much that now it's just like the algorithm of CompCert, but with a modification for Lcond instructions (see the new linearize_aux_cb). However, I never tested that theory: the code worked, so I left it as is, without any simplification. But now that I need to get a clear version for my manuscript, I'm digging into it. It turns out my theory is not really exact. A difference is that instead of taking the minpc across the chain, I take the pc of the very first block of the chain I create. This was (I think) out of laziness in the middle of two iterations, except that I forgot about it. I tested my new theory by deleting all the stuff about dependencies calculation (commited), and also computing a minpc just like original compcert (not commited): I get the same exact Mach code than linearize_aux_cb. So right now, the only difference between linearize_aux_cb and linearize_aux_trace is that slightly different minpc computation. I think transitionning to linearize_aux_cb will be 1) much clearer than this Frankenstein monster of linearize_aux_trace that I made, and 2) might be better performing too. I don't have access to Kalray machines today so i'm leaving this on hold for now, but tomorrow I will test performance wise to see if there is a regression. If there isn't, I will commit this (and it will be the version narrated by my manuscript). If there is a regression, it would mean selecting the pc of the first node (in opposition to the minpc) is more performant, so i'd backtrack the change to linearize_aux_cb anyway and there should then be 0 difference in the generated code.
generated by cgit (git 2.34.1) at 2024-06-30 11:37:24 +0000