From math to machine: translating a function to machine code (briansteffens.github.io)

108 points by briansteffens 9y ago ↗ HN

14 comments

[ 3.9 ms ] story [ 79.7 ms ] thread

LeanderK 9y ago ↗

out of interest, can somebody check how GHC compiles the factorial function as defined in the blogpost?

grenoire 9y ago ↗

Not GHC, but GCC 6.3 with -O2 is https://godbolt.org/g/ATkIr1 for reference.

rnhmjoj 9y ago ↗

https://gist.github.com/b097fded87a2b16863947acd3a975b2a

This is code produced by GHC 8.0.2 for the program

    module Test where
    factorial :: Int -> Int
    factorial n = product [1 .. n]

The module thing is necessary to produce the object file without a "main" function.

minimax 9y ago ↗

What calling convention passes the first integer argument in rax and the return value in rdi? Thats exactly backwards from what I usually see.

conistonwater 9y ago ↗

I wonder: since there are only thirteen factorials that fit into int32, and thus only 13 possible valid inputs, is it faster or slower to use a very small lookup table? https://godbolt.org/g/9ii0S0 It seems like this is the sort of thing a good compiler can figure out on its own, but I don't fully understand what clang is doing with this loop: https://godbolt.org/g/ze5ycb

bogomipz 9y ago ↗

This was neat. I enjoyed reading it. It wouldn't take much more to add the level below the machine code to this write up showing how the bits in the in the opcode generate control signals to carry out the micro-ops that make up the function.

nickpsecurity 9y ago ↗

I used to have a visual example of how it works. Couldn't find it in a quick search. Anyway, here's a text example for PDP-11 to illustrate what it looks like along with a detailed paper on concepts and some tooling.

http://www.cdf.toronto.edu/~ajr/258/notes/micro/microcode.ht...

http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.472...

bogomipz 9y ago ↗

Oh sure, I know. I was just staying it would be a nice addition, since the post is pretty original and novel. By the way was this the link you were thinking of?

https://cseweb.ucsd.edu/classes/wi13/cse141-b/slides/05-Sing...

By the they way second link is a nice read. Thanks.

nickpsecurity 9y ago ↗

People wanting to go from math to machine might like a work that starts with formal specs.

http://www.cl.cam.ac.uk/~mom22/miniml/hol2miniml.pdf

The resulting ML can be compiled to assembly by verified, CakeML compiler.

https://cakeml.org

iheartmemcache 9y ago ↗

It's only Monday and that paper lead me to L3 and the UNSW course[1] notes. There goes my next weekend or four. Thanks, ya son of a gun ;)

[1] https://www.cse.unsw.edu.au/~cs4161/lect.html

nickpsecurity 9y ago ↗

Glad you found something fun. If it's L3 for CPU's you mean, then one project of value nobody has done is put in specs for VAMP processor. It was mathematically verified in PVS as part of Verisoft project. They did OS and C subset for it. Adding it to L3 and Myreen et al's toolkit for doing machine code in Isabelle/HOL would let their spec-to-machine-code verifications run on a verified processor.

Just throwing that out there for you or anyone interested in lengthening the chain of verification. VAMP doesn't get enough attention. On HW side, someone could do a verified front-end for RISC-V on top of the VAMP components to get a mostly-verified RISC-V. Lots of low-hanging fruit out there.

pjmlp 9y ago ↗

Thanks as well, I join my opinion to iheartmemcache's one. :)

chmaynard 9y ago ↗

If the author is reading this thread, would you please comment on how math expressions are rendered in your blog? The factorial definition near the beginning looks absolutely perfect. I'd like to learn how to do this in Jekyll.

alevskaya 9y ago ↗

Not the author, but their page is using the client-side javascript MathJax renderer https://www.mathjax.org/ which renders the mathematical subset of LaTeX.