In the final blog in this series I want to talk about how TS not only survived, but bounced back with a vengeance.

This is much more fun to write than the previous blog, which was truly painful. I had to spend hours trawling through emails that made me re-live all the insanity, dishonesty, deceit and other unethical behaviour we have experienced in CSIRO. Reading this still makes my blood boil.

Why did all this happen? Clearly, TS with its uncompromising culture of excellence and outspokenness was a misfit to the Data61 culture of mediocrity and incrementalism, and I knew that for a long time. It’s not hard to imagine that many people felt threatened by the combination of ambition and delivering the “impossible” that characterises TS. If all you can do is marginal improvements over other people’s work, or applying other people’s research to a narrow class of problems, then looking at TS must feel intimidating.

But I happen to think that the taxpayer deserves the best. And the taxpayer isn’t getting good value from Data61. Eventually the powers that be will realise this (after far too many tax dollars will have been wasted) and pull the plug. The earlier the better.

10 months later, where are we?

In short: TS is in great shape, the best it’s been in for years.

For years I had brought millions of external research funding into NICTA and then Data61/CSIRO every year. I was highly confident that within 6–12 months I would line up enough project funding to keep the group going, the main challenge was to keep the group alive until then. Turns out I was a pessimist: Lining up funding was even faster. In fact, I had never raised as much research money in any year as I have in the past 10 months.

But all the world’s project funding doesn’t help if there are no people to put onto those projects, and that was the prospect we were facing. Most people in TS had job offers within days, and many took them – who could blame them when the group seems to be dying?

This is when Aaron, my UNSW Head of School, came to the rescue with his offer to fund the group to the end of the year – exactly the break we needed! The figure shows what happened: Between people being kicked out of CSIRO (the dark red downward slope) and the new funding cutting in (the steep green mountain) there’s a valley of death – bridged by the UNSW funding. Without that, TS would be dead.

What’s not visible from the graph is the turnover in people. Despite having the (initially short-term) funding, we lost many people, especially those highly skilled in operating systems (OS). This is when the second amazing thing happened: The strongest influx of students (current ones as well as fresh graduates) we have had in many years. And it’s not only the quantity, but also the quality, they’re awesome! Nothing like it happened in the past 10–15 years – just when we really needed it!

One benefit of the transition whose value is hard to overestimate is the high degree of autonomy we have at the university. When I brought money into CSIRO, I lost control. When I bring money into UNSW, I retain control, meaning I always know exactly how much money I have, and I’m the one controling spending – this is so important to operating well and gives us the stability and flexibility we need. And UNSW is in general a so much saner environment than CSIRO – hard to appreciate fully if you haven’t experienced them both.

What does this mean for the seL4 Community?

Had TS gone under, it would have spelt real trouble for seL4. The community has grown and matured a lot, but some leadership is still needed (now jointly provided by TS and Proofcraft). And while TS has been temporarily weakened, this is being quickly reversed, as evident from the recent pull requests coming from some of the new TSers.

Beyond this temporary rebuilding phase, there is a strong overall benefit to the community, in that core seL4 skills are now spread much wider, to a larger number of organisations, where people continue to be paid to contribute to seL4. This is critical to scaling up – to be successful, the community must reduce its dependency on TS. The part labelled “community” in the graphic represents those ex-TS people now working for other ecosystem players. In the past, most people leaving TS were lost from the ecosystem, now many are moving inside the ecosystem, strengthening it in the process. Furthermore, I have hope to draw some of the “lost” souls back into the community with some of the exciting things happening in the background.

This migration of talent goes along with a refocus of TS: Arguably, for the past few years we were focussed too much on technology transfer and applied research (although we have kept performing ambitious research, such as the multi-award-winning time protection project). Some of that tech transfer work was needed to accelerate the adoption of seL4, but the short-term focus and pressure to earn revenue in Data61 didn’t help. The maturing of the commercial seL4 ecosystem allows us to get away from pure engineering work and focus on research, with a healthy mix of applied and fundamental work (but always driven by real-world problems).

The old model is shown in the first diagram: TS did everything. Obviously, this is not a sustainable model for a growing ecosystem. The new model is shown in the second diagram: TS still drives the research, but development and deployment is now mostly done in industry – as they should. TS is also broadening its research from the kernel to the full system, an example is the provably secure general-purpose OS project, which is defining the next generation secure OS design.

At the same time, we keep close contacts with industry, which helps us understand real-world problems, which, in turn, drives our research. The seL4 Foundation is a great enabler of all this. The obvious advantage of this model is that it scales better, and we hope that eventually other universities will join on the research side to improve scalability further. Another advantage is that development and deployment is now mostly industry-funded, so public-sector support can focus on the research. And indeed, most of the financial support to TS is from government organisations; not all of the sources are public knowledge yet, you’ll hear more of it over the next few months .

If you want to hear a bit more about TS’s transformation, watch my LCA talk.

TS Rocks – Again!

It was a near-death experience for TS, but we survived and are now stronger than we have been in a long time.

We’re operating in the massively saner environment of UNSW, where we have autonomy and, importantly, retain control over the money we bring in. We have the money to work towards our vision (we can always do with more, there are projects I’d like to accelerate, but our present financial position is strong). We have lost a lot of experience, but we have an incredibly strong team of fast learners, so it won’t take too long to recover that aspect, and the culture of the team is more inclusive and supportive than it’s ever been.

And we have awesome support from management. I had all but forgotten how it feels to be considered an asset rather than a problem, and, instead of wasting most energy on pushing management out of the way, having a boss who sees it as his main job to help you succeed. Management that thinks it’s their job to enable you to work at your best? Feels like heaven. What a difference from an environment where excellence is a problem, and people are treated like crap!

In short, TS is back, and moving fast. You’ll keep hearing our success stories – stay tuned!

I’ll leave you with the future of TS: The students and graduates who have joined us in the past 6 months. Clearly, the future is bright!

Newcomers to TS since September’21