![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
the SPIN paper, which we're reading for 712 (grad OS), drinks the PL koolaid:
"Our decision to use Modula-3 was made with some care. Originally, we had intended to define and implement a compiler for a safe subset of C. All of us, being C programmers, were certain that it was infeasible to build an efficient operating system without using a language having the syntax, semantics and performance of C. As the design of our safe subset proceeded, we faced the difficult issues that typically arise in any language design or redesign. For each major issue that we considered in the context of a safe version of C (type semantics, objects, storage management, naming, etc.), we found the issue already satisfactorily addressed by Modula-3. Moreover, we understood that the definition of our service interfaces was more important than the language with which we implemented them.
"Ultimately, we decided to use Modula-3 for both the system and its extensions. Early on we found evidence to abandon our two main prejudices about the language: that programs written in it are slow and large, and that C programmers could not be effective using another language. In terms of performance, we have found nothing remarkable about the language's code size or execution time, as shown in the previous section. In terms of programmer effectiveness, we have found that it takes less than a day for a competent C programmer to learn the syntax and more obvious semantics of Modula-3, and another few days to become proficient with its more advanced features. Although anecdotal, our experience has been that the portions of the SPIN kernel written in Modula-3 are much more robust and easier to understand than those portions written in C."
"Our decision to use Modula-3 was made with some care. Originally, we had intended to define and implement a compiler for a safe subset of C. All of us, being C programmers, were certain that it was infeasible to build an efficient operating system without using a language having the syntax, semantics and performance of C. As the design of our safe subset proceeded, we faced the difficult issues that typically arise in any language design or redesign. For each major issue that we considered in the context of a safe version of C (type semantics, objects, storage management, naming, etc.), we found the issue already satisfactorily addressed by Modula-3. Moreover, we understood that the definition of our service interfaces was more important than the language with which we implemented them.
"Ultimately, we decided to use Modula-3 for both the system and its extensions. Early on we found evidence to abandon our two main prejudices about the language: that programs written in it are slow and large, and that C programmers could not be effective using another language. In terms of performance, we have found nothing remarkable about the language's code size or execution time, as shown in the previous section. In terms of programmer effectiveness, we have found that it takes less than a day for a competent C programmer to learn the syntax and more obvious semantics of Modula-3, and another few days to become proficient with its more advanced features. Although anecdotal, our experience has been that the portions of the SPIN kernel written in Modula-3 are much more robust and easier to understand than those portions written in C."
![[identity profile]](https://www.dreamwidth.org/img/silk/identity/openid.png){kind=small}
no subject
Date: 2010-02-15 06:57 pm (UTC)From:how 'safe' exactly does writing in a language like this really force you to be? can you prove there are no race conditions, or only that there are no "oops, i overstepped this array boundary" bugs?
will the innermost guts (context switcher, etc) still have to be written in asm, or does the language provide facilities for it?
no subject
Date: 2010-02-16 05:26 am (UTC)From:exactly as safe as the type system is. this paper didn't provide any formal proofs or statements of properties, so i really don't know what they mean. it seems like they were mostly talking about memory safety. proving things about concurrent code is still a Hard Problem as far as i'm aware.
will the innermost guts (context switcher, etc) still have to be written in asm, or does the language provide facilities for it?
they also, frustratingly, didn't talk about much of their implementation, other than the blurb i posted. but some of it is certainly in c, and i would assume the context switcher is in asm. maybe typed assembly? but at any rate, the kernel they provide is a trusted code base. they just want to keep that part small.
no subject
Date: 2010-02-16 06:02 am (UTC)From:Coincidentally, Emin Gun Sirer, who was one of the hotshot young networking/systems guys at Cornell at the time, was the main implementor of SPIN OS while he was a UW grad student, so I talked with him about his experiences implementing it.
The choice of Modula 3 was mostly based on what was hip and suitable at the time. Gun suspected if the project began a few years later, it might have been implemented in Java or something similar.
There really were no proofs of anything involved, so any memory safety properties were contingent on the memory safety of the implementation of Modula 3 used. From the OS perspective, I believe the fact that it was a microkernel architecture was important in minimizing the TCB. SPIN either predates or was contemporary with the original TAL papers, and almost certainly did not use it.
According to Gun, the actual implementation was to some degree *nix compatible, and could do basic things like check e-mail and whatnot. An annoying performance drawback was the lags caused by the garbage collection technology available at the time.
no subject
Date: 2010-02-15 07:08 pm (UTC)From:no subject
Date: 2010-02-16 01:54 am (UTC)From:no subject
Date: 2010-02-16 05:27 am (UTC)From:no subject
Date: 2010-02-16 06:08 am (UTC)From:no subject
Date: 2010-02-16 10:47 pm (UTC)From:Maybe next he'll come out with Oh My God! Scala!