aboutsummaryrefslogtreecommitdiffstats
path: root/scheduling
Commit message (Expand)AuthorAgeFilesLines
...
| * | | prove fsem2cfgsem_ibistep_simuSylvain Boulmé2021-05-311-19/+13
| * | | 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
| |\ \ \ \
| * | | | | 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-05-20 02:31:16 +0000