Re: Trustworthiness of build farms (was Re: CDN performance)

[Mark H Weaver <mhw@netris.org>]

Hi Jeremiah,

Jeremiah@pdp10.guru writes:

>> To truly solve that problem, we need bug-free compilers.
> Impossible for all but the simplest of languages as the complexity of
> implementing a compiler/assembler/interpreter is ln(c)+a but the
> complexity of implementing a bug-free compiler/assembler/interpreter
> is (e^(c))! - a. Where a is the complexity cost of supporting it's
> host architecture.

Where are you getting those complexity expressions from?  Can you cite
references to back them up?  If not, can you explain how you arrived at
them?

What is 'c'?

>> In practice, this requires provably correct compilers.
> Which in practice turn out *NOT* to be bug free nor complete in regards
> to the standard specification.

If you're referring to the bugs found in CompCert, the ones I know about
were actually bugs in the unverified parts of the toolchain.  In the
past, its frontend was unverified, and several bugs were found there.
Even today, it produces assembly code, and depends on an unverified
assembler and linker.

Bugs can also exist in the specifications themselves, of course.

However, in the areas covered by the proofs, the results are quite
dramatic.  For example, in the paper "Finding and Understanding Bugs in
C Compilers" by Xuejun Yang, Yang Chen, Eric Eide, and John Regehr,

  https://web.stanford.edu/class/cs343/resources/finding-bugs-compilers.pdf

the authors state on page 6:

     The striking thing about our CompCert results is that the middle-
  end bugs we found in all other compilers are absent.  As of early
  2011, the under-development version of CompCert is the only compiler
  we have tested for which Csmith cannot find wrong-code errors.  This
  is not for lack of trying: we have devoted about six CPU-years to the
  task.  The apparent unbreakability of CompCert supports a strong
  argument that developing compiler optimizations within a proof
  framework, where safety checks are explicit and machine-checked, has
  tangible benefits for compiler users

> Now, don't get me wrong; provably correct
> compilers are a correct step in the right direction but the real
> solution is to first generate simplified languages that don't have
> undefined behavior and human model first behavior.

I'm not sure what "and human model first behavior" means, but if you
mean that the semantics of languages should strive to match what a human
would naturally expect, avoiding surprising or unintuitive behavior, I
certainly agree.  I consider Standard ML, and some subsets of Scheme and
Lisp, to be such languages.

>> Does that make sense?
> Absolutely, certainly something possible to do; but extremely human
> effort intensive and I don't see anyone willing to throw 2+ years of
> human effort at the problem outside of non-free Businesses like
> CompCert.

If I understand correctly, what you don't expect to happen has already
been done.  CakeML is free software, and formally proven correct all the
way down to the machine code.  Moreover, it implements a language with
an exceptionally clear semantics and no undefined behavior.

Anyway, you've made it fairly clear that you're not interested in this
line of work, and that's fine.  I appreciate the work you're doing
nonetheless.

     Regards,
       Mark