3 ms·

I have little systems programming experience, could someone explain to me what this does?

by teddyknox 12y ago

l_dopa 12y ago
It's a semantics for the intermediate representation used by most of the LLVM optimization passes defined in a theorem prover. With it you can, for example, write your own LLVM pass in Coq's specification language and prove that it can't introduce bugs by changing the meaning of a program. See also Compcert[1] and CakeML[2] for some other recent work in this area. [1] http://compcert.inria.fr/ http://compcert.inria.fr/ [2] https://cakeml.org/ https://cakeml.org/
exDM69 12y ago
Here's a dumbed down explanation. This actually isn't systems programming, this is compiler technology. It is an effort to prove that the LLVM compiler framework (or at least parts of it) work correctly. Proving here means formal verification, not too dissimilar from making a mathematical proof that something holds. Basically the idea is to look at the optimizations that the LLVM compiler performs and verify that the program after the optimization does the same thing as before optimization. It is easy to write compilers that emit fast code, but a lot harder to write compilers that emit fast and correct code.
- dspillett 12y ago
  > but a lot harder to write compilers that emit fast and correct code. The hard part is being confident you have correct code for all cases even the rare edge cases. Producing something that works for the happy path is easy. Producing something that works correctly for a wide range of input test conditions is more long winded but still not difficult. This sort of work is about mapping the inputs, assumptions, and outputs into a minimal (mathematical) form and using that to prove that for all cases the process correctly maps one to the other - to try prove that there can be no input for which the output is invalid.

3 ms·

I have little systems programming experience, could someone explain to me what this does?

by teddyknox 12y ago

I have little systems programming experience, could someone explain to me what this does?

l_dopa 12y ago
It's a semantics for the intermediate representation used by most of the LLVM optimization passes defined in a theorem prover. With it you can, for example, write your own LLVM pass in Coq's specification language and prove that it can't introduce bugs by changing the meaning of a program. See also Compcert[1] and CakeML[2] for some other recent work in this area. [1] http://compcert.inria.fr/ http://compcert.inria.fr/ [2] https://cakeml.org/ https://cakeml.org/
exDM69 12y ago
Here's a dumbed down explanation. This actually isn't systems programming, this is compiler technology. It is an effort to prove that the LLVM compiler framework (or at least parts of it) work correctly. Proving here means formal verification, not too dissimilar from making a mathematical proof that something holds. Basically the idea is to look at the optimizations that the LLVM compiler performs and verify that the program after the optimization does the same thing as before optimization. It is easy to write compilers that emit fast code, but a lot harder to write compilers that emit fast and correct code.
- dspillett 12y ago
  > but a lot harder to write compilers that emit fast and correct code. The hard part is being confident you have correct code for all cases even the rare edge cases. Producing something that works for the happy path is easy. Producing something that works correctly for a wide range of input test conditions is more long winded but still not difficult. This sort of work is about mapping the inputs, assumptions, and outputs into a minimal (mathematical) form and using that to prove that for all cases the process correctly maps one to the other - to try prove that there can be no input for which the output is invalid.