Memory Model Verification at the Trisection of Software, Hardware, ISA (2017)

Memory Model Verification at the Trisection of Software, Hardware, ISA (2017)(arxiv.org)

6 points by supercasio 7 years ago | 3 comments

gumby 7 years ago |

The paper looks interesting (though I'm not sure how practical it is) but what prompts me to comment is the horrible neologism "trisection".

A "dissection" is to take apart (to transitively section, in other words). If it were to section something in two there would be only one "s". And even reading the paper, the word the authors should have used is good old "intersection".

supercasio 7 years ago | |

What do mean by practical? They find problems with the RISC-V MCM and also with the C11 -> Power and ARMv7 compiler mappings.

gumby 7 years ago | | |

That's a good question -- I should not have been so terse/flip. I agree they do find some interesting issues and that's why I liked the paper.

On the practicality side: If I read the paper correctly this is a lint like tool for finding suspected problems (hence e.g. the "litmus tests" -- the tool iterates out the possible states, which is great). It isn't a tool for finding new problems. The compiler testing is interesting (I'm an former compiler guy) but reading Sec 7 didn't lead me to believe it could identify code generation problems in cases of very high optimizations.

Also a lot of recent security issues have been in the implementation of the microarchitecture (not just microcode bugs but functional unit errors such as the recent hyper threading leaks).

Maybe I am being too harsh?