Ada

Spunky: a Genode Kernel in Ada/SPARK

AW1.125
Martin Stein
The Genode OS framework is an open-source tool kit for building highly secure component-based operating systems scaling from embedded devices to dynamic desktop systems. It runs on a variety of microkernels like SeL4, NOVA, and Fiasco OC as well as on Linux and the Muen SK. But the project also features its own microkernel named "base-hw" written in C like most of the Genode framework. Spunky is a pet project of mine. Simply put it's an approach to re-implement the design of the "base-hw" kernel first in Ada and later in SPARK with the ultimate goal to prove its correctness. It is also an opportunity to learn how Genode can benefit from Ada and SPARK in general and promote the use of safety-oriented languages in the project.

Additional information

Type devroom

More sessions

2/1/20
Ada
AW1.125
Welcome to the Ada Developer Room at FOSDEM 2020, which is organized by Ada-Belgium in cooperation with Ada-Europe.
2/1/20
Ada
Jean-Pierre Rosen
AW1.125
An overview of the main features of the Ada language, with special emphasis on those features that make it especially attractive for free software development.
2/1/20
Ada
Gautier de Montmollin
AW1.125
In the Ada world, we are surrounded by impressive and professional tools that can handle large and complex projects. Did you ever dream of a tiny, incomplete but compatible system to play with? Are you too impatient, when developing small pieces of code, for long compile-bind-link-run cycles? Are you a beginner intimidated by project files and sophisticated tools? Then HAC (the HAC Ada Compiler, or the Hello-world Ada Compiler) is for you.
2/1/20
Ada
Philippe Waroquiers
AW1.125
This talk describes how performance aspects of a big Air Traffic Flow Management mission critical application are tracked from development to operations.
2/1/20
Ada
Johannes Kliemann
AW1.125
Last year I presented Cappulada, a C binding generator for Ada that intended to overcome the shortcomings of existing solutions and to provide usable bindings even for complex C code. This year I want to show our conclusions on why automatic bindings between C and Ada are hard (if not impossible) and where existing solutions (including our own) fail.
2/1/20
Ada
Alejandro Mosteo
AW1.125
The Robot Operating System (ROS) is one of the chief frameworks for service robotics research and development. The next iteration of this framework, ROS2, aims to improve critical shortcomings of its predecessor like deterministic memory allocation and real-time characteristics. RCLAda is a binding to the ROS2 framework that enables the programming of ROS2 nodes in pure Ada with seamless integration into the ROS2 workflow.
2/1/20
Ada
Jean-Pierre Rosen
AW1.125
Ada incorporates in its standard a model for distributed execution. It is an abstract model that does not depend on a particular kind of network or any other communication mean, and that preserves full typing control across partitions. This presentation briefly exposes the principles of Ada's distribution model, then shows the possibilities with life demos across different machines and operating systems.