Re: [seL4] Are there any plans to re-add seL4_Untyped_RetypeAtOffset?

Hi Andrew! I warn and apologize that this message is long; however I think there is a misconception at work here and I'd like to clear it up. At 2020-01-22T21:22:41-0700, Andrew Warkentin wrote:

On 1/22/20, Heiser, Gernot (Data61, Kensington NSW) wrote:

...

However, there is always going to be some in-house experimental code, especially student work, that never makes it out.

That's exactly the kind of thing that I think might be a problem for UX/RT because it means that the development process isn't truly community-based.

No, that's not what that means. Every FLOSS license, every Free Software license[1] permits private development. Experimental code is just that, and happens all the time in both professional and personal development environments. We all write toy programs or slapdash implementations to develop and verify our understanding of the systems we're creating or interfacing with. Or, frequently, to discover the undefined behavior of the C compiler we're using. :P Student projects are a case of this written large. Not everybody wants the code they write in their novice years to be unleashed upon the world. In the case of UNSW's AOS (Advanced Operating Systems) course[2], which is seL4-based, the students are discouraged from sharing their solutions to the project milestones because doing so would frustrate the educational objective of the course. That is, the course directors would have to redevelop it every term and that would make them unhappy; also, you'd eventually run out of well-understood operating system concepts with which to easily evaluate their solutions. Fortunately, since the AOS course builds _on top of_ instead of altering the seL4 kernel, this does create a GNU GPL section 7 problem[3]. If you're thinking of skunkworks-style projects, or secret modules that get released only to paying customers, then Gernot can answer with certainty but I can tell you that I've neither seen nor heard of any such thing in the year I've worked at the Trustworthy Systems Group; that proprietary work product is opposed to the mission of the lab as I understand it; and that such a thing is not congruent with the workplace culture and opinions of staff. I'm not entirely comfortable citing my own reputation in the FLOSS community, but I have a public record as a strident FLOSS activist, particularly in the area of copyleft. You can find my fingerprints on the LaTeX Project Public License v1.3 per Frank Mittelbach, find me sparring with Richard Stallman over Invariant Sections and Cover Texts in the GNU FDL, find me exhorting David Dawes of the XFree86 Project not to slap a GPL-incompatible license over all of its (a decision he took anyway and which swiftly led to XFree86's death). I strove with "Gabucino" of the MPlayer project and Jörg Schilling of cdrtools to resolve GNU GPL incompatibilities within their codebases; the former attempt was ultimately successful while the latter was not. My most famous windmill-tilt was at Red Hat Software, Inc., for obfuscating the form of source distribution they used for the Linux kernel, presumably so as to impose an effort-tax on Oracle's Enterprise Linux efforts[4]. This last earned me (what I interpreted as) praise from Bradley M. Kuhn, who said I'm an even more strict interpreter of the GNU GPL than he is[5]. I also did FLOSS license-compliance work for several years professionally, in-house at Cisco.

UX/RT won't have any such thing as "in-house code" (except for code that hasn't yet been committed). All development will be public (except security fixes under temporary embargoes).

That is almost isomorphic (so, "cospectral"?) to what Trustworthy Systems does. Its developers push to internally-hosted Git repositories, upon which various continuous integration tests are run. If and only if the changed repos pass all the tests are the affected repositories then mirrored out to publicly hosted sites. This is quality control, and when the master branches of internal and external repos get out of sync it is a problem that the developers regard as urgent to fix.

I want UX/RT to be as easy as possible to contribute to, and that should include contributing to the kernel (which be much less necessary in general with a microkernel OS, but for stuff like platform support it will still be necessary).

Yes, and that is an objective shared by Trustworthy Systems.

Even just having a copyright-assignment-equivalent CLA would very likely scare off a lot of companies (and some individuals) from contributing. Things are already difficult enough in the industry at large for alternative OSes, and I don't want excessive barriers to contribution to be the thing that keeps UX/RT from succeeding.

That's true. Since the FSF (usually) requires copyright assignment as well, I can hardly cast stones at Trustworthy Systems for requiring this. I think CLAs come down to cases. Trustworthy Systems is part of Data61, which is in turn part of Australia's CSIRO. If you're American, that's sort of like the National Science Foundation. In organizations like these, a great deal of concern about liability exists. Such firms are regarded as having deep pockets (even when they don't), and so they attract civil suits in the hope of extracting a monetary settlement or judgment (the former is preferred, because the latter requires more billable hours in proving claims). However, I've gathered from encountering you on mailing lists over the past few years (no stalking, we simply seem to have similar interests :) ), that you're a lone developer working on a personal project. If you tried to impose a CLA on people I think you'd meet with a lot of resistance. And any contributor who valued their contribution would be pathologically selfless to assign copyright with no strings attached.

I really don't want to fork it unless I have to (and if I did I would rename my fork of course). I just know that my priorities for UX/RT (a general-purpose "better Linux than Linux" OS for production use) seem to be rather different from the those of the seL4 developers (research on static deeply embedded systems), and the development process isn't fully open, and that could possibly lead to differences requiring a fork in the future.

I think that if and when you can come to seL4 engineers at Trustworthy Systems with concrete use cases and measurable problems, they'll be happy to gnaw on the problem with you. It pays to remember that much of the staff are academics. Solving problems in microkernel performance and scalability, or showing how something once thought to be only achievable in a kernel can be done efficiently in user space, leads to conference papers and journal articles. They like that. I look forward to the continued development of UX/RT. Regards, Branden [1] https://www.gnu.org/philosophy/free-sw.html [2] https://www.cse.unsw.edu.au/~cs9242/current/ [3] https://www.gnu.org/licenses/old-licenses/gpl-2.0.en.html [4] https://lwn.net/Articles/432012/ [5] personal communication at DebConf 17 in Montréal, Canada