5 ms·
Half of what you mentioned doesn't come close to some of the research you see MSR publishing. The ones you mentioned are nice, but check out their papers. Some
by ktta 9y ago
Half of what you mentioned doesn't come close to some of the research you see MSR publishing. The ones you mentioned are nice, but check out their papers. Some of their papers are so outlandish (for the lack of a better word), that I doubt they can even find a proper conference/publication to submit them to.
The most surprised I've been was when they started using P lang for drivers (which is also used for verification, so your last two points fall under a single point if I'm not wrong). This was the first time I've seen them using a new language/tool rather than make additions like the rest of the points you made. (Also FPGAs in their data centers but that's a different topic)
I'm not deriding their decision to do so, just an observation. Google's X does research which can possibly be an actual product, and I guess I expected Microsoft to do the same. Using such cutting-edge research and include it in their products might earn them cool points from HN, but I'd say the management is perfectly content with the numbers in front of them. OTOH, I doubt any manager is willing to take the blame if their initiative fails in a released product. Microsoft has enough bugs that people complain about as it is (refer to the front page submission about performance)
- pjmlp 9y agoSo I feel that I need to provide the background of the items I mentioned Research on ExtVOS: - .NET - generics for .NET - UWP based on COM (.NET was to be originally based on COM, not CLR which came to be due to Java's influence) By products of Singularity and Midori projects: - MDIL .NET AOT compiler for Windows 8 and .NET Native for UWP - async/await for .NET - Task Programming Library for .NET By products of DrawBridge and IronClad projects: - Pico-processes on Windows 10 - Secure kernel on Windows 10 - Hyper-V based containers By products of Dafney, Z3 and theorem proving research: - Driver verification framework using a theorem proving framework - The P language used for writing Windows 8 USB drivers
- ktta 9y agoLooks like I was wrong on multiple counts. Thanks for taking the time. Any links on the driver verification framework? I've only seen people talk about using z3 for hardware verification but didn't know about MS doing it and talking about it publicly (could only find this: https://pdfs.semanticscholar.org/b100/b1562ba0e75191d29d4c15bfe4dc1d1f9c3b.pdf https://pdfs.semanticscholar.org/b100/b1562ba0e75191d29d4c15...)
- pjmlp 9y agoYes, here they are: "SMT in Verification, Modeling, and Testing at Microsoft" https://link.springer.com/chapter/10.1007%2F978-3-642-39611-3_3 https://link.springer.com/chapter/10.1007%2F978-3-642-39611-... "Efficient evaluation of pointer predicates with Z3 SMT Solver in SLAM2" https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/axioms.submitted.pdf https://www.microsoft.com/en-us/research/wp-content/uploads/... "Tools for Verifying Drivers" https://docs.microsoft.com/en-us/windows-hardware/drivers/devtest/tools-for-verifying-drivers https://docs.microsoft.com/en-us/windows-hardware/drivers/de...