aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
...
| * | | | dockerfile for buildingDavid Monniaux2021-05-101-0/+8
| | | | |
| * | | | Increasing required OCaml version (Pervasives <-> Stdlib module renaming)Cyril SIX2021-05-041-2/+2
| | | | |
| * | | | for OCaml 4.13David Monniaux2021-04-301-1/+1
| | | | |
| * | | | Compatibilité Coq 8.13David Monniaux2021-04-285-8/+3
| | | | |
| * | | | 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
| | | | | |
| | * | | | Adding a flag to test fp_init_expLéo Gourdin2021-03-023-150/+159
| | | | | |
| | * | | | Adding fp init expansionsLéo Gourdin2021-03-022-3/+18
| | | | | |
generated by cgit (git 2.34.1) at 2024-07-07 01:36:27 +0000