aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
...
| * | | Comment updateCyril SIX2020-10-161-1/+7
| |/ /
| * | Merge remote-tracking branch 'origin/kvx-work-unroll-fixcse3' into kvx-workDavid Monniaux2020-10-169-17/+491
| |\|
| | * reorder phasesDavid Monniaux2020-10-162-2/+4
| | * kill useless moves (not yet connected)David Monniaux2020-10-162-0/+401
| | * extracted from Polybench syrkDavid Monniaux2020-10-161-0/+28
| | * larger stack size for yarpgen 89David Monniaux2020-10-151-1/+1
| | * some more tuning of CSE3David Monniaux2020-10-152-10/+23
| | * a bit of progressDavid Monniaux2020-10-143-4/+34
| * | Comment updateCyril SIX2020-10-161-0/+1
| * | test/kvx/sort : timeout of 20s instead of 10sCyril SIX2020-10-161-1/+1
| * | Merge branch 'kvx-work-unroll' into kvx-workCyril SIX2020-10-167-142/+355
| |\|
| | * Merge remote-tracking branch 'origin/kvx-work' into kvx-work-unrollCyril SIX2020-10-145-15/+24
| | |\
| | * | -O0 desactivates -fpredict and -ftracelinearizeCyril SIX2020-10-141-0/+1
| | * | Ignoring Inops for counting number of instructionsCyril SIX2020-10-141-6/+15
| | * | Updated --helpCyril SIX2020-10-141-9/+5
| | * | Only unrolling on a given instruction limitCyril SIX2020-10-091-12/+16
| | * | new flags: -fpredict, -ftailduplicate n, -funrollsingle n instead of just -fd...Cyril SIX2020-10-093-39/+53
| | * | Changing duplicate verifier to be non optionalCyril SIX2020-10-093-6/+1
| | * | Performing branch prediction before loop unrollingCyril SIX2020-10-071-8/+10
| | * | [EXP] First draft of 1st iteration unrollingCyril SIX2020-10-071-73/+102
| | * | [BROKEN] Some progress, need to figure out conversion HashedPSet -> ListCyril SIX2020-10-061-14/+111
| | * | Detecting inner loops with LICMaux.inner_loopsCyril SIX2020-10-021-12/+75
| | * | Rewriting some print to use a oc argumentCyril SIX2020-10-021-16/+11
| | * | Moving some code from Duplicateaux to LICMaux to prevent cyclic depsCyril SIX2020-10-022-55/+63
| * | | Updating builtins for Accesscore 4.2 (atomic stuff)Cyril SIX2020-10-141-1/+14
| | |/ | |/|
| * | centralize if_sameDavid Monniaux2020-10-093-12/+6
| * | do not synthesize select if both operands are identicalDavid Monniaux2020-10-092-7/+22
| * | update the title of our paperSylvain Boulmé2020-10-071-2/+2
| |/
* | simplify HSop (and merge hSop and hSop_Sinit)Sylvain Boulmé2020-10-172-42/+23
* | update op_valid_pointer_eq proof on the KVXSylvain Boulmé2020-10-171-22/+4
* | proves op_valid_pointer_eq lemma for RISC-V (necessary for the pre-pass sched...Sylvain Boulmé2020-10-172-0/+32
* | fixing the move of the verified prepass scheduler into scheduling/ directorySylvain Boulmé2020-10-174-762/+2
* | Merge remote-tracking branch 'origin/kvx-test-prepass' into mppa-RTLpathSE-verifCyril SIX2020-10-1692-11356/+3357
|\ \
| * | pour ARMDavid Monniaux2020-10-021-4/+4
| * | fix need for kvx-elfDavid Monniaux2020-10-021-5/+1
| * | so that all architectures compileDavid Monniaux2020-10-027-8/+24
| * | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-027-19/+38
| |\|
| | * Duplicate no longer overwrites existing prediction informationCyril SIX2020-10-011-2/+9
| | * Updating test/kvx for KVX toolsCyril SIX2020-10-016-17/+29
| * | ccomp.force target for forcing compilation without Coq processingDavid Monniaux2020-10-012-0/+8
| * | non pipelined units = none on KVXDavid Monniaux2020-09-301-1/+3
| * | non trapping opDavid Monniaux2020-09-304-88/+73
| * | non trappingDavid Monniaux2020-09-301-2/+0
| * | AArch64 division no longer "traps"David Monniaux2020-09-306-81/+221
| * | floating-point division uses the divisorDavid Monniaux2020-09-291-4/+5
| * | attempt at separating the divisionsDavid Monniaux2020-09-292-1/+18
| * | try to model resourcesDavid Monniaux2020-09-291-5/+164
| * | attempt at latencies for Cortex A53David Monniaux2020-09-291-2/+147
| * | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-09-2924-770/+766
| |\|
| | * simpl -> cbnDavid Monniaux2020-09-2923-793/+789