4 ms·
Compcert is a verified compiler. It guarantees that the generated code does what the source code requires. It doesn't turn unsafe C programs into safe ones. "F
by roca 5y ago
Compcert is a verified compiler. It guarantees that the generated code does what the source code requires. It doesn't turn unsafe C programs into safe ones.
"Fail-Safe C" is a research project that has been dead for ten years. Note:
> Some benchmark results show that the execution time are around 3 to 5 times of the original, natively-compiled programs, in avarage
That overhead is actually a lot higher than similar projects I also consider failures, such as CCured.
To be clear, when we talk about "an alternative implementation of C", it needs to give similar performance and other properties (e.g. function and data interop) to other C compilers. You can't impose a 3-5x slowdown and say "look, C is safe".
- pjmlp 5y agoActually that is what Oracle did with SPARC ADI, Google/ARM are pushing for with MTE, Apple is trying to do with PAC, Microsoft with Phonon. When everything else fails, kill the bug with hardware memory tagging spray.
- h_anna_h 5y agoThe CompCert C reference interpreter aborts execution on undefined behavior. > To be clear, when we talk about "an alternative implementation of C", it needs to give similar performance and other properties (e.g. function and data interop) to other C compilers. You can't impose a 3-5x slowdown and say "look, C is safe". Pretty much every language (except rust) which claims to be "C but safe" has the same issue, except you have to rewrite your program in it.
- the_why_of_y 5y ago> The CompCert C reference interpreter aborts execution on undefined behavior. A C interpreter is not exactly the sort of thing that the embedded software industry has been waiting to deploy in production.