Hello, I will briefly present you here two breakthroughs that we did for formally verified
compilers in Coq. A formally verified compiler is a compiler
with a proof of correctness. So, all the transformations have to be proven
correct. Our first breakthrough is to provide scalable
scheduling optimizations. A scheduling optimization is one where the
instructions are reordered. This kind of transformation is very hard to
prove structurally, so we split it into an untrusted oracle which gives us a schedule
proposition, and then we execute symbolically the returned schedule to check its correctness.
Our second contribution is that we are the first to target an interlocked VLIW processor,
that is, a processor with explicit instruction parallelism.
So here is a tiny example to introduce you the impact of scheduling.
In this example, we assume that the ADD and SUB have a latency of 1, and the LOAD has
a latency of 2. So we consider here a simple model, a 3 stage
pipeline. There is the DECODE stage, the EXEC1 stage
where ADD and SUB finish, and EXEC2 where LOAD finishes.
In this example, if we run the instructions in order, there will be a stall because of
the R3 register not being available. However, if we permute the instructions 2
and 1, we see that we win one cycle but there is no more stall.
In practice, our untrusted oracle has a bunch of resource constraints, and also latency
constraints which depend on both the processor latencies and the original program.
Then, to ensure that this scheduling is actually correct, we execute symbolically the original
code and the scheduled code, and we check that they are the same.
For architectures such as the Kalray processor, a bundle is a group of instructions that are
to be executed in parallel. In our work, we defined semantics for bundle
execution. And then we used a scheduling pass in order
to generate bundles into CompCert. So, our verifier works in two steps.
As mentionned earlier, the first step verifies the equivalence of the unordered and ordered
basic block. And then the last step verifies that each
bundle has the same execution between sequential and parallel semantics.
Finally, we give some performance comparisons. The top chart compares the performance of
the original code to the scheduler. Compared to the original version without any
scheduling we gain 40% in average, and compared to the greedy bundler we gain 20% in average.
The bottom chart compares CompCert to the GCC of Kalray.
Most safety critical applications use GCC without any optimization.
We can see that we always beat GCC -O0 by a large margin.
We also beat GCC -O1 most of the time. As for -O2 and -O3, we are not there yet,
but we are getting closer. In order to further bridge the gap, we are
currently working on superblock scheduling before register allocation.
I'm going to demonstrate the CompCert compiler and our optimizations on a simple example.
We are going here to see an example of a matrix multiplication.
So this is the very simple code that performs the matrix multiplication.
We are going to compile it, and we are then going to execute it and measure the amount
of cycles. Now we will run CompCert on the example without
any postpass optimization. So you will see the actual original code.
So here is the code from the innermost loop - that one.
That code isn't optimal at all because we only have one instruction per bundle.
And also we have some stalls in the pipeline. For example we have this multiply-add here
that takes two cycles, except that we issue a load on the cycle right after.
So that makes for a very suboptimal performance. If we try to run it, we get this amount of
cycles.
Now we will try to run CompCert with the first version of the scheduler, which will just
pack instructions together into bundles. On this example, the oracle packed together
some instructions, and the verificator verified that this is actually correct.
This will give a better performance, however we still have issues with stalls as you can
see here. We can try to run it.
And we see we are slightly better, but it could still be improved.
So now let's try to re-order the instructions with our list scheduler.
Here is the result. We can see that a lot of instructions have been moved, which result
in a much more efficient code. In particular, we can execute four instructions
at the same time on the same bundle. Now if you run that example, we can see we
have a much better performance than before.
Thanks for your attention.