Disclaimer

The content of this blog is my personal opinion only. Although I am an employee - currently of Nvidia, in the past of other companies such as Iagination Technologies, MIPS, Intellectual Ventures, Intel, AMD, Motorola, and Gould - I reveal this only so that the reader may account for any possible bias I may have towards my employer's products. The statements I make here in no way represent my employer's position, nor am I authorized to speak on behalf of my employer. In fact, this posting may not even represent my personal opinion, since occasionally I play devil's advocate.

See http://docs.google.com/View?id=dcxddbtr_23cg5thdfj for photo credits.

Friday, April 20, 2012

Compiler: use and prove asm

Here's a compiler switch I would like to see:

  • Use the assembly code I give you (or some other forfm - RTL, transformed C code, etc.)
  • But you, Mr. Compiler, should do a formal equivalence proof
    • using various command line switches
    • heck, I can even sketch the steps of the proof.  But I want you, the compiler, to chedck it.
Reason: oftentimes I optimize code by
  1. Looking at compiler output
  2. Handwriting assembly
  3. Then trying to figure out compiler switches to cause the compiler to GENERATE this code.
Seems wasteful, since I already know the code that I want the compiler to generate.

It is often easier to verify equivalence of unoptimized and optimized form than it is to generate the optimized form.  Similarly, it is often easier to check a proof than it is to generate a proof.

Moreover, if you can specify code generation for just a small subset, then you can let the compiler do what it does well: the bookkeeping to connect that small subset to the rest of the world.


1 comment:

Paul A. Clayton said...

This is very similar to something I call overloading. From http://dandelion-watcher.blogspot.com/2012/04/nitpicking-on-no-silver-bullets-part-1.html :

«inability to use layered abstraction (e.g., providing a generic implementation of an operation with an optimized implementation that can "overload" the generic implementation with constraints [additional information] expressed so that the optimized implementation can be validated; furthermore optimized implementations could be provided as hints--"compiler, try this implementation"--or directives--"compiler, do it this way" and multiple implementations could be provided for different constraints--and the compiler might even use different implementations to generate a new implementation).»

Note that this is somewhat more general than your desired feature in that multiple specialized implementations could be provided with the same interface. It also extends your validating is easier than finding observation by proposing that the compiler could synthesize an implementation based on a limited set of examples.