How Does Ada's Memory Safety Compare Against Rust?
This article takes a look at the most common memory-related errors, and compares how well Rust and Ada prevent you from making them in the first place.
Foreword #
The Rust programming language has exploded in popularity in the last few years, consistently ranking as one of the most loved languages in Stack Overflow's Developer Survey. Designed by Mozilla to be memory-safe, it's steadily gaining ground as a viable alternative to languages like C++. This focus on safety has invited comparisons with Ada; An older, but battle-tested language designed for safety-critical industries. Despite all the things they have in common, a bitter rivalry has grown between the Ada and Rust communities. For years I've been defending Ada online from a motley crew of angry Rustaceans, crusty old greybeards, and bitter old haters. Most of whom either haven't used it, or haven't used it since Reagan was in office. I've been critical of Rust's design in the past, but have I actually given Rust a fair go? When it comes to memory safety, how do the two languages really stack up? Does Rust offer us anything new that Ada doesn't? Let's find out!
Before we begin, it's worth noting that you can do a lot in Ada without ever allocating heap memory, or even using pointers at all. In fact, most guides on Ada programming recommend avoiding pointers altogether. Language constructs such as in/out parameter modes, creating dynamically sized arrays at runtime, and the ability to return variable length arrays from functions address many of the scenarios where pointers would be necessary in other languages. Keep this in mind when reading: You can avoid many of these situations altogether in Ada.
Common Memory Errors #
Memory Leaks #
CWE-401: Memory Leak
refers to a program failing to release the memory that it's allocated.
Left unchecked, a leaky program could drain all your system's memory.
The most common cause of
memory leaks
in C is mismatched malloc(), and free() statements.
While not impossible1, Rust does actually make leaking memory pretty difficult. Variables in Rust are automatically deallocated when their owner goes out of scope. Most of the time this means a variable will be deallocated at the end of the scope it's declared in.
For
reference counted
smart pointers, like Rc<T> and Arc<T>,
Rust will automatically deallocate the memory they point to when the reference count reaches zero.
In Ada, dynamically allocated memory needs to be deallocated manually with the generic
Ada.Unchecked_Deallocation procedure.
With unchecked
referring to checking whether the variable being deallocated is still in use.
While Ada's controlled types do support implementing RAII-like functionality, under normal circumstances forgetting to manually deallocate heap memory will cause it to leak.
The only scenario where Ada will automatically2
deallocate memory is when the user specifies a static size for an access type's storage pool
using the Storage_Size aspect.
This controls exactly how many bytes of heap memory can be allocated for variables of a particular type.
If this is specified, the compiler automatically allocates all the required memory up front3,
and automatically deallocates it when the type goes out of scope.
If this pool is exhausted, the program will raise a Storage_Error exception.
procedure Access_Type_With_Explicit_Pool_Size is -- This sets aside a total of 128 bytes for the pool of Int_Access. -- Allocating more than 128 bytes will raise a Storage_Error exception. type Int_Access is access Integer with Storage_Size => 128; begin for I in 1 .. 16 loop declare Q : constant Int_Access := new Integer'(I); begin Put_Line (Q.all'Image); end; end loop; end Access_Type_With_Explicit_Pool_Size;
Running Valgrind on the example above shows that the memory is indeed deallocated automatically.
Buffer Overflow #
CWE-119: Buffer Overflow refers to reading or writing past the end of an array, and into adjacent memory. Buffer overflows are probably responsible for more security vulnerabilities than any other kind of bug, and are a common technique for jailbreaking hardware. The infamous Morris Worm, and Heartbleed vulnerabilities both relied on buffer overflows.
void buffer_overflow() { char email_address[10]; printf("Please enter your email address:\n"); // Modern versions of GCC will spew a litany of warnings about using 'gets'. gets(email_address); printf("Sending welcome email to %s\n", email_address); } // $ gcc -o buffer_overflow buffer_overflow.c // $ ./buffer_overflow // $ Please enter your email address: // $ anthony@this_will_overwrite_the_function's_return_address_on_the_stack.com // $ Segmentation fault
One of the few things that Rust and Ada agree on is runtime bounds checking. Attempting to access an out-of-bounds array index will result in a 'panic'.
fn overflow_this_buffer() { let mut buffer = [0; 10]; let mut raw_input = String::new(); println!("What array index should be cleared? "); io::stdin() .read_line(&mut raw_input) .expect("Failed to read line"); let index: usize = raw_input .trim() .parse() .expect("Please enter a valid integer"); buffer[index] = 0; } // $ cargo run // $ What array index should be cleared? // $ 12 // $ thread 'main' panicked at buffer_overflow.rs:14:5: // $ index out of bounds: the len is 10 but the index is 12 // $ note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace // $ ...
Similar to Rust,
attempting to access an array index outside of its valid range will raise a
Constraint_Error exception at runtime,
which can be handled programmatically.
This is the same type of exception raised in the case of a scalar range constraint violation,
such as an integer overflow.
procedure Buffer_Overflow is Email_Address : String (1 .. 10); begin Put_Line ("Please enter your email address:"); Email_Address := Get_Line; Put_Line ("Sending welcome email to " & Email_Address); exception when Constraint_Error => Put_Line ("Buffer overflowed!"); end Buffer_Overflow; -- $ alr run -- $ Please enter your email address: -- $ anthony@this_will_overflow_the_buffer.com -- $ Buffer overflowed!
SPARK
SPARK is a subset of Ada which can be formally verified. Meaning that it's possible to verify the absence of runtime errors in your code using formal methods.
alr with gnatprove.
Let's see if we can reimplement the previous Rust example in SPARK, and prove that a buffer overflow can't occur.
procedure Overflow_This_Buffer with SPARK_Mode => On is type Integer_Array is array (Positive range <>) of Integer; Int_Array : Integer_Array (1 .. 10) := [others => 1]; Index_To_Clear : Integer; begin Ada.Text_IO.Put ("What array index should be cleared? "); -- Read the new array size from stdin. Ada.Integer_Text_IO.Get (Index_To_Clear); Int_Array (Index_To_Clear) := 0; end Overflow_This_Buffer;
Attempting to prove the absence of runtime errors gives us the following warnings:
buffer_overflow.adb:162:26: medium: unexpected exception might be raised
162 | Ada.Integer_Text_IO.Get (Index_To_Clear);
| ~~~~~~~~~~~~~~~~~~~^~~~~~~~~~~~~~~~~~~~
buffer_overflow.adb:164:18: medium: array index check might fail
164 | Int_Array (Index_To_Clear) := 0;
| ^~~~~~~~~~~~~~
reason for check: value must be a valid index into the array
possible fix: postcondition of call at line 162 should mention Item
(for argument Index_To_Clear)
162 | Ada.Integer_Text_IO.Get (Index_To_Clear);
| ^ here
The SPARK prover correctly notices that there's nothing stopping us
from entering a value outside the array bounds.
It also points out that the Get
call we're using to read the integer from stdin
can raise an unexpected Constraint_Error
at runtime if you type in anything that can't be parsed as an integer.
To keep this example simple, we'll ignore this warning and push on.
We'll talk more about exceptions in SPARK
later
in the article.
If we wrap the Get call in a loop,
and poll the user continuously until we have a value within the array bounds,
SPARK can actually prove that a buffer overflow can't occur.
(Remember to initialise the Index_To_Clear
variable to something outside this range!)
procedure Overflow_This_Buffer with SPARK_Mode => On is type Integer_Array is array (Positive range <>) of Integer; Int_Array : Integer_Array (1 .. 10) := [others => 1]; Index_To_Clear : Integer := Int_Array'First - 1; begin while Index_To_Clear not in Int_Array'Range loop Ada.Text_IO.Put ("What array index should be cleared? "); -- Read the new array size from stdin. Ada.Integer_Text_IO.Get (Index_To_Clear); end loop; Int_Array (Index_To_Clear) := 0; end Overflow_This_Buffer;
Use After Free #
CWE-416: Use After Free refers to dereferencing a pointer after the value it points to has been freed. The C standard specifies that doing so is Undefined Behaviour (ISO/IEC 9899:2018, Section J.2), potentially leading to a variety of different stability and security issues. (ISO/IEC 9899:2018, Section 3.4.3).
Most of the time this just results in unpredictable behaviour because the pointer now points to memory reallocated to something else. But occasionally use-after-free's can be leveraged for something more sinister.
Rust's borrow checker automatically prevents you from using a value after it's been freed.
Calling drop to manually free a variable moves it,
meaning that any attempt to use it afterwards will raise a compile-time error.
fn use_after_free() { let greeting = "Hello, World!".to_string(); drop(greeting); // This will trigger an error at compile-time, because the variable // `something` was moved by the first call to `std::mem::drop`. println!("{}", greeting); }
Nothing prevents you from writing Ada code that dereferences an access type after it's been freed;
However any access dereference triggers a runtime check to ensure it's non-null.
Unlike in C,
freeing an access type in Ada automatically sets its value to null,
and any subsequent attempt to dereference it will raise a
Constraint_Error exception,
which can be caught and handled.
procedure Use_After_Free is type String_Access is access String; Example_String : String_Access := null; -- The Ada.Unchecked_Deallocation package is a generic package, and -- needs to be instantiated for each type to be deallocated. procedure Free is new Ada.Unchecked_Deallocation (String, String_Access); begin Example_String := new String'("Hello, world!"); Free (Example_String); -- This will raise a Constraint_Error exception at runtime. Put_Line (Example_String.all); exception when Constraint_Error => Put_Line ("Used after freed!"); end Use_After_Free;
-gnatp compiler switch.
In this case, dereferencing a null access type will result in the same kind of undefined behaviour you'd get in C.
Ada allows you to specify a null-excluding constraint on access types, This restricts assignment to only non-null values, and forbids any unchecked deallocation.
type Non_Null_String_Access is not null access String; -- Since this is a 'null-excluding' access type, it must be initialised, -- otherwise a Constraint_Error exception will occur immediately at runtime. Example_String : Non_Null_String_Access := new String'("Hello, world!"); -- This will raise a compile-time error. The compiler won't let us -- create an instance of Ada.Unchecked_Deallocation for a -- null-excluding access type. procedure Free is new Ada.Unchecked_Deallocation (String, Non_Null_String_Access);
SPARK
GNATprove will detect the use-after-free error in the above code, and issue a warning4:
procedure Use_After_Free with SPARK_Mode => On is type String_Access is access String; Example_String : String_Access; procedure Free is new Ada.Unchecked_Deallocation (String, String_Access); begin Example_String := new String'("Hello, world!"); Free (Example_String); -- This line will raise a warning during static analysis. Put_Line (Example_String.all); end Use_After_Free;
use_after_free.adb:13:32: medium: pointer dereference check might fail
13 | Put_Line (Example_String.all);
| ~~~~~~~~~~~~~~~^~~
Note the removal of the exception handling block.
SPARK does technically allow run-time exception handling,
but only exceptions that are explicitly raised in the code.
Exceptions in SPARK are
complicated:
You can still explicitly raise exceptions with the raise statement,
but to be valid SPARK, the flow analyser will need to prove that the statement raising the exception can never actually be reached;
Making exceptions almost like a form of compile-time assertion.
This means that our Constraint_Error exception handler is unreachable,
and needs to be removed.
Double Free #
CWE-415: Double Free refers to freeing a heap allocated variable more than once. The C standard (as usual) specifies that doing so is Undefined Behaviour (ISO/IEC 9899:2018, Section J.2). Double frees can be exploited in various ways to cause all kinds of nonsense.
On Linux,
glibc
stores extra metadata about each allocated memory block right before the block's address,
such as its size, and a magic number to identify it as a valid allocation.
When you pass an address to free,
glibc uses this metadata to determine the amount of memory being freed.
Freeing a small block of heap memory can place it in a cache of recently freed blocks,
known as a fast bin.
The next time you call malloc for a block of the same size,
glibc will give you the recently deallocated block from the fast bin,
rather than allocating new memory.
This process is much quicker than allocating a new block, hence the fast in the name.
Freeing the same address twice runs the risk of the same block being placed in the fast bin
multiple times.
This could lead to multiple subsequent memory allocations pointing to the same address.
This article contains a great in-depth look at glibc's heap implementation.
Rust's borrow checker effectively prevents you from freeing the same variable more than once.
As mentioned earlier,
calling drop to free a variable will move it out of scope forever.
fn double_free() { let something = "Hello, World!".to_string(); drop(something); // This will trigger an error at compile-time, because the variable // `something` was moved by the first call to `std::mem::drop`. drop(something); }
According to
section 13.11.2
of the Ada Reference Manual,
freeing an access type with a null value has no effect,
just like in C (ISO/IEC 9899:2018, Section 7.22.3.3).
That's a relief!
As mentioned earlier, freeing a pointer in Ada will automatically set its value to null,
preventing most accidental double free errors from causing any serious issues.
It's still possible to cause a double free in Ada by creating an alias to a pointer.
procedure Double_Free is type String_Access is access String; Str_Acc : String_Access; Str_Acc_Alias : String_Access; procedure Free is new Ada.Unchecked_Deallocation (String, String_Access); begin Str_Acc := new String'("Hello, world!"); Put_Line ("Pointer Address: " & Str_Acc.all'Address'Image); Str_Acc_Alias := Str_Acc; Free (Str_Acc); Put_Line ("Pointer Alias Address: " & Str_Acc_Alias.all'Address'Image); Free (Str_Acc_Alias); exception when Program_Error => Put_Line ("Program Error!"); end Double_Free; -- $ alr run -- $ Pointer Address: 25715368 -- $ Pointer Alias Address: 25715368 -- $ free(): double free detected in tcache 2 -- $ Program Error!
As you can see in the example above,
actually freeing the same memory location twice5 will raise a
Program_Error exception at runtime.
The below example shows how you can corrupt the heap by double freeing a pointer in Ada.
Again, Ada will raise a Program_Error exception when it gets the error signal from glibc,
which can be handled at runtime.
procedure Double_Free is type String_Access is access String; type String_Access_Array is array (1 .. 16) of String_Access; procedure Free is new Ada.Unchecked_Deallocation (String, String_Access); Str_Acc_Array : String_Access_Array; Str_Acc_Array_2 : String_Access_Array; -- Create a pointer to alias one of the elements in the array. Str_Acc_Alias : String_Access; begin for I in Str_Acc_Array'Range loop Str_Acc_Array (I) := new String'("Hello, world!"); end loop; Str_Acc_Alias := Str_Acc_Array (8); for I in Str_Acc_Array'Range loop Free (Str_Acc_Array (I)); end loop; -- Freeing the alias will add the same address to the fast bin twice, -- leading to a double free error. Free (Str_Acc_Alias); for I in Str_Acc_Array_2'Range loop Str_Acc_Array_2 (I) := new String'("Hello, again!"); end loop; exception when Program_Error => Put_Line ("Program Error!"); end Double_Free; -- $ alr run -- $ malloc(): unaligned fastbin chunk detected 3 -- $ Program Error!
SPARK
Like Rust, SPARK has its own concept of 'ownership'. Assignment between access objects creates a transfer of ownership, with the source object losing permission to read or write to the underlying allocated memory.
In this case, aliasing the string pointers in the examples above is not valid SPARK, preventing us from causing this particular double free error.
alr gnatprove
Phase 1 of 3: generation of data representation information ...
Phase 2 of 3: generation of Global contracts ...
Phase 3 of 3: flow analysis and proof ...
double_free.adb:14:13: error: "Str_Acc" is not readable
14 | Free (Str_Acc);
| ^~~~~~~
object was moved at line 12 [E0010]
12 | Str_Acc_Alias := Str_Acc;
| ^ here
launch "gnatprove --explain=E0010" for more information
SPARK doesn't allow you to use Unchecked_Deallocation
with a general access type (which we'll discuss in more detail later),
so we can't try to sidestep SPARK's ownership system by doing something tricky like this:
procedure Double_Free with SPARK_Mode => On is type String_Access is access all String; Str_Acc : String_Access; Str_Acc_Alias : String_Access; procedure Free is new Ada.Unchecked_Deallocation (String, String_Access); begin Str_Acc := new String'("Hello, world!"); Put_Line (Str_Acc.all); -- Here we create an access to the dereferenced value of Str_Acc. Str_Acc_Alias := Str_Acc.all'Access; Free (Str_Acc); Free (Str_Acc_Alias); end Double_Free;
SPARK sees what we're up to and stops us in our tracks:
double_free.adb:13:17: error: instance of Unchecked_Deallocation with a
general access type is not allowed in SPARK
13 | procedure Free is new Ada.Unchecked_Deallocation (String, String_Access);
| ^~~~
violation of aspect SPARK_Mode at line 6
6 | with SPARK_Mode => On
| ^ here
Race Conditions #
In a multi-threaded program, a Race condition is a situation where the outcome of the program depends on the order in which the threads execute. Because an operating system can switch between threads at any time in any order, it's impossible to guarantee when threads will access shared resources. This really becomes a problem when two threads try to write to the same memory at the same time; Leading to some of the most infuriating, time-consuming, and hair-raising bugs in software development.
One common race condition is a Time-of-check to time-of-use error, or TOC/TOU; In which a resource changes between the time it's checked for validity, and the time it's used. Maybe one thread checks to see if a file already exists before creating it, gets interrupted after the initial check, and then another thread creates the new file before the first thread can. This has led to real world vulnerabilities in the past.
Consider the following example:
#define THREAD_COUNT 2 #define STARTING_BALANCE 10000 int balance = STARTING_BALANCE; int withdrawn_amounts[THREAD_COUNT]; void update_account_balance(int new_balance) { // Simulate a delay consistent with a real-world system. nanosleep(&(struct timespec){0, rand() % 100000}, NULL); balance = new_balance; } bool withdraw(int thread_id, int amount) { bool result = false; if (balance >= amount) { update_account_balance (balance - amount); withdrawn_amounts[thread_id] += amount; result = true; } return result; } void *spend_recklessly(void *_thread_id) { while(withdraw((long)_thread_id, 100 + (rand() % 5) * 200)); return NULL; } int main() { pthread_t threads[THREAD_COUNT]; for (int i = 0; i < THREAD_COUNT; i++) { withdrawn_amounts[i] = 0; pthread_create(&threads[i], NULL, spend_recklessly, (void *)i); } for (int i = 0; i < THREAD_COUNT; i++) { pthread_join(threads[i], NULL); } printf("Starting balance: %d\nFinal balance: %d\n", STARTING_BALANCE, balance); int total_withdrawn = 0; for (int i = 0; i < THREAD_COUNT; i++) { printf("Thread %d withdrew: %d\n", i, withdrawn_amounts[i]); total_withdrawn += withdrawn_amounts[i]; } printf("Total amount withdrawn: %d\n", total_withdrawn); return EXIT_SUCCESS; } // $ gcc -o bank_race_condition bank_race_condition.c // $ ./bank_race_condition // $ Starting balance: 10000 // $ Final balance: 400 // $ Thread 0 withdrew: 9700 // $ Thread 1 withdrew: 7700 // $ Total amount withdrawn: 17400
This example spawns two threads using the POSIX threads API. Each thread withdraws money from a shared 'bank account' until there's nothing left. I've introduced an artificial delay when 'saving' the new account balance to simulate real world conditions, like communicating over a network, or writing to a database. Because of the delay between checking the available balance and updating it after a withdrawal, over time each thread will consistently withdraw much more than the account's total balance. This bank might have a hard time balancing its sheets.
The most common way to resolve this problem is to use a mutex. A mutex (from Mutual Exclusion) is a construct that restricts access to a certain section of code to only one thread at a time. The first thread to acquire the mutex gets access, other threads need to wait until the first thread releases it. This area of code protected by the mutex is known as a critical section
Wrapping the withdraw
function in a mutex so that only one thread can withdraw at a time will prevent the race condition:
// ... pthread_mutex_t bank_account_mutex = PTHREAD_MUTEX_INITIALIZER; // ... bool withdraw(int thread_id, int amount) { pthread_mutex_lock(&bank_account_mutex); bool result = false; if (balance >= amount) { update_account_balance (balance - amount); withdrawn_amounts[thread_id] += amount; result = true; } pthread_mutex_unlock(&bank_account_mutex); return result; } // ... // $ gcc -o bank_race_condition bank_race_condition.c // $ ./bank_race_condition // $ Starting balance: 10000 // $ Final balance: 0 // $ Thread 0 withdrew: 4700 // $ Thread 1 withdrew: 5300 // $ Total amount withdrawn: 10000
Out of the box, Rust supports two methods of synchronising threads: shared-state concurrency using Mutexes, and message-passing using Channels.
When spawning a new thread,
Rust's memory model guarantees that any memory it accesses lives at least as long as the thread itself,
and that the data can't be moved into two threads at the same time.
The Rust compiler prevents race conditions by enforcing that shared data access only takes place through Rust's concurrency primitives:
The only way to actually share memory between threads is to wrap it in a Mutex,
and access it using Rust's
Atomic Reference Counted smart pointer type (Arc<T>).
The below example demonstrates a simplified version of our 'bank' program in Rust:
fn spending_safely() { let account_balance = Arc::new(Mutex::new(STARTING_BALANCE)); let withdrawn_amounts = Arc::new(Mutex::new(vec![0; THREAD_COUNT])); let mut thread_handles = vec![]; for thread_id in 0..THREAD_COUNT { let balance_pointer = Arc::clone(&account_balance); let amounts_pointer = Arc::clone(&withdrawn_amounts); thread_handles.push(thread::spawn(move || { let mut rng = rand::thread_rng(); let amount = 100 + rng.gen_range(0..5) * 200; while (*balance_pointer.lock().unwrap()) >= amount { *balance_pointer.lock().unwrap() -= amount; amounts_pointer.lock().unwrap()[thread_id] += amount; std::thread::sleep(Duration::from_nanos(100)); } })); } for handle in thread_handles { handle.join().unwrap(); } println!("Starting balance: {}", STARTING_BALANCE); println!("Final balance: {}", *account_balance.lock().unwrap()); let total_withdrawn: i32 = withdrawn_amounts.lock().unwrap().iter().sum(); for (thread_id, &amount) in withdrawn_amounts.lock().unwrap().iter().enumerate() { println!("Thread {} withdrew: {}", thread_id, amount); } println!("Total amount withdrawn: {}", total_withdrawn); } // $ cargo run // $ Starting balance: 10000 // $ Final balance: 0 // $ Thread 0 withdrew: 7500 // $ Thread 1 withdrew: 2500 // $ Total amount withdrawn: 10000
Ada has its own nomenclature for multithreading: Tasks, and provides its own built-in mechanism for preventing data races between them. Ada's Protected Objects encapsulate data inside an implicit mutex, allowing only one thread access at a time via a public interface.
The following example builds on the previous one, showing two Ada 'tasks' sharing access to a single, 'protected' resource:
procedure Bank is Float_Generator : Ada.Numerics.Float_Random.Generator; function Get_Random_Delay return Duration is (Duration (Ada.Numerics.Float_Random.Random (Float_Generator))); function Get_Random_Amount return Integer is (Integer (Ada.Numerics.Float_Random.Random (Float_Generator) * 999.0)); protected Bank_Account is function Get_Balance return Integer; procedure Withdraw (Amount : Integer); private Balance : Integer := 10000; end Bank_Account; protected body Bank_Account is function Get_Balance return Integer is (Balance); procedure Withdraw (Amount : Integer) is begin Balance := Balance - Amount; end Withdraw; end Bank_Account; task type Reckless_Spender_Task (Id : Integer); task body Reckless_Spender_Task is Amount : Integer := Get_Random_Amount; Cash : Integer := 0; begin while not (Bank_Account.Get_Balance < Amount) loop Bank_Account.Withdraw (Amount); Cash := Cash + Amount; Amount := Get_Random_Amount; delay Get_Random_Delay; end loop; Put_Line ("Spender" & Id'Image & " withdrew" & Cash'Image); end Reckless_Spender_Task; Spender_1 : Reckless_Spender_Task (1); Spender_2 : Reckless_Spender_Task (2); begin null; end Bank;
Wrapping the Balance
variable inside the protected Bank_Account
object ensures that only the task holding the mutex can access it.
Unfortunately, like in C, nothing actually prevents you from writing code that accesses shared memory from multiple tasks.
procedure Bank is Float_Generator : Ada.Numerics.Float_Random.Generator; function Get_Random_Delay return Duration is (Duration (Ada.Numerics.Float_Random.Random (Float_Generator))); function Get_Random_Amount return Integer is (Integer (Ada.Numerics.Float_Random.Random (Float_Generator) * 999.0)); Balance : Integer := 10000; task type Reckless_Spender_Task (Id : Integer); task body Reckless_Spender_Task is Amount : Integer := Get_Random_Amount; Cash : Integer := 0; begin while not (Balance < Amount) loop Cash := Cash + Amount; delay Get_Random_Delay; Amount := Get_Random_Amount; Balance := Balance - Amount; end loop; Put_Line ("Spender" & Id'Image & " withdrew" & Cash'Image); end Reckless_Spender_Task; Spender_1 : Reckless_Spender_Task (1); Spender_2 : Reckless_Spender_Task (2); Spender_3 : Reckless_Spender_Task (3); Spender_4 : Reckless_Spender_Task (4); begin null; end Bank; -- $ alr run -- $ Spender 2 withdrew 1711 -- $ Spender 3 withdrew 3910 -- $ Spender 1 withdrew 2269 -- $ Spender 4 withdrew 2254
SPARK
SPARK supports tasking when the Ravenscar profile is used, and is able to prove the absence of race conditions and other concurrency-related errors. Ravenscar is a build configuration designed for hard real-time, safety-critical systems. It restricts language features unsuitable for safe multi-threaded programming.
Describing how to write formally verifiable concurrent code in SPARK would need an article all of its own. For a good starting point, check out AdaCore's SPARK Reference Manual, and their Introduction To SPARK course.
Dangling Pointer #
A pointer that still points to an object in memory after it's been deallocated is known as a Dangling Pointer.
Try as I might, I couldn't find a way to create a dangling pointer in safe Rust. The borrow-checker was way ahead of me.
fn create_dangling_pointer() -> &String { let s = String::from("hello"); &s } // $ cargo run // $ Compiling dangling_pointer v0.1.0 (/home/ajxs/src/rust_examples) // $ error[E0106]: missing lifetime specifier // $ --> src/main.rs:10:33 // $ | // $ 10 | fn create_dangling_pointer() -> &String { // $ | ^ expected named lifetime parameter // $ | // $ = help: this function's return type contains a borrowed value, // $ but there is no value for it to be borrowed from // $ ...
I had to heavily abridge the avalanche of warnings the Rust compiler generated from this example.
Ada has a mechanism for preventing dangling pointers,
called accessibility levels.
An object's accessibility level reflects the nesting of the scope it's defined in,
and determines what objects an access type is allowed to point to.
For example, if Procedure_B is nested within Procedure_A,
it's said to have a deeper accessibility level than its parent.
An access type in Ada can only point to an object at the same accessibility level,
or shallower,
ensuring that an object lives at least as long as any access types pointing to it.
Every type has its own accessibility level,
and objects have the same accessibility level as their type.
The following example illustrates how Ada's accessibility levels prevent dangling pointers.
procedure Accessibility_Levels is type Level_0_Integer_Access_T is access all Integer; Level_0_Integer : aliased Integer := 0; Level_0_Integer_Access : Level_0_Integer_Access_T := Level_0_Integer'Access; procedure Level_1_Procedure is type Level_1_Integer_Access_T is access all Integer; Level_1_Integer_Access : Level_1_Integer_Access_T := null; Level_1_Integer : aliased Integer := 1; begin -- LEGAL: Level_1_Integer_Access is declared at the same -- accessibility level as Level_1_Integer. Level_1_Integer_Access := Level_1_Integer'Access; -- LEGAL: Level_1_Integer_Access is declared at a deeper -- accessibility level as Level_0_Integer. -- An object of type Level_1_Integer_Access can't possibly outlive -- the Level_0_Integer object. Level_1_Integer_Access := Level_0_Integer'Access; -- ILLEGAL: This will cause a compile-time error. -- The object Level_1_Integer is declared at a deeper accessibility -- level than Level_0_Integer_Access. -- The compiler can't be sure that the object would live as long as -- the access type pointing to it. Level_0_Integer_Access := Level_1_Integer'Access; end Level_1_Procedure; begin Level_1_Procedure; Put_Line ("Value: " & Level_0_Integer_Access.all'Image); end Accessibility_Levels;
Ada allows developers to ignore the accessibility levels system with the
Unchecked_Access aspect.
The above code would compile without any errors if the failing line above was replaced with:
-- ... -- LEGAL: No problem! The compiler figures you know what you're doing... Level_0_Integer_Access := Level_1_Integer'Unchecked_Access; end Level_1_Procedure; begin Level_1_Procedure; -- Uh oh... Put_Line ("Value: " & Level_0_Integer_Access.all'Image); end Accessibility_Levels;
Freeing Stack Memory #
As mentioned earlier in the section on double freeing memory, glibc stores metadata about each allocated memory block right before the block's address. This lets it determine the amount of memory being freed, and check whether the address actually points to something allocated on the heap.
Attempting to free an object allocated on the stack will bring your program to a screeching halt once glibc figures out what you're upto.
void free_stack_memory() { // Note that modern versions of gcc will issue a warning about this: // warning: ‘free’ called on unallocated object ‘x’ [-Wfree-nonheap-object] int x = 10; free(&x); printf("Phew! We made it!\n"); } // $ gcc -o free_stack_memory free_stack_memory.c // $ ./free_stack_memory // $ free(): invalid pointer // $ Aborted
As mentioned earlier, Rust automatically deallocates variables when they go out of scope;
Calling their destructor when necessary.
Calling std::mem::drop
on a stack allocated variable (that implements the Drop trait6)
will explicitly call its destructor, and deallocate the object.
The fact that it was allocated in stack memory has no effect.
In Ada, access types ordinarily only point to heap-allocated memory;
However you can create a general access type by adding the
all keyword to its type declaration,
which allows it to point to any object of its type,
including objects allocated on the stack,
provided they are actually addressable7.
Freeing a general access type pointing to stack memory will raise a
Program_Error exception at runtime,
which can be caught and handled in the normal way.
procedure Free_Stack_Memory is -- The 'all' specifier here indicates that this is a 'general access type', -- which can point to objects allocated on the heap OR the stack. type String_Access is access all String; String_On_Stack : aliased String := "Hello from the stack!"; Example_String : String_Access := String_On_Stack'Access; procedure Free is new Ada.Unchecked_Deallocation (String, String_Access); begin -- Attempting to free this variable will raise a 'Program_Error' exception. Free (Example_String); exception when E : Program_Error => Put_Line ("Program_Error: " & Exception_Message (E)); end Free_Stack_Memory;
Am I Being Unfair to Ada? #
Am I being unfair to Ada? Have I turned my back on the Ada community, betrayed my own kind? Have I been converted from an Ada zealot into a born-again Rustacean? Not quite.
A comparison on memory safety might tilt slightly in Rust's favour, but Ada's real strengths lie elsewhere. Its strong typing, intuitive low-level programming semantics, and static analysis capability are still unmatched by other systems languages.
As I stated earlier you can do a lot in Ada without ever needing to use pointers, or even using heap memory at all, sparing yourself the risk of most of these problems.
Unlike Rust, Ada allows stack variables of statically unknown size.
The Vec type in Rust's standard library is great,
but it stores its contents on the heap,
and won't be suitable for all use-cases.
procedure Variable_Size_Stack_Array is Array_Size : Integer; begin Ada.Text_IO.Put ("What array size would you like? "); -- Read the new array size from stdin. Ada.Integer_Text_IO.Get (Array_Size); Integer_Array : array (1 .. Array_Size) of Integer := [others => 0]; Ada.Text_IO.Put_Line ("Array Size: " & Integer_Array'Length'Image); end Variable_Size_Stack_Array;
In Ada, stack-allocated, variable length arrays are first-class values. You can return them from functions, and accept them as function parameters. They implicitly contain their bounds as part of their value. The following example builds on the code above. Note that everything here is happening on the stack.
procedure Stack_Allocated_Array_Examples is type Integer_Array is array (Positive range <>) of Integer; -- Ada has no problem returning a variable length, stack-allocated -- array from a function. function Create_Variable_Size_Stack_Array return Integer_Array is Array_Size : Integer; begin Ada.Text_IO.Put ("What array size would you like? "); -- Read the new array size from stdin. Ada.Integer_Text_IO.Get (Array_Size); Int_Array : constant Integer_Array (1 .. Array_Size) := [others => 0]; return Int_Array; end Create_Variable_Size_Stack_Array; -- Ada also has no problem accepting a variable length, stack-allocated -- array as a parameter. procedure Print_Variable_Length_Array (Int_Array : Integer_Array) is begin for I in Int_Array'Range loop Ada.Text_IO.Put_Line (Int_Array (I)'Image); end loop; end Print_Variable_Length_Array; begin Int_Array : constant Integer_Array := Create_Variable_Size_Stack_Array; Print_Variable_Length_Array (Int_Array); end Stack_Allocated_Array_Examples;
Ada's aversion to dynamic memory allocation is reminiscent of a different time; When embedded systems ran on 16-bit microcontrollers, with no operating system, no heap memory, and memory fragmentation could —quite literally— send your program crashing down to earth.
Despite this, the systems programming language ecosystem is only just now catching up to where Ada has been since the 90s. That's not to say Ada has stood still! Under AdaCore's stewardship the language has moved forward in leaps and bounds, and the Alire package manager has made Ada more accessible than ever. Whether you're ever going to write Ada or not, there's a lot you can learn from it. If you're designing a modern systems language, understanding what makes Ada good is essential8.
Conclusions? #
I actually came away from writing this article with more respect for Rust. It does a great job of preventing lots of common bugs entirely at compile-time. I still think Rust is clunky and frustrating at times, but all in all it's an impressive language that really advances the state of the art.
A lot of people are put off by the excessive technicality of Rust's semantics. Myself included. One thing Ada does really well is keeping a lot of its complicated machinery hidden. That might sound a bit dangerous for a low-level programming language, but Ada manages it perfectly, and has been battle-tested by decades of use in safety-critical systems. You never miss worrying about whether a parameter is passed by value or reference, or envy Rust's confusing multitude of string types.
To give Rust its due, I think its designers had the right idea. For all its technicality, Rust's design is forward-thinking and modern. I hope the new programming languages of 2050 will look at both Ada and Rust, see what each of them did right, and be better than both of them.
References #
- ISO/IEC 9899 (2018) Information technology — Programming languages — C
-
The Rust Handbook even gives us a recipe for creating our very own memory leak! By creating a reference cycle, where two smart pointers reference each other. When this happens, the amount of references to each pointer will never reach zero, and the objects will never be deallocated.
#[derive(Debug)] struct Node { value: i32, next: Option<Rc<RefCell<Node>>>, prev: Option<Rc<RefCell<Node>>>, } fn reference_cycle() { let node1 = Rc::new(RefCell::new(Node { value: 1, next: None, prev: None, })); let node2 = Rc::new(RefCell::new(Node { value: 2, next: None, prev: None, })); // Create a reference cycle between the two nodes. node1.borrow_mut().next = Some(Rc::clone(&node2)); node2.borrow_mut().prev = Some(Rc::clone(&node1)); println!( "Reference counts: \n First = {}\n Second = {}", Rc::strong_count(&node1), Rc::strong_count(&node2) ); }
Running the above code in Valgrind confirms there's a memory leak:
$ valgrind ./target/debug/reference_cycle_example ==60830== Memcheck, a memory error detector ==60830== Copyright (C) 2002-2022, and GNU GPL'd, by Julian Seward et al. ==60830== Using Valgrind-3.19.0 and LibVEX; rerun with -h for copyright info ==60830== Command: ./target/debug/reference_cycle_example ==60830== Reference counts: First = 2 Second = 2 ==60830== ==60830== HEAP SUMMARY: ==60830== in use at exit: 96 bytes in 2 blocks ==60830== total heap usage: 11 allocs, 9 frees, 2,256 bytes allocated ==60830== ==60830== LEAK SUMMARY: ==60830== definitely lost: 48 bytes in 1 blocks ==60830== indirectly lost: 48 bytes in 1 blocks ==60830== possibly lost: 0 bytes in 0 blocks ==60830== still reachable: 0 bytes in 0 blocks ==60830== suppressed: 0 bytes in 0 blocks ==60830== Rerun with --leak-check=full to see details of leaked memory ==60830== ==60830== For lists of detected and suppressed errors, rerun with: -s ==60830== ERROR SUMMARY: 0 errors from 0 contexts (suppressed: 0 from 0)
It's also interesting that printing the value of either of the nodes in the above code will result in a stack overflow. ↲
- Section 4.8 of the Ada Reference Manual states that an implementation is free, but not required, to implement a garbage collector. Aside from one experimental patch for GCC, I'm not aware of any mainstream Ada compiler that uses a garbage collector. However at one point there were several commercial Ada compilers that targeted the Java Virtual Machine, which would have featured the JVM's default garbage collector. ↲
- Ada's storage pool feature gives it native support for arena allocators, and gives developers fine-grained control of how an access type is allocated, and deallocated. This can be used to create custom reference-counted types, or give a program control over its own memory management at runtime. ↲
- Funnily enough, the static analyser can only prove the absence of runtime errors. When it can't prove that a runtime error won't occur, it'll give you a warning. Here, the static analyser has identified a situation where it's possible that the pointer could be null when accessed. ↲
-
Note also that glibc will only detect freeing the same address consecutively.
Also note that dereferencing the already freed aliased pointer to print its address
doesn't raise a
Constraint_Errorexception for some unknown reason. ↲ -
Explicitly calling
std::mem::dropon a variable that doesn't implement theDroptrait does nothing, other than raising a compile-time warning. ↲ -
The C standard specifies that objects must be addressable,
unless they are declared with the
registerstorage-class specifier (ISO/IEC 9899:2018, Section 6.5.3.2). The Ada standard does not impose this restriction, and Ada compilers are free to allocate objects entirely within registers. In Ada, thealiasedkeyword is used to indicate that a particular object must be addressable. ↲ - For what it's worth, I'm led to believe the Rust designers did study Ada to some extent. Discussions of Ada's features have featured in Rust's RFCs in the past. ↲