aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c/PostpassScheduling.v
Commit message (Expand)AuthorAgeFilesLines
* generalize bblock_equiv into bblock_simuSylvain Boulmé2019-05-071-7/+7
* seems to workDavid Monniaux2019-05-021-2/+4
* Merge remote-tracking branch 'origin/mppa_vliw_essai_sylvain' into mppa_postpassDavid Monniaux2019-03-281-3/+4
|\
| * simplification of the proofSylvain Boulmé2019-03-211-3/+4
* | Pseudo instruction for 32 bits division, no code generation yetCyril SIX2019-03-191-12/+13
|/
* [BROKEN] Added parallelizability check - breaks all the conditional jumpsCyril SIX2019-03-121-1/+11
* No more axioms remaining (scheduling completely proven), however error at ext...Cyril SIX2019-03-051-53/+7
* No more axiom remaining in PostpassScheduling.v (but still a couple remaining...Cyril SIX2019-03-051-33/+65
* Float conversion fixes + some more conversionsCyril SIX2019-02-271-1/+0
* Proving the trans_block_header axiomsCyril SIX2019-02-271-41/+7
* Plugged Asmblockdeps into PostpassSchedulingCyril SIX2019-02-251-552/+500
* PostpassScheduling: outcome' = option state'Cyril SIX2019-02-211-4/+4
* FIX axiom to be realized issueCyril SIX2019-02-151-2/+27
* Generalizing state' in PostpassSchedulingCyril SIX2019-02-141-32/+23
* More lemmas in PostpassSchedulingCyril SIX2019-02-141-6/+26
* Some more lemma proving in PostpassSchedulingCyril SIX2019-02-141-10/+73
* Proving verify_schedule_correct with axiomsCyril SIX2019-02-141-3/+132
* Minor refactorizationCyril SIX2019-02-121-0/+12
* Proof of axiom verified_schedule_headerCyril SIX2019-02-121-0/+133
* Proving the axiom verified_schedule_single_instCyril SIX2019-02-121-3/+35
* Proving verified_schedule_size axiomCyril SIX2019-02-111-11/+58
* Un peu de refactorisationCyril SIX2019-02-071-22/+65
* idee de refactoringSylvain Boulmé2019-01-311-24/+54
* Added a simple postpass oracle that splits a bblock into single instruction b...Cyril SIX2018-12-171-0/+2
* Generalizing PostpassScheduling to include bblock splittingCyril SIX2018-12-051-12/+18
* Added definitions and proof sketch for PostpassSchedulingCyril SIX2018-12-041-15/+19
* Tout début de développement d'un postpass Asmblock en CoqCyril SIX2018-12-031-0/+38
generated by cgit (git 2.34.1) at 2024-07-02 11:58:45 +0000