Introduction - uros Link to heading

uros (micro-ros) is a very minimal version of ROS (robot operating system) - a well known robotics middleware suite. It is meant run on resource constrained environments where features taken for granted in traditional ROS programming might not be available.

uROS Architecture

Introduction - sel4 Link to heading

sel4 is formally verified (security-enchanced) L4 microkernel, it claims to be the world’s most highly assured and the world’s fastest operating system kernel. It is a very minimal kernel and majority of the functionality is encouraged to be implemented at the user space.

sel4 replaces processes with the concept of protected-domains, each protected domain is an event driven program with init, fault and notified routines which run on the corresponding event.

sel4 can also be used as an hypervisor which enables us to startup a linux virtual machine inside sel4. Porting a linux system to sel4 is done by moving the applications of the system to sel4 one by one out of the linux VM as sel4 protected domains.

We will port the micro ros demo examples into sel4 protected domains and discuss how it has been done.

Setup explained Link to heading

uROS Architecture

We have 3 main components in the sel4 microkernel

  1. Linux VM which runs the ROS Data distribution service (ROS agent)
  2. VMM (Virtual machine monitor) which manages the Linux VM
  3. Protected Domain(s) which run uROS applications - publishers, subscribers, executors

uROS is configured to use custom transport and, the custom transport read and write functions.

  • Read function - reads packet from the queue and writes it into the buffer provided.
  • Write function - accepts payload, constructs pkt and pushes it into the queue and notifies VMM which pops the pkt out of the queue and injects into virtio for the Linux VM to accept

Protected domain code comparison Link to heading

micro-ros-demos
// micro-ros-demos (RTOS)
allocator = rcl_get_default_allocator();
rclc_support_init(&support, 0, NULL, &allocator);
rclc_node_init_default(&node, ...);

rclc_publisher_init_default(&pingPub, ...);
rclc_publisher_init_best_effort(&pongPub, ...);

rclc_subscription_init_best_effort(&pingSub, ...);
rclc_subscription_init_best_effort(&pongSub, ...);

rclc_timer_init_default(...);

executor = rclc_executor_get_zero_initialized_executor();

rclc_executor_init(&executor, &support.context, 3, &allocator);
rclc_executor_add_timer(&executor, &timer);

rclc_executor_add_subscription(&executor, &pingSub, &incoming_ping, &ping_subscription_callback, ON_NEW_DATA);
rclc_executor_add_subscription(&executor, &pongSub, &incoming_pong, &pong_subscription_callback, ON_NEW_DATA);



// seL4 is event based OS, 
// so we spin some on notification 
// instead of constantly spinning
rclc_executor_spin(&executor);
sel4 example
// seL4 init
allocator = rcl_get_default_allocator();
rclc_support_init(&support, 0, NULL, &allocator);
rclc_node_init_default(&node, ...);

rclc_publisher_init_best_effort(&pingPub, ...);
rclc_publisher_init_best_effort(&pongPub, ...);

rclc_subscription_init_best_effort(&pingSub, ...);
rclc_subscription_init_best_effort(&pongSub, ...);

// no timer in seL4 yet

executor = rclc_executor_get_zero_initialized_executor();

rclc_executor_init(&executor, &support.context, 3, &allocator);
// no timer in seL4 yet

rclc_executor_add_subscription(&executor, &pingSub, &incomingPing, send_pong, ON_NEW_DATA);
rclc_executor_add_subscription(&executor, &pongSub, &incomingPong, send_ping, ON_NEW_DATA);

// seL4 notified
void notified(microkit_channel ch)
{
    if(ch == CHAN_VMM_TRANSPORT): {
        ... // error case handling
        rclc_executor_spin_some(&executor, 0);
        break;
    }
}