[seL4] LionsOS as basis for mobile/handheld OS

Interesting! So in the case of the device I’ve got here with privacy switches, my drivers would detect the removal of the modem and respond by dropping queued packets? Or some other mechanism, depending.

On Aug 9, 2024, at 5:30 AM, Peter Chubb wrote:



...

...

...

...

...

"Isaac" == Isaac Beckett writes:

Isaac> I was looking at LionsOS docs recently, and noted it is meant Isaac> for static systems with no support for changing hardware at Isaac> runtime. This is less of a problem for phones and other Isaac> handhelds given they generally keep the same hardware Isaac> throughout their service life, but I was concerned about Isaac> peripheral support. What if I want to be able to connect an Isaac> external display to a phone or tablet running a LionsOS based Isaac> userspace? Or I have privacy switches on the device that Isaac> physically disconnect components such as the modem or camera Isaac> assembly?

This kind of thing is doable, or rather will be doable, by swapping out modules. Although the _architecture_ is static, not all the modules need to be runnable at any one time. In LionsOS one will be able to instantiate template PDs that can run a range of different payloads loaded at run-time, to allow a degree of dynamism.

We have a student working on the hotplug problem at the moment. But it's unclear, in the general case, what should happen when something appears in, or disappears from, the system. Utimately it's going to be up to the system designer to design something that works for each system.

For example, if you remove a storage device (SDHC card, or USB stick). Your alternatives are: -- discard all in-flight requests for the device, unmount any filesystems etc. -- Mark the device as 'gone'; but if there are any in-flight requests, or if any new requests get queued, ask the GUI to pop up something asking for reinsertion of the device (like AmigaDOS did) -- something else I haven't thought of...

In whatever case, you need system policy to decide what to do, and code to implement it.

I expect the handheld device _will_ eventually be a target for a LionsOS system, but there's a fair bit of work to do.

In the near term, there will have to be more device drivers and virtualisers in the sDDF; more higher-level components in LionsOS itself; and the template PDs that are currently being worked on here by an undergraduate student.

-- Dr Peter Chubb https://trustworthy.systems/ Trustworthy Systems Group CSE, UNSW Core hours: Mon 8am-3pm; Wed: 8am-5pm; Fri 8am-12pm.