Commit message (Expand) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | - make non trapping loads in scheduling dependent on option (which was ignore... | David Monniaux | 2021-09-14 | 1 | -1/+1 |
* | fix compil for coq 8.13.2 | Léo Gourdin | 2021-09-02 | 1 | -2/+1 |
* | cleanup | Léo Gourdin | 2021-09-01 | 14 | -8415/+1 |
* | Merge remote-tracking branch 'origin/kvx-work' into kvx-work | Léo Gourdin | 2021-09-01 | 1 | -6/+12 |
|\ | |||||
| * | Merge remote-tracking branch 'origin/kvx-sched-w-reg-press' into kvx-work | David Monniaux | 2021-08-23 | 1 | -6/+12 |
| |\ | |||||
| | * | Changes heuristic for case "no instruction decreases pressure" | nicolas.nardino | 2021-07-28 | 1 | -9/+12 |
* | | | [MERGE] BTL into kvx-work (replacing RTLpath) | Léo Gourdin | 2021-09-01 | 23 | -95/+8911 |
|\ \ \ | |/ / |/| | | |||||
| * | | CI fix on arm | Léo Gourdin | 2021-08-02 | 1 | -2/+2 |
| * | | non-trapping loads fix | Leo Gourdin | 2021-08-02 | 1 | -3/+11 |
| * | | ci fix? | Léo Gourdin | 2021-07-28 | 3 | -25/+17 |
| * | | remove todos, clean | Léo Gourdin | 2021-07-28 | 7 | -143/+69 |
| * | | test ci2 | Léo Gourdin | 2021-07-27 | 1 | -3/+3 |
| * | | Merge branch 'BTL-SEimpl' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompC... | Léo Gourdin | 2021-07-27 | 1 | -12/+14 |
| |\ \ | |||||
| | * \ | Merge branch 'BTL-SEimpl' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompC... | Léo Gourdin | 2021-07-27 | 9 | -64/+103 |
| | |\ \ | |||||
| | * | | | prepass act | Léo Gourdin | 2021-07-27 | 1 | -12/+14 |
| * | | | | test non-trapping loads using CI... | Léo Gourdin | 2021-07-27 | 1 | -2/+93 |
| | |/ / | |/| | | |||||
| * | | | non trapping loads | Léo Gourdin | 2021-07-23 | 9 | -64/+103 |
| |/ / | |||||
| * | | nothing admitted !! | Léo Gourdin | 2021-07-22 | 2 | -17/+25 |
| * | | branches expansions support | Léo Gourdin | 2021-07-22 | 2 | -16/+17 |
| * | | expansions btl proofs | Léo Gourdin | 2021-07-21 | 4 | -8/+10 |
| * | | new expansion oracle for BTL | Léo Gourdin | 2021-07-20 | 3 | -4/+8 |
| * | | Fix compile on ARM/x86 backends | Léo Gourdin | 2021-07-20 | 3 | -217/+28 |
| * | | op simplify BTL intro | Léo Gourdin | 2021-07-20 | 1 | -9/+7 |
| * | | proof for symbolic simu, need to finish equiv_inputs | Léo Gourdin | 2021-07-20 | 3 | -23/+31 |
| * | | Finish implem proof, need to adapt scheduler proof | Léo Gourdin | 2021-07-19 | 3 | -113/+371 |
| * | | hrexec_correct1 | Léo Gourdin | 2021-07-08 | 1 | -25/+48 |
| * | | some progress in canonbuilding | Léo Gourdin | 2021-07-07 | 1 | -14/+106 |
| * | | symbolic_simu impl definitions | Léo Gourdin | 2021-07-07 | 1 | -47/+9 |
| * | | hrexec1 | Léo Gourdin | 2021-07-07 | 1 | -27/+81 |
| * | | progress in simulation test | Léo Gourdin | 2021-07-07 | 1 | -57/+250 |
| * | | Some advance, need to finish canonbuilding proofs | Léo Gourdin | 2021-07-06 | 1 | -13/+270 |
| * | | lemma on HC_set_reg | Léo Gourdin | 2021-07-05 | 2 | -52/+165 |
| * | | red_PTree lemmas | Léo Gourdin | 2021-07-01 | 2 | -10/+77 |
| * | | cbranch expanse | Léo Gourdin | 2021-06-30 | 1 | -0/+25 |
| * | | coercions and simplify | Léo Gourdin | 2021-06-30 | 2 | -3/+91 |
| * | | some advance | Léo Gourdin | 2021-06-30 | 1 | -14/+154 |
| * | | Starting symbolic execution implementation | Léo Gourdin | 2021-06-30 | 1 | -0/+314 |
| * | | BTLroadmap: combinaison liveness et invariants ? | Sylvain Boulmé | 2021-06-25 | 1 | -9/+47 |
| * | | update BTLroadmap | Sylvain Boulmé | 2021-06-24 | 1 | -5/+6 |
| * | | transf fct correct in BTL scheduler proof | Léo Gourdin | 2021-06-20 | 1 | -5/+5 |
| * | | finish main proof | Léo Gourdin | 2021-06-19 | 1 | -18/+128 |
| * | | lemma on eqregs? | Léo Gourdin | 2021-06-18 | 2 | -14/+7 |
| * | | finish RTLtoBTL proof | Léo Gourdin | 2021-06-18 | 1 | -2/+18 |
| * | | End of main scheduling proof | Léo Gourdin | 2021-06-18 | 3 | -59/+90 |
| * | | some advance, new section to simplify context from symbolic exec | Léo Gourdin | 2021-06-17 | 3 | -66/+151 |
| * | | some advance in sched proof | Léo Gourdin | 2021-06-15 | 1 | -24/+92 |
| * | | Preparation for scheduling proof, main lemmas ok | Léo Gourdin | 2021-06-14 | 4 | -16/+41 |
| * | | begin scheduler BTL proof | Léo Gourdin | 2021-06-14 | 2 | -5/+142 |
| * | | stub match_states | Sylvain Boulmé | 2021-06-11 | 1 | -1/+3 |
| * | | add hid in BTL_SEtheory: this avoids duplication of types (and should not be ... | Sylvain Boulmé | 2021-06-11 | 2 | -150/+157 |