From Rust to SPARK: Formally Proven Bip-Buffers

by Fabien Chouteau – May 05, 2021

I am following the evolution of the embedded Rust community and in particular the work of James Munns from Ferrous-Systems. One of the projects that caught my attention is bbqueue, a single producer, single consumer, lockless, thread safe queue, based on BipBuffers.

The main usage for this library is asynchronous handling of data coming in or going out of a peripheral, in particular when using Direct Memory Access (DMA).

When receiving data from a peripheral, say an Ethernet controller, the user has to provide a chunk of memory where a packet can be stored when it is received. Once the packet is fully received, there will usually be an interrupt to signal the arrival of the packet and another chunk of memory has to be provided very quickly in case another packet arrives during the processing of the first one. Most of the time the reception and the processing of the data will be handled in different contexts, for example an interrupt handler and a thread. The packet has to be decoded through various stacks of protocol and in the end the data has to be presented to the user. Copying potentially large blocks of data as it moves through the protocol stacks to the user must be minimized for the sake of performance.

With bip-buffers, the producer part of the application can request a “write grant” for a contiguous chunk of writable memory. Once data is written to this chunk, the producer “commits” it, which means it is ready for the consumer to read. On the other side, the consumer can request a “read grant” for a contiguous chunk of data that was previously committed by the producer. Once the read data is no longer needed, the consumer can “release” it, which means that it is available for the producer.

The fact that the areas provided by the buffer are guaranteed contiguous is central to the purpose. That’s essential for DMA use, but something that a more typical circular bounded buffer cannot guarantee. Furthermore, the “commit/release” protocol means clients can work directly within the buffer. There’s no need to copy data from the buffer into a user memory area to make it contiguous.

James’ bbqueue uses atomic operations to provide a lock-free implementation of bip-buffers. This means that producer and consumer can run in different execution threads (or interrupts) and use the bbqueue safely without resorting to synchronisation primitives such as mutexes or protected objects in the Ada world.

I recommend looking at James Munns’ blog post to learn more about the algorithm and his implementation, the rest of this post will be easier to understand if you do so. Note that the Rust implementation that I used as a basis for this project has changed since the publication of James’ blog post, some minor discrepancies are to be expected in the implementation.

From Rust to SPARK #

As I try to explain above, bip-buffers can be very useful for embedded systems, even more so a lock-free implementation. So I started a project to bring this solution to the Ada ecosystem. But I wanted to bring more than just a translation from Rust to Ada, and therefore used this opportunity to bring SPARK formal verification in the mix.

The bbqueue implementation mostly deals with indexes in a buffer. There is an index that keeps track of the next memory to be written to, another one for the memory to be read, etc (see James’ blog post).

With SPARK I wanted to prove some functional properties that will show that the implementation is correct. For instance, I wanted to prove that when a writable slice of the buffer is granted:

The slice is valid: lower and upper bounds are within the bounds of the buffer
The slice is writable: the lower and upper bounds are within a writable part of the buffer
The size of the slice is equal to the requested size, or zero if there is not enough free space available

To be able to prove those properties, I wrote helper functions to refine the problem. The function below expresses what it means for an index to be within a writable area:

function In_Writable_Area (This : Buffer; Offset : Buffer_Offset) return Boolean
   is (if Is_Inverted (This) then
          --  Already inverted
          --  |---W==========R----|
          --  Inverted (R > W):
          --  We can write between W .. R - 1
          Offset in This.Write .. This.Read - 1
       else (
             --  |====R---------W=====|
             --  Not Inverted (R <= W):
             --  We can write between W .. Size - 1, or 0 .. R - 1 if we invert
               (Offset in This.Write .. This.Size - 1)
             or else
               (Offset in 0 .. This.Read - 1)));

From this function it is easy to write a definition of a valid writable slice, and then use this definition as a postcondition for the subprogram that grants writable slices.

function Valid_Write_Slice (This : Buffer; Slice : Slice_Rec) return Boolean
is (Valid_Slice (This, Slice)
    and then In_Writable_Area (This, Slice.From)
    and then In_Writable_Area (This, Slice.To));

procedure Grant (This : in out Buffer;
                 G    : in out Write_Grant;
                 Size : Count)
     with Post => (if Size = 0 then State (G) = Empty)
                   and then
                  (if State (G) = Valid
                       then Write_Grant_In_Progress (This)
                   and then Slice (G).Length = Size
                   and then Valid_Slice (This, Slice (G))
                   and then Valid_Write_Slice (This, Slice (G)));
--  Request indexes of a contiguous writeable slice of exactly Size elements

Another important part of achieving the proof was the definition of invariants on the buffer type. In a way, I consider this as explaining the algorithm to SPARK’s automatic provers.

In the end I managed to get 100% proof on the code. I also used the GitHub actions workflow to run the GNATprove automatically on pull-requests. If you try to break the code (https://github.com/Fabien-Chouteau/bbqueue-spark/pull/2) you should see a message like this:

How to use the SPARK bbqueue #

This Ada/SPARK implementation of bbqueue is available in the Alire package manager alire.ada.dev. To import it to your project, you simply have to run this command:

$ alr with bbqueue

Offsets_Only #

The root package of the bbqueue crate implements a type that only deals with indexes, without having an internal buffer. This is useful in multiple cases.

1) Using the same slices in multiple buffers. For instance in an audio application the stereo left and right channels can be in separate buffers:

declare
   Left  : Sample_Array (1 .. 64) := (others => 0);
   Right : Sample_Array (Left’Range) := (others => 0);
   Q     : aliased Offsets_Only (Left'Length);
   WG    : Write_Grant := BBqueue.Empty;
   S     : Slice_Rec;
begin
   Grant (Q, WG, 8);
   if State (WG) = Valid then
      S := Slice (WG);
      Left (Left'First + S.From .. Left'First + S.To) := (others => 42);
      Right (Right'First + S.From .. Right'First + S.To) := (others => -42);
      Commit (Q, WG);
   end if;

2) Using bbqueue for allocating slices on something other than an array of bytes:

declare
   type My_Data is record
      A, B, C : Integer;
   end record;
   type My_Data_Array is array (Natural range <>) of My_Data;

   Buf : My_Data_Array (1 .. 64);
   Q   : aliased Offsets_Only (Buf'Length);
   WG  : Write_Grant := BBqueue.Empty;
   S   : Slice_Rec;
begin
   Grant (Q, WG, 8);
   if State (WG) = Valid then
      S := Slice (WG);
      Buf (Buf'First + S.From .. Buf'First + S.To) := (others => (1, 2, 3));
      Commit (Q, WG);
   end if;

Buffers #

The package BBqueue.Buffers is based on Offsets_Only but provides an internal buffer. This is a more convenient package if you just want to allocate chunks of memory:

declare
   Q   : aliased Buffer (64);
   WG  : Write_Grant := Empty;
   S   : Slice_Rec;
begin
   Grant (Q, WG, 8);
   if State (WG) = Valid then
      declare
         B : Storage_Array (1 .. Slice (WG).Length)
           with Address => Slice (WG).Addr;
      begin
         B := (others => 42);
      end;
      Commit (Q, WG);
   end if;

Framed Buffers #

The last variant of bbqueue is Framed_Buffer. With the bbqueue implementations presented so far, when the consumer requests data, the biggest readable slice is returned. Framed_Buffer however keeps track of the length of each commit from the producer, and the slices returned to the consumer correspond to the commits. This is very useful for protocols with variable length packets.

declare
   Q   : aliased Framed_Buffer (64);
   WG  : Write_Grant := Empty;
   RG  : Read_Grant := Empty;
   S   : Slice_Rec;
begin
   Grant (Q, WG, 8); -- Get a grant of 8
   Commit (Q, WG, 4); -- Only commit 4
   Grant (Q, WG, 8); -- Get a grant of 8
   Commit (Q, WG, 5); -- Only commit 5
   Read (W, RG); -- Returns a grant of size 4

Atomics #

As said at the beginning of this post, bbqueue is a lockless, thread safe implementation of bip-buffers. To achieve the lockless property of the implementation, atomic operations are used to read, write and modify indexes.

For this I created another Alire crate that provides SPARK bindings over GCC intrinsic atomic functions.

Contracts are added to the binding subprogram specifications to allow SPARK provers to understand what the atomic intrinsics do. For example:

generic
   type T is mod <>;
package Atomic.Generic8
with Preelaborate, Spark_Mode
is

   type Instance is limited private;
   --  This type is limited and private, it can only be manipulated using the
   --  primitives below.


   procedure Add_Fetch (This   : aliased in out Instance;
                        Val    : T;
                        Result : out T;
                        Order  : Mem_Order := Seq_Cst)
     with Post => Result = (Value (This)'Old + Val)
                   and then
                  Value (This) = Result;

Conclusion #

This project was my first SPARK project, and getting to 100% automatic proof was a challenging task. Now that it is done, the cost of maintaining the code is greatly reduced and this initial effort will pay in the long run.

As always, feedback is welcome, and don’t hesitate to let us know if you find this implementation useful for your projects.

Posted in

About Fabien Chouteau

Fabien joined AdaCore in 2010 after his engineering degree at the EPITA (Paris). He is involved in real-time, embedded and hardware simulation technology. Maker/DIYer in his spare time, his projects include electronics, music and woodworking.