index
:
compcert-kvx
CPP22_if_lifting
CPP22_main
master
patched_for_velus
riscV-cmov
ssa
vericert
vericert-kvx
Unnamed repository; edit this file 'description' to name the repository.
about
summary
refs
log
tree
commit
diff
stats
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
Files
Lines
...
|
*
|
|
Comment update
Cyril SIX
2020-10-16
1
-1
/
+7
|
|
/
/
|
*
|
Merge remote-tracking branch 'origin/kvx-work-unroll-fixcse3' into kvx-work
David Monniaux
2020-10-16
9
-17
/
+491
|
|
\
|
|
|
*
reorder phases
David Monniaux
2020-10-16
2
-2
/
+4
|
|
*
kill useless moves (not yet connected)
David Monniaux
2020-10-16
2
-0
/
+401
|
|
*
extracted from Polybench syrk
David Monniaux
2020-10-16
1
-0
/
+28
|
|
*
larger stack size for yarpgen 89
David Monniaux
2020-10-15
1
-1
/
+1
|
|
*
some more tuning of CSE3
David Monniaux
2020-10-15
2
-10
/
+23
|
|
*
a bit of progress
David Monniaux
2020-10-14
3
-4
/
+34
|
*
|
Comment update
Cyril SIX
2020-10-16
1
-0
/
+1
|
*
|
test/kvx/sort : timeout of 20s instead of 10s
Cyril SIX
2020-10-16
1
-1
/
+1
|
*
|
Merge branch 'kvx-work-unroll' into kvx-work
Cyril SIX
2020-10-16
7
-142
/
+355
|
|
\
|
|
|
*
Merge remote-tracking branch 'origin/kvx-work' into kvx-work-unroll
Cyril SIX
2020-10-14
5
-15
/
+24
|
|
|
\
|
|
*
|
-O0 desactivates -fpredict and -ftracelinearize
Cyril SIX
2020-10-14
1
-0
/
+1
|
|
*
|
Ignoring Inops for counting number of instructions
Cyril SIX
2020-10-14
1
-6
/
+15
|
|
*
|
Updated --help
Cyril SIX
2020-10-14
1
-9
/
+5
|
|
*
|
Only unrolling on a given instruction limit
Cyril SIX
2020-10-09
1
-12
/
+16
|
|
*
|
new flags: -fpredict, -ftailduplicate n, -funrollsingle n instead of just -fd...
Cyril SIX
2020-10-09
3
-39
/
+53
|
|
*
|
Changing duplicate verifier to be non optional
Cyril SIX
2020-10-09
3
-6
/
+1
|
|
*
|
Performing branch prediction before loop unrolling
Cyril SIX
2020-10-07
1
-8
/
+10
|
|
*
|
[EXP] First draft of 1st iteration unrolling
Cyril SIX
2020-10-07
1
-73
/
+102
|
|
*
|
[BROKEN] Some progress, need to figure out conversion HashedPSet -> List
Cyril SIX
2020-10-06
1
-14
/
+111
|
|
*
|
Detecting inner loops with LICMaux.inner_loops
Cyril SIX
2020-10-02
1
-12
/
+75
|
|
*
|
Rewriting some print to use a oc argument
Cyril SIX
2020-10-02
1
-16
/
+11
|
|
*
|
Moving some code from Duplicateaux to LICMaux to prevent cyclic deps
Cyril SIX
2020-10-02
2
-55
/
+63
|
*
|
|
Updating builtins for Accesscore 4.2 (atomic stuff)
Cyril SIX
2020-10-14
1
-1
/
+14
|
|
|
/
|
|
/
|
|
*
|
centralize if_same
David Monniaux
2020-10-09
3
-12
/
+6
|
*
|
do not synthesize select if both operands are identical
David Monniaux
2020-10-09
2
-7
/
+22
|
*
|
update the title of our paper
Sylvain Boulmé
2020-10-07
1
-2
/
+2
|
|
/
*
|
simplify HSop (and merge hSop and hSop_Sinit)
Sylvain Boulmé
2020-10-17
2
-42
/
+23
*
|
update op_valid_pointer_eq proof on the KVX
Sylvain Boulmé
2020-10-17
1
-22
/
+4
*
|
proves op_valid_pointer_eq lemma for RISC-V (necessary for the pre-pass sched...
Sylvain Boulmé
2020-10-17
2
-0
/
+32
*
|
fixing the move of the verified prepass scheduler into scheduling/ directory
Sylvain Boulmé
2020-10-17
4
-762
/
+2
*
|
Merge remote-tracking branch 'origin/kvx-test-prepass' into mppa-RTLpathSE-verif
Cyril SIX
2020-10-16
92
-11356
/
+3357
|
\
\
|
*
|
pour ARM
David Monniaux
2020-10-02
1
-4
/
+4
|
*
|
fix need for kvx-elf
David Monniaux
2020-10-02
1
-5
/
+1
|
*
|
so that all architectures compile
David Monniaux
2020-10-02
7
-8
/
+24
|
*
|
Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass
David Monniaux
2020-10-02
7
-19
/
+38
|
|
\
|
|
|
*
Duplicate no longer overwrites existing prediction information
Cyril SIX
2020-10-01
1
-2
/
+9
|
|
*
Updating test/kvx for KVX tools
Cyril SIX
2020-10-01
6
-17
/
+29
|
*
|
ccomp.force target for forcing compilation without Coq processing
David Monniaux
2020-10-01
2
-0
/
+8
|
*
|
non pipelined units = none on KVX
David Monniaux
2020-09-30
1
-1
/
+3
|
*
|
non trapping op
David Monniaux
2020-09-30
4
-88
/
+73
|
*
|
non trapping
David Monniaux
2020-09-30
1
-2
/
+0
|
*
|
AArch64 division no longer "traps"
David Monniaux
2020-09-30
6
-81
/
+221
|
*
|
floating-point division uses the divisor
David Monniaux
2020-09-29
1
-4
/
+5
|
*
|
attempt at separating the divisions
David Monniaux
2020-09-29
2
-1
/
+18
|
*
|
try to model resources
David Monniaux
2020-09-29
1
-5
/
+164
|
*
|
attempt at latencies for Cortex A53
David Monniaux
2020-09-29
1
-2
/
+147
|
*
|
Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass
David Monniaux
2020-09-29
24
-770
/
+766
|
|
\
|
|
|
*
simpl -> cbn
David Monniaux
2020-09-29
23
-793
/
+789
[prev]
[next]