aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
...
| | * | | | | improved testingDavid Monniaux2019-03-221-5/+16
| | | | | | |
| | * | | | | uses yarpgen random generatorDavid Monniaux2019-03-221-0/+37
| | | | | | |
| | * | | | | some more testingDavid Monniaux2019-03-221-1/+1
| | | | | | |
| | * | | | | Merge branch 'mppa-mul' into mppa-jumptableDavid Monniaux2019-03-22302-6460/+51288
| | |\ \ \ \ \
| | * | | | | | 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-215-8/+57
| | | | | | | |
| * | | | | | | missing config.hDavid Monniaux2019-03-291-0/+3
| | | | | | | |
| * | | | | | | Makefile for picosatDavid Monniaux2019-03-293-62/+0
| | |_|_|_|/ / | |/| | | | |
| * | | | | | ocaml benchmarkDavid Monniaux2019-03-283-8/+22
| | | | | | |
| * | | | | | MakefileDavid Monniaux2019-03-285-1025/+35
| | | | | | |
| * | | | | | NDEBUGDavid Monniaux2019-03-281-0/+6
| | | | | | |
| * | | | | | some more inlineDavid Monniaux2019-03-282-12/+13
| | | | | | |
| * | | | | | add some INLINE markersDavid Monniaux2019-03-281-36/+38
| | | | | | |
| * | | | | | picosat now uses the same Makefile system as the restDavid Monniaux2019-03-283-3/+49
| | | | | | | | | | | | | | | | | | | | | | | | | | | | we are 27% slower than gcc
* | | | | | | Merge branch 'mppa-ternary' of ↵David Monniaux2019-04-0213-1551/+1113
|\ \ \ \ \ \ \ | | |_|_|_|_|/ | |/| | | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-ternary
| * | | | | | 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
| | | | | | | |
* | | | | | | | script for creduceDavid Monniaux2019-03-291-0/+20
| | | | | | | |
* | | | | | | | bitsliced-tea slightly more efficient with ternaries at some placesDavid Monniaux2019-03-292-4/+18
|/ / / / / / /
* | | | | | | 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
| | | | | | |
generated by cgit (git 2.34.1) at 2024-07-14 04:49:55 +0000