aboutsummaryrefslogtreecommitdiffstats
path: root/aarch64/PostpassSchedulingOracle.ml
Commit message (Expand)AuthorAgeFilesLines
* Make prepass scheduling sensitive to register pressure, by Nicolas Nardino.David Monniaux2021-07-161-0/+3
* Adding fp loads pairLéo Gourdin2021-01-201-4/+4
* Big improvment in peephole, changing LDP/STP semanticsLéo Gourdin2020-12-101-124/+69
* a first working draft on ldp/stp peepholeLéo Gourdin2020-12-041-3/+25
* Adding semantics for PldpLéo Gourdin2020-12-021-3/+16
* add option in scheduler to record bb sizeLéo Gourdin2020-11-301-0/+5
* Changing weights system at asmblock level instead of asmLéo Gourdin2020-11-301-240/+71
* Main part of postpasssch proof now completedLéo Gourdin2020-11-241-1/+5
* Postpass scheduling OKLéo Gourdin2020-11-181-146/+13
* Builtin mem spec in scheduler and some needed proof in Postpasssch.vLéo Gourdin2020-11-171-1/+1
* Remaining ctl insts except Pbuiltin (maps to error)Léo Gourdin2020-11-161-31/+45
* Loads and stores opLéo Gourdin2020-11-131-26/+35
* Arith inst OK for the verifierLéo Gourdin2020-11-121-6/+36
* Preparing the repo for debugging postpass and executing testsLéo Gourdin2020-11-061-4/+4
* set debug to false in oracleLéo Gourdin2020-11-051-1/+1
* A first (not well-tuned) working version of postpass scheduling for A64Léo Gourdin2020-11-051-714/+713
* Smart scheduler build problem and flatten solution OKLéo Gourdin2020-11-041-237/+245
* Dumb (identity) scheduling working and integratedLéo Gourdin2020-11-031-858/+753
* Preparation for postpass in aarch64 and refactoringLéo Gourdin2020-11-021-0/+1029
generated by cgit (git 2.34.1) at 2024-05-09 10:12:31 +0000