guix-devel
[Top][All Lists]
Advanced

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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


From: jeremiah
Subject: Re: Trustworthiness of build farms (was Re: CDN performance)
Date: Sat, 05 Jan 2019 20:15:32 +0000

> In other words, it's anecdotal.
True, it definitely was not a formal proof just data based upon real
world development with large teams of programmers and formal
specifications for correct behavior.

> Obviously, the flaw in this argument is that there exist much more
> efficient ways to add numbers than counting beads.  A claim of
> complexity doesn't mean anything unless you can prove that it's a lower
> bound.
I don't deny that there are possibly lower bounds for the work, rather
that is the observed values from large teams doing that development are
what I have available to share.

> There's a reason that I followed my call for bug-free compilers with the
> claim: "In practice, this requires provably correct compilers."  I wrote
> that because I know that it's the only known practical way to do it for
> non-trivial languages.
Perfection is a road, not a destination.
One requires a "provabily correct compiler" to bootstrap a "provabily
correct compiler". A step completely skipped.

> Interesting.  I hadn't heard of those.  Can you cite the details?
One the most obvious is the float size definition and rounding behavior
on x86 hardware. The C standard requires rounding towards even, IEEE
only supports rounding towards infinity, negative infinity and zero. The
C standard allows floats to be expanded (to 80bits) but IEEE doesn't as
it can change the stability of some algorithms.


> Right, which shows the problems with depending on unverified components,
> but CompCert is no longer the state of the art in this regard.
It goes deeper than that.

> In contrast, the CakeML compiler not only produces raw machine code,
> moreover the proofs apply to the raw machine code of the CakeML compiler
> itself.  As a result, the only trusted specifications are those of the
> source language and of the underlying machine code behavior (for the
> subset of instructions that are actually generated).
So either CakeML must refuse to compile valid code or will generate
invalid binaries or both.

> I agree that IEEE floating point (and more generally inexact arithmetic)
> is a problem, but a great many useful programs can be written without
> using them, including most (if not all) of the programs that are most
> important for us to trust.  Operating systems, compilers, editors, and
> communication tools such as chat clients and mail readers, have no need
> for inexact arithmetic.  These are the programs I care most about.
Aside from the compilers that janneke and I have written, no other real
world compilers don't depend upon floating point; why do you think
janneke spent so many hours adding floating point to Mescc?
Try to build Linux without floating point support, it can't be done.
To to build emacs or vim without floating point support in your
compiler.

The reason is simple: Math libraries abuse it for performance and
performance is the only metric most people care about.

The Countless sins of our Industry exit because of those cursed words.

> Why do you include garbage collection in this list?  I consider garbage
> collection to be a _requirement_ for human model first behavior.  Do you
> consider it a hindrance?  Also, multiple verified garbage collectors
> already exist, e.g. those used in the runtimes of CakeML and Jitawa.
Find me one Enterprise grade Operating system that isn't a Lisp machine
that includes garbage collection at the native level.

> I think it's too ambitious to target non-programmers, because they do
> not have the required skills to understand the behavior of complex
> programs, regardless of what language is used.  They could perhaps
> understand toy programs, but that's not useful for helping them evaluate
> the trustworthiness of the computing tools they actually use, which is
> what I'm interested in.
Fair preference to have

> Anyway, what language(s) would you consider to be superior to ML or a
> subset of Scheme, based on the goal of human model first behavior?
As much as I hate to admit it but C# and Go tend to be far easier for
most people new to programming. Not that I would ever claim they are
superior languages in any technical sense.

> Would you consider your low-level macro languages to be better suited to
> this task?
Oh no, it exists solely to create a floor for bootstrapping ease and
simplify the problem of cross-platform bootstrap verification.

> I might agree that such simple assembly-like languages are more
> straightforward for understanding the behavior of toy programs, where
> one can keep all of the moving parts in one's head.  However, I would
> argue that those desirable properties of assembly-like languages do not
> scale to larger programs.
A self-hosting C compiler isn't exactly a toy program and if you read
it's code, you'll quickly discover there is no need to keep very much in
one's head at all.

It's real weakness is it's type system and lack of runtime.

One must remember a language's greatest strength is also it's greatest
weakness as well. Every desired feature must be paid for, usually in
regards to other desired features.

Performance, correctness and ease of development.
Pick one (the Industry picked Performance)

Things that should have been done differently if correctness was the
goal:
Hardware support for typed memory
Hardware support for garbage collection
Hardware support protecting against memory corruption (ECC, rowhammer
resistence circuits and SRAM instead of DRAM)
Barrel processor architectures (No risk from Spectre, Meltdown or
Raiden)
Hardware Capability tagging of processes
Flatten virtualization down to user processes.
Stack space and Heap Space different from each other and Program space.
Atleast a single attempt in the last 60 years from any military on the
planet to deal with the risks written in the Nexus Intruder Report
published in 1958.

I could spend literal weeks ranting and raving about modern hardware
makes correctness impossible for all but the trivial or the so isolated
from the hardware that performance makes it a non-starter for anything
but journal articles which are never read and forgotten within a
generation.

-Jeremiah



reply via email to

[Prev in Thread] Current Thread [Next in Thread]