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 tutorial develops from scratch a collection of bare-metal SPARK Ada software components that can be used as an infrastructure to develop multicore system-level software in Ada, for AArch64-based embedded platforms. They can be used as a foundation to develop boot ROMs, bootloaders, multicore RTOS kernels, separation kernels and hypervisors in Ada, for AArch64-based platforms. The Raspberry Pi 4 and Raspberry Pi 5 boards are used as the target platforms

This is a hands-on tutorial and to get the most out of it, attendees are encouraged to bring their own Raspberry Pi 4 or Raspberry Pi 5 boards, a microSD card already formatted with Raspbian, a development laptop (preferably running Linux or MacOS) with a microSD card reader, and a USB-to-serial cable to connect the laptop to the Raspberry Pi's UART0 serial port.

Below is the road map of this tutorial. The end goal is to teach everything necessary to enable you to develop your own RTOS kernel or your own separation kernel or hypervisor for AArch64 platforms.

Presentation topics

  • Setting up the development host environment
  • Setting up Raspberry Pi board for bare-metal development
  • Building the GNAT cross-toolchain from sources for bare-metal AArch64 (aarch64-elf-gnat)
  • Minimal platform-independent bare-metal Ada Runtime library (RTS)
  • AArch64 bare-metal Ada "Hello World" program:
    • Raspberry Pi boot sequence
    • AArch64 startup code
    • Minimal UART driver
  • Writing your own UART bootloader for Raspberry Pi bare-metal programs
  • Writing your own bare-metal debug message logger in Ada
  • AArch64 bare-metal exception handling in Ada
  • Writing your own self-hosted mini GDB server in Ada
  • AArch64 bare-metal memory protection using the ARMv8-A MMU
  • AArch64 bare-metal interrupt handling in Ada
    • GICv2 interrupt controller (GIC-400)
    • ARMv8 generic timer interrupt (PPI interrupt)
    • UART Rx interrupt (SPI interrupt)
  • AArch64 bare-metal multicore in Ada
    • Bare-metal multicore boot in Ada
    • Spinlocks
  • AArch64 bare-metal multicore interrupt handling in Ada
  • Writing your own multicore RTOS for AArch64

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.