Tutorial: Developing Bare-metal Embedded Software in SPARK Ada for 64-bit ARM Platforms

J. Germán Rivera, Tesla

This tutorial teaches how to develop 64-bit bare-metal embedded software for the 64-bit ARMv8-A (AArch64) architecture in SPARK Ada. The Raspberry PI 4 (model B) board will be used as the target platform. The tutorial will start by explaining how to build the GNAT cross-toolchain for barematal AArch64 (aarch64-elf). Then it will describe how to write your own UART boot loader for the Raspberry PI, to make testing bare-metal code on the board easier. Next, it will describe how to write a self-hosted bare-metal mini GDB server, which can be used to set hardware break points and to examine stack traces and memory from a GDB client over UART. The second half of the tutorial will teach incrementally how to write a simple 64-bit multi-core RTOS, from the reset handler all the way to the thread scheduler, explaining how to implement all the necessary building blocks in SPARK Ada along the way. This is a hands-on tutorial and to get the most out of it, attendees are encouraged to bring their own RaspberryPI boards (4 model B or later), a development laptop (preferably running Linux or MacOS) and a USB-to-serial cable to connect the laptop to the Raspberry PI's UART0 serial port.

Presentation topics

  • How to build the GNAT cross-tool chain from sources for bare-metal AArch64
  • How to build a minimal platform-independent Ada Runtime library (RTS)
  • Bare-metal Ada "Hello world" program: AArch64 startup code and minimal UART driver
  • Writing a UART boot loader in Ada for RaspberryPI bare-metal programs
  • AArch64 interrupt and exception handling in Ada
  • Writing a self-hosted bare-metal mini GDB server in Ada
  • Aarch64 GICv3 interrupt controller
  • Aarch64 generic timer
  • Memory protection using the AArch64 MMU
  • Multi-core AArch64 startup code
  • Designing a simple multicore RTOS
  • Writing the RTOS thread scheduler in SPARK Ada
  • Writing the RTOS thread synchronization primitives in SPARK Ada

Duration: Full-day

Level: Intermediate to Advanced

Reason for attending

If you are an experienced bare-metal embedded Ada developer for 32-bit ARM architectures, such as ARMv7-M ARMv7-R or ARMv8-R AArch32, or you are a hard-core embedded Ada enthusiast, and would like to expand your skills to know how to write 64-bit ARM bare-metal embedded software in SPARK Ada, this tutorial is for you.

Presenter

J. Germán Rivera is a senior staff software engineer at Tesla, where he develops low-level embedded software for automotive system-on-chip platforms. He has 35 years of industry experience developing system-level software. He has also held software development positions at Google, NXP, Microsoft, Cisco, IBM, NetApp and HP. He holds a Master of Software Engineering degree from Carnegie Mellon University (USA) and a Bachelor's degree in Computer Science, from the University of Los Andes (Colombia). In his spare time, he writes Ada/SPARK embedded software for hobby projects, in which he also experiments with practical applications of formal methods.