[TUHS] In Memoriam: Per Brinch Hansen

Perry E. Metzger perry at piermont.com
Mon Aug 6 09:18:18 AEST 2018


On Thu, 02 Aug 2018 08:44:56 -0400 Doug McIlroy
<doug at cs.dartmouth.edu> wrote:
> A tangential connection to early Unix experience:
> 
> My collection of early computer manuals includes Brinch Hansen's
> manual for the RC 4000, which stands out for its precise
> description of the CPU logic--in Algol 60! It's the only manual I
> have seen that offers a good-to-the-last-bit formal description of
> the hardware.
> 
> DEC presented something of the sort for the PDP-11, but punted where
> the woods got thick. When I wanted to know how they computed the
> last bit of floating-point results, I got no satisfaction. Amidst a
> thorough description of addressing came this formulation of the
> actual computation: "form floating point result".

For those that are familiar with the RISC V architecture, there's a
formal specification of the architecture that was done in a system
built on Coq, and also a fully formally verified translation of the
specification into RTL. (The spec didn't include floating point as of
about a year ago but it may by now.)

A good overview of the system involved is here:

http://plv.csail.mit.edu/kami/papers/icfp17.pdf

Followups might belong on the coff list, not sure.

Perry
-- 
Perry E. Metzger		perry at piermont.com



More information about the TUHS mailing list