aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c
Commit message (Collapse)AuthorAgeFilesLines
...
| | * Finition de la preuve de AsmblockgenproofCyril SIX2019-03-291-2/+5
| | |
| * | Preuve de Jumptable dans Asmblockdeps.vCyril SIX2019-03-292-1/+24
| | |
| * | Merge remote-tracking branch 'origin/mppa_postpass' into mppa-jumptableCyril SIX2019-03-297-23/+1120
| |\ \ | | |/ | |/| | | | | | | | | | Conflicts: mppa_k1c/Asmblock.v mppa_k1c/Asmblockdeps.v
| | * No more AdmittedCyril SIX2019-03-291-55/+102
| | |
| * | Avancement dans la preuve du MBjumptableCyril SIX2019-03-291-1/+21
| | |
| * | FIX BUG in TargetPrinter (nandd immediate wrongly printed as andd)David Monniaux2019-03-221-1/+1
| | |
| * | Merge branch 'mppa-mul' into mppa-jumptableDavid Monniaux2019-03-2214-719/+123
| |\ \
| * | | Jump tables now work. There is still an "Admitted" subcase in a proof.David Monniaux2019-03-223-5/+15
| | | |
| * | | on avance sur la jumptableDavid Monniaux2019-03-222-3/+3
| | | |
| * | | jumptable avanceDavid Monniaux2019-03-221-1/+8
| | | |
| * | | Fixed proof of Asmblockdeps wrt PjumptableCyril SIX2019-03-221-25/+28
| | | |
| * | | begin jumptables (does not work)David Monniaux2019-03-214-3/+57
| | | |
* | | | merge VLIW proofsDavid Monniaux2019-03-287-23/+1073
|\ \ \ \ | | | | | | | | | | | | | | | Merge branch 'mppa-mul' into mppa-ternary
| * \ \ \ merge proof of VLIWDavid Monniaux2019-03-287-23/+1073
| |\ \ \ \ | | | |_|/ | | |/| | | | | | | Merge branch 'mppa_postpass' into mppa-mul
| | * | | Merge remote-tracking branch 'origin/mppa_vliw_essai_sylvain' into mppa_postpassDavid Monniaux2019-03-289-74/+1071
| | |\ \ \
| | | * \ \ Merge branch 'mppa_vliw_essai_sylvain' of ↵Sylvain Boulmé2019-03-272-67/+80
| | | |\ \ \ | | | | | | | | | | | | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_vliw_essai_sylvain
| | | | * | | Proof of the entire forward simulation (still stuck to do + permutations)Cyril SIX2019-03-271-3/+10
| | | | | | |
| | | | * | | Preuve du forward_simu du parexec_wio_bblock_auxCyril SIX2019-03-272-60/+70
| | | | | | |
| | | * | | | dealing with permutationsSylvain Boulmé2019-03-272-29/+100
| | | |/ / /
| | | * | | Avancement dans Asmblockdeps.vCyril SIX2019-03-272-91/+113
| | | | | |
| | | * | | 1 coup de pouce !Sylvain Boulmé2019-03-261-9/+29
| | | | | |
| | | * | | Un peu d'avancementCyril SIX2019-03-262-4/+287
| | | | | |
| | | * | | slight simplificationSylvain Boulmé2019-03-231-5/+4
| | | | | |
| | | * | | Avancement dans la preuve des bundlesCyril SIX2019-03-221-3/+51
| | | | | |
| | | * | | fix for Coq.8.8 ??Sylvain Boulmé2019-03-222-4/+3
| | | | | |
| | | * | | Décomposition de la preuve en une forward_simu_par_stuck et une ↵Cyril SIX2019-03-222-1/+72
| | | | | | | | | | | | | | | | | | | | | | | | forward_simu_par
| | | * | | simplification of the proofSylvain Boulmé2019-03-212-29/+70
| | | | | |
| | | * | | yet another step backwardSylvain Boulmé2019-03-201-18/+39
| | | | | |
| | | * | | one step further...Sylvain Boulmé2019-03-201-6/+28
| | | | | |
| | | * | | premier decoupageSylvain Boulmé2019-03-201-2/+56
| | | | | |
| | | * | | Integrating Asmvliw.v in the proof chainCyril SIX2019-03-203-16/+29
| | | | | |
| | | * | | Idée de preuve VLIWCyril SIX2019-03-181-2/+21
| | | | | |
| | | * | | fix the step_internal of AsmvliwSylvain Boulmé2019-03-141-19/+23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - Actually, we want to show that the outcome is the same for any order of "writes" in the parallel execution. (ie we ask that bundles have a deterministic semantics for parallel execution) - we relax the condition that the outcome should be given for sequential execution instead, we ask that the it is given for the "in order" writes. In theory, the semantics would also accept bundles like "R1 := R2 R2 := R1" which are deterministic for parallel execution But, of course, in practice, we will also prove the sequential execution.
| | | * | | definition of VLIW semanticsSylvain Boulmé2019-03-143-14/+342
| | | | | |
| | * | | | FIX BUG in TargetPrinter (nandd immediate wrongly printed as andd)David Monniaux2019-03-221-1/+1
| | | | | |
* | | | | | improvements on cmoved etc.David Monniaux2019-03-272-93/+7
| | | | | |
* | | | | | match some 'and'David Monniaux2019-03-272-10/+34
| | | | | |
* | | | | | selectl generationDavid Monniaux2019-03-266-14/+205
| | | | | |
* | | | | | ternary unsignedDavid Monniaux2019-03-262-0/+47
| | | | | |
* | | | | | rm cruftDavid Monniaux2019-03-262-167/+9
| | | | | |
* | | | | | cmoved worksDavid Monniaux2019-03-261-4/+5
| | | | | |
* | | | | | ternary / cmove demo now worksDavid Monniaux2019-03-261-2/+2
| | | | | |
* | | | | | ternary begins workingDavid Monniaux2019-03-262-13/+11
| | | | | |
* | | | | | some progressDavid Monniaux2019-03-262-19/+12
| | | | | |
* | | | | | implemented ternary patternDavid Monniaux2019-03-262-1/+57
| | | | | |
* | | | | | more on ternaryDavid Monniaux2019-03-262-6/+149
| | | | | |
* | | | | | select basic operatorsDavid Monniaux2019-03-261-0/+24
| | | | | |
* | | | | | selectlDavid Monniaux2019-03-252-0/+21
| | | | | |
* | | | | | more on cmoveDavid Monniaux2019-03-254-66/+42
| | | | | |
* | | | | | progress on cmoveDavid Monniaux2019-03-255-3/+17
| | | | | |
generated by cgit (git 2.34.1) at 2024-07-12 05:22:03 +0000