aboutsummaryrefslogtreecommitdiffstats
path: root/scheduling
Commit message (Expand)AuthorAgeFilesLines
* [MERGE] BTL into kvx-work (replacing RTLpath)Léo Gourdin2021-09-0123-95/+8911
|\
| * CI fix on armLéo Gourdin2021-08-021-2/+2
| * non-trapping loads fixLeo Gourdin2021-08-021-3/+11
| * ci fix?Léo Gourdin2021-07-283-25/+17
| * remove todos, cleanLéo Gourdin2021-07-287-143/+69
| * test ci2Léo Gourdin2021-07-271-3/+3
| * Merge branch 'BTL-SEimpl' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompC...Léo Gourdin2021-07-271-12/+14
| |\
| | * Merge branch 'BTL-SEimpl' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompC...Léo Gourdin2021-07-279-64/+103
| | |\
| | * | prepass actLéo Gourdin2021-07-271-12/+14
| * | | test non-trapping loads using CI...Léo Gourdin2021-07-271-2/+93
| | |/ | |/|
| * | non trapping loadsLéo Gourdin2021-07-239-64/+103
| |/
| * nothing admitted !!Léo Gourdin2021-07-222-17/+25
| * branches expansions supportLéo Gourdin2021-07-222-16/+17
| * expansions btl proofsLéo Gourdin2021-07-214-8/+10
| * new expansion oracle for BTLLéo Gourdin2021-07-203-4/+8
| * Fix compile on ARM/x86 backendsLéo Gourdin2021-07-203-217/+28
| * op simplify BTL introLéo Gourdin2021-07-201-9/+7
| * proof for symbolic simu, need to finish equiv_inputsLéo Gourdin2021-07-203-23/+31
| * Finish implem proof, need to adapt scheduler proofLéo Gourdin2021-07-193-113/+371
| * hrexec_correct1Léo Gourdin2021-07-081-25/+48
| * some progress in canonbuildingLéo Gourdin2021-07-071-14/+106
| * symbolic_simu impl definitionsLéo Gourdin2021-07-071-47/+9
| * hrexec1Léo Gourdin2021-07-071-27/+81
| * progress in simulation testLéo Gourdin2021-07-071-57/+250
| * Some advance, need to finish canonbuilding proofsLéo Gourdin2021-07-061-13/+270
| * lemma on HC_set_regLéo Gourdin2021-07-052-52/+165
| * red_PTree lemmasLéo Gourdin2021-07-012-10/+77
| * cbranch expanseLéo Gourdin2021-06-301-0/+25
| * coercions and simplifyLéo Gourdin2021-06-302-3/+91
| * some advanceLéo Gourdin2021-06-301-14/+154
| * Starting symbolic execution implementationLéo Gourdin2021-06-301-0/+314
| * BTLroadmap: combinaison liveness et invariants ?Sylvain Boulmé2021-06-251-9/+47
| * update BTLroadmapSylvain Boulmé2021-06-241-5/+6
| * transf fct correct in BTL scheduler proofLéo Gourdin2021-06-201-5/+5
| * finish main proofLéo Gourdin2021-06-191-18/+128
| * lemma on eqregs?Léo Gourdin2021-06-182-14/+7
| * finish RTLtoBTL proofLéo Gourdin2021-06-181-2/+18
| * End of main scheduling proofLéo Gourdin2021-06-183-59/+90
| * some advance, new section to simplify context from symbolic execLéo Gourdin2021-06-173-66/+151
| * some advance in sched proofLéo Gourdin2021-06-151-24/+92
| * Preparation for scheduling proof, main lemmas okLéo Gourdin2021-06-144-16/+41
| * begin scheduler BTL proofLéo Gourdin2021-06-142-5/+142
| * stub match_statesSylvain Boulmé2021-06-111-1/+3
| * add hid in BTL_SEtheory: this avoids duplication of types (and should not be ...Sylvain Boulmé2021-06-112-150/+157
| * Roadmap: precision sur le cout de verification des superblocksSylvain Boulmé2021-06-111-2/+9
| * Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int...Sylvain Boulmé2021-06-114-39/+43
| |\
| | * Merge branch 'kvx-work' into BTLLéo Gourdin2021-06-104-39/+43
| | |\
| * | | proving the remaining lemma for sexec_rec_okpreservSylvain Boulmé2021-06-111-123/+162
| |/ /
| * | theorem rexec_simu_correctSylvain Boulmé2021-06-101-25/+111
| * | fix rst_simu_correctSylvain Boulmé2021-06-101-27/+21
generated by cgit (git 2.34.1) at 2024-06-02 18:51:51 +0000