From bfc3ce4bda595be60915810c320be6c519ed3639 Mon Sep 17 00:00:00 2001
From: Antonin Reitz <antonin.reitz@inria.fr>
Date: Sat, 21 Oct 2023 01:44:03 +0200
Subject: [PATCH] cleaning: add proper README

+ remove useless code in Makefile
---
 Makefile  |   3 +-
 README.md | 125 ++++++++++++++++++++++++++++++++++++++++++++++++++----
 2 files changed, 118 insertions(+), 10 deletions(-)

diff --git a/Makefile b/Makefile
index 4bdb40ed..24e4d585 100644
--- a/Makefile
+++ b/Makefile
@@ -51,8 +51,6 @@ obj/%.krml:
 	$(Q)$(FSTAR) $(notdir $(subst .checked,,$<)) --codegen krml \
 	--extract_module $(basename $(notdir $(subst .checked,,$<)))
 
-ALL_MODULE_NAMES=$(basename $(ALL_SOURCE_FILES))
-
 # TODO: remove following hack:
 # add-include 'Steel_Spinlock:"steel_base.h"'
 # steel_base.h defines symbols required by Steel.ArrayArith
@@ -219,6 +217,7 @@ c/lib-alloc.c \
 #bench: testopt testocaml testcpp
 #	./bench/bench.sh
 
+#ALL_MODULE_NAMES=$(basename $(ALL_SOURCE_FILES))
 #ALL_C_FILES=$(addsuffix .c,$(ALL_MODULE_NAMES))
 #
 #$(ALL_C_FILES): extract
diff --git a/README.md b/README.md
index 0fb63f25..c3b6b21f 100644
--- a/README.md
+++ b/README.md
@@ -1,12 +1,121 @@
-# Steel Experiments
+# StarMalloc
 
-Some experiments as a F*/Steel beginner.
+A verified security-oriented general-purpose userspace memory allocator,
+that can be used as a drop-in replacement for the libc allocator.
+It is heavily inspired from hardened\_malloc's design.
 
-## StarMalloc
+The following symbols are/will be/will not be provided: except when explicitly mentioned, symbols are provided.
+1. as part of stdlib.h
+- malloc
+- calloc
+- realloc
+- free
+- aligned\_alloc (C11, TODO: check current implem)
+- free\_sized (C23, TODO: refine)
+- free\_aligned\_sized (C23, TODO: provide it)
 
-- `make test-slab`: small slab allocator test
-- `make test-mmap`: small large allocator (AVL+mmap) test
-- `make test-both`: small allocator test
-- `make lib`: `bench/starmalloc.so` compilation
+2. misc
+- posix\_memalign (POSIX, TODO: provide it)
+- malloc\_usable\_size (GNU)
+- memalign (?, TODO: provide it)
+- valloc (?, TODO: provide it)
+- (deprecated) pvalloc (GNU, TODO: provide it)
+- (deprecated) cfree (?, defined symbol as a fatal\_error, removed since glibc 2.26 (Debian oldoldstable glibc = 2.28, as of 2023-10-21))
 
-Working with quite complicated programs (e.g. zathura, a PDF viewer)... when compiled with clang
+## Build everything
+
+`bash setup-all.sh`:
+- build StarMalloc,
+- clone mimalloc-bench inside `extern/mimalloc-bench`,
+- build all of mimalloc-bench allocators + benches,
+- install StarMalloc within mimalloc-bench dir (`extern/mimalloc-bench/extern/st`),
+- tweaks mimalloc-bench.
+
+Then, lets bench StarMalloc against the system allocator (`sys`) and hardened\_malloc (`hm`) on all benches (`allt`).
+```
+cd extern/mimalloc-bench/out/bench
+bash ../../bench.sh sys hm st allt
+```
+
+## Build process
+
+Requirements:
+- z3 in the $PATH,
+- FSTAR\_HOME environment variable set to F* installation path,
+- STEEL\_HOME environment variable set to Steel installation path,
+- KRML\_HOME environment variable set to KaRaMeL installation path,
+- C compiler: clang or gcc.
+
+Steps with corresponding Makefile build targets:
+- verify: verification phase of F\*+Steel files, producing `obj/*.checked` files;
+- extract: extraction phase of F\*+Steel files, producing `obj/*.krml` files then `dist/` C files;
+- lib: produces `out/starmalloc.so`;
+- hardened\_lib: produces `out/h_starmalloc.so`.
+
+tl;dr:
+- `make lib hardened_lib -j $CORES` produces `out/*.so` files;
+- `OTHERFLAGS="--admit_smt_queries true" make lib hardened_lib -j $CORES` is faster, as no SMT query is sent to z3.
+
+## Some tests
+
+A few examples:
+- `make test-alloc`: sequential basic local test,
+- `make test-alloc2`: multithreaded basic local test,
+- `LD_PRELOAD=out/h_starmalloc.so zathura` was empirically a good test (requires the zathura PDF reader).
+
+## Benchmarks
+
+### mimalloc-bench
+
+[...]
+
+### WIP: Firefox
+
+[...]
+
+## Properties of the allocator
+
+Verified code:
+- functional correctness 1: malloc returns NULL or an array of at least the requested size
+- functional correctness 2: malloc returns a 16-bytes aligned array
+- memory safety
+- deadlock-free(?)
+
+C wrapper/low-level initialization:
+- based on hardened\_malloc's init, relies on atomic instructions to avoid race conditions
+- short, auditable
+- defensive programming
+
+## TODO
+- remove last assume (t\_of casts...)
+- replace last sladmits with proper fatal\_error stubs
+- pthread\_atfork hook
+- initial large memory mappings should have PROT\_NONE permissions
+- debug flag/distinct debug targets (remove -g as default compilation flag)
+- compilation flags
+  - limit visible symbols
+  - -fhardened flag: FORTIFY\_SOURCE, stack-clash protection, etc
+- use hacl-star libmemzero
+- C defensive programming:
+  - more memory-related errno checks wrt ENOMEM
+  - limit allocation size to PTRDIFF\_MAX (glibc behaviour)
+  - calloc: remove overflow risk
+  - fatal\_error if StarMalloc\_free fails
+- C++ stubs
+- remaining warnings using -Wall
+  - -Wlogical-op-parentheses: krml fix?
+  - -Wc++17-extensions (static\_assert with no message)
+  - -Wunused
+    - src/lib-alloc.c, free: replace init with enforce\_init
+    - src/lib-alloc.c, free: StarMalloc\_free returned value
+- benches
+  - fix mimalloc-bench/perf
+    - rptest: missing memalign symbol
+    - lua: bad-alloc, missing symbol?
+    - rocksdb: missing posix\_memalign symbol
+    - fix sh6bench/sh8bench exit statuses(?)
+  - fix mimalloc-bench/security
+  - large application: Firefox?
+  - HardsHeap?
+- cleaning
+  - remove