3 ms·

The interesting this out of all this is that Microsoft is the one often doing research like this, from F*, Project Everest, to complete kernels, but I've yet to

by ktta 9y ago

The interesting this out of all this is that Microsoft is the one often doing research like this, from F*, Project Everest, to complete kernels, but I've yet to see Windows have any of the new techniques/tools arising from MSR. I wonder if it is a problem of the research being fairly new, or a lack of software developers inside Microsoft willing to replace their existing code and learn new tools and languages.

pjmlp 9y ago
Because you are not looking into the right spots: - Windows 7 kernel reorganization - MDIL .NET AOT compiler for Windows 8 and .NET Native for UWP - async/await for .NET - generics for .NET - UWP based on COM (original idea was called ExtVOS before .NET existed) - Task Programming Library for .NET - Pico-processes on Windows 10 - Secure kernel on Windows 10 - Hyper-V based containers - Driver verification framework using a theorem proving framework - The P language used for writing Windows 8 USB drivers I guess they just don't adopt more due to management, and how the windev and devtools relate to each other in regards to technology adoption.
- 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 ago
    So 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 ago
      Looks 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 ago
        Yes, 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...
- deleted 9y ago
  [deleted]
Blaisorblade0 9y ago
Until recently, MSR was also very disconnected from product development. There was a distinct change last year. Also, in general most papers are more useful for writing further papers to improve on their limitations (until something's great), than to be adopted right away. This one is pretty cool, but both the conclusion and the benchmarks set out significant challenges for further research. After all, this is the first OS using automated verification, not the last. > a lack of software developers inside Microsoft willing to replace their existing code and learn new tools and languages. I'm sure research on the topic hasn't ended, so should they switch now or wait for more research? Or wait for research on verifying existing code? And if a new paper comes out, should they switch again? Also, do universities train enough developers to use such technology?

by ktta 9y ago

pjmlp 9y ago

Because you are not looking into the right spots: - Windows 7 kernel reorganization - MDIL .NET AOT compiler for Windows 8 and .NET Native for UWP - async/await for .NET - generics for .NET - UWP based on COM (original idea was called ExtVOS before .NET existed) - Task Programming Library for .NET - Pico-processes on Windows 10 - Secure kernel on Windows 10 - Hyper-V based containers - Driver verification framework using a theorem proving framework - The P language used for writing Windows 8 USB drivers I guess they just don't adopt more due to management, and how the windev and devtools relate to each other in regards to technology adoption.

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 ago
  So 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 ago
    Looks 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 ago
      Yes, 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...
deleted 9y ago
[deleted]

Blaisorblade0 9y ago

Until recently, MSR was also very disconnected from product development. There was a distinct change last year. Also, in general most papers are more useful for writing further papers to improve on their limitations (until something's great), than to be adopted right away. This one is pretty cool, but both the conclusion and the benchmarks set out significant challenges for further research. After all, this is the first OS using automated verification, not the last. > a lack of software developers inside Microsoft willing to replace their existing code and learn new tools and languages. I'm sure research on the topic hasn't ended, so should they switch now or wait for more research? Or wait for research on verifying existing code? And if a new paper comes out, should they switch again? Also, do universities train enough developers to use such technology?