aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c/PostpassScheduling.v
Commit message (Collapse)AuthorAgeFilesLines
* [BROKEN] Added parallelizability check - breaks all the conditional jumpsCyril SIX2019-03-121-1/+11
|
* No more axioms remaining (scheduling completely proven), however error at ↵Cyril SIX2019-03-051-53/+7
| | | | extraction
* No more axiom remaining in PostpassScheduling.v (but still a couple ↵Cyril SIX2019-03-051-33/+65
| | | | remaining in Asmblockdeps)
* 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 ↵Cyril SIX2018-12-171-0/+2
| | | | bundles
* 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-12 08:58:07 +0000