There’s No Rust On This Ironclad Kernel

November 12, 2025 by Tyler August 2 Comments

Rust is the new hotness in programming languages because of how solid its memory protections are. Race conditions and memory leaks are hardly new issues however, and as greybeards are wont to point out, they were kind of a solved problem already: we have Ada. So if you want a memory-protected kernel but aren’t interested in the new kids’ rusty code, you might be interested in the Ironclad OS kernel, written entirely in Ada.

OK, not entirely in classic Ada– they claim to use SPARK, too, but since SPARK and Ada converged syntax-wise over a decade ago, we’re just going to call it Ada. The SPARK toolchain means they can get this kernel “formally-verified” however, which is a big selling point. If you’re not into CS, that just means the compiler can confirm the code is going to do what we want under all possible conditions — which is a nice thing to be able to say about the heart of your operating system, I think we can all agree. It’s a nice thing to be able to say about any code, which is one reason why you might want to be programming in Ada.

Continue reading “There’s No Rust On This Ironclad Kernel” →

Programming Ada: Atomics And Other Low-Level Details

January 2, 2025 by Maya Posch 6 Comments

Especially within the world of multi-threaded programming does atomic access become a crucial topic, as multiple execution contexts may seek to access the same memory locations at the same time. Yet the exact meaning of the word ‘atomic’ is also essential here, as there is in fact not just a single meaning of the word within the world of computer science. One type of atomic access refers merely to whether a single value can be written or read atomically (e.g. reading or writing a 32-bit integer on a 32-bit system versus a 16-bit system), whereas atomic operations are a whole other kettle of atomic fish.

Until quite recently very few programming languages offered direct support for the latter, whereas the former has been generally something that either Just Worked™ if you know the platform you are on, or could often be checked fairly trivially using the programming language’s platform support headers. For C and C++ atomic operations didn’t become supported by the language itself until C11 and C++11 respectively, previously requiring built-in functions provided by the toolchain (e.g. GCC intrinsics).

In the case of Ada there has been a reluctance among the language designers to add support for atomic operations to the language, with the (GNU) toolchain offering the same intrinsics as a fallback. With the Ada 2022 standard there is now direct support in the System.Atomic_Operations library, however.

Continue reading “Programming Ada: Atomics And Other Low-Level Details” →

Programming Ada: Implementing The Lock-Free Ring Buffer

August 1, 2024 by Maya Posch 20 Comments

In the previous article we looked at designing a lock-free ring buffer (LFRB) in Ada, contrasting and comparing it with the C++-based version which it is based on, and highlighting the Ada way of doing things. In this article we’ll cover implementing the LFRB, including the data request task that the LFRB will be using to fill the buffer with. Accompanying the LFRB is a test driver, which will allow us to not only demonstrate the usage of the LFRB, but also to verify the correctness of the code.

This test driver is uncomplicated: in the main task it sets up the LFRB with a 20 byte buffer, after which it begins to read 8 byte sections. This will trigger the LFRB to begin requesting data from the data request task, with this data request task setting an end-of-file (EoF) state after writing 100 bytes. The main task will keep reading 8-byte chunks until the LFRB is empty. It will also compare the read byte values with the expected value, being the value range of 0 to 99.

Continue reading “Programming Ada: Implementing The Lock-Free Ring Buffer” →

Programming Ada: Designing A Lock-Free Ring Buffer

July 30, 2024 by Maya Posch 7 Comments

Ring buffers are incredibly useful data structures that allow for data to be written and read continuously without having to worry about where the data is being written to or read from. Although they present a continuous (ring) buffer via their API, internally a definitely finite buffer is being maintained. This makes it crucial that at no point in time the reading and writing events can interfere with each other, something which can be guaranteed in a number of ways. Obviously the easiest solution here is to use a mutual exclusion mechanism like a mutex, but this comes with a severe performance penalty.

A lock-free ring buffer (LFRB) accomplishes the same result without something like a mutex (lock), instead using a hardware feature like atomics. In this article we will be looking at how to design an LFRB in Ada, while comparing and contrasting it with the C++-based LFRB that it was ported from. Although similar in some respects, the Ada version involves Ada-specific features such as access types and the rendezvous mechanism with task types (‘threads’).

Continue reading “Programming Ada: Designing A Lock-Free Ring Buffer” →

Programming Ada: Records And Containers For Organized Code

June 4, 2024 by Maya Posch 5 Comments

Writing code without having some way to easily organize sets of variables or data would be a real bother. Even if in the end you could totally do all of the shuffling of bits and allocating in memory by yourself, it’s much easier when the programming language abstracts all of that housekeeping away. In Ada you generally use a few standard types, ranging from records (equivalent to structs in C) to a series of containers like vectors and maps. As with any language, there are some subtle details about how all of these work, which is where the usage of these types in the Sarge project will act as an illustrative example.

In this project’s Ada code, a record is used for information about command line arguments (flag names, values, etc.) with these argument records stored in a vector. In addition, a map is created that links the names of these arguments, using a string as the key, to the index of the corresponding record in the vector. Finally, a second vector is used to store any text fragments that follow the list of arguments provided on the command line. This then provides a number of ways to access the record information, either sequentially in the arguments vector, or by argument (flag) name via the map.

Continue reading “Programming Ada: Records And Containers For Organized Code” →

Programming Ada: Packages And Command Line Applications

May 1, 2024 by Maya Posch 5 Comments

In the previous installment in this series we looked at how to set up an Ada development environment, and how to compile and run a simple Ada application. Building upon this foundation, we will now look at how to create more complex applications, along with how to parse and use arguments passed to Ada applications on the command line (CLI). After all, passing flags and strings to CLI applications when we launch them is a crucial part of user interaction, as well as when automating systems as is the case with system services.

The way that a program is built-up is also essential, as well-organized code eases maintenance and promotes code reusability through e.g. modularity. In Ada you can organize subprograms (i.e. functions and procedures) in a declarative fashion as stand-alone units, as well as embed subprograms in other subprograms. Another option is packages, which roughly correspond to C++ namespaces, while tagged types are the equivalent of classes. In the previous article we already saw the use of a package, when we used the Ada.Text_IO package to output text to the CLI. In this article we’ll look at how to write our own alongside handling command line input, after a word about the role of the binding phase during the building of an Ada application.

Continue reading “Programming Ada: Packages And Command Line Applications” →

Programming Ada: First Steps On The Desktop

April 23, 2024 by Maya Posch 67 Comments

Who doesn’t want to use a programming language that is designed to be reliable, straightforward to learn and also happens to be certified for everything from avionics to rockets and ICBMs? Despite Ada’s strong roots and impressive legacy, it has the reputation among the average hobbyist of being ‘complicated’ and ‘obscure’, yet this couldn’t be further from the truth, as previously explained. In fact, anyone who has some or even no programming experience can learn Ada, as the very premise of Ada is that it removes complexity and ambiguity from programming.

In this first part of a series, we will be looking at getting up and running with a basic desktop development environment on Windows and Linux, and run through some Ada code that gets one familiarized with the syntax and basic principles of the Ada syntax. As for the used Ada version, we will be targeting Ada 2012, as the newer Ada 2022 standard was only just approved in 2023 and doesn’t change anything significant for our purposes.

Continue reading “Programming Ada: First Steps On The Desktop” →