aboutsummaryrefslogtreecommitdiffstats
path: root/scheduling
Commit message (Expand)AuthorAgeFilesLines
* Merge branch 'kvx-work' into BTLLéo Gourdin2021-06-104-39/+43
|\
| * Merge remote-tracking branch 'origin/kvx-work' into merge_master_8.13.1Cyril SIX2021-06-017-31/+24
| |\
| * | replacing omega with lia in some fileLéo Gourdin2021-03-294-39/+43
* | | theorem rexec_simu_correctSylvain Boulmé2021-06-101-25/+111
* | | fix rst_simu_correctSylvain Boulmé2021-06-101-27/+21
* | | remove historySylvain Boulmé2021-06-102-196/+121
* | | fix sstate_simuSylvain Boulmé2021-06-092-32/+35
* | | valid_pointer_preserv dans BTL_SEtheory => opportunites de *grosses* simplifi...Sylvain Boulmé2021-06-092-87/+42
* | | generalize nestedSylvain Boulmé2021-06-091-71/+74
* | | Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int...Sylvain Boulmé2021-06-081-28/+172
|\ \ \
| * | | End of liveness proofLéo Gourdin2021-06-071-54/+45
| * | | ugly complete version of liveness proof (I will clean in next commits)Léo Gourdin2021-06-071-34/+40
| * | | Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int...Léo Gourdin2021-06-073-27/+351
| |\ \ \
| * | | | advance for tr_input proofLéo Gourdin2021-06-071-24/+171
* | | | | preuve de rexec_rec_correct via les notions history/histOKSylvain Boulmé2021-06-081-41/+251
| |/ / / |/| | |
* | | | avancement ref de l'exe symboliqueSylvain Boulmé2021-06-072-26/+306
* | | | mSylvain Boulmé2021-06-061-1/+3
* | | | IDEE pour la STRENGTH-REDUCTIONSylvain Boulmé2021-06-061-1/+43
|/ / /
* | | Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int...Léo Gourdin2021-06-042-12/+115
|\ \ \
| * | | starting refinement of symbolic executionSylvain Boulmé2021-06-042-12/+115
* | | | preparation and starting final lemmaLéo Gourdin2021-06-041-21/+100
|/ / /
* | | Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int...Léo Gourdin2021-06-043-35/+77
|\ \ \
| * | | progress in BTL_SEsimurefSylvain Boulmé2021-06-043-35/+77
* | | | Some advance in Liveness lemmasLéo Gourdin2021-06-041-71/+138
|/ / /
* | | Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int...Léo Gourdin2021-06-032-109/+112
|\ \ \
| * \ \ Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int...Sylvain Boulmé2021-06-031-21/+112
| |\ \ \
| * | | | progress in BTL_SEsimurefSylvain Boulmé2021-06-032-109/+112
* | | | | update a more general version of the liveness checkerLéo Gourdin2021-06-031-93/+118
| |/ / / |/| | |
* | | | Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int...Léo Gourdin2021-06-022-176/+255
|\| | |
| * | | minor renamingSylvain Boulmé2021-06-021-9/+9
| * | | fix the definition of [symbolic_simu] in BTL_SEtheorySylvain Boulmé2021-06-022-172/+251
* | | | lemmas on entrypoint, tr_inputs, eqlive_regs, ...Léo Gourdin2021-06-021-21/+112
|/ / /
* | | Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int...Léo Gourdin2021-06-023-110/+416
|\ \ \
| * | | the current "high-level" specification of the simulation test will not work !Sylvain Boulmé2021-06-023-37/+124
| * | | starting BTL_SEsimurefSylvain Boulmé2021-06-012-99/+318
* | | | some advance in main liveness lemmasLéo Gourdin2021-06-021-28/+68
|/ / /
* | | Some others main lemmasLéo Gourdin2021-06-011-7/+33
* | | preparing liveness proof main theoremLéo Gourdin2021-06-011-2/+43
* | | Lemma liveness_checker_correctLéo Gourdin2021-06-011-0/+12
* | | Lemma list_iblock_checker_correctLéo Gourdin2021-06-011-0/+20
* | | Dupmap bugfix and some advance in LivegenLéo Gourdin2021-05-314-29/+89
* | | 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
generated by cgit (git 2.34.1) at 2024-06-11 17:37:47 +0000