sidereal
Joined 13 years ago
Karma
323
Submissions
22
Member since
Sep 2
Recent submissions
Comment · 5 years ago
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
Comment · 7 years ago
They're specifications in the K Framework, developed by the same group of folks: http://www.kframework.org/index.php/Main_Page
Comment · 7 years ago
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/
Comment · 8 years ago
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 : 3Comment · 8 years ago
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.
Comment · 8 years ago
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
Comment · 8 years ago
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).
Comment · 8 years ago
MSR also has Tony Hoare.
Comment · 9 years ago
Today's branch predictors use ideas from machine learning: https://news.ycombinator.com/item?id=12340348