aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* add more debug infonicolas.nardino2021-07-081-2/+10
|
* Deactivate sched validator (i think)nicolas.nardino2021-07-081-10/+11
|
* Add debug infonicolas.nardino2021-07-061-0/+2
|
* Change temporary solution (see prev commits), and add option for itnicolas.nardino2021-06-283-4/+20
|
* Changed printfs into debugsnicolas.nardino2021-06-251-6/+5
|
* Another schedulernicolas.nardino2021-06-243-1/+204
|
* Merge branch 'kvx-sched-w-reg-press' of ↵nicolas.nardino2021-06-2216-86/+225
|\ | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into kvx-sched-w-reg-press
| * Merge branch 'kvx-sched-w-reg-press' of ↵David Monniaux2021-06-171-1/+2
| |\ | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into kvx-sched-w-reg-press
| * \ Merge branch 'kvx-sched-w-reg-press' of ↵David Monniaux2021-06-170-0/+0
| |\ \ | | | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into kvx-sched-w-reg-press
| * | | fix for Risc-VDavid Monniaux2021-06-172-0/+4
| | | |
| * | | Merge remote-tracking branch 'origin/kvx-work' into kvx-sched-w-reg-pressDavid Monniaux2021-06-1714-84/+221
| |\ \ \
| | * | | fix modeling issue (Vundef for load outside of bounds)David Monniaux2021-06-161-2/+7
| | | | |
| | * | | Use qemu-6.0.0 for PPC as the 3.1.0 version shipping with the Debian in the ↵David Monniaux2021-06-121-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 versionDavid Monniaux2021-06-111-0/+1
| | | | |
| | * | | disable ppc partiallyDavid Monniaux2021-06-111-2/+6
| | | | |
| | * | | compile non yarpgen tests without -static; this should workDavid Monniaux2021-06-111-4/+4
| | | | |
| | * | | disable PPC64; can't link and don't know whyDavid Monniaux2021-06-111-2/+2
| | | | |
| | * | | fix bad pathsDavid Monniaux2021-06-111-2/+2
| | | | |
| | * | | don't use -static on ppcDavid Monniaux2021-06-111-4/+4
| | | | |
| | * | | path issuesDavid Monniaux2021-06-111-6/+6
| | | | |
| | * | | add PPC to CI and remove ugly hack for qemu linker pathsDavid Monniaux2021-06-111-56/+62
| | | | |
| | * | | Merge branch 'kvx-work' of ↵David Monniaux2021-06-111-39/+0
| | |\ \ \ | | | | | | | | | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into kvx-work
| | | * | | remove filter fileLéo Gourdin2021-06-101-39/+0
| | | | | |
| | * | | | Merge branch 'master' of https://github.com/AbsInt/CompCert into kvx-workDavid Monniaux2021-06-112-3/+13
| | |\ \ \ \ | | | |/ / / | | |/| | | | | | | | | fix for comments on x86-64 MacOS
| | | * | | x86 assembly: fix the comment delimiter for macos and make it per-OSXavier Leroy2021-06-101-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 exampleLéo Gourdin2021-06-092-0/+21
| | | | | |
| | * | | | Merge branch 'kvx-work' of ↵Olivier Lebeltel2021-06-091-1/+1
| | |\ \ \ \ | | | | | | | | | | | | | | | | | | | | | https://gricad-gitlab.univ-grenoble-alpes.fr/sixcy/CompCert into kvx-work
| | | * | | | comment is now ## due to some weird MacOS bugDavid Monniaux2021-06-091-1/+1
| | | | | | |
| | * | | | | added config_macos_x86_64.shOlivier Lebeltel2021-06-091-0/+1
| | |/ / / /
| | * | | | MacOS compatibilityDavid Monniaux2021-06-091-1/+1
| | | | | |
| | * | | | run CI on kvx-work-ssa kvx-work-velusDavid Monniaux2021-06-081-49/+57
| | | | | |
| | * | | | omega -> liaDavid Monniaux2021-06-081-8/+8
| | | | | |
| | * | | | coq 8.13.2David Monniaux2021-06-071-2/+1
| | | | | |
| | * | | | divisionDavid Monniaux2021-06-072-3/+4
| | | | | |
| | * | | | timingDavid Monniaux2021-06-072-0/+117
| | | | | |
| | * | | | Merge branch 'kvx-work' of ↵David Monniaux2021-06-06340-6016/+11801
| | |\ \ \ \ | | | | | | | | | | | | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into kvx-work
| | * | | | | omega -> liaDavid Monniaux2021-06-062-26/+28
| | | | | | |
* | | | | | | Changed default threshold value following testsnicolas.nardino2021-06-222-9/+3
| |_|_|_|_|/ |/| | | | |
* | | | | | changed type of schedule_seq in x86 for compatibilitynicolas.nardino2021-06-171-1/+2
| |_|_|_|/ |/| | | |
* | | | | fix riscv/Machregsaux.mlinicolas.nardino2021-06-171-0/+2
|/ / / /
* | | | Add option to set thresold and support for riscvnicolas.nardino2021-06-174-2/+12
| | | |
* | | | Now working, tests show a decrease in spillagenicolas.nardino2021-06-162-59/+61
| | | | | | | | | | | | | | | | | | | | Should still find a proper way to treat the case mentioned in earlier commits
* | | | kinda fixednicolas.nardino2021-06-152-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
* | | | fixingnicolas.nardino2021-06-154-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, fixingnicolas.nardino2021-06-145-20/+80
| | | |
* | | | One fewer spill with new sched on `test/.../spille_forw.c`nicolas.nardino2021-06-141-3/+50
| | | |
* | | | scheduler written, need to test nownicolas.nardino2021-06-142-18/+68
| | | |
* | | | work on the schedulernicolas.nardino2021-06-124-41/+114
| | | |
* | | | Work on new schedluernicolas.nardino2021-06-109-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_entrynicolas.nardino2021-06-081-2/+3
| | | |