aboutsummaryrefslogtreecommitdiffstats
path: root/scheduling
Commit message (Expand)AuthorAgeFilesLines
* BTL Scheduler oracle and some draftsLéo Gourdin2021-05-315-12/+91
* BTLroadmap: jumptableSylvain Boulmé2021-05-291-1/+1
* maj roadmapSylvain Boulmé2021-05-281-36/+32
* declare a checker for the symbolic simulationSylvain Boulmé2021-05-281-2/+13
* remove dupmap from BTL_Scheduler !Sylvain Boulmé2021-05-283-36/+22
* archi pour la verif du schedulerSylvain Boulmé2021-05-283-11/+82
* starting to extend RTLtoBTL with Liveness checking (on BTL side)Sylvain Boulmé2021-05-287-36/+98
* splitting BTL by introducing BTLmatchRTLSylvain Boulmé2021-05-286-634/+614
* fix some merge errorsLéo Gourdin2021-05-283-3/+4
* Merge branch 'BTL_fsem' into BTLLéo Gourdin2021-05-285-284/+840
|\
| * most of the proof BTL.fsem -> BTL.cfgsem.Sylvain Boulmé2021-05-284-46/+280
| * cleaning BTL_SEtheorySylvain Boulmé2021-05-272-190/+187
| * end of BTL_SEtheory w.r.t fsemSylvain Boulmé2021-05-273-182/+194
| * fix tr_sis definitionSylvain Boulmé2021-05-262-81/+132
| * avancement roadmapSylvain Boulmé2021-05-261-11/+28
| * fix Builtin semanticsSylvain Boulmé2021-05-252-37/+27
| * starting to experiment SE of fsemSylvain Boulmé2021-05-252-72/+232
| * improve fsemSylvain Boulmé2021-05-211-15/+30
| * update roadmapSylvain Boulmé2021-05-201-3/+10
| * defines fsem (aka functional semantics) of BTLSylvain Boulmé2021-05-204-19/+92
* | Improvements in scheduling and renumbering BTL codeLéo Gourdin2021-05-285-94/+65
* | Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int...Léo Gourdin2021-05-272-349/+302
|\ \
| * | simplification of normRTLSylvain Boulmé2021-05-251-67/+27
| * | Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int...Sylvain Boulmé2021-05-244-21/+231
| |\ \
| * | | tiny simplifications in RTLtoBTLproofSylvain Boulmé2021-05-242-349/+342
* | | | [disabled checker] BTL Scheduling and Renumbering OK!Léo Gourdin2021-05-2714-181/+348
| |/ / |/| |
* | | a draft frontend for prepassLéo Gourdin2021-05-244-21/+231
|/ /
* | Moving common tools, adding liveness input/output information to BTL generati...Léo Gourdin2021-05-247-50/+32
* | splitting is_expand property with a weak version for conditionsLéo Gourdin2021-05-232-78/+117
* | Now supporting Bnop insertion in conditionsLéo Gourdin2021-05-215-139/+135
* | Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int...Sylvain Boulmé2021-05-2013-165/+550
|\ \ | |/ |/|
| * working oracles (no renumber for now)Léo Gourdin2021-05-205-79/+144
| * Changing to an opaq record in BTL info, this is a broken commitLéo Gourdin2021-05-207-125/+141
| * Merge branch 'BTL' into BTL-translationLéo Gourdin2021-05-194-10/+9
| |\
| * | Adding a BTL record to help oraclesLéo Gourdin2021-05-197-165/+265
| * | Grouping common RTL functions, printer improvementLéo Gourdin2021-05-194-108/+26
| * | first oracle seems okLéo Gourdin2021-05-182-11/+15
| * | oracle simplification, BTL printer, and error msg specLéo Gourdin2021-05-183-97/+253
| * | First draft of the RTL2BTL oracleLéo Gourdin2021-05-181-4/+105
| * | todosLéo Gourdin2021-05-181-1/+1
| * | preparing compiler passes and ml oraclesLéo Gourdin2021-05-176-12/+37
* | | correction de l'idee de la Functional semanticsSylvain Boulmé2021-05-201-26/+17
| |/ |/|
* | Merge branch 'kvx-work' into BTLLéo Gourdin2021-05-193-8/+3
|\ \
| * | Compatibilité Coq 8.13David Monniaux2021-04-283-8/+3
* | | status updateLéo Gourdin2021-05-181-2/+6
| |/ |/|
* | finishing RTLtoBTLLéo Gourdin2021-05-173-42/+35
* | mib lemmaLéo Gourdin2021-05-171-26/+29
* | Lemmas on ISTEPLéo Gourdin2021-05-172-194/+127
* | Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int...Léo Gourdin2021-05-171-24/+61
|\ \
| * | fix roadmap on "Simulation modulo liveness"Sylvain Boulmé2021-05-121-24/+61
generated by cgit (git 2.34.1) at 2024-06-12 00:26:40 +0000