aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorCyril SIX <cyril.six@kalray.eu>2020-05-04 16:35:59 +0200
committerCyril SIX <cyril.six@kalray.eu>2020-05-04 16:35:59 +0200
commit9bb82668364d31dfff19b1d926fb5aebabae7a31 (patch)
tree7f0f435d93d347cc7b6865f5383802cb064c630b
parentc22a1828063756fdc11876993e6f1e2ca3bba04d (diff)
downloadcompcert-kvx-9bb82668364d31dfff19b1d926fb5aebabae7a31.tar.gz
compcert-kvx-9bb82668364d31dfff19b1d926fb5aebabae7a31.zip
README Kalray
-rw-r--r--README_Kalray.md32
1 files changed, 32 insertions, 0 deletions
diff --git a/README_Kalray.md b/README_Kalray.md
new file mode 100644
index 00000000..7516daa6
--- /dev/null
+++ b/README_Kalray.md
@@ -0,0 +1,32 @@
+# CompCert Kalray port
+The verified C compiler ported to Kalray.
+
+## Features
+
+This delivery contains (in addition to features from CompCert master branch):
+- A fully functional port of CompCert to Coolidge k1c VLIW core
+- Postpass scheduling optimization, only for k1c. Activated by default, it can be deactivated with the compiler flag `-fno-postpass`
+- Some experimental features that are work in progress:
+ - Slightly better subexpression eliminations, called CSE2 and CSE3. Both go through loops and feature a small alias analysis.
+ - `-fduplicate 0` to activate static branch prediction information. The branch prediction is basic, it annotates each `Icond` node by an `option bool`. A `Some true` annotation indicates we predict the branch will be taken. `Some false` indicates the fallthrough case is predicted. `None` indicates we could not predict anything, and are not sure about which control will be preferred.
+ - It is also possible to provide a number to perform tail duplication: `-fduplicate 5` will tail duplicate, stopping when more than 5 RTL instructions have been duplicated. This feature offers very variable performance (from -20% up to +20%) because of variations in the later register allocation phase that impacts the postpass scheduling. We intend to work on fine tuning the tail duplication phase once we have the prepass superblock scheduling.
+ - `-ftracelinearize` uses the branch prediction information to linearize LTL basic blocks in a slightly better way (in the `Linearize` phase).
+
+## Installing
+
+Please follow the instructions in `INSTALL.md`
+
+## Testing
+
+We modified most of the CompCert tests of the `c` folder in order for them to be executable in reasonable time by the simulator.
+
+To pass the testsuite, first, build and install CompCert using the instructions in `INSTALL.md`, then:
+```
+cd test/c
+make
+make test
+```
+
+The reference files were generated using `k1-cos-gcc -O1`.
+
+We also have our own tests in `test/mppa/` - to run them, execute the script `simucheck.sh` located in that folder. These consist in comparing `compcert` output to `k1-cos-gcc` output.