AdaCore Blog

From Rust to SPARK: Formally Proven Bip-Buffers

by Fabien Chouteau

I am fol­low­ing the evo­lu­tion of the embed­ded Rust com­mu­ni­ty and in par­tic­u­lar the work of James Munns from Fer­rous-Sys­tems. One of the projects that caught my atten­tion is bbqueue, a sin­gle pro­duc­er, sin­gle con­sumer, lock­less, thread safe queue, based on Bip­Buffers.

The main usage for this library is asyn­chro­nous han­dling of data com­ing in or going out of a periph­er­al, in par­tic­u­lar when using Direct Mem­o­ry Access (DMA).

When receiv­ing data from a periph­er­al, say an Eth­er­net con­troller, the user has to pro­vide a chunk of mem­o­ry where a pack­et can be stored when it is received. Once the pack­et is ful­ly received, there will usu­al­ly be an inter­rupt to sig­nal the arrival of the pack­et and anoth­er chunk of mem­o­ry has to be pro­vid­ed very quick­ly in case anoth­er pack­et arrives dur­ing the pro­cess­ing of the first one. Most of the time the recep­tion and the pro­cess­ing of the data will be han­dled in dif­fer­ent con­texts, for exam­ple an inter­rupt han­dler and a thread. The pack­et has to be decod­ed through var­i­ous stacks of pro­to­col and in the end the data has to be pre­sent­ed to the user. Copy­ing poten­tial­ly large blocks of data as it moves through the pro­to­col stacks to the user must be min­i­mized for the sake of performance.

With bip-buffers, the pro­duc­er part of the appli­ca­tion can request a write grant” for a con­tigu­ous chunk of writable mem­o­ry. Once data is writ­ten to this chunk, the pro­duc­er com­mits” it, which means it is ready for the con­sumer to read. On the oth­er side, the con­sumer can request a read grant” for a con­tigu­ous chunk of data that was pre­vi­ous­ly com­mit­ted by the pro­duc­er. Once the read data is no longer need­ed, the con­sumer can release” it, which means that it is avail­able for the producer.

The fact that the areas pro­vid­ed by the buffer are guar­an­teed con­tigu­ous is cen­tral to the pur­pose. That’s essen­tial for DMA use, but some­thing that a more typ­i­cal cir­cu­lar bound­ed buffer can­not guar­an­tee. Fur­ther­more, the commit/​release” pro­to­col means clients can work direct­ly with­in the buffer. There’s no need to copy data from the buffer into a user mem­o­ry area to make it contiguous.

James’ bbqueue uses atom­ic oper­a­tions to pro­vide a lock-free imple­men­ta­tion of bip-buffers. This means that pro­duc­er and con­sumer can run in dif­fer­ent exe­cu­tion threads (or inter­rupts) and use the bbqueue safe­ly with­out resort­ing to syn­chro­ni­sa­tion prim­i­tives such as mutex­es or pro­tect­ed objects in the Ada world.

I rec­om­mend look­ing at James Munns’ blog post to learn more about the algo­rithm and his imple­men­ta­tion, the rest of this post will be eas­i­er to under­stand if you do so. Note that the Rust imple­men­ta­tion that I used as a basis for this project has changed since the pub­li­ca­tion of James’ blog post, some minor dis­crep­an­cies are to be expect­ed in the implementation.

From Rust to SPARK #

As I try to explain above, bip-buffers can be very use­ful for embed­ded sys­tems, even more so a lock-free imple­men­ta­tion. So I start­ed a project to bring this solu­tion to the Ada ecosys­tem. But I want­ed to bring more than just a trans­la­tion from Rust to Ada, and there­fore used this oppor­tu­ni­ty to bring SPARK for­mal ver­i­fi­ca­tion in the mix.

The bbqueue imple­men­ta­tion most­ly deals with index­es in a buffer. There is an index that keeps track of the next mem­o­ry to be writ­ten to, anoth­er one for the mem­o­ry to be read, etc (see James’ blog post). 

With SPARK I want­ed to prove some func­tion­al prop­er­ties that will show that the imple­men­ta­tion is cor­rect. For instance, I want­ed to prove that when a writable slice of the buffer is granted:

  • The slice is valid: low­er and upper bounds are with­in the bounds of the buffer
  • The slice is writable: the low­er and upper bounds are with­in a writable part of the buffer
  • The size of the slice is equal to the request­ed size, or zero if there is not enough free space available

To be able to prove those prop­er­ties, I wrote helper func­tions to refine the prob­lem. The func­tion below express­es what it means for an index to be with­in 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 func­tion it is easy to write a def­i­n­i­tion of a valid writable slice, and then use this def­i­n­i­tion as a post­con­di­tion for the sub­pro­gram 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

Anoth­er impor­tant part of achiev­ing the proof was the def­i­n­i­tion of invari­ants on the buffer type. In a way, I con­sid­er this as explain­ing the algo­rithm to SPARK’s auto­mat­ic provers. 

In the end I man­aged to get 100% proof on the code. I also used the GitHub actions work­flow to run the GNAT­prove auto­mat­i­cal­ly on pull-requests. If you try to break the code (https://​github​.com/​F​a​b​i​e​n​-​C​h​o​u​t​e​a​u​/​b​b​q​u​e​u​e​-​s​p​a​r​k​/​p​ull/2) you should see a mes­sage like this:

How to use the SPARK bbqueue #

This Ada/​SPARK imple­men­ta­tion of bbqueue is avail­able in the Alire pack­age man­ag­er To import it to your project, you sim­ply have to run this command:

$ alr with bbqueue

Offsets_​Only #

The root pack­age of the bbqueue crate imple­ments a type that only deals with index­es, with­out hav­ing an inter­nal buffer. This is use­ful in mul­ti­ple cases.

1) Using the same slices in mul­ti­ple buffers. For instance in an audio appli­ca­tion the stereo left and right chan­nels can be in sep­a­rate buffers:

   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;
   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 allo­cat­ing slices on some­thing oth­er than an array of bytes: 

   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;
   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 pack­age BBqueue.Buffers is based on Offsets_​Only but pro­vides an inter­nal buffer. This is a more con­ve­nient pack­age if you just want to allo­cate chunks of memory:

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

Framed Buffers #

The last vari­ant of bbqueue is Framed_​Buffer. With the bbqueue imple­men­ta­tions pre­sent­ed so far, when the con­sumer requests data, the biggest read­able slice is returned. Framed_​Buffer how­ev­er keeps track of the length of each com­mit from the pro­duc­er, and the slices returned to the con­sumer cor­re­spond to the com­mits. This is very use­ful for pro­to­cols with vari­able length packets.

   Q   : aliased Framed_Buffer (64);
   WG  : Write_Grant := Empty;
   RG  : Read_Grant := Empty;
   S   : Slice_Rec;
   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

Atom­ics #

As said at the begin­ning of this post, bbqueue is a lock­less, thread safe imple­men­ta­tion of bip-buffers. To achieve the lock­less prop­er­ty of the imple­men­ta­tion, atom­ic oper­a­tions are used to read, write and mod­i­fy indexes.

For this I cre­at­ed anoth­er Alire crate that pro­vides SPARK bind­ings over GCC intrin­sic atom­ic functions.

Con­tracts are added to the bind­ing sub­pro­gram spec­i­fi­ca­tions to allow SPARK provers to under­stand what the atom­ic intrin­sics do. For example:

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

   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;

Con­clu­sion #

This project was my first SPARK project, and get­ting to 100% auto­mat­ic proof was a chal­leng­ing task. Now that it is done, the cost of main­tain­ing the code is great­ly reduced and this ini­tial effort will pay in the long run.

As always, feed­back is wel­come, and don’t hes­i­tate to let us know if you find this imple­men­ta­tion use­ful for your projects.

Posted in

About Fabien Chouteau

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.