From 5a7afabcca43984df4d052a7f2697d9ea34327a4 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Wed, 17 Jul 2019 15:44:50 +0200 Subject: README file --- test/monniaux/README.md | 127 +++++++++++++++++++++++++----------------------- 1 file changed, 67 insertions(+), 60 deletions(-) (limited to 'test/monniaux/README.md') diff --git a/test/monniaux/README.md b/test/monniaux/README.md index 1a4f8e9e..dbb3f337 100644 --- a/test/monniaux/README.md +++ b/test/monniaux/README.md @@ -1,64 +1,71 @@ -## Folders with just source code -- acswap -- bitfields -- crypto-algorithms -- des -- fill_buffer -- jumptable -- k1_builtins -- latency -- longjmp -- loop -- madd -- math -- memcpy -- multithreaded_volatile -- nand -- predicated -- regalloc -- rotate -- send_through -- sizeof -- slow_globals -- ternary_builtin -- tiny-AES-c -- uzlib -- varargs -- volatile -- xor_and_mat +# Benchmarking CompCert and GCC -## Special folders -- csmith -- jpeg-6b -- mbedtls -- quest -- yarpgen +rules.mk contains generic rules to compile with gcc and ccomp, with different +optimizations, and producing different binaries. It also produces a +measures.csv file containing the different timings given by the bench. -## Just to be compiled -- frame_pointer +Up to 5 different optimizations can be used. -## Benches to fix -- BearSSL : does not compile (to fix) -- ncompress : error on comparing -- ocaml : error during postpass scheduling -- micro-bunzip : -O3 buggy with gcc ? -- mod_int_mat : does not include rules.mk -- pcre2test : Trap MEMORY ACCESS VIOLATION sur le binaire ccomp -- picosat : compilation error : implicit declaration +To use this rule.mk, create a folder, put inside all the .c/.h source files, +and write a Makefile ressembling: +```make +TARGET=float_mat +MEASURES="c1 c2 c3 c4 c5 c6 c7 c8" -## Benches that work -- binary_search -- bitsliced-aes -- bitsliced-tea -- complex -- float_mat -- glibc_qsort -- heapsort -- idea -- number_theoretic_transform -- quicksort -- sha-2 -- tacle-bench-lift -- tacle-bench-powerwindow -- ternary -- too_slow +include ../rules.mk +``` + +This is all that is required to write, the rules.mk handles everything. + +There is the possibility to define some variables to finetune what you want. +For instance, `ALL_CFILES` describes the .c source files whose objects are +to be linked. + +Here is an exhaustive list of the variables: +- `TARGET`: name of the binary to produce +- `MEASURES`: list of the different timings. This supposes that the program +prints something of the form "c3 cycles: 44131" for instance. In the above +example, the Makefile would generate such a line: +``` +float_mat c3, 1504675, 751514, 553235, 1929369, 1372441 +``` +- `ALL_CFILES`: list of .c files to compile. By default, `$(wildcard *.c)` +- `CLOCK`: basename of the clock file to compile. Default `../clock` +- `ALL_CFLAGS`: cflags that are to be included for all compilers +- `ALL_GCCFLAGS`: same, but GCC specific +- `ALL_CCOMPFLAGS`: same, but ccomp specific +- `K1C_CC`: GCC compiler (default k1-cos-gcc) +- `K1C_CCOMP`: compcert compiler (default ccomp) +- `EXECUTE_CYCLES`: running command (default `k1-cluster` with some options) +- `GCCiFLAGS` with i from 0 to 4: the wanted optimizations. If one of these flags is empty, nothing is done. Same for `CCOMPiFLAGS`. For now, the default values: +``` +# You can define up to GCC4FLAGS and CCOMP4FLAGS +GCC0FLAGS?= +GCC1FLAGS?=$(ALL_GCCFLAGS) -O1 +GCC2FLAGS?=$(ALL_GCCFLAGS) -O2 +GCC3FLAGS?=$(ALL_GCCFLAGS) -O3 +GCC4FLAGS?= +CCOMP0FLAGS?= +CCOMP1FLAGS?=$(ALL_CCOMPFLAGS) -fno-postpass +CCOMP2FLAGS?=$(ALL_CCOMPFLAGS) +CCOMP3FLAGS?= +CCOMP4FLAGS?= + +# Prefix names +GCC0PREFIX?= +GCC1PREFIX?=.gcc.o1 +GCC2PREFIX?=.gcc.o2 +GCC3PREFIX?=.gcc.o3 +GCC4PREFIX?= +CCOMP0PREFIX?= +CCOMP1PREFIX?=.ccomp.o1 +CCOMP2PREFIX?=.ccomp.o2 +CCOMP3PREFIX?= +CCOMP4PREFIX?= +``` + +The `PREFIX` are the prefixes to add to the .s, .o, etc.. You should be careful that if a FLAGS is set, then the according PREFIX should be set as well. + +Assembly files will be generated in `asm/`, objects in `obj/`, binaries in `bin/` and outputs in `out/`. + +To compile and execute all the benches : `make` -- cgit