|
|
|
|
|
|
by grumblenum
1811 days ago
|
|
|
>I imagine it's pretty similar to how you verify or audit the output of a compiler with a specification. I must be missing the humor here. You can test against a specification to verify implementation. Testing an implementation against itself is meaningless. I would think that this is obvious. Also I don't typically use the word "empirical" to indicate purely qualitative assessments or intuition. You also provided a dead link. |
|
|
There's no attempt at humor here - I'm just trying to get you to explain what, precisely, you mean by "test against a specification to verify implementation" so that we're in agreement on terms.
When I hear "test against a specification" and "verify implementation," I think about things like CompCert. But the Linux kernel does not use CompCert, it uses GCC or Clang. To the best of my knowledge, neither is tested against a specification and neither has a verified implementation.
Actually, when we first started discussing mainlining this, we had a bit of discussion about whether it was safe to allow rustc-compiled Rust code to link against GCC-compled C code. The specific worry was potential compiler bugs, of which the kernel has historically run into many. We eventually decided the risk was low, but the kernel has gone through periods where it insisted you use the exact same compiler for the kernel and for modules because of bugs. Those bugs have gone away through the normal human process of writing better code, not through formal verification. And when they existed, the kernel's response was not to reject those compilers, it was to work around the bugs.
Also, CompCert does not test against the C standard, which is written in English prose. It tests against the CompCert developers' attempt to re-express the C standard in terms of machine-checkable theorems. The C standard is confusing even to human readers, so it would be misleading to say that CompCert has verified their compiler against the standard as published by the standards committee. (Hence my claim that they're similar; you can verify a compiler of any language provided you write your own machine-checkable statements about what you expect it to do, and you still need other humans to read those theorems and convince themselves that they're the right ones.)
For those reasons, I'm trying to understand what your question is in a precise manner. Are you asking about things like CompCert? Because if so, I don't follow the relevance to our work, though again, I'm happy to point you at interesting research.