4 ms·

Not really. The 3439 page Intel® 64 and IA-32 Architectures Software Developer’s Manual is a specification. It just isn't a formal specification suitable for u

Not really. The 3439 page Intel® 64 and IA-32 Architectures Software Developer’s Manual is a specification. It just isn't a formal specification suitable for use in proving properties of programs. ARM on the other hand, released a machine readable architecture specification for ARMv8 but that architecture isn't as old or as large as x86_64. Nor is Intel/AMD in the business of selling architecture licenses where having a machine readable architecture specification would be useful for verifying implementations and proving properties. Indeed they're kind of in the business of preventing that from happening. https://alastairreid.github.io/ARM-v8a-xml-release/ https://alastairreid.github.io/ARM-v8a-xml-release/

schoen 8y ago
I was going to ask if you could then fuzz a physical CPU to find CPU bugs, but sure enough, the paper authors have already been doing that!
- jchw 8y ago
  There was a really good Blackhat talk a year or two ago in a sort of similar vein: they developed an approach to iterate and find undocumented opcodes. https://youtu.be/KrksBdWcZgQ https://youtu.be/KrksBdWcZgQ The software they developed is called Sandsifter.
  - xelxebar 8y ago
    Oh yeah. That's Christopher Domas, the same guy that built a functioning compiler that only emits MOV instructions [0] [1]. His other talks are quite interesting, as well! [0]:https://github.com/xoreaxeaxeax/movfuscator https://github.com/xoreaxeaxeax/movfuscator [1]:https://www.youtube.com/watch?v=2VF_wPkiBJY https://www.youtube.com/watch?v=2VF_wPkiBJY
johnbender 8y ago
Formal specifications aren't only useful for proving properties of programs. They can also be useful for providing definitive answers to questions about example program behavior which is useful for regular programmers. For example the Herd tool kit can take small concurrent programs with some constraints and a memory model and then answer whether any executions are possible. http://diy.inria.fr/doc/herd.html http://diy.inria.fr/doc/herd.html Alternately there is the online tool for the same purpose for ARMv8: https://www.cl.cam.ac.uk/~sf502/regressions/rmem/ https://www.cl.cam.ac.uk/~sf502/regressions/rmem/
userbinator 8y ago
Also, if the specification is too formal, no one besides academics would understand it and thus it would pretty useless as practical documentation.
- pcwalton 8y ago
  Right. Also, sometimes you want to leave things undefined. This killed the attempt to create a formal specification for ECMAScript 4 back in the day. For example, it was hard to formally specify things like "Array.sort calls the sorting order callback in such a way as to make the array sorted" without mandating a particular sorting algorithm.
  - sanxiyn 8y ago
    Maybe formal specification could have been done for the language but not for the standard library. Note that formal specification of ECMAScript 5 does exist (JSCert), although it is not de jure and it does not handle the standard library.
- StillBored 8y ago
  Which is why there is a 7000+ page ARM ARM https://static.docs.arm.com/ddi0487/da/DDI0487D_a_armv8_arm.pdf https://static.docs.arm.com/ddi0487/da/DDI0487D_a_armv8_arm.... which is mostly written in plain English for the common programmer, but frequently suffers due to lack of specificity or general clarity.

schoen 8y ago

I was going to ask if you could then fuzz a physical CPU to find CPU bugs, but sure enough, the paper authors have already been doing that!

jchw 8y ago
There was a really good Blackhat talk a year or two ago in a sort of similar vein: they developed an approach to iterate and find undocumented opcodes. https://youtu.be/KrksBdWcZgQ https://youtu.be/KrksBdWcZgQ The software they developed is called Sandsifter.
- xelxebar 8y ago
  Oh yeah. That's Christopher Domas, the same guy that built a functioning compiler that only emits MOV instructions [0] [1]. His other talks are quite interesting, as well! [0]:https://github.com/xoreaxeaxeax/movfuscator https://github.com/xoreaxeaxeax/movfuscator [1]:https://www.youtube.com/watch?v=2VF_wPkiBJY https://www.youtube.com/watch?v=2VF_wPkiBJY

johnbender 8y ago

Formal specifications aren't only useful for proving properties of programs. They can also be useful for providing definitive answers to questions about example program behavior which is useful for regular programmers. For example the Herd tool kit can take small concurrent programs with some constraints and a memory model and then answer whether any executions are possible. http://diy.inria.fr/doc/herd.html http://diy.inria.fr/doc/herd.html Alternately there is the online tool for the same purpose for ARMv8: https://www.cl.cam.ac.uk/~sf502/regressions/rmem/ https://www.cl.cam.ac.uk/~sf502/regressions/rmem/

userbinator 8y ago

Also, if the specification is too formal, no one besides academics would understand it and thus it would pretty useless as practical documentation.

pcwalton 8y ago
Right. Also, sometimes you want to leave things undefined. This killed the attempt to create a formal specification for ECMAScript 4 back in the day. For example, it was hard to formally specify things like "Array.sort calls the sorting order callback in such a way as to make the array sorted" without mandating a particular sorting algorithm.
- sanxiyn 8y ago
  Maybe formal specification could have been done for the language but not for the standard library. Note that formal specification of ECMAScript 5 does exist (JSCert), although it is not de jure and it does not handle the standard library.
StillBored 8y ago
Which is why there is a 7000+ page ARM ARM https://static.docs.arm.com/ddi0487/da/DDI0487D_a_armv8_arm.pdf https://static.docs.arm.com/ddi0487/da/DDI0487D_a_armv8_arm.... which is mostly written in plain English for the common programmer, but frequently suffers due to lack of specificity or general clarity.