aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Merge branch 'kvx-work-velus' of ↵patched_for_velusDavid Monniaux2021-04-271-1/+1
|\ | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into HEAD
| * fix 64-bitDavid Monniaux2021-04-271-1/+1
| |
* | fix 4David Monniaux2021-04-271-1/+1
|/
* fix pour ARMDavid Monniaux2021-04-271-1/+2
|
* Merge branch 'kvx-work-velus' of ↵David Monniaux2021-04-2715-227/+456
|\ | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into patched_for_velus
| * disable builds that don't workDavid Monniaux2021-04-191-84/+84
| |
| * Merge remote-tracking branch 'origin/kvx-work' into kvx-work-velusDavid Monniaux2021-04-19386-11069/+41602
| |\
| * \ Merge remote-tracking branch 'origin/kvx-work' into kvx-work-velusDavid Monniaux2020-09-1818-255/+290
| |\ \
| * | | keep Velus happyDavid Monniaux2020-07-291-0/+20
| | | |
| * | | fix stacklayout for velusDavid Monniaux2020-07-281-1/+1
| | | |
| * | | rm 'range' causing compilation to endDavid Monniaux2020-07-281-1/+1
| | | |
| * | | applied the Velus patchDavid Monniaux2020-07-282-1/+2
| | | |
| * | | Merge branch 'v3.7-velus' of github.com:inria-parkas/CompCert into ↵David Monniaux2020-07-2811-140/+368
| |\ \ \ | | | | | | | | | | | | | | | kvx-work-velus
| | * \ \ Merge pull request #1 from Lionel-Rieg/v3.7-velusTimothy Bourke2020-04-21307-7791/+28881
| | |\ \ \ | | | | | | | | | | | | V3.7 velus
| | | * | | More rewriting for SeparationTimothy Bourke2020-04-211-14/+34
| | | | | |
| | | * | | Fix rebase of Stackingproof/elab_char_constantTimothy Bourke2020-04-213-10/+6
| | | | | |
| | | * | | Fix other stacking proofs for range'Timothy Bourke2020-04-212-2/+2
| | | | | |
| | | * | | Rewrites in disjoint_footprintTimothy Bourke2020-04-211-0/+15
| | | | | |
| | | * | | Fix out-of-date comment about function allocsTimothy Bourke2020-04-211-4/+2
| | | | | |
| | | * | | Generalize definition of rangeTimothy Bourke2020-04-212-105/+108
| | | | | |
| | | * | | Streamline range weakening lemmaTimothy Bourke2020-04-211-13/+13
| | | | | |
| | | * | | Add range_w for writeable static variablesTimothy Bourke2020-04-212-74/+119
| | | | | |
| | | * | | Minor typo in docs: RTLtyping -> CtypingTimothy Bourke2020-04-211-1/+2
| | | | | |
| | | * | | Expose the kind of elaborated char constantsTimothy Bourke2020-04-212-5/+5
| | | | | |
| | | * | | Expose constant elaboration functionsTimothy Bourke2020-04-211-0/+4
| | | | | |
| | | * | | pretty printer for ClightLélio Brun2020-04-212-7/+3
| | | | | |
| | | * | | Some more separation lemmasTimothy Bourke2020-04-211-0/+90
| | | | | |
| | | * | | Strengthen contains massertTimothy Bourke2020-04-211-27/+50
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The idea is to be able to exchange a "contains" for a "range" over the same footprint, i.e., m |= contains chunk b ofs spec ** P -> m |= range b ofs (ofs + size_chunk chunk) ** P This requires knowing that ofs + size_chunk chunk <= Int.modulus.
| | | * | | Remove unnecessary module pathsTimothy Bourke2020-04-211-0/+20
| | | | | |
| | | * | | Semantics parametrized by function entryLélio Brun2020-04-211-36/+53
| | | | | |
* | | | | | 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
| | | | | | |
generated by cgit (git 2.34.1) at 2024-05-19 10:28:22 +0000