sidereal

The folks involved gave a neat talk about the verification techniques and tools they used as part of AWS Pi Week recently: https://www.twitch.tv/videos/951537246?t=1h10m10s

They're specifications in the K Framework, developed by the same group of folks: http://www.kframework.org/index.php/Main_Page

Before learning about Alloy*, you might want to learn about Alloy itself: http://alloy.lcs.mit.edu/alloy/index.html

Hillel Wayne has a great series of blog posts on using Alloy to solve software design problems: https://www.hillelwayne.com/tags/alloy/

Looks like A72. Here's the cpuinfo:

  processor	: 0
  BogoMIPS	: 166.66
  Features	: fp asimd evtstrm aes pmull sha1 sha2 crc32 cpuid
  CPU implementer	: 0x41
  CPU architecture: 8
  CPU variant	: 0x0
  CPU part	: 0xd08
  CPU revision	: 3

I cleaned up that text a little bit -- the 7700K doesn't draw the full 91W TDP when only a single core is loaded, as in this experiment.

It’s certainly possible, though it comes with a different set of challenges to software verification. Here’s a recent paper in this direction, proving the correctness of a RISC-V CPU: http://plv.csail.mit.edu/kami/papers/icfp17.pdf

Polyhedral optimisation is cool (Facebook has been using it to great effect for ML kernels recently [1]), but it’s not the end of the story. It’s complementary to this paper, which seems to be about learning an effective and transferrable cost model to guide the optimisation process (you could use that learned cost model in a polyhedral optimiser).

[1]: https://arxiv.org/abs/1802.04730

MSR also has Tony Hoare.

Today's branch predictors use ideas from machine learning: https://news.ycombinator.com/item?id=12340348

Running on a Zedboard is quite well documented; only took me a couple of hours to do it from scratch following their instructions: https://github.com/ucb-bar/fpga-zynq

Intel last year released a preview of their Control-flow Enforcement Technology instructions, which appear to implement these proposed extensions (shadow stack + indirect branch tracking): https://software.intel.com/sites/default/files/managed/4d/2a...