aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Trying a inductive predicate for BTL-RTL proofLéo Gourdin2021-05-031-10/+41
|
* more implem notes in BTLroadmapSylvain Boulmé2021-05-021-1/+8
|
* BTL roadmapSylvain Boulmé2021-05-021-0/+79
|
* debroussaillage et precisions...Sylvain Boulmé2021-05-012-23/+73
|
* BTLtoRTL: proof for internal/external/return statesLéo Gourdin2021-04-302-2/+27
|
* start the new "BTL" IR.Sylvain Boulmé2021-04-286-2/+735
|
* add auxfileDavid Monniaux2021-04-271-0/+17
|
* Merge branch 'kvx-work' of ↵Léo Gourdin2021-04-2218-566/+370
|\ | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into kvx-work
| * fix broken link in index-kvx.htmlSylvain Boulmé2021-04-161-1/+1
| |
| * Merge remote-tracking branch 'origin/manuscript' into kvx-worksubmission_OOPSLA2021_AARCH64_KVXCyril SIX2021-04-135-525/+173
| |\
| | * 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-022-2/+50
| | |
| | * 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-023-0/+57
| | |
| | * 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.
| | * Code simplification of get_path_map (no functionality change)Cyril SIX2021-01-261-14/+16
| | |
| * | 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
| * | Adding distinction between kvx-cos and kvx-mbr (for trapping loads)Cyril SIX2021-04-137-4/+22
| | |
| * | rm spurious filesDavid Monniaux2021-04-1239-1705/+0
| | |
| * | test profilingDavid Monniaux2021-04-1242-0/+1720
| | |
| * | collision of registersDavid Monniaux2021-04-122-3/+3
| | |
* | | moving my testsLéo Gourdin2021-04-2226-157/+0
|/ /
* | removing unusued proof lineLéo Gourdin2021-04-091-1/+0
| |
* | adding missing xorimm expLéo Gourdin2021-04-092-0/+77
| |
* | Merge branch 'riscv-work' into kvx-workLéo Gourdin2021-04-0921-1514/+2642
|\ \
| * | Remove flagsLéo Gourdin2021-04-094-10/+3
| | |
| * | Removing expansions from AsmgenLéo Gourdin2021-04-096-1401/+49
| | |
| * | Removing addptrofs draft, next will be mergingLéo Gourdin2021-04-099-254/+104
| | |
| * | bugfixLéo Gourdin2021-04-082-2/+3
| | |
| * | Important commit on expansions' mini CSE, and a draft for addptrofsLéo Gourdin2021-04-0613-762/+1081
| | |
| * | a more general way to manage special registers before introducing SPLéo Gourdin2021-03-308-560/+593
| | |
| * | Now a more general way to perform imm operationsLéo Gourdin2021-03-309-38/+68
| | |
| * | Refactoring the mayundef OP to be more general...Léo Gourdin2021-03-305-201/+191
| | |
| * | bugfix and printOpLéo Gourdin2021-03-262-19/+29
| | |
| * | fix admitLéo Gourdin2021-03-261-2/+1
| | |
| * | Compiler options to manage expansionsLéo Gourdin2021-03-263-179/+176
| | |
| * | Adding more expansions, improving miniCSE, and tuning prepassLéo Gourdin2021-03-269-388/+1518
| | |
| * | Bugfix livenessLéo Gourdin2021-03-231-12/+8
| | |
| * | Remove first nop when doing expansionLéo Gourdin2021-03-212-188/+213
| | |
| * | fp testLéo Gourdin2021-03-101-0/+7
| | |
| * | Adding miniCSE here tooLéo Gourdin2021-03-081-10/+10
| | |
| * | Merge remote-tracking branch 'origin/riscv-work' into riscv-work-fpinit-stillexpLéo Gourdin2021-03-0610-187/+250
| |\ \
| | * | some simplification in miniCSELéo Gourdin2021-03-061-17/+14
| | | |
| | * | Adding a mini CSE pass in the expansion oracleLéo Gourdin2021-03-0610-197/+268
| | | |
generated by cgit (git 2.34.1) at 2024-07-07 00:49:24 +0000