On June 26th, co-located with the TockWorld conference, a group of Tock developers (about 30 of us) met in person to discuss the state of Tock development and share future goals for the ecosystem. We heard summaries of the year's work from the core, networking, OpenTitan, documentation, libtock-c and tools working groups. Those slides are all available from the conference agenda page (<https://world.tockos.org/tockworld7#day1>). In addition, we had a number of very productive breakout sessions focused on future development directions and a preview of Treadmill---the in-development testing and remote development system. ## Breakouts ### Non execute-in-place (XIP) platforms In integrated settings---for example where a root-of-trust microcontroller is on the same SoC as a more powerful application core---there is often no persistent storage from which to execute code directly. This may be, for example, because the SoC is too thin to fit any flash storage. In such cases, Tock must be adapted to load code (the kernel, processes) from persistent storage into RAM and execute from their, raising several challenges and opportunities. If persistent storage is not part of the TCB, there may need to be some mechanism to validate code and permissions before executing them. Loading code into RAM puts more pressure on memory and, in turn, requires more careful consideration of code size. Conversely, loading code into RAM means code and data can be predictably located near each other, thus making relocation much simpler. Action items from this breakout are to put together documentation describing the use cases and goals for non-XIP settings (already begun in <https://github.com/tock/tock/pull/4081>) as well as upstream a specific implementation (probably virtualized) of a non-XIP "board." ### Tock registers This breakout focused on the ongoing effort (lead by @jrvanwhy to revise Tock registers to be both more sound and more ergonomic (<https://github.com/tock/tock/pull/4001/files>). Downstream users raised a number of edge cases that would be good to support in the library. ### Formal methods with Tock This breakout gathered a number of developers either interested in or engaged in formally verifying parts of Tock. In particular, one group at Google had tried to do some verification using Kani with limited success, primarily due to issues with Kani. UCSD is doing work with Flux and Verus to verify portions of the Tock system call API and memory. Action items include setting up a communication channel for folks interested in verification, reaching out to Verus to propose Tock as a real-world verification target, and plugging other stakeholders in---Google downstream users, Rust verification groups. ### Automated driver implementations An idea raised in one of the discussions related to userspace maintenance got its breakout to discuss the potential for automatically generating userland bindings from specifications of a system call ABI in the kernel. Several ideas were raised for how to accomplish this. The outcome is a plan to move Markdown documentation of system call interfaces to Rust source files and build tooling to parse that documentation and generate boilerplate C and/or Rust userland bindings. ### Panic-free kernel This breakout discussed options towards a kernel with no `panic`. While Tock generally tries to avoid explicit panics in the kernel, sometimes that sneak in anyway, and sometimes they are hidden behind core language features (e.g. slice operations). Action items proposed were to open an RFC to solicit feedback, focus first on kernel board files, followed by capsules. ### Multi-core This breakout discussed adapting Tock to multi-MCU settings. A number of use cases were raised: - Separate security domains on different MCUs (e.g. cc26x2-style application and communication cores) - Applications that require enough performance to use two cores, and platforms like the RPi have them. Different cores would handle distinct set of peripherals. - Chips with asymmetric cores (e.g. an M4 and M7, or a Cortex-M and Cortex-R) - Platforms with multiple cores and _no shared memory_ (e.g. Signpost or two nrf52840DKs) - SoCs where Tock runs on some co-processor, but another core which runs some different OS. Action items from this breakout include fixing IPC (potentially revising completely), finishing work on CoreLocal, and a timeline for upstreaming current downstream muti-core implementations. ### CHERI A small group of developers discussed using Tock in CHERI-enabled hardware---CHERI is a hardware-based capability system that can provide extremely fine grained and expressive memory protection. At least one port currently exists, but a major blocker for significant upstream support is support for CHERI in Rust itself (currently people using Rust on CHERI have forked toolchains). The main action item is to propose to the Rust project to upstream support for CHERI and, in particular, support a stabilized version of pointer provenance. ## Takeaways This was an extremely productive TockWorld! Thanks to everyone who participated and sorry for those who couldn't make it. Stay tuned for upcoming call-to-actions following up on each of the action items from the breakouts. -Amit