aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Adding both RV expansion methods in kvx-workLéo Gourdin2021-05-198-48/+1410
|
* Merge branch 'riscv-work-fpinit-stillexp' into kvx-workLéo Gourdin2021-05-190-0/+0
|\
| * xorimmsubmission_OOPSLA2021_RISCVLéo Gourdin2021-04-092-0/+77
| |
| * removing useless flag checkLéo Gourdin2021-04-091-3/+1
| |
* | debug prints uniformizedLéo Gourdin2021-05-181-69/+66
| |
* | for making the dockerDavid Monniaux2021-05-114-0/+3
| |
* | for pruning the dockerDavid Monniaux2021-05-111-1/+2
| |
* | pruning the imageDavid Monniaux2021-05-111-0/+4
| |
* | adjust to compile for various archDavid Monniaux2021-05-111-3/+3
| |
* | progress being madeDavid Monniaux2021-05-101-2/+15
| |
* | build for aarch64David Monniaux2021-05-101-1/+4
| |
* | dockerfilesDavid Monniaux2021-05-102-8/+9
| |
* | 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
| | |
generated by cgit (git 2.34.1) at 2024-07-01 05:39:13 +0000