From math to machine: translating a function to machine code (opens in new tab)

(briansteffens.github.io)

108 pointsbriansteffens9y ago14 comments

14 comments

14 comments · 6 top-level

nickpsecurity9y ago· 3 in thread

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

iheartmemcache9y 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

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

pjmlp9y ago

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

bogomipz9y ago· 2 in thread

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.

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

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

LeanderK9y ago· 2 in thread

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

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

grenoire9y ago

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

chmaynard9y ago· 1 in thread

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.

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

conistonwater9y 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

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

j / k navigate · click thread line to collapse

14 comments

14 comments · 6 top-level

nickpsecurity9y ago· 3 in thread

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

iheartmemcache9y 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

nickpsecurity9y ago

pjmlp9y ago

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

bogomipz9y ago· 2 in thread

nickpsecurity9y ago

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

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

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

LeanderK9y ago· 2 in thread

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

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

grenoire9y ago

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

chmaynard9y ago· 1 in thread

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

conistonwater9y ago

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

j / k navigate · click thread line to collapse