The Coq mailing list

[Chan Ngo <chan.ngo2203 AT gmail.com>]

Hello,

> On Jan 5, 2016, at 11:22 AM, Gabriel Scherer 
> <gabriel.scherer AT gmail.com>
>  wrote:
> 
> Note that there has already been work on verifying LLVM passes using a
> variant of your approach M2:
> 
>  Vellmv: Verifying the LLVM
>  Steve Zdancewic, Dmitri Garbuzov, William Mansky, Vivien Durey, Milo
> M. K. Martin, Jianzhou Zhao, Santosh Nagarakatte
>  2012-2015
>  http://www.cis.upenn.edu/~stevez/vellvm/
> 
> This project does not try to generate C++ code, it instead compiles
> and run the OCaml program extracted from Coq. I think this is a
> reasonable approach (using either inter-process communication of
> textual or binary IR representations, or even directly OCaml bindings
> to the LLVM machinery).
> 

Yes, thanks for the pointers. Somehow I already know these projects. However, 
you see that an interface between OCaml code and C++ code supported by LLVM 
is needed. In addition, developers cannot employ the full power of LLVM’s API 
provided. It is interesting and useful if there exists a toolchain that can 
at least provide a way to make specification of LLVM’s pass implementation in 
C++ and prove it is correct. Or it is better if it can allows developer to 
specify the pass he wants to build, then the toolchain generates the actual 
code (in the same way as Model-based development works) and the proof of 
correctness provided by Coq (somehow we can consider formally certified 
model-based development toolchain).

---
Chan Ngo
INRIA,
(+33)02 99 84 72 84
chan.ngo AT inria.fr
http://people.rennes.inria.fr/Chan.Ngo


> 
> On Tue, Jan 5, 2016 at 11:06 AM, Chan Ngo 
> <chan.ngo2203 AT gmail.com>
>  wrote:
>> Dear all,
>> 
>> Thanks for the references. The Herms’ thesis is exactly what I wanted to
>> point out in the previous emails.
>> 
>> This thread becomes interesting as on my side :-) By the way, I would like
>> to turn the subject a little bit but in the same track. We consider the 
>> LLVM
>> compiler, I assume that its core implementation is formally proved (e.g.,
>> some work based on translation validation for proving the correctness of 
>> the
>> compiler’s transformations and optimizations). Now, assume that I want to
>> develop a new “pass” (an optimization - in C++ and uses the data structures
>> and API functions provided by LLVM) for  LLVM and I want to make sure that
>> my pass implementation is formally proved. I end up with two methods below:
>> 
>> M1.
>> - Develop a translation module that translates my code in C++ to Gallina (I
>> think it is not easy task)
>> - Prove the correctness of this module
>> - Prove the correctness of the pass implementation based on the translated
>> Gallina in Coq (i.e., based on the tool like VST)
>> 
>> M2.
>> - Specify the pass implementation in Coq, meaning that somehow we define a
>> programming language with constructors coming from the data structures and
>> API functions in LLVM (i.e., the concept of Basic Block, Functions, Modules
>> in LLVM IR)
>> - Prove the correctness of the pass based on the above specification in Coq
>> (i.e., based on the tool like VST)
>> - Automatically generated the C++ code of the pass from Coq
>> 
>> How do you think about pros and cons of each methods?
>> 
>> Thanks,
>> 
>> ---
>> Chan Ngo
>> INRIA,
>> (+33)02 99 84 72 84
>> chan.ngo AT inria.fr
>> http://people.rennes.inria.fr/Chan.Ngo