Frame Acquisition Without Drops Using Ada Tasks — A Protected-Object Ring Buffer and Priorities

When you receive images from an industrial camera, the camera keeps sending frames at a fixed interval and does not wait for the receiver. If inspection occasionally slows down, the receiving side backs up and images are lost somewhere. If they are lost outside the application (inside the driver or SDK), the application cannot see the dropped frames.

In this article I build the skeleton of the acquisition in Ada. I use a periodic task that simulates camera arrivals, a worker task, and a fixed-length ring buffer made of protected objects, and I pass slot numbers rather than the images themselves. When the buffer is full, the camera task drops the frame instead of waiting, and records how many it dropped. I measure what actually happens when processing is slow, and describe when priorities take effect on Linux and what SPARK can verify.

The measurements showed that when processing is slower than arrival on average, adding slots does not change the drop rate. Slots absorb only temporary delays. If the camera task is made to wait, the number dropped inside the application becomes 0, but that backlog instead accumulates as camera lateness, and with a real camera those frames are lost outside the application. On Linux, both priorities and priority ceiling checks require privileges, and without them they were silently ignored.

I built and ran every example. I measured on November 10, 2026 in a Linux container (Ubuntu 24.04, 4 vCPUs) with GNAT 13.3.0 from the Ubuntu packages. I did not test on Windows. The SPARK proofs were run with GNATprove 16.1.0, installed with Alire, on a GitHub Actions Ubuntu runner. The basics of tasks and protected objects are in “Safe Concurrency with Ada”, and a general explanation of priorities and delay until is in “Real-Time Systems Programming in Ada”. This article focuses on camera acquisition.

The roles of the camera task, the worker task and the slots

I build the acquisition from three parts: the camera task that receives frames, the worker task that inspects images, and the slots that hold the images. A slot is an area for one 640×480 8-bit image, and I prepare exactly 8 of them at startup. The camera task writes an image into a free slot, and the worker task reads and inspects it.

What the two tasks pass between them is not an image but a slot number. Copying a 300KB image every time would mean copying 30MB per second at 100fps. A number is a single integer, and memory never grows beyond what was allocated at startup. SDKs usually also cycle through a fixed number of buffers in turn. The number of SDK buffers and how images are received are covered in “Dropped Frames with GigE Vision and USB3 Vision Cameras”.

There are two queues that hold numbers: Free, which holds the numbers of free slots, and Ready, which holds the numbers of slots that contain an image. A number travels from Free to the camera task, to Ready, to the worker task, and back to Free.

flowchart TB
        accTitle: The path the slot numbers travel
        accDescr: Shows that the number of a free slot goes from Free to the camera task, enters Ready after the image is written, is taken out and inspected by the worker task, and is returned to Free.
        F["Free (numbers of free slots)"] --> C["Camera task"]
        C -->|"writes the image"| R["Ready (numbers of slots with an image)"]
        R --> W["Worker task"]
        W -->|"returns it after inspection"| F

Figure 1: A slot number travels through Free, the camera task, Ready and the worker task, and returns to Free.

In this design, the number of any slot is, at any given moment, in exactly one of four places: inside Free, held by the camera task, inside Ready, or held by the worker task. Only the task that holds a number touches that slot, so the worker task never reads a slot while the camera task is writing it. The protected-object queues pass the numbers along, but the convention that only the task holding a number touches the slot is kept by how the code is written; the image areas themselves have no mutual exclusion.

flowchart TB
        accTitle: The four places one slot number can be
        accDescr: Shows that the number of one slot is in exactly one of four places, inside Free, held by the camera task, inside Ready, or held by the worker task, and that only the task holding the number touches the image area.
        S["Number of slot 3"] --> A["Inside Free"]
        S --> B["Held by the camera task"]
        S --> D["Inside Ready"]
        S --> E["Held by the worker task"]
        B -.-> B2["May write"]
        E -.-> E2["May read"]

Figure 2: At any moment one slot number is in exactly one of four places, and only the task holding it touches the image.

In the diagram a solid line marks a relation that always holds and a dashed line marks a conditional one (the conditions are given per relation on the detail page). The full list of relations (11 in total, with evidence and certainty) and the definitions of the main concepts are collected on the knowledge map detail page (in Japanese). Data: JSON-LD / Turtle

A ring buffer for slot numbers

Free and Ready are two protected objects of the same protected type, Slot_Queue. The capacity is 8, the same as the total number of slots. Ring positions are indexed with Ring_Index, a modular type mod 8, so wrapping from the end back to the start never overflows.

with Capture_Priorities;

package Slot_Queues with SPARK_Mode is

   Capacity : constant := 8;

   type Slot_Index is range 1 .. Capacity;
   type Count_Type is range 0 .. Capacity;
   type Ring_Index is mod Capacity;
   type Slot_Ring is array (Ring_Index) of Slot_Index;

   protected type Slot_Queue (Initially_Full : Boolean)
     with Priority => Capture_Priorities.Camera_Priority
   is
      procedure Put (Slot : Slot_Index; Accepted : out Boolean);
      procedure Try_Take (Slot : out Slot_Index; Found : out Boolean);
      entry Take (Slot : out Slot_Index);
      function Length return Count_Type;
      function Max_Length return Count_Type;
   private
      Items : Slot_Ring := [for I in Ring_Index => Slot_Index (Integer (I) + 1)];
      Head  : Ring_Index := 0;
      Count : Count_Type := (if Initially_Full then Capacity else 0);
      Peak  : Count_Type := (if Initially_Full then Capacity else 0);
   end Slot_Queue;

end Slot_Queues;

If the discriminant Initially_Full is true, the queue starts with all of the numbers 1 to 8 in it. Free is created this way, and Ready is created empty. The Priority on the type is the priority ceiling, which I explain later.

The numbers in the queue are the Count entries of the array Items counted from Head. Taking a number reads the position Head and advances Head by one; putting a number writes at position Head + Count. Both are Ring_Index arithmetic, so 0 follows 7.

flowchart TB
        accTitle: Position arithmetic in the ring buffer
        accDescr: Shows that the numbers in the queue are the Count entries of the array Items counted from Head, that taking reads the position Head and advances Head, that putting writes at position Head plus Count, and that 0 follows 7.
        I["Items (indices 0 to 7)"] --> H["Count numbers starting at Head"]
        H --> T["Take: read position Head, advance Head by one"]
        H --> P["Put: write at position Head + Count"]
        T -.-> M["0 follows 7 (modular type mod 8)"]
        P -.-> M

Figure 3: The numbers in the queue are the Count entries from Head, and position arithmetic wraps around modulo 8.

package body Slot_Queues with SPARK_Mode is

   protected body Slot_Queue is

      procedure Put (Slot : Slot_Index; Accepted : out Boolean) is
      begin
         if Count = Capacity then
            Accepted := False;
         else
            Items (Head + Ring_Index'Mod (Count)) := Slot;
            Count := Count + 1;
            if Count > Peak then
               Peak := Count;
            end if;
            Accepted := True;
         end if;
      end Put;

      procedure Try_Take (Slot : out Slot_Index; Found : out Boolean) is
      begin
         if Count = 0 then
            Slot := Slot_Index'First;
            Found := False;
         else
            Slot := Items (Head);
            Head := Head + 1;
            Count := Count - 1;
            Found := True;
         end if;
      end Try_Take;

      entry Take (Slot : out Slot_Index) when Count > 0 is
      begin
         Slot := Items (Head);
         Head := Head + 1;
         Count := Count - 1;
      end Take;

      function Length return Count_Type is (Count);

      function Max_Length return Count_Type is (Peak);

   end Slot_Queue;

end Slot_Queues;

There are three operations, and they differ in whether they wait. Put and Try_Take are procedures, so they never make the calling task wait on a barrier (it may wait briefly while taking the protected object’s lock). When the queue is full or empty, they return the result in Accepted or Found. Take is an entry, and it makes the calling task wait until the barrier when Count > 0 becomes true. The camera task must not wait, so it uses only the procedures, while the worker task waits for the next image with Ready.Take.

flowchart TB
        accTitle: The three operations of Slot_Queue
        accDescr: Shows that Put returns with Accepted false when the queue is full, Try_Take returns with Found false when it is empty, and Take makes the calling task wait until the barrier is true.
        Q["Slot_Queue"] --> P["Put (procedure)"]
        Q --> T["Try_Take (procedure)"]
        Q --> K["Take (entry)"]
        P -.-> P2["If full, returns with Accepted false"]
        T -.-> T2["If empty, returns with Found false"]
        K -.-> K2["Waits while Count is 0"]

Figure 4: Put and Try_Take return a result without waiting, and only Take makes the calling task wait on a barrier.

The barrier Count > 0 can be written under the Jorvik profile I use later, but not under the Ravenscar profile. A Ravenscar barrier is limited to a static expression or a name that denotes a single component of the protected object (Simple_Barriers)¹. The SPARK User’s Guide shows an example that adds a Boolean component for this reason². Jorvik relaxes this to expressions that combine components of the protected object and static expressions with comparison and logical operators (Pure_Barriers)³.

Peak keeps the largest number of entries the queue has held so far. Looking at Peak for Ready tells you how many accumulated while processing was behind.

Never making the camera task wait

There are two possible policies when no slot is free: make the camera task wait until one frees up, or drop that frame. In the design in this article I drop it and record the count.

The waiting approach looks as if it never drops anything. But a real camera sends the next frame whether or not the application receives it. Frames that arrive while the application is waiting are discarded, without the application knowing, once the driver or SDK buffers overflow. If the application drops and counts frames itself, it can record the frames it lost because processing could not keep up separately from frames lost on the network or USB.

flowchart TB
        accTitle: Two policies when no slot is free
        accDescr: Shows that when no slot is free, the drop policy can record the number dropped inside the application, while the waiting policy loses frames outside the application in the driver or SDK where the application cannot see them.
        N{"Is a slot free?"} -->|"Yes"| OK["Write the image and put it in Ready"]
        N -->|"No"| P{"Policy"}
        P -->|"Drop"| D["Count the frames dropped inside the application"]
        P -->|"Wait"| W["The camera task stops"]
        W -.-> L["Frames in that interval are lost in the driver or SDK"]

Figure 5: With the waiting policy, lost frames become invisible to the application.

The camera task is as follows. Wait_For_Slot is a setting that switches to the waiting policy for comparison; it is false (the drop policy) by default.

   task body Camera is
      Next     : Time := Clock;
      Now      : Time;
      Slot     : Slot_Index;
      Found    : Boolean;
      Accepted : Boolean;
      Returned : Boolean;
      Left     : Count_Type;
   begin
      for Frame in 1 .. Frames loop
         Next := Ticks.Add (Next, Period);
         delay until Next;
         if Wait_For_Slot then
            Free.Take (Slot);   --  Wait until a slot frees up (for comparison)
            Found := True;
         else
            Free.Try_Take (Slot, Found);
         end if;
         if Found then
            Frame_Pool.Fill (Slot, Frame, Next);
            Ready.Put (Slot, Accepted);
            if not Accepted then
               Free.Put (Slot, Returned);
            end if;
         else
            Accepted := False;
         end if;
         Now := Clock;
         Stats.Arrived (Frame, Ticks.Since (Now, Next), Dropped => not Accepted);
      end loop;

      --  Wait until every slot is free again, then signal the end
      loop
         Left := Free.Length;
         exit when Left = Capacity;
         Next := Ticks.Add (Next, Period);
         delay until Next;
      end loop;
      Stats.Finish;

      loop
         delay until Time_Last;
      end loop;
   end Camera;

delay until Next waits until the absolute time obtained by adding the period to the previous scheduled time. Even if processing runs a little late, the next scheduled time does not drift, so the task simulates an arrival every 10 milliseconds. Time addition and subtraction are done with Ticks.Add and Ticks.Since (the reason is explained in the SPARK section). Instead of writing a received image, Frame_Pool.Fill fills every pixel with the frame number. Ready has the same capacity as the total number of slots, so Put should never refuse; if it ever does, the slot is returned to Free. Stats.Arrived records how far behind the scheduled time the camera task finished, and whether the frame was dropped.

The last loop keeps the task asleep after the measurement instead of stopping it. The reason lies in the restrictions of the Jorvik profile, which I explain in the next section.

Choosing priorities and priority ceilings

The worker task takes a number from Ready, reads and inspects the image, and returns the number to Free. Instead of a real inspection it keeps the CPU busy for a set time (Simulate_Work). Frame_Pool.Inspect computes the sum of all pixels, so if it read an image while another task was rewriting it, the sum would not match.

   task body Worker is
      Slot     : Slot_Index;
      Frame    : Frame_Number;
      Arrival  : Time;
      Started  : Time;
      Sum      : Unsigned_32;
      Accepted : Boolean;
   begin
      loop
         Ready.Take (Slot);
         Started := Clock;
         Frame_Pool.Inspect (Slot, Frame, Arrival, Sum);
         Simulate_Work (Frame, Started);
         --  Record first, then return the slot. If the slot were returned
         --  first, the camera task could see every slot free and signal
         --  the end before this record.
         Stats.Processed
           (Frame, Ticks.Since (Started, Arrival),
            Intact => Sum = Frame_Pool.Expected_Checksum (Frame));
         Free.Put (Slot, Accepted);
      end loop;
   end Worker;

The worker task records with Stats.Processed before it returns the number to Free. The camera task signals the end of the measurement once it sees every slot back in Free. If the number were returned first, the end could be signaled before the last frame is recorded, and that frame might be counted neither as processed nor as dropped.

flowchart TB
        accTitle: The worker task records before returning the number
        accDescr: Shows that when the worker task finishes an inspection it first records it in Stats and then returns the slot number to Free, and that the camera task signals the end when it sees every number back in Free, so the last frame is recorded before the end is signaled.
        W1["Worker task finishes inspection"] --> W2["Records in Stats"]
        W2 --> W3["Returns the number to Free"]
        W3 --> C["Camera task sees all numbers returned"]
        C --> F["Stats.Finish signals the end"]
        W3 -.-> X["In the reverse order the last frame's record can be missed"]

Figure 6: Because the worker task records before returning the number, the last frame is recorded before the end is signaled.

The two tasks and the two queues are placed in a library-level package. The camera task has priority 20 and the worker task 10, so that the camera task can run at its scheduled times even while the worker keeps the CPU busy.

with Slot_Queues;    use Slot_Queues;
with Capture_Priorities; use Capture_Priorities;

package Capture_Tasks with SPARK_Mode is

   --  Numbers of free slots, and numbers of slots that contain an image
   Free  : Slot_Queue (Initially_Full => True);
   Ready : Slot_Queue (Initially_Full => False);

   task Camera with Priority => Camera_Priority;
   task Worker with Priority => Worker_Priority;

end Capture_Tasks;

The priority of a protected object is treated as its priority ceiling. Under the Ceiling_Locking policy, when a task calls an operation of a protected object, the runtime checks whether the task’s priority is higher than the ceiling, and if it is, Program_Error is raised⁴. Free and Ready are called from the camera task at priority 20, so the ceiling of the type Slot_Queue is 20 (Camera_Priority). At first I passed the ceiling as a discriminant, but GNATprove 16.1.0 could not fully prove that the calling tasks’ priorities do not exceed it, so I changed to writing a constant on the type. The protected object Stats, used for recording, also has a ceiling of 20. The main program, which displays the results, runs at priority 1 so that it exceeds no protected object’s ceiling. The main program also calls functions of Stats and Ready, but because the main program is outside SPARK, the ceiling checks for those calls are not included in the GNATprove count given later.

flowchart TB
        accTitle: Task priorities and protected object priority ceilings
        accDescr: Shows that the camera task at priority 20 and the worker task at priority 10 call Free, Ready and Stats, whose ceiling is 20, and that the main program at priority 1 also calls Stats.
        C["Camera task (priority 20)"] --> Q["Free and Ready (ceiling 20)"]
        W["Worker task (priority 10)"] --> Q
        C --> S["Stats (ceiling 20)"]
        W --> S
        M["Main program (priority 1)"] --> S
        Q -.-> R["The ceiling must be at least the caller's priority"]

Figure 7: A protected object’s priority ceiling must not be lower than the priority of any task that calls it.

What the Jorvik profile decides

The Jorvik profile is specified for the whole program in the configuration pragma file gnat.adc. To use tasks in SPARK you need the Ravenscar or Jorvik profile and Partition_Elaboration_Policy (Sequential), which keeps tasks from running until elaboration is complete².

pragma Profile (Jorvik);
pragma Partition_Elaboration_Policy (Sequential);

The Jorvik profile is equivalent to specifying the task dispatching policy (Task_Dispatching_Policy) FIFO_Within_Priorities, the locking policy Ceiling_Locking, Detect_Blocking, and a set of restrictions together³. The restrictions include tasks only at library level (No_Task_Hierarchy), no task termination (No_Task_Termination), and no select statements (No_Select_Statements). The camera task sleeps forever after the measurement because tasks are assumed never to terminate. The main program waits for the end of the measurement with Stats.Wait_Done, displays the results, and then ends the process with GNAT.OS_Lib.OS_Exit.

flowchart TB
        accTitle: What the Jorvik profile specifies
        accDescr: Shows that the Jorvik profile specifies together the task dispatching policy FIFO_Within_Priorities, the locking policy Ceiling_Locking, and restrictions such as library-level tasks and tasks that never terminate.
        J["pragma Profile (Jorvik)"] --> D["FIFO_Within_Priorities"]
        J --> L["Ceiling_Locking"]
        J --> R["Restrictions"]
        R --> R1["Tasks only at library level"]
        R --> R2["Tasks never terminate"]
        R --> R3["No select statements"]

Figure 8: The Jorvik profile specifies priority handling and concurrency restrictions together.

What happened when processing was slow

I measured with frames arriving every 10 milliseconds (100fps), running 1000 frames at a time. The worker task was given its processing time by keeping the CPU busy. I ran as root, so priorities were in effect (I confirm this in the next section). “Wait before processing” is the time from a frame’s scheduled arrival until the worker task takes it out, and “camera lateness” is the time from the scheduled time until the camera task has finished putting that frame’s number into Ready (or, when it drops the frame, has finished dropping it).

In every measurement, the sum of each image the worker task read matched the value that had been written. There was never a mismatch indicating that a slot was read while the camera was writing it.

When processing takes 12 milliseconds every time, it is slower than arrival on average, so no number of slots is enough. 172 of 1000 frames were dropped, somewhat more than the roughly 17% expected from the ratio of the 10-millisecond arrival to the 12-millisecond processing (about 167 frames, or about 160 frames excluding the 8 slots free at the start); three other runs under the same conditions dropped 173 to 177. Up to 7 numbers accumulated in Ready (the remaining one held by the worker task), and the wait before processing grew to about 80 milliseconds. Adding slots in this state does not change the drop rate; it only lengthens the wait. Basler’s documentation also notes that adding buffers lets you tolerate temporary delays at the cost of more latency, and that buffers can overflow if processing is slow continuously⁵. When processing is slow on average, you have to decide whether to make it faster or to skip frames.

flowchart TB
        accTitle: Two kinds of processing delay
        accDescr: Shows that when processing is slower than arrival on average, adding slots does not change the drop rate, and that a temporary delay can be absorbed if there are more slots than frames arriving during the delay.
        A{"Kind of processing delay"} -->|"Slower than arrival on average"| B["More slots, same drop rate"]
        A -->|"Temporarily slow"| C{"More free slots than frames arriving during the delay?"}
        C -->|"More"| D["Absorbed without drops"]
        C -->|"Fewer"| E["The shortfall is dropped"]
        B -.-> F["Decide whether to speed up processing or skip frames"]

Figure 9: If processing is slow on average, slots do not help; for a temporary delay, the number of slots decides whether it can be absorbed.

Whether a temporary delay can be absorbed is decided by the number of slots. When processing took 60 milliseconds every 100 frames, the 6 frames that arrived in the meantime accumulated in Ready (at most 6) and none were dropped. At 120 milliseconds, 12 frames arrive in the meantime, but only up to 7 can be queued. 5 frames were dropped per delay, and there were 9 delays, for 45 frames in total (the delay at frame 1000 happened after every frame had arrived, so it did not count). You can estimate the number of slots you need as the longest delay you want to tolerate divided by the arrival interval, plus one for the frame being processed and some margin.

flowchart TB
        accTitle: Why 5 frames were dropped during a 120-millisecond delay
        accDescr: Shows that while processing takes 120 milliseconds, 12 frames arrive at 10-millisecond intervals, that only 7 can be queued in Ready because one of the 8 slots is being processed, and that the remaining 5 frames were dropped.
        A["Processing takes 120ms"] --> B["12 frames arrive meanwhile"]
        B --> C["Only 7 can be queued in Ready"]
        C --> D["The remaining 5 frames are dropped"]
        C -.-> E["One of the 8 slots is being processed"]

Figure 10: Of the 12 frames arriving during the 120-millisecond delay, the 5 that could not be queued were dropped.

Comparing with the waiting policy

Under the same conditions I also tried the policy that makes the camera task wait until a slot frees up (setting the camera task’s Wait_For_Slot to true).

With the waiting policy the drop count is 0, but when processing is slow on average the camera lateness builds up, and by the end it was about 2.2 seconds behind schedule. A real camera finishes sending 1000 frames in 10 seconds, so the frames corresponding to that lateness are lost before they reach the application. Even with temporary delays, the camera task stopped for up to 41 milliseconds. If the SDK buffers cannot hold the frames that arrive in the meantime, those frames are again lost outside the application.

flowchart TB
        accTitle: How the results differ between the drop and waiting policies
        accDescr: Shows that when processing is slow on average, the drop policy records the drop count and keeps camera lateness small, while the waiting policy builds up camera lateness to about 2.2 seconds even though the drop count is 0.
        S["Processing is slow on average"] --> D["Drop policy"]
        S --> W["Waiting policy"]
        D --> D1["Records 172 dropped"]
        D --> D2["Camera lateness at most 6.0ms"]
        W --> W1["0 dropped"]
        W --> W2["Camera lateness up to about 2.2 s"]
        W2 -.-> W3["Actually lost outside the application"]

Figure 11: Even when the waiting policy brings the drop count to 0, the difference becomes camera lateness, and with a real camera those frames are lost outside the application.

When priorities take effect on Linux

The measurements so far were run as root. Looking at each thread’s scheduling policy with chrt -p during the run, the threads of the main program, the worker task and the camera task were SCHED_FIFO, with priorities 2, 11 and 21. These are the Ada priorities plus one. The Linux version of GNAT sets SCHED_FIFO on the threads of FIFO_Within_Priorities tasks⁶.

Running the same program as an unprivileged user (nobody) produced no errors at all, and every thread ran as SCHED_OTHER at priority 0. The Linux version of GNAT sets thread priorities with pthread_setschedparam, and when that fails for lack of privilege (EPERM) it simply carries on⁶. Whether an unprivileged user’s threads can use SCHED_FIFO is decided by CAP_SYS_NICE and RLIMIT_RTPRIO. Without CAP_SYS_NICE, a priority higher than the RLIMIT_RTPRIO value cannot be set⁷. This program asks for Linux priorities 2, 11 and 21, so RLIMIT_RTPRIO must be at least 21. If it is smaller, threads whose priority exceeds the value should remain SCHED_OTHER. For example, with 5 only the main program would become SCHED_FIFO, while the camera and worker tasks would remain SCHED_OTHER, inverting the order of priorities. In this environment RLIMIT_RTPRIO was 0, and I lacked the privilege to change it, so I did not test with a higher RLIMIT_RTPRIO.

flowchart TB
        accTitle: When task priorities take effect
        accDescr: Shows that task priorities take effect as SCHED_FIFO if there is CAP_SYS_NICE or a sufficient RLIMIT_RTPRIO, otherwise become SCHED_OTHER without an error, and that RLIMIT_RTPRIO must be at least the highest priority plus one.
        P["Task priorities"] --> P1{"CAP_SYS_NICE or sufficient RLIMIT_RTPRIO"}
        P1 -->|"Present"| P2["Take effect as SCHED_FIFO"]
        P1 -->|"Absent"| P3["SCHED_OTHER (no error)"]
        P1 -.-> N["RLIMIT_RTPRIO at least highest priority + 1"]

Figure 12: Thread priorities take effect only with CAP_SYS_NICE or a sufficient RLIMIT_RTPRIO, and are otherwise ignored without an error.

Priority ceiling checks depend on a different condition from thread priorities. The Linux GNAT runtime uses priority-ceiling mutexes (PTHREAD_PRIO_PROTECT) for protected object locks when the process is running as root or when it can determine that the process has CAP_SYS_NICE. Otherwise it ignores the Ceiling_Locking specification⁶. For root it checks only whether the process is root, so a root process without CAP_SYS_NICE gets priority-ceiling locks while its threads cannot become SCHED_FIFO.

The CAP_SYS_NICE check calls libcap functions through a weak reference. Using nm, I confirmed that cap_get_proc is a weak symbol in libgnat from GNAT 13 on Ubuntu. If libcap is not linked, the check returns false even when the privilege is granted with setcap cap_sys_nice=ep. Ubuntu’s gcc uses --as-needed by default, so merely adding libcap to the link options gets it removed as an unused library.

In this environment I took a program whose ceiling had been lowered so that a violation would occur, linked it in three different ways, applied setcap cap_sys_nice=ep to each binary, and ran each as nobody. The one not linked with libcap and the one where libcap was merely added to the link options (libcap does not appear in ldd) ran to completion without detecting the violation. Only the one linked with libcap using -Wl,--no-as-needed (libcap appears in ldd) stopped on the violation, as it did under root. When the correct program, without the lowered ceiling, was run with the same linking, its threads became SCHED_FIFO even under nobody, and it ran to completion. This environment has no libcap development package, so I specified the shared library directly with -l:libcap.so.2. Normally you install libcap-dev, write -lcap, and confirm with ldd that libcap is linked.

flowchart TB
        accTitle: How libcap is linked and whether violations are detected
        accDescr: Shows that when run as nobody with CAP_SYS_NICE granted by setcap, the version not linked with libcap and the version where libcap was only added to the link options did not detect the violation, and only the version linked with -Wl,--no-as-needed stopped on the violation.
        L["Lowered ceiling run as nobody"] --> A["libcap not linked"]
        L --> B["libcap only added"]
        L --> C["Linked with --no-as-needed"]
        A --> N["Violation not detected"]
        B --> N
        C --> D["Stops on the violation"]

Figure 13: Even with CAP_SYS_NICE granted, only the build that actually linked libcap detected the violation.

flowchart TB
        accTitle: When priority ceiling checks take effect
        accDescr: Shows that for root with CAP_SYS_NICE a violation becomes Program_Error and without it even correct code gets Program_Error, and that for an unprivileged user violations are detected when both CAP_SYS_NICE and a libcap link are present and are not checked when either is missing.
        C["Priority ceiling checks"] --> C1{"Root?"}
        C1 -->|"Root"| C2{"Has CAP_SYS_NICE?"}
        C2 -->|"Yes"| OK["Violation raises Program_Error"]
        C2 -->|"No"| BAD["Even correct code raises Program_Error"]
        C1 -->|"Unprivileged user"| C3{"CAP_SYS_NICE and libcap linked"}
        C3 -->|"Both"| OK
        C3 -->|"Either missing"| NO["Not checked (no error)"]

Figure 14: Priority ceiling checks take effect for root with CAP_SYS_NICE, or for an unprivileged user with CAP_SYS_NICE and libcap linked; for root without CAP_SYS_NICE even correct code stops.

To see what changes when priorities do not take effect, I pinned the process to CPU 0 alone and ran a separate process spinning on the same CPU. Processing took 5 milliseconds each time.

flowchart TB
        accTitle: Setup of the measurement that shares CPU 0
        accDescr: Shows that the camera task, the worker task and a separate spinning process share CPU 0, that with SCHED_FIFO the camera task runs first, and that with SCHED_OTHER the three share time.
        C["Camera task"] --> CPU["CPU 0"]
        W["Worker task (busy for 5ms)"] --> CPU
        H["Separate spinning process"] --> CPU
        CPU -.-> F["SCHED_FIFO: camera task runs first"]
        CPU -.-> O["SCHED_OTHER: the three share time"]

Figure 15: When the three share CPU 0, whether priorities take effect changes how the camera task runs.

As an unprivileged user, the camera task shares the CPU with the spinning process and the worker task, so it ran 3.2 milliseconds behind schedule on average. In three further runs under the same conditions, the mean was 3.1 to 3.6 milliseconds and the maximum 14.8 to 17.6 milliseconds. As root, all four runs had a mean of 0.1 to 0.2 milliseconds and a maximum of 2.6 to 6.2 milliseconds. This environment is a container on a virtual machine, so delays of a few milliseconds remain even as root.

Detecting priority ceiling violations, and privileges

I also tried lowering the priority ceiling to see what happens. If the ceiling of Slot_Queue is set to 10, the same as the worker task, the camera task at priority 20 violates the ceiling the first time it calls Free.Try_Take.

When the program was run as root, PROGRAM_ERROR : ... ceiling violation was raised in the camera task. Because the exception was not handled, the camera task ended without printing anything, and the main program hung waiting for the end of the measurement (I confirmed the exception’s contents by adding an exception handler separately). As described above, an unprivileged user does not get priority-ceiling mutexes, so the violation was not detected, and the program ran to completion and displayed its results. The Linux version of GNAT treats an EINVAL returned when locking this mutex as a ceiling violation⁶.

Under root with CAP_SYS_NICE removed (run with setpriv --bounding-set -sys_nice), the correct program, without the lowered ceiling, stopped with raised PROGRAM_ERROR : s-tarest.adb:664 explicit raise, with exit code 1. This is the combination where locks have priority ceilings but threads cannot become SCHED_FIFO, so the lock presumably failed, but I did not confirm the value the lock returned. Docker’s default capabilities do not include CAP_SYS_NICE⁸, so when running in a container, check not only that the process is root but also, in CapEff in /proc/self/status, whether it has CAP_SYS_NICE.

Testing in an environment with different privileges gives different results for both priorities and their checks. Tests before deploying to the equipment need to be run with the same user and privileges as production.

CPU assignment

The Ada Reference Manual notes that under Ravenscar or Jorvik, all tasks with no CPU specified run on a single CPU³. With GNAT 13.3.0 in this environment, every thread was allowed to run on all four CPUs (Cpus_allowed_list was 0-3). The worker task and the camera task may run at the same time on different CPUs, so reasoning about priorities that assumes a single CPU does not apply as is. I pinned to CPU 0 in the comparison above to remove this difference and look only at the effect of priorities.

I did not test on Windows. Thread priorities and CPU assignment on Windows are covered in “A Windows App Developer’s Primer on CPU Settings” and “A Practical Guide to Getting as Close to Soft Real-Time as Possible on Ordinary Windows”.

What SPARK can and cannot verify

The queues, the two tasks and the protected object for recording are placed under SPARK_Mode and analyzed with GNATprove. In SPARK, the only things tasks may share are objects protected against concurrent access, such as protected objects and atomic variables, and variables that do not change after elaboration². If two tasks share an unprotected variable, GNATprove reports it as a possible data race.

GNATprove could not show that time addition and subtraction (Next + Period and Now - Next) do not overflow when the time approaches the upper bound of the type. So I gathered just this arithmetic into a small package, Ticks, whose body is outside SPARK. The main program that aggregates and displays the measurement records, and the body that reads the arguments, are also outside SPARK.

flowchart TB
        accTitle: What was placed inside and outside SPARK
        accDescr: Shows that the queues, the tasks, the recording object Stats, and the specs of Ticks and Frame_Pool were placed inside SPARK and analyzed with GNATprove, while the bodies of Ticks and Frame_Pool, the body that reads the arguments, and the main program were placed outside.
        P["Acquisition program"] --> S["Inside SPARK (GNATprove)"]
        P --> O["Outside SPARK"]
        S --> A["Queues, tasks, Stats"]
        S --> D["Ticks, Frame_Pool specs"]
        O --> E["Ticks, Frame_Pool bodies"]
        O --> F["Argument reader, main"]

Figure 16: The queues, tasks and recording are inside SPARK; the bodies of the time arithmetic and the image area, and the main program, are outside.

with Ada.Real_Time; use Ada.Real_Time;

--  Time addition and subtraction. GNATprove cannot show that these do
--  not overflow when the time approaches the upper bound of the type,
--  so the body is outside the SPARK checks.
package Ticks with SPARK_Mode is

   function Add (T : Time; D : Time_Span) return Time
   with Global => null;

   function Since (Later, Earlier : Time) return Time_Span
   with Global => null;

end Ticks;

Running GNATprove 16.1.0 with --level=2 on a GitHub Actions Ubuntu runner ended with “Success: all checks proved (43 checks).”: all 43 checks were proved (25 by flow analysis and 18 by the provers). No data races were reported, and the proved checks include range checks, priority ceiling checks for six combinations of calling task and protected operation, and the fact that the two tasks do not terminate.

That the two tasks never touch the same slot’s image at the same time is upheld only by the number-passing convention; the image area itself is not protected. This convention cannot be expressed with SPARK types or protected objects, so the package that holds the image area has only its spec in SPARK, with its body outside the analysis.

with Interfaces;
with Ada.Real_Time;
with Slot_Queues;    use Slot_Queues;
with Capture_Config; use Capture_Config;

--  The image area. Only the task holding a slot's number touches that slot.
--  This convention cannot be proved in SPARK, so it is declared
--  Synchronous and the body is outside the checks.
package Frame_Pool with
  SPARK_Mode,
  Abstract_State => (Pixels with Synchronous, External),
  Initializes    => Pixels
is

   procedure Fill
     (Slot    : Slot_Index;
      Frame   : Frame_Number;
      Arrival : Ada.Real_Time.Time)
   with Global => (In_Out => Pixels);

   procedure Inspect
     (Slot     : Slot_Index;
      Frame    : out Frame_Number;
      Arrival  : out Ada.Real_Time.Time;
      Checksum : out Interfaces.Unsigned_32)
   with Global => (In_Out => Pixels);

   function Expected_Checksum (Frame : Frame_Number) return Interfaces.Unsigned_32
   with Global => null;

end Frame_Pool;

Synchronous on the abstract state Pixels declares that this state consists only of things protected against concurrent access². Initializes => Pixels declares that the area is created by the package’s initialization. If the body were inside SPARK, GNATprove would check both, but here the body is outside, so it cannot. GNATprove reported the initialization of Pixels as proved, but that result rests on this declaration; the contents of the body were not analyzed. Synchronous is not a proved fact but an assumption based on the slot-number convention.

As an experiment, removing Synchronous made GNATprove report possible data race when accessing variable "frame_pool.pixels" twice. In code with the ceiling of Slot_Queue lowered to 10, it reported ceiling priority protocol might not be respected twice. Both reports were for calls from the camera task at priority 20 (Free.Take and Ready.Put); calls from the worker task at priority 10 were not reported.

flowchart TB
        accTitle: What was proved and what was assumed
        accDescr: Shows that GNATprove proved the absence of data races and run-time errors in the queues and tasks, that not touching the image area concurrently and the time arithmetic not overflowing are assumptions, and that the image area was checked by comparing sums at run time.
        G["Proved by GNATprove"] --> A["No data races"]
        G --> B["No run-time errors"]
        P["Assumptions"] --> C["Images are not touched concurrently"]
        P --> T["Time arithmetic does not overflow"]
        C -.-> D["Sums compared at run time"]

Figure 17: The queues and tasks could be proved; that the image area is not touched concurrently is an assumption, backed by a run-time comparison.

To back up the assumption, the worker task compares the sum of each image it reads with the sum computed from the value that was written. All of the measurements above matched. However, this shows only that no mismatch occurred in the runs I tried. For example, if you introduce a mistake such as returning the same number to Free twice, two tasks end up holding the same slot, but the SPARK analysis does not detect it. When you change how numbers are passed, someone needs to read the code and confirm that this convention still holds.

How to carry out SPARK proofs is covered in “Introduction to Formal Verification with SPARK” and “Proving AI-Written Code with SPARK”.

Test environment and what was not verified

• Build and measurement: a Linux container (Ubuntu 24.04, a virtual machine with 4 vCPUs, kernel 6.18), with GNAT 13.3.0 and gprbuild from the Ubuntu packages, on November 10, 2026. The compiler switches were -gnat2022 -O2 -gnata, and the Jorvik profile was specified in the configuration pragma file gnat.adc (the bracket aggregate in Slot_Queues is Ada 2022 syntax, so it does not compile without -gnat2022). Measurements were run both as root and as nobody, and for the privilege comparison CAP_SYS_NICE was added and removed with setpriv and setcap.
• The full project used for verification is not published; the code in this article is an excerpt from it.
• Proofs: GNAT 16.1.0 and GNATprove 16.1.0 (FSF edition), installed with Alire, run with --level=2 on a GitHub Actions Ubuntu 24.04 runner. All values in the article’s tables were measured with GNAT 13.3.0 in the container above.
• No camera was connected. Frame arrivals were simulated with a delay until period, and reception was simulated by filling pixels with the frame number. The load of real SDK callbacks and DMA is not included.
• Inspection was simulated by keeping the CPU busy. Processing that reads a lot of memory, as real inspection does, adds the effects of caches and memory bandwidth.
• I did not test on Windows or on a real-time kernel (such as PREEMPT_RT). I also did not test with RLIMIT_RTPRIO greater than 0, because I lacked the privilege to change it.
• The measured values are results on this virtual machine and vary from run to run. Maximum values in particular sometimes differed several-fold under the same conditions.

Related Articles

This article is part of the series “Ada and Machine Vision”. The other articles in the series are:

• Proving Image Processing Free of Out-of-Bounds Access with SPARK — Binarization, Smoothing, Labeling and a Speed Comparison with C
• Receiving GigE Vision Packets with Ada Types — Pitfalls of Representation Clauses and a SPARK-Proved Parser
• Calling Ada Inspection Logic from a C# Inspection App — Passing Image Buffers Without Copying and Guarding the Boundary
• Separating Pixels and Millimeters with Types — Preventing Unit Mix-ups in Dimensional Inspection with Ada

Related existing articles:

• Dropped Frames with GigE Vision and USB3 Vision Cameras — Locating the Cause and the Windows Settings to Review
• Safe Concurrency with Ada — A Practical Guide to Tasks and Protected Objects
• Real-Time Systems Programming in Ada — Priorities, Periodic Execution, and CPU Time Control in Practice
• What’s New in Ada 2022 — What Works in GNAT and the Parallel Syntax You Can’t Write Yet
• Starting an Ada Project with Alire — Creating a Project, Adding Dependencies, Build Profiles, and GNATprove

References

Related Articles

Recent articles sharing the same tags. Deepen your understanding with closely related topics.

Related Topics

These are topic pages close to this theme. Starting from the article, you can go on to related services and other articles.

Services Connected to This Topic

This article leads to the following service pages. Start from the entry point closest to your situation.

Frequently Asked Questions

Questions commonly asked at the time of consultation about the topic of this article.

Should the task that receives camera images wait when the buffer is full?

In the design in this article it does not wait; it drops that frame and records the count. When I tried the waiting approach, the drop count stayed at 0, but the lateness behind the scheduled arrival time built up to about 2.2 seconds at most. A real camera does not wait, so the frames in that interval are lost inside the driver or SDK, where the application cannot see them.

If I add more slots to the ring buffer, can I prevent dropped frames even when processing is slow?

More slots absorb temporary delays, but they cannot fix processing that is slower than arrival on average. In a measurement where frames arriving every 10 milliseconds took 12 milliseconds each to process, 172 of 1000 frames were dropped even with 8 slots. A delay of 60 milliseconds every 100 frames was absorbed without drops, and a delay of 120 milliseconds dropped 5 frames each time.

On Linux, is giving Ada tasks priorities enough for them to take effect?

It depends on privileges. For thread priorities to take effect, the process needs CAP_SYS_NICE or an RLIMIT_RTPRIO at least one higher than the highest Ada priority. Priority ceiling checks take effect for root with CAP_SYS_NICE, or for an unprivileged user with CAP_SYS_NICE when libcap is linked with -Wl,--no-as-needed. In this article's environment, every thread ran as SCHED_OTHER under an unprivileged user, and ceiling violations were not detected. Under root without CAP_SYS_NICE, a correct program stopped with a Program_Error for a ceiling violation. You need to test with the same user and privileges as production.

Author Profile

Profile page for the article author.

Go Komura

Representative of KomuraSoft LLC

Focused on Windows software development, technical consulting, and bug investigation, with particular strength in projects where existing assets remain and in investigating failures whose cause is hard to see.