If you suspend your transcription on amara.org, please add a timestamp below to indicate how far you progressed! This will help others to resume your work!
Please do not press “publish” on amara.org to save your progress, use “save draft” instead. Only press “publish” when you're done with quality control.
This is an overview of the 6 year project to create (and publicly release) formal specifications of the Arm processor architecture.
The meat of the talk consists of the things I have done to make the specification correct:
- testing the specification with the test programs that Arm uses as part of the sign-off criteria for processors
- formally validating processor pipelines against the specification (which has the side-effect of finding bugs in the spec)
- formally verifying properties of the specification
- getting lots of different users - they all find different bugs
There are a lot of things that you can do with a formal specification: binary analysis, proving compilers or OSes correct, driving a superoptimizer, etc. so I hope that this will inspire the audience to go off and do something amazing with Arm's specification.
English: Finished