aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* rename parameterized versionsDavid Monniaux2021-07-162-38/+38
|
* make CSE3 condition parametricDavid Monniaux2021-07-162-29/+42
|
* rm condition parametrization in CSE3analysisDavid Monniaux2021-07-162-13/+6
|
* Make prepass scheduling sensitive to register pressure, by Nicolas Nardino.David Monniaux2021-07-1629-36/+2146
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Squashed commit of the following: commit cf033ec29391d5358dea1d3b25da1738957478c4 Author: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> Date: Fri Jul 16 18:01:03 2021 +0200 comment for authors commit 2ff766a18432fd75739abab0b5741ded6b67a2a5 Author: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> Date: Fri Jul 16 15:29:25 2021 +0200 activate register pressure by default commit 67f4ae2b702cc95ed7cef67b726e15abbf18e768 Author: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> Date: Fri Jul 16 15:26:03 2021 +0200 use a more recognizable option name commit 6121be54b80a55fdadd8b64dfad53357148c9090 Author: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> Date: Fri Jul 16 14:13:50 2021 +0200 fix for KVX commit 43d4932e8ba9e00eb8c8788c86f56b6bddd46392 Author: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> Date: Fri Jul 16 13:28:26 2021 +0200 setup registers commit 169a221104c37737f12abe79711009fc0d88ce09 Author: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> Date: Fri Jul 16 13:00:56 2021 +0200 rm useless code commit d6a846b641787ea6a5ed113b1d7275ffb5028d9c Author: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> Date: Fri Jul 16 12:54:19 2021 +0200 rm "Admitted" commit fd4d085aa988a6044f89fc17e8422be23bc87f9d Merge: 70f5867e 56498b64 Author: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> Date: Fri Jul 16 12:30:25 2021 +0200 Merge remote-tracking branch 'origin/kvx-work' into kvx-sched-w-reg-press commit 70f5867e441e253869cb3b432af77636a186d1cb Author: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> Date: Fri Jul 16 12:26:27 2021 +0200 rm TODO commit f86f5df47b69053702661671340b0fcb31506aa3 Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr> Date: Thu Jul 8 11:22:17 2021 +0200 add more debug info commit a4a0b36f56a94c19da301265a4e3acad1fbdf6c4 Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr> Date: Thu Jul 8 11:20:49 2021 +0200 Deactivate sched validator (i think) commit af97fca0f1d824f3becf9c6895f44ad234e262f8 Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr> Date: Tue Jul 6 15:32:35 2021 +0200 Add debug info commit b96a48de58e1969535865b7b345514a24f7178a6 Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr> Date: Mon Jun 28 16:04:44 2021 +0200 Change temporary solution (see prev commits), and add option for it commit 9ac49c465f9c8969fba00e6242da0c188a6a3080 Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr> Date: Fri Jun 25 09:42:41 2021 +0200 Changed printfs into debugs commit dfa09586ae40c70769eeda688a0e7f59f611749f Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr> Date: Thu Jun 24 18:33:20 2021 +0200 Another scheduler commit c5e8595480604c78260017cc771b0e4195fdd182 Merge: 10cbe4b2 cf2aa686 Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr> Date: Tue Jun 22 15:58:10 2021 +0200 Merge branch 'kvx-sched-w-reg-press' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into kvx-sched-w-reg-press commit 10cbe4b28ef6dc5d02c9a5d4d369484e4943a18d Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr> Date: Tue Jun 22 15:57:21 2021 +0200 Changed default threshold value following tests commit cf2aa686bcf9a823562fe977df6dd778d5467985 Merge: eddbce33 fe557bf6 Author: David Monniaux <david.monniaux@univ-grenoble-alpes.fr> Date: Thu Jun 17 17:05:30 2021 +0200 Merge branch 'kvx-sched-w-reg-press' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into kvx-sched-w-reg-press commit eddbce33e28c49bf7b9e83ebd5dbf6cb0d770090 Merge: 8f399dfa fae8d9b5 Author: David Monniaux <david.monniaux@univ-grenoble-alpes.fr> Date: Thu Jun 17 17:05:20 2021 +0200 Merge branch 'kvx-sched-w-reg-press' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into kvx-sched-w-reg-press commit 8f399dfa9d794f2f728f523ff1aa7788cc3599b2 Author: David Monniaux <david.monniaux@univ-grenoble-alpes.fr> Date: Thu Jun 17 17:04:52 2021 +0200 fix for Risc-V commit fe557bf65ec738eaa078bc5e398ff690eb1f2b9e Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr> Date: Thu Jun 17 17:03:53 2021 +0200 changed type of schedule_seq in x86 for compatibility commit fae8d9b5c5f93d5eda36f800eb0ca1837b237cba Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr> Date: Thu Jun 17 17:00:57 2021 +0200 fix riscv/Machregsaux.mli commit 9759e94256fd09f4995418b67b7aedbcf84b4b10 Merge: 4413c27d 04b2489d Author: David Monniaux <david.monniaux@univ-grenoble-alpes.fr> Date: Thu Jun 17 16:52:09 2021 +0200 Merge remote-tracking branch 'origin/kvx-work' into kvx-sched-w-reg-press commit 4413c27d6c6a3d69df34955d9d453c38b32174c7 Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr> Date: Thu Jun 17 15:38:13 2021 +0200 Add option to set thresold and support for riscv commit 21278bd87e89210bcc287116f6e35fc1b52d0df2 Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr> Date: Wed Jun 16 20:27:31 2021 +0200 Now working, tests show a decrease in spillage Should still find a proper way to treat the case mentioned in earlier commits commit 87c82b6fcf2bf825a8c60fc6a95498aac9f826d4 Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr> Date: Tue Jun 15 14:44:56 2021 +0200 kinda fixed 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 commit 19464b3992eadf7670acc7231896103ab54885e5 Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr> Date: Tue Jun 15 12:07:43 2021 +0200 fixing Still need to find what to do when pressure is high but there are no instructions available that decrease it commit bff4e6ff0b782619b6fcc18751fa575cbb11de68 Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr> Date: Mon Jun 14 17:39:58 2021 +0200 was very wrong, fixing commit 3eb3751f84348a20b7ce211fdbf1d01a9c4685a8 Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr> Date: Mon Jun 14 14:46:01 2021 +0200 One fewer spill with new sched on `test/.../spille_forw.c` commit 66e15205c40de54639387a4c9b1cc78994525d55 Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr> Date: Mon Jun 14 13:53:08 2021 +0200 scheduler written, need to test now commit 2b814b1f9bb30d9c8b59a713f69bced808bca7c7 Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr> Date: Sat Jun 12 10:52:59 2021 +0200 work on the scheduler commit 1701e43316ee8e69e794a025a8c9979af6bb8c93 Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr> Date: Thu Jun 10 16:31:51 2021 +0200 Work on new schedluer 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 commit 386b9053177bb4ef2801cec00b717c400a828139 Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr> Date: Tue Jun 8 16:53:19 2021 +0200 Fix RTLpathScheduleraux.get_live_regs_entry commit 9b6247b7996f3e0181d27ec0e20daffd28e0884f Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr> Date: Tue Jun 8 16:06:36 2021 +0200 Another test : one spill when scheduled forward, none if not commit 52378f0600652a94edcc8c78e4b426243f717a89 Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr> Date: Tue Jun 8 15:11:03 2021 +0200 Add some tests commit 2249f3c7771c285ccd25f6e94478be388a741da5 Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr> Date: Sun Jun 6 20:49:34 2021 +0200 Adding debug info commit 9118878bd14e24cc04c2f36cab7aa7271a0f1852 Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr> Date: Sun Jun 6 12:11:15 2021 +0200 Fixing scope error, and non-exhaustive pattern matching commit 599823a6410f1629f2b8704291839e0974bce83b Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr> Date: Sat Jun 5 19:52:59 2021 +0200 function written, now needs testing commit 98a7a04258f2cf6caf9f18925cbeeae2f5b17be4 Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr> Date: Fri Jun 4 16:56:32 2021 +0200 computing live regs at sb entry from its live output regs commit 7ae1fb0faea68ce5cfe04a232e49659247c244e9 Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr> Date: Fri Jun 4 14:24:07 2021 +0200 Passing info of live regs to scheduler: beginning
* adding mayundef resource_bounds (not changing perfs)Léo Gourdin2021-06-251-1/+2
|
* Replacing default notrap load value by Vundef everywherecsix-PhDCyril SIX2021-06-1821-49/+39
|
* 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
| * | Remove install path bricolage for kvxv3.9_kvxCyril SIX2021-06-012-4/+5
| | |
| * | Merge remote-tracking branch 'verimag/manuscript' into kvx-workCyril SIX2021-06-011-13/+11
| |\ \
| | * | Do not rotate if the CB was already at the end.Cyril SIX2021-04-281-1/+5
| | | |
| | * | Heuristic counter updateCyril SIX2021-04-281-12/+6
| | | |
| * | | Update INSTALL.mdCyril SIX2021-06-011-0/+6
| | | |
| * | | Fixing build for KVX (missing ccomp_kvx_fixes.h for runtime)Cyril SIX2021-06-011-0/+1
| | | |
| * | | Add target ELFCyril SIX2021-06-014-2/+7
| | | |
| * | | Merge remote-tracking branch 'absint/master' into kvx-workCyril SIX2021-06-013-4/+6
| |\ \ \ | | | |/ | | |/|
| | * | Support `# 0 ...` preprocessed line directiveXavier Leroy2021-06-011-1/+1
| | | | | | | | | | | | | | | | | | | | | | | | | | | | Before, the line number had to start with a nonzero digit. However, the GCC 11 preprocessor was observed to produce `# 0 ...` directives. Fixes: #398
| | * | Register X1 is destroyed by some built-in functionsXavier Leroy2021-05-132-3/+5
| | | | | | | | | | | | | | | | E.g. __builtin_bswap. Update Asm modeling of builtins accordingly.
| | * | Update for release 3.9Xavier Leroy2021-05-101-1/+1
| | | |
| | * | Update Changelog for release 3.9Xavier Leroy2021-05-091-0/+3
| | | |
| | * | Update for release 3.9Xavier Leroy2021-05-091-4/+5
| | | | | | | | | | | | | | | | Also: limit the max width of the page, to avoid very long lines.
| | * | Update ChangelogXavier Leroy2021-05-081-1/+11
| | | |
| | * | Use the LGPL instead of the GPL for dual-licensed filesXavier Leroy2021-05-08149-860/+1171
| | | | | | | | | | | | | | | | | | | | | | | | The GPL makes sense for whole applications, but the dual-licensed Coq and OCaml files are more like libraries to be combined with other code, so the LGPL is more appropriate.
| | * | Fix evaluation order in emulation of bitfield assignmentXavier Leroy2021-05-021-2/+2
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | A bitfield assignment `x.b = f()` is expanded into a read-modify-write on `x.carrier`. Wrong results can occur if `x.carrier` is read before the call to `f()`, and `f` itself modifies a bitfield with the same carrier `x.carrier`. In this temporary fix, we play on the evaluation order implemented by the SimplExpr pass of CompCert (left-to-right for side-effecting subexpression) to make sure the read part of the read-modify-write sequence occurs after the evaluation of the right-hand side. More substantial fixes will be considered later. Fixes: #395
| | * | Support __builtin_expectXavier Leroy2021-05-021-0/+5
| | | | | | | | | | | | | | | | | | | | | | | | | | | | Not yet used for optimizations. Actually, __builtin_expect is removed during C2C conversion, otherwise the conversion to type "long" produces inefficient code on 64-bit platforms.
| | * | Support __builtin_unreachableXavier Leroy2021-05-028-2/+32
| | | | | | | | | | | | | | | | Not yet used for optimizations.
| | * | Fix spurious error on initialization of struct with flexible array memberXavier Leroy2021-05-021-0/+3
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The following is correct but was causing a "wrong type for array initializer" fatal error. ``` struct s { int n; int d[]; }; void f(void) { struct s x = {0}; } ``` Co-authored-by: Michael Schmidt <github@mschmidt.me>
generated by cgit (git 2.34.1) at 2024-06-30 11:18:24 +0000