aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* merge VLIW proofsDavid Monniaux2019-03-2813-1551/+1113
|\ | | | | | | Merge branch 'mppa-mul' into mppa-ternary
| * merge proof of VLIWDavid Monniaux2019-03-288-24/+1074
| |\ | | | | | | | | | Merge branch 'mppa_postpass' into mppa-mul
| | * Merge remote-tracking branch 'origin/mppa_vliw_essai_sylvain' into mppa_postpassDavid Monniaux2019-03-2810-75/+1072
| | |\
| | | * 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-204-17/+30
| | | |
| | | * 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
| | | |
| * | | some more ternaryDavid Monniaux2019-03-241-6/+6
| | | |
| * | | experiments with ternary operatorDavid Monniaux2019-03-241-1/+6
| | | |
| * | | experiments with ternaryDavid Monniaux2019-03-244-1526/+36
| | | |
| * | | another ternary implementationDavid Monniaux2019-03-241-1/+7
| | | |
* | | | don't penalize x86 CompCertDavid Monniaux2019-03-271-1/+1
| | | |
* | | | put both compilers in their best moodDavid Monniaux2019-03-271-5/+18
| | | |
* | | | switch off ternary if not CompCertDavid Monniaux2019-03-271-14/+4
| | | |
* | | | improvements on cmoved etc.David Monniaux2019-03-273-97/+18
| | | |
* | | | work on ternaryDavid Monniaux2019-03-272-8/+21
| | | |
* | | | hand optimizedDavid Monniaux2019-03-272-0/+3271
| | | |
* | | | match some 'and'David Monniaux2019-03-274-14/+50
| | | |
* | | | essai du cmoveDavid Monniaux2019-03-273-3/+30
| | | |
* | | | selectl generationDavid Monniaux2019-03-266-14/+205
| | | |
* | | | ternary transfoDavid Monniaux2019-03-262-1/+37
| | | |
* | | | ternary unsignedDavid Monniaux2019-03-263-0/+54
| | | |
* | | | 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
| | | |
* | | | draft commentDavid Monniaux2019-03-251-0/+3
| | | |
* | | | some version of select/selectl that runs through ValueAOpDavid Monniaux2019-03-251-5/+32
| | | |
generated by cgit (git 2.34.1) at 2024-07-11 19:45:42 +0000