Blogging about Midori (2015)
joeduffyblog.comSee also "Safe Systems Software and the Future of Computing" by Joe Duffy, the closing keynote at RustConf 2017:
https://www.youtube.com/watch?v=CuD7SCqHB7k
Midori and Rust have several striking similarities, and Microsoft's recent uptick in interest in Rust (and Rust-like languages) bodes well for improved software quality.
"Three safeties: memory, type, concurrency, for all code."
Right. I've been saying that for, sadly, decades now, ever since my proof of correctness days. I sometimes word this as the three big questions: "how big is it", "who owns it", and "who locks it". C is notorious for totally failing to address any of those, which is the cause of many of the troubles in computing.
Then, for way too long, we had the "but we can't afford memory safety" era, or "Python/Java/Javascript/whatever are too slow". It took way too long to get past that. Ada was supposed to address safety with speed, but it never caught on.
Rust looked promising at first. Huge step in the right direction with the borrow checker. But Rust was captured by the template and functional people, and seems to have become too complicated to replace C and C++ for the average programmer. We have yet to see the simplicity and stability of Go combined with the safety of Rust.
Duffy makes the point that slices are an important construct for safety. Most things expressed with pointer arithmetic in C are expressible as slices. I once proposed slices for C [1] but the political problems outweigh the technical ones. I'd like to see a C/C++ to Rust translator smart enough to convert pointer arithmetic to safe slice syntax. I've seen one that just generates C pointers in Rust syntax, which is not that useful.
The Midori people seem to have gone through the effort of understanding why "unsafe" code was being used, and tried to formalize that area to make it safe again. When I looked at Rust libraries a few years ago, I saw "unsafe" too often, and not just in code that interfaces with other languages.
Duffy writes, in connection with casting "For example, we did have certain types that were just buckets of bits. But these were just PODs." (Plain Old Data, not some Apple product.) I referred to these as "fully mapped types" - that is, any bit pattern is valid for the type. True for integers and raw characters. Not true for enums, etc. One way to look at casts is to treat them as constructors to be optimized. The constructor takes in an array of bytes and outputs a typed object. If the representation of both is identical, the constructor can be optimized into a byte copy, and maybe even into just returning a reference, if the output is immutable or the constructor consumes the input. So that's a way to look at sound casting.
Once you have that, you can separate allocation from construction and treat a constructor as something that takes in an array of bytes, consumes it, and outputs a typed object. Constructors are now isolated from the memory allocator.
For arrays, you need some way to talk about partially initialized arrays within the language. Then you can build arrays which grow as safe code.
That takes care of some of the common cases for unsafe code. It looks like Duffy's group got that far and went further. I need to read the papers.
[1] http://animats.com/papers/languages/safearraysforc43.pdf
I agree that partially initialized data structures are important for low-level, performance-oriented programming. But it is not clear how to do this within a Rust-style type-based approach to memory safety. Naturally, one can always wrap the problematic code that deals with partially initialised data in an unsafe-block, but you can already do that in Rust. By Rice's theorem we know that we cannot have a feasible typing system that allows us always to deal with partially initialised data in a safe way, but could there be a compromise, covering most of the standard uses of partially initialised data (e.g. what you find in a standard algorithm text book like CLRS, or a standard library like C++'s)? I don't see how right now, because the order of initialisation can be quite complex, too complex to fit neatly into well-bracked lifetimes a la Rust.partially initialized arraysHave you got any ideas how to do better?
Sure, having dealt with this formally in 1981 with machine proofs.[1]
In the Pascal-F verifier, we treated array cells as if they had a "defined()" predicate. Clearly, if you have a flag indicating whether an array cell was defined, you could handle partially initialized arrays.
Then you prove that such a flag is unnecessary.
We had a predicate
which means the entries of the array a from i to j are initialized. Theorems about DEFINED are:DEFINED(a,i,j)
Given this, you can do inductive proofs of definedness as you use more slots in an array that started out un-initialized.j<i => DEFINED(a,i,j) // empty case is defined DEFINED(a,i,j) AND DEFINED(a,j+1,k) => DEFINED(a,i,k) // extension DEFINED(a[i]) => DEFINED(a,i,i) // single element defined DEFINED(a,i,j) AND k >= i AND k <= j => DEFINED(a[k]) // elt is definedTo do proofs like this, you have to be able to express how much of the array is defined from variables in the program. Then you have to prove that for each change, the "defined" property is preserved. Not that hard when you're just growing an array. You can construct data structures where this is hard, such as some kinds of hash tables, but if you can't prove them safe, they probably have a bug.
This was new 40 years ago, but many others have been down this road since. Rice's theorem isn't a problem. That just says that you can construct some undecidable programs, not that all programs are undecidable. If your program is undecidable or the computation required to decide it is enormous, it's broken. Microsoft puts a time limit on their static driver verifier - if they can't prove safety after some number of minutes, your driver needs revision. Really, if you're writing kernel code and you're anywhere near undecidability, you're doing it wrong.
[1] http://www.animats.com/papers/verifier/verifiermanual.pdf
Thanks.
We were talking cross-purposes. I was thinking about partially initialized arrays in the context of a Rust-like type-checker. I don't think the analysis you ran in 1981 in a prover is possible in 2020 in a type-checker, at least without putting most of the bits dealing with partial initialization into unsafe-boxes.
It would be great if Rust-style type-based lifetime analysis could cope with partial initialization.
The language team of that time participated also in the C# 7.2/7.3 performance wave and the technology which makes .NET Core so we'll performing nowadays.
Rust moves system programming up. At the same time, C# moves application development down. Interesting.
> My biggest regret is that we didn’t OSS it from the start, where the meritocracy of the Internet could judge its pieces appropriately.
This would have been interesting, but it's not too late. Correct me if I'm wrong, but there isn't anything stopping Microsoft from releasing this research to the public today. It seems like something the "new" Microsoft of 2020 would be likely to do.
There was a copy of the code for Singularity, the predecessor to Midori, on CodePlex. Not sure if it ever got moved to Github.
It has to be said, though. It's more like "source available", not open source. I can't remember what the license is specifically, but it's not a proper open source license.
You could see it, build it, and play with it, but you couldn't do anything else with it. No sharing changes, no derivatives, etc.
Singularity would be a neat place to start working on a managed code OS, though.
I would prefer that they properly open source Midori.
You can judge it, though.
It was a really cool project. The software isolated processes concept is something that I really like.
Everyone I have worked with from the Midori team has been very impressive. Regardless of the direct success of the project, I believe it (to some extent) improved the quality of Microsoft's engineering culture.
Engineering culture especially in he Windows NT kernel was always impressive. A search for David Cutler the lead behind Windows NT immediately also talks about engineering.
That said, Midori influenced later many team, including the .NET one.
One comment at the time: https://news.ycombinator.com/item?id=10545353
Related from 2016: https://news.ycombinator.com/item?id=11054912
https://news.ycombinator.com/item?id=10871222
My experience with Midori people was a little like the jokes people tell about BMW owners and vegans.
You knew who they were because they wouldn't stop talking about Midori. It's a neat project, I liked hearing the stories.
I was on the Midori team for just a year, and this is certainly true for me. I think that it's a combination of things, the project itself was very cool from a pure technical perspective, and the team was made up of brilliant engineers, most of whom appeared to have nothing to prove, so technical discussions revolved about technical merit not ego.
There was a fair bit of ego.
Turns out when you have a project staffed with extremely high up engineers and no real production deployment, it's easy to keep up engineering standards. The idea that a normal team with normal issues wasn't as good seemed to really upset one of the midori people I worked with.
I'm certainly not saying that there was no ego on the team, but rather that (in comparison to the rest of MS over the 14 years I was there) engineers weren't as ego involved in technical decision making
I definitely recall seeing passionate discussions with engineers whose levels ranged from 62 to 69+ where the technical merit of the arguments was the gold standard, not what the most senior engineer said. In contrast, my experience working with partner and DE level engineers in other parts of MS was that of "what I say goes"
Nah, this was the sort of guy who decided to leave the team (not midori this was years later in a different org) and then figures it's okay to act like a jerk on the way out the door. Some (junior) engineer on another team made a bad suggestion. Wasn't enough to say no, he had to tear a strip off him. To the point the manager of the other team asked if they could talk about it (he refused).
Guy was passionate and smart and just a lousy leader.
Okay, I guess I'm talking about the culture on the team as I experienced it, and culture definitely comes from the top in this case. I'm sure that some individuals behaved differently in other environments.
Why was it called midori? My only knowledge of this word is that it means green is Japanese.
We brainstormed a bunch of names one day, and Midori won. I think it was Chris Brumme's suggestion.
There is also a lightweight web browser called Midori.
And a melon based drink, which I never associated with japan but probably is (japan views melon as very much a delicacy)
Yeah, my first thought. But then the Microsoft link didn't make sense. Both like Japanese, and green, I guess.
Wild guess: it's a Greenfield OS project
I had never heard of this, but thank you.
That's fair:) A greenfield project is a project done from scratch or as a fresh start. This ranges from "new startup so we're starting from scratch" to " we've decided that the right thing to do in this huge Enterprise environment is to throw out everything we have and make a completely new pass at everything".