From math to machine: translating a function to machine code | Hacker News Reader

From math to machine: translating a function to machine code

briansteffens.github.io

108 pointsbriansteffens14 comments

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

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

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

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.

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

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

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.

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...

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.

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.

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.

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

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

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.

Reply on news.ycombinator.com