Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Merge branch 'kvx-sched-w-reg-press' of ↵ | David Monniaux | 2021-06-17 | 1 | -1/+2 |
|\ | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into kvx-sched-w-reg-press | ||||
| * | changed type of schedule_seq in x86 for compatibility | nicolas.nardino | 2021-06-17 | 1 | -1/+2 |
| | | |||||
* | | Merge branch 'kvx-sched-w-reg-press' of ↵ | David Monniaux | 2021-06-17 | 0 | -0/+0 |
|\| | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into kvx-sched-w-reg-press | ||||
| * | fix riscv/Machregsaux.mli | nicolas.nardino | 2021-06-17 | 1 | -0/+2 |
| | | |||||
* | | fix for Risc-V | David Monniaux | 2021-06-17 | 2 | -0/+4 |
| | | |||||
* | | Merge remote-tracking branch 'origin/kvx-work' into kvx-sched-w-reg-press | David Monniaux | 2021-06-17 | 14 | -84/+221 |
|\ \ | |/ |/| | |||||
| * | fix modeling issue (Vundef for load outside of bounds) | David Monniaux | 2021-06-16 | 1 | -2/+7 |
| | | |||||
| * | Use qemu-6.0.0 for PPC as the 3.1.0 version shipping with the Debian in the ↵ | David Monniaux | 2021-06-12 | 1 | -2/+5 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | docker has buggy float Squashed commit of the following: commit 54d1983cd8d8551c28109a506a752a971897f4ed Author: David Monniaux <david.monniaux@univ-grenoble-alpes.fr> Date: Sat Jun 12 00:48:02 2021 +0200 sudo make install commit 49af5c63eff29a49f3cb466a6b6af44570d85352 Author: David Monniaux <david.monniaux@univ-grenoble-alpes.fr> Date: Sat Jun 12 00:43:17 2021 +0200 pixman commit d78ab98e5751dd3ae0299a3e8c271472ebd8bb63 Author: David Monniaux <david.monniaux@univ-grenoble-alpes.fr> Date: Sat Jun 12 00:36:30 2021 +0200 libglib commit 0808bf51be42b04c2db4ccc914633407c1309585 Author: David Monniaux <david.monniaux@univ-grenoble-alpes.fr> Date: Sat Jun 12 00:31:46 2021 +0200 don't show verbose untar commit 972c244c72d9a30fee41dc7cbcc3698a49b6cde6 Author: David Monniaux <david.monniaux@univ-grenoble-alpes.fr> Date: Sat Jun 12 00:30:32 2021 +0200 ninja-build commit a1c261d01abc1c62ea94d56cfc9cce90887db680 Author: David Monniaux <david.monniaux@univ-grenoble-alpes.fr> Date: Sat Jun 12 00:28:14 2021 +0200 install ninja commit 92990598283f624d598853851c3edb2650f45b4b Author: David Monniaux <david.monniaux@univ-grenoble-alpes.fr> Date: Sat Jun 12 00:25:17 2021 +0200 untar commit a225a0dcea26dd8888be535aa1aec4a58007679d Author: David Monniaux <david.monniaux@univ-grenoble-alpes.fr> Date: Sat Jun 12 00:20:32 2021 +0200 install wget first commit 3b2c30ab6a953bde9d09034d38c5919a9425163d Author: David Monniaux <david.monniaux@univ-grenoble-alpes.fr> Date: Sat Jun 12 00:17:09 2021 +0200 install recent qemu | ||||
| * | show qemu version | David Monniaux | 2021-06-11 | 1 | -0/+1 |
| | | |||||
| * | disable ppc partially | David Monniaux | 2021-06-11 | 1 | -2/+6 |
| | | |||||
| * | compile non yarpgen tests without -static; this should work | David Monniaux | 2021-06-11 | 1 | -4/+4 |
| | | |||||
| * | disable PPC64; can't link and don't know why | David Monniaux | 2021-06-11 | 1 | -2/+2 |
| | | |||||
| * | fix bad paths | David Monniaux | 2021-06-11 | 1 | -2/+2 |
| | | |||||
| * | don't use -static on ppc | David Monniaux | 2021-06-11 | 1 | -4/+4 |
| | | |||||
| * | path issues | David Monniaux | 2021-06-11 | 1 | -6/+6 |
| | | |||||
| * | add PPC to CI and remove ugly hack for qemu linker paths | David Monniaux | 2021-06-11 | 1 | -56/+62 |
| | | |||||
| * | Merge branch 'kvx-work' of ↵ | David Monniaux | 2021-06-11 | 1 | -39/+0 |
| |\ | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into kvx-work | ||||
| | * | remove filter file | Léo Gourdin | 2021-06-10 | 1 | -39/+0 |
| | | | |||||
| * | | Merge branch 'master' of https://github.com/AbsInt/CompCert into kvx-work | David Monniaux | 2021-06-11 | 2 | -3/+13 |
| |\ \ | | |/ | |/| | | | | fix for comments on x86-64 MacOS | ||||
| | * | x86 assembly: fix the comment delimiter for macos and make it per-OS | Xavier Leroy | 2021-06-10 | 1 | -3/+11 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | As reported in #399, it seems better to use `##` instead of `#` as comment delimiter under macOS. For the time being we keep using `#` for Linux and Cygwin. Closes: #399 | ||||
| * | | push afadl test example | Léo Gourdin | 2021-06-09 | 2 | -0/+21 |
| | | | |||||
| * | | Merge branch 'kvx-work' of ↵ | Olivier Lebeltel | 2021-06-09 | 1 | -1/+1 |
| |\ \ | | | | | | | | | | | | | https://gricad-gitlab.univ-grenoble-alpes.fr/sixcy/CompCert into kvx-work | ||||
| | * | | comment is now ## due to some weird MacOS bug | David Monniaux | 2021-06-09 | 1 | -1/+1 |
| | | | | |||||
| * | | | added config_macos_x86_64.sh | Olivier Lebeltel | 2021-06-09 | 1 | -0/+1 |
| |/ / | |||||
| * | | MacOS compatibility | David Monniaux | 2021-06-09 | 1 | -1/+1 |
| | | | |||||
| * | | run CI on kvx-work-ssa kvx-work-velus | David Monniaux | 2021-06-08 | 1 | -49/+57 |
| | | | |||||
| * | | omega -> lia | David Monniaux | 2021-06-08 | 1 | -8/+8 |
| | | | |||||
| * | | coq 8.13.2 | David Monniaux | 2021-06-07 | 1 | -2/+1 |
| | | | |||||
| * | | division | David Monniaux | 2021-06-07 | 2 | -3/+4 |
| | | | |||||
| * | | timing | David Monniaux | 2021-06-07 | 2 | -0/+117 |
| | | | |||||
| * | | Merge branch 'kvx-work' of ↵ | David Monniaux | 2021-06-06 | 340 | -6016/+11801 |
| |\ \ | | | | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into kvx-work | ||||
| * | | | omega -> lia | David Monniaux | 2021-06-06 | 2 | -26/+28 |
| | | | | |||||
* | | | | Add option to set thresold and support for riscv | nicolas.nardino | 2021-06-17 | 4 | -2/+12 |
| | | | | |||||
* | | | | Now working, tests show a decrease in spillage | nicolas.nardino | 2021-06-16 | 2 | -59/+61 |
| | | | | | | | | | | | | | | | | | | | | Should still find a proper way to treat the case mentioned in earlier commits | ||||
* | | | | kinda fixed | nicolas.nardino | 2021-06-15 | 2 | -25/+57 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Spills are definitely reduced, but lots of arbitrary in there: See previous commit: need to determine what to do if pressure is too high but no schedulable instruction can reduce it. For now, advance time for at most 5 cycles, if still no suitable instruction, go back to CSP | ||||
* | | | | fixing | nicolas.nardino | 2021-06-15 | 4 | -53/+139 |
| | | | | | | | | | | | | | | | | | | | | Still need to find what to do when pressure is high but there are no instructions available that decrease it | ||||
* | | | | was very wrong, fixing | nicolas.nardino | 2021-06-14 | 5 | -20/+80 |
| | | | | |||||
* | | | | One fewer spill with new sched on `test/.../spille_forw.c` | nicolas.nardino | 2021-06-14 | 1 | -3/+50 |
| | | | | |||||
* | | | | scheduler written, need to test now | nicolas.nardino | 2021-06-14 | 2 | -18/+68 |
| | | | | |||||
* | | | | work on the scheduler | nicolas.nardino | 2021-06-12 | 4 | -41/+114 |
| | | | | |||||
* | | | | Work on new schedluer | nicolas.nardino | 2021-06-10 | 9 | -16/+165 |
| | | | | | | | | | | | | | | | | | | | | | | | | Renamed a test file, wrote function to compute pressure deltas, Still need to pass the info in some way; beginning of the actual scheduler function | ||||
* | | | | Fix RTLpathScheduleraux.get_live_regs_entry | nicolas.nardino | 2021-06-08 | 1 | -2/+3 |
| | | | | |||||
* | | | | Another test : one spill when scheduled forward, none if not | nicolas.nardino | 2021-06-08 | 1 | -0/+119 |
| | | | | |||||
* | | | | Add some tests | nicolas.nardino | 2021-06-08 | 4 | -3/+133 |
| | | | | |||||
* | | | | Adding debug info | nicolas.nardino | 2021-06-06 | 1 | -42/+53 |
| | | | | |||||
* | | | | Fixing scope error, and non-exhaustive pattern matching | nicolas.nardino | 2021-06-06 | 1 | -5/+6 |
| | | | | |||||
* | | | | function written, now needs testing | nicolas.nardino | 2021-06-05 | 1 | -10/+40 |
| | | | | |||||
* | | | | computing live regs at sb entry from its live output regs | nicolas.nardino | 2021-06-04 | 2 | -6/+24 |
| | | | | |||||
* | | | | Passing info of live regs to scheduler: beginning | nicolas.nardino | 2021-06-04 | 5 | -2/+17 |
| |/ / |/| | | |||||
* | | | Remove install path bricolage for kvxv3.9_kvx | Cyril SIX | 2021-06-01 | 2 | -4/+5 |
| | | |