aboutsummaryrefslogtreecommitdiffstats
path: root/backend
Commit message (Collapse)AuthorAgeFilesLines
* Heuristic counter updateCyril SIX2021-04-281-12/+6
|
* 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.
* | Adding more precise heuristic measuresCyril SIX2021-04-131-2/+62
| |
* | Adding overpredictsCyril SIX2021-04-131-3/+6
| |
* | Recording of prediction stats with COMPCERT_PROFILING_STATS environment flagCyril SIX2021-04-131-33/+93
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | It only works correctly if both profiling and static prediction are used: it then compares both and gives stats in COMPCERT_PREDICT_STATS file. The stats are of the form: total correct mispredicts missed total = number of total CBs encountered correct = number of correct predictions mispredicts = times when static prediction did a wrong guess (predicted the opposite from profiling, or predicted Some _ when profiling said None) missed = times when static prediction was not able to give a verdict, though the profiling gave one
* | removing unusued proof lineLéo Gourdin2021-04-091-1/+0
| |
* | Important commit on expansions' mini CSE, and a draft for addptrofsLéo Gourdin2021-04-061-1/+2
| |
* | add has_type infoDavid Monniaux2021-01-311-1/+3
|/
* Conditions now propagated by CSE3David Monniaux2021-01-205-264/+934
|\ | | | | | | Merge remote-tracking branch 'origin/kvx-better2-cse3' into kvx-work
| * totally switch off conditions in cse3David Monniaux2020-12-092-16/+21
| |
| * begin implementing -fcse3-conditionsDavid Monniaux2020-12-092-8/+15
| |
| * CSE3 + conditions proofDavid Monniaux2020-12-092-34/+58
| |
| * apply_cond_soundDavid Monniaux2020-12-091-0/+14
| |
| * apply_cond0_soundDavid Monniaux2020-12-091-1/+25
| |
| * apply_cond1_soundDavid Monniaux2020-12-091-0/+30
| |
| * proof for jumptableDavid Monniaux2020-12-091-1/+27
| |
| * one 'admit' lessDavid Monniaux2020-12-091-2/+36
| |
| * avancement dans les preuvesDavid Monniaux2020-12-091-1/+34
| |
| * CSE3 compiles again, but some admitted lemmasDavid Monniaux2020-12-091-10/+8
| |
| * progress moving to list of itemsDavid Monniaux2020-12-093-92/+233
| |
| * analysis with Abst_sameDavid Monniaux2020-12-083-22/+39
| |
| * CSE3 now runs on its own fixpoint iterator not based on Kildall.vDavid Monniaux2020-12-082-114/+3
| |
| * Merge remote-tracking branch 'origin/kvx-work' into kvx-better2-cse3David Monniaux2020-12-0813-80/+183
| |\
| * | start checking for bugsDavid Monniaux2020-12-021-2/+115
| | |
| * | attempt at initial analysisDavid Monniaux2020-12-021-1/+35
| | |
| * | Merge remote-tracking branch 'origin/kvx-work' into kvx-better2-cse3David Monniaux2020-12-024-5/+487
| |\ \
| * | | not yet the transfer functions that record predicatesDavid Monniaux2020-11-263-9/+78
| | | |
| * | | remains one admitDavid Monniaux2020-11-261-8/+46
| | | |
| * | | is_condition_present_soundDavid Monniaux2020-11-263-5/+23
| | | |
| * | | begin implementing cond tableDavid Monniaux2020-11-261-6/+13
| | | |
| * | | ajouté Cond, tout passeDavid Monniaux2020-11-263-40/+168
| | | |
| * | | passage à EquDavid Monniaux2020-11-263-189/+196
| | | |
| * | | cond_valid_pointer_eqDavid Monniaux2020-11-251-0/+14
| | | |
* | | | remove some useless "OK tt"Sylvain Boulmé2021-01-072-11/+11
| | | |
* | | | Merge branch 'kvx-work' of ↵David Monniaux2021-01-074-92/+13
|\ \ \ \ | | | | | | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into kvx-work
| * | | | Making verify_mapping_mn_rec tail recursive (should fix arm CI) #231Cyril SIX2021-01-062-3/+2
| | | | |
| * | | | Solving a stack overflow issue (was failing in yarpgen ran000089 for armhf)Cyril SIX2021-01-061-9/+9
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Note : the issue is still present later in Duplicateproof. This is because I am examining an "identity ptree" which is way too big. I am having a look to see if I could make this ptree less big - to not include nodes that are identity
| * | | | Uniformizing a couple of debug print functionsCyril SIX2020-12-172-80/+2
| | | | |
* | | | | -fcse3-trivial-opsDavid Monniaux2021-01-072-3/+4
|/ / / /
* | | | Fixing wrong predictions on imbricated loopsCyril SIX2020-12-111-104/+114
| | | |
* | | | Fixing exponential blowup on get_loop_info.mark_path.exploreCyril SIX2020-12-091-33/+44
| | | |
generated by cgit (git 2.34.1) at 2024-07-04 02:37:42 +0000