For this three-part series, we implemented a ‘pedal to the metal’ GPIO driven, flashing of a LED, in the context of a Linux kernel module for the NVIDIA Jetson Nano development board (kernel-based v4.9.294, arm64) in my favorite programming language … Ada!

• Part 1. Review of a kernel module, build strategy, and Ada integration.
• Part 2. Modeling of the problem in Ada.
• Part 3. Practical Ada binding to the C kernel APIs.

You can find the whole project published at https://github.com/ohenley/adacore_jetson. It is known to build and run properly. All instructions to be up and running in 5 minutes are included in the accompanying front-facing README.md. Do not hesitate to fill a GitHub issue if you find any problem.

Disclaimer: This text is meant to appeal to both Ada and non-Ada coders. Therefore I try to strike a balance between code story simplicity, didactic tractability, and features density. As I said to a colleague, this is the text I would have liked to cross before starting this experiment.

Binding 101

The binding thickness

Our code boundary to the Linux kernel C methods lies in kernel.ads. For an optional “adaptation” opportunity, kernel.adb exists before breaking into the concrete C binding. Take printk (printf equivalent in kernel space) for example. In C, you would call printk(“hello\n”). Ada strings are not null-terminated, they are an array of characters. To make sure the passed Ada string stays valid on the C side, you expose specification signatures .ads that make sense when programming from an Ada point of view and “adapt” in body implementation .adb before calling directly into the binding. Strictly speaking, our exposed Ada Printk would qualify as a “thick” binding even though the adaptation layer is minimal. This is in opposition to a “thin” binding which is really a one-to-one mapping on the C signature as implemented by Printk_C.

-- kernel.ads
procedure Printk (S : String); -- only this is visible for clients of kernel

-- kernel.adb
procedure Printk_C (S : String) with -- considered a thin binding
    Import        => true,
    Convention    => C,
    External_Name => "printk";

procedure Printk (S : String) is -- considered a thick binding
begin
   Printk_C (S & Ascii.Lf & Ascii.Nul); -- because we ‘mangle’ for Ada comfort
end;

The wrapper function

Binding to a wrapped C macro or static inline is often convenient, potentially makes you inherit fixes, upgrades happening inside/under the macro implementation and are, depending on the context, potentially more portable. create_singlethread_workqueue used in printk_wq.c as found in Part 1 makes a perfect example. Our driver has a C home in main.c. You create a C wrapping function calling the macro.

/* main.c */
extern struct workqueue_struct * wrap_create_singlethread_wq (const char* name)
{
   return create_singlethread_workqueue(name); /* calling the macro */
}

You then bind to this wrapper on the Ada side and use it. Done.

-- kernel.ads
function Create_Singlethread_Wq (Name : String) return Workqueue_Struct_Access with
   Import        => True,
   Convention    => C,
   External_Name => "wrap_create_singlethread_wq";

-- flash_led.adb
...
Wq := K.Create_Singlethread_Wq ("flash_led_work");

The reconstruction

Sometimes a macro called on the C side creates stuff, in place, which you end up needing on the Ada side. You can probably always bind to this resource but I find it often impedes code story. Take DECLARE_DELAYED_WORK(dw, delayed_work_cb) for example. From an outside point of view, it implicitly creates struct delayed_work dw in place.

/* https://elixir.bootlin.com/linux/v4.9.294/source/include/linux/workqueue.h */
#define DECLARE_DELAYED_WORK(n, f)					\
	struct delayed_work n = __DELAYED_WORK_INITIALIZER(n, f, 0)

Using this macro, the only way I found to get a hold of dw from Ada without crashing (returning dw from a wrapper never worked) was to globally call DECLARE_DELAYED_WORK(n, f) in main.c and then bind only to dw. Having to maintain this from C, making it magically appear in Ada felt “breadboard wiring” to me. In the code repository, you will find that we fully reconstructed this macro under the procedure of the same name Declare_Delayed_Work.

The pointer shortcut

Most published Ada to C bindings implement full definition parity. This is an ideal situation in most cases but it also comes with complexity, may generate many 3rd party files, sometimes buried deep, out-of-sync definitions, etc. What can you do when complete bindings are missing or you just want to move lean and fast? If you are making a prototype, you want minimal dependencies, the binding part is peripheral eg. you may only need a quick native window API. You get the point.

Depending on the context you do not always need the full type definitions to get going. Anytime you are strictly dealing with a handle pointer (not owning the memory), you can take a shortcut. Let’s bind to gpio_get_value to illustrate. Again, I follow and layout all C signatures found in the kernel sources leading to concrete stuff, where we can bind.

/* https://elixir.bootlin.com/linux/v4.9.294/source(-) */
/* (+)include/linux/gpio.h */
static inline int gpio_get_value(unsigned int gpio)
{
	return __gpio_get_value(gpio);
}

/* (+)include/asm-generic/gpio.h */
static inline int __gpio_get_value(unsigned gpio)
{
	return gpiod_get_raw_value(gpio_to_desc(gpio));
}
/* (+)include/linux/gpio/consumer.h */
struct gpio_desc *gpio_to_desc(unsigned gpio);            /* bindable */

int gpiod_get_raw_value(const struct gpio_desc *desc);    /* bindable */

/* (+)drivers/gpio/gpiolib.h */
struct gpio_desc {
	struct gpio_device	*gdev;
	unsigned long		flags;
...
	const char		*name;
};

Inspecting the C definitions we find that gpiod_get_raw_value and gpio_to_desc are our available functions for binding. We note gpio_to_desc uses a transient pointer of type gpio_desc *. Because we do not touch or own a full gpio_desc instance we can happily skip defining it in full (and any dependent leads eg. gpio_device).

By declaring type Gpio_Desc_Acc is new System.Address; we create an equivalent to gpio_desc *. After all, a C pointer is a named system address. We now have everything we need to build our Ada version of gpio_get_value.

-- kernel.ads
package Ic renames Interfaces.C;

function Gpio_Get_Value (Gpio : Ic.Unsigned) return Ic.Int; -- only this is visible for clients of kernel

-- kernel.adb
type Gpio_Desc_Acc is new System.Address; -- shortcut

function Gpio_To_Desc_C (Gpio : Ic.Unsigned) return Gpio_Desc_Acc with
   Import        => True,
   Convention    => C,
   External_Name => "gpio_to_desc";
 
function Gpiod_Get_Raw_Value_C (Desc : Gpio_Desc_Acc) return Ic.Int with
   Import        => True,
   Convention    => C,
   External_Name => "gpiod_get_raw_value";

function Gpio_Get_Value (Gpio : Ic.Unsigned) return Ic.Int is
   Desc : Gpio_Desc_Acc := Gpio_To_Desc_C (Gpio);
begin
   return Gpiod_Get_Raw_Value_C (Desc);
end;

The Raw bindings, “100% Ada”

In most production contexts we cannot recommend reconstructing unbindable kernel API calls in Ada. Wrapping the C macro or static inline is definitely easier, safer, portable and maintainable. The following goes full blown Ada for the sake of illustrating some interesting nuts and bolts and to show that it is always possible. 

Flags, first take

Given the will power you can always reconstruct the targeted macro or static inline in Ada. Let’s come back to create_singlethread_workqueue. If you take the time to expand its macro using GCC this is what you get.

$ gcc -E [~ 80_switches_for_valid_ko] printk_wq.c 
...
wq = __alloc_workqueue_key(("%s"),
                          (WQ_UNBOUND |
                           __WQ_ORDERED |
                           __WQ_ORDERED_EXPLICIT |
                          (__WQ_LEGACY | WQ_MEM_RECLAIM)),
                          (1),
                          ((void *)0),
                          ((void *)0),
                          "my_wq");

All arguments are straightforward to map except the OR‘ed flags. Let’s search the kernel sources for those flags.

/* https://elixir.bootlin.com/linux/v4.9.294/source/include/linux/workqueue.h */
enum {
   WQ_UNBOUND             = 1 << 1,
   ...
   WQ_POWER_EFFICIENT     = 1 << 7,

   __WQ_DRAINING          = 1 << 16,
   ...
   __WQ_ORDERED_EXPLICIT  = 1 << 19,

   WQ_MAX_ACTIVE          = 512,     
   WQ_MAX_UNBOUND_PER_CPU = 4,      
   WQ_DFL_ACTIVE          = WQ_MAX_ACTIVE / 2,
};

Here are our design decisions for reconstruction

• WQ_MAX_ACTIVE, WQ_MAX_UNBOUND_PER_CPU, WQ_DFL_ACTIVE are constants, not flags, so we keep them out.
• The enum is anonymous, let’s give it a proper named type.
• __WQ pattern is probably a convention but at the same times usage is mixed, eg. WQ_UNBOUND | __WQ_ORDERED, so let’s flatten all this.

Because we do not use these flags elsewhere in our code base, the occasion is perfect to show that in Ada we can keep all this modeling local to our unique function using it.

-- kernel.ads
package Ic renames Interfaces.C;

type Wq_Struct_Access is new System.Address;      -- shortcut
type Lock_Class_Key_Access is new System.Address; -- shortcut
Null_Lock : Lock_Class_Key_Access := 
Lock_Class_Key_Access (System.Null_Address); -- typed ((void *)0) equiv.

-- kernel.adb
type Bool is (NO, YES) with Size => 1;       -- enum holding on 1 bit
for Bool use (NO => 0, YES => 1);            -- "represented" by 0, 1 too

function Alloc_Workqueue_Key_C ...
   External_Name => "__alloc_workqueue_key";      -- thin binding

function Create_Singlethread_Wq (Name : String) return Wq_Struct_Access is
   type Workqueue_Flags is record
      ...
      WQ_POWER_EFFICIENT  : Bool;
      WQ_DRAINING         : Bool;
      ...
   end record with Size => Ic.Unsigned'Size;
   for Workqueue_Flags use record
      ...
      WQ_POWER_EFFICIENT  at 0 range  7 ..  7;
      WQ_DRAINING         at 0 range 16 .. 16;
      ...
   end record;
   Flags : Workqueue_Flags := (WQ_UNBOUND          => YES,
                               WQ_ORDERED          => YES,
                               WQ_ORDERED_EXPLICIT => YES,
                               WQ_LEGACY           => YES,
                               WQ_MEM_RECLAIM      => YES,
                               Others              => NO);
   Wq_Flags : Ic.Unsigned with Address => Flags'Address;
begin
   return Alloc_Workqueue_Key_C ("%s", Wq_Flags, 1, Null_Lock, "", Name);
end;

• In C, each flag is implicitly encoded as an integer literal, bit swapped by an amount. Because __alloc_workqueue_key signature expects flags encoded as an unsigned int It should be reasonable to use Ic.Unsigned’Size, to hold a Workqueue_Flags.
• We build the representation of Workqueue_Flags type similar to what we learned in Part 2 to model registers. Compared to the C version we now have NO => 0, YES => 1 semantic and no need for bitwise operations.
• Remember, in Ada we roll with strong user-defined types for the greater goods. Therefore something like Workqueue_Flags does not match the expected Flags : Ic.Unsigned parameter of our __alloc_workqueue_key thin binding. What should we do? You create a variable Wq_Flags : Ic.Unsigned and overlay it the address of Flags : Workqueue_Flags which you can now pass in to __alloc_workqueue_key.

Wq_Flags : Ic.Unsigned with Address => Flags'Address; -- voila!

Ioremap and iowrite32

The core work of the raw_io version happens in Set_Gpio. Using Ioremap, we retrieve the kernel mapped IO memory location for the GPIO_OUT register physical address. We then write the content of our Gpio_Control to this IO memory location through Io_Write_32.

-- kernel.ads
type Iomem_Access is new System.Address;

-- led.adb
package K renames Kernel;
package C renames Controllers;

procedure Set_Gpio (Pin : C.Pin; S : Led.State) is

   function Bit (S : Led.State) return C.Bit renames Led.State'Enum_Rep;

   Base_Addr : K.Iomem_Access;
   Control   : C.Gpio_Control := (Bits  => (others => 0), 
                                  Locks => (others => 0));
   Control_C : K.U32 with Address => Control'Address;
begin
   ...
   Control.Bits (Pin.Reg_Bit) := Bit (S); -- set the GPIO flags
   ...
   Base_Addr := Ioremap (C.Get_Register_Phys_Address (Pin.Port, C.GPIO_OUT),
                         Control_C'Size); -- get kernel mapped register addr.
   K.Io_Write_32 (Control_C, Base_Addr);  -- write our GPIO flags to this addr.
   ...
end;

Let’s take the hard paths of full reconstruction to illustrate interesting stuff. We first implement ioremap. On the C side we find

/* https://elixir.bootlin.com/linux/v4.9.294/source(-) */
/* (+)arch/arm64/include/asm/io.h */
#define ioremap(addr, size) \
   __ioremap((addr), (size), __pgprot(PROT_DEVICE_nGnRE))

extern void __iomem *__ioremap(phys_addr_t phys_addr, size_t size, pgprot_t prot);                       

Flags, second take

Here we are both lucky and unlucky. __ioremap is low hanging while __pgprot(PROT_DEVICE_nGnRE) turns out to be a rabbit hole. I skip the intermediate expansion by reporting the final result

$ gcc -E [~ 80_switches_for_valid_ko] test_using_ioremap.c
…
void* membase = __ioremap(  
   (phys_addr + offset),
   (4),
   ((pgprot_t) {
      (((((((pteval_t)(3)) << 0) |
      (((pteval_t)(1)) << 10) |
      (((pteval_t)(3)) << 8)) |
      (arm64_kernel_unmapped_at_el0() ? (((pteval_t)(1)) << 11) : 0)) |
      (((pteval_t)(1)) << 53) |
      (((pteval_t)(1)) << 54) |
      (((pteval_t)(1)) << 55) |
      ((((pteval_t)(1)) << 51)) |
      (((pteval_t)((1))) << 2)))
   }))

Searching for definitions in the kernel sources: (meaningful sampling only)

/* https://elixir.bootlin.com/linux/v4.9.294/source(-) */
/* (+)arch/arm64/include/asm/pgtable-hwdef.h */
#define PTE_TYPE_MASK       (_AT(pteval_t, 3) << 0)
...
#define PTE_NG		    (_AT(pteval_t, 1) << 11) 
...
#define PTE_ATTRINDX(t)     (_AT(pteval_t, (t)) << 2)    

/* (+)arch/arm64/include/asm/mmu.h */
static inline bool arm64_kernel_unmapped_at_el0(void)   
{
   return IS_ENABLED(CONFIG_UNMAP_KERNEL_AT_EL0) &&
   cpus_have_const_cap(ARM64_UNMAP_KERNEL_AT_EL0);
}

/* (+)arch/arm64/include/asm/pgtable-prot.h */
#define PTE_DIRTY           (_AT(pteval_t, 1) << 55)    

/* (+)arch/arm64/include/asm/memory.h */
#define MT_DEVICE_nGnRE     1                           

The macro pattern _AT(pteval_t, x) can be cleared right away. IIUC, it serves to handle calling both from assembly and C. When you are concerned by the C case, like we do, it boils down to x, eg. ((pteval_t)(1)) << 10) becomes 1 << 10.

arm64_kernel_unmapped_at_el0 is in part ‘kernel configuration dependant’, defaulting to ‘yes’, so let’s simplify our job and bring it in, PTE_NG which is the choice ? (((pteval_t)(1)) << 11), for all cases.

(((pteval_t)((1))) << 2))) turns out to be PTE_ATTRINDX(t) with MT_DEVICE_nGnRE as input. Inspecting the kernel sources, there are four other values intended as input to PTE_ATTRINDX(t). PTE_ATTRINDX behaves like a function so let implement it as such.

type Pgprot_T is mod 2**64; -- type will hold on 64 bits 

type Memory_T is range 0 .. 5;
MT_DEVICE_NGnRnE : constant Memory_T := 0;
MT_DEVICE_NGnRE  : constant Memory_T := 1;
...
MT_NORMAL_WT     : constant Memory_T := 5;

function PTE_ATTRINDX (Mt : Memory_T) return Pgprot_T is
   (Pgprot_T(Mt * 2#1#e+2)); -- base # based_integer # exponent

Here I want to show another way to replicate C behavior, this time using bitwise operations. Something like PTE_TYPE_MASK value ((pteval_t)(3)) << 0 cannot be approached like we did before. 3 takes two bits and is somewhat a magic number. What we can do is improve on the representation. We are doing bit masks so why not express using binary numbers directly. It even makes sense graphically.

PTE_VALID      : Pgprot_T := 2#1#e+0;
...
PTE_TYPE_MASK  : Pgprot_T := 2#1#e+0 + 2#1#e+1; -- our famous 3
...
PTE_HYP_XN     : Pgprot_T := 2#1#e+54;

-- kernel.ads
type Phys_Addr_T is new System.Address;
type Iomem_Access is new System.Address;

-- kernel.adb
function Ioremap (Phys_Addr : Phys_Addr_T; 
                  Size      : Ic.Size_T) return Iomem_Access is
...         
   Pgprot : Pgprot_T := (PTE_TYPE_MASK or
                         PTE_AF        or
                         PTE_SHARED    or
                         PTE_NG        or
                         PTE_PXN       or
                         PTE_UXN       or
                         PTE_DIRTY     or
                         PTE_DBM       or
                         PTE_ATTRINDX (MT_DEVICE_NGnRE));
begin
   return Ioremap_C (Phys_Addr, Size, Pgprot);
end;

So what is interesting here?

• Ada is flexible. The original Pgprot_T values arrangement did not allow record mapping like we previously did for type Workqueue_Flags. We adapted by replicating the C implementation, OR‘ing all values to create a final mask.
• Everything has been tidied up by strong typing. We are now stuck with disciplined stuff.
• Representation is explicit, expressed in the intended base.
• Once again this typing machinery lives at the most restrictive scope, inside the Ioremap function. Because Ada “scoping” has few special rules, refactoring up/out of scopes usually boils down to a simple blocks swapping game.

Emitting assembly

Now we give a look at ioread32 and iowrite32. Turns out those are, again, a cascade of static inline and macros ending up directly emitting GCC assembly directives (detailing only iowrite32).

/* https://elixir.bootlin.com/linux/v4.9.294/source(-) */
/* (+)include/asm-generic/io.h */
static inline void iowrite32(u32 value, volatile void __iomem *addr)
{
   writel(value, addr);
}
/* (+)include/asm/io.h */
#define writel(v,c)     ({ __iowmb(); writel_relaxed((v),(c)); })
#define __iowmb()       wmb()    

/* (+)include/asm/barrier.h */
#define wmb()           dsb(st) 
#define dsb(opt)        asm volatile("dsb " #opt : : : "memory")

/* (+)arch/arm64/include/asm/io.h */
#define writel_relaxed(v,c) \
   ((void)__raw_writel((__force u32)cpu_to_le32(v),(c)))
   
static inline void __raw_writel(u32 val, volatile void __iomem *addr)   
{
   asm volatile("str %w0, [%1]" : : "rZ" (val), "r" (addr));
}

In Ada it becomes

with System.Machine_Code
...
procedure Io_Write_32 (Val : U32; Addr : Iomem_Access) is
   use System.Machine_Code;
begin
   Asm (Template => "dsb st",
        Clobber  => "memory",
        Volatile => True);

   Asm (Template => "str %w0, [%1]",
        Inputs   => (U32'Asm_Input ("rZ", Val), 
                     Iomem_Access'Asm_Input ("r", Addr)),
        Volatile => True);
end;

This Io_Write_32 implementation is not portable as we rebuilt the macro following the expansion tailored for arm64. A C wrapper would be less trouble while ensuring portability. Nevertheless, we felt this experiment was a good opportunity to show assembly directives in Ada.

That’s it!

I hope you appreciated this moderately dense overview of Ada in the context of Linux kernel module developpement. I think we can agree that Ada is a really disciplined and powerful contender when it comes to system, pedal to the metal, programming. I thank you for your time and concern. Do not hesitate to reach out and, happy Ada coding!

I want to thank Quentin Ochem, Nicolas Setton, Fabien Chouteau, Jerome Lambourg, Michael Frank, Derek Schacht, Arnaud Charlet, Pat Bernardi, Leo Germond, and Artium Nihamkin for their different insights and feedback to nail this experiment.

The author, Olivier Henley, is a UX Engineer at AdaCore. His role is exploring new markets through technical stories. Prior to joining AdaCore, Olivier was a consultant software engineer for Autodesk. Prior to that, Olivier worked on AAA game titles such as For Honor and Rainbow Six Siege in addition to many R&D gaming endeavors at Ubisoft Montreal. Olivier graduated from the Electrical Engineering program in Polytechnique Montreal. He is a co-author of patent US8884949B1, describing the invention of a novel temporal filter implicating NI technology. An Ada advocate, Olivier actively curates GitHub’s Awesome-Ada list.

For this three part series, we implemented a ‘pedal to the metal’ GPIO driven, flashing of a LED, in the context of a Linux kernel module for the NVIDIA Jetson Nano development board (kernel-based v4.9.294, arm64) in my favorite programming language … Ada!

• Part 1. Review of a kernel module, build strategy, and Ada integration.
• Part 2. Modeling of the problem in Ada.
• Part 3. Practical Ada binding to the C kernel APIs.

You can find the whole project published at https://github.com/ohenley/adacore_jetson. It is known to build and run properly. All instructions to be up and running in 5 minutes are included in the accompanying front-facing README.md. Do not hesitate to fill a Github issue if you find any problem.

Disclaimer: This text is meant to appeal to both Ada and non-Ada coders. Therefore I try to strike a balance between code story simplicity, didactic tractability, and features density. As I said to a colleague, this is the text I would have liked to cross before starting this experiment.

Pascal on steroids you quoted?

led.ads (specification file, Ada equivalent to C .h header file) is where we model a simple interface for our LED.

with Controllers;
package Led is -- this bit of Ada code provides an interface to our LED

  package C Renames Controllers;

  type State is (Off, On);
  type Led_Type (Size : Natural) is tagged private;

  subtype Tag Is String;

  procedure Init       (L : out Led_Type; P : C.Pin; T : Tag; S : State);
  procedure Flip_State (L : in out Led_Type);
  procedure Final      (L : Led_Type);

private

  for State use (Off => 0, On => 1);

  function "not" (S : State) return State is
      (if S = On then Off else On);
  type Led_Type (Size : Natural) is tagged record
      P     : C.Pin;
      T     : Tag (1 .. Size);
      S     : State;
  end record;

end Led;

For those new to Ada, many interesting things happen for a language operating at the metal.

The driver translation

The top-level code story resides in flash_led.adb. Immediately when the module is loaded by the kernel, Ada_Init_Module executes, called from our main.c entry point. It first imports the elaboration procedure flash_ledinit generated by GNATbind, runs it, Init our LED object, and then setup/registers the delayed work queue.

with Kernel;
with Controllers;
with Interfaces.C; use Interfaces.C;
...
   package K renames Kernel;
   package C renames Controllers;

   Wq             : K.Workqueue_Struct_Access := K.Null_Wq;
   Delayed_Work   : aliased K.Delayed_Work; -- subject to alias by some pointer on it

   Pin            : C.Pin := C.Jetson_Nano_Header_Pins (18);
   Led_Tag        : Led.Tag := "my_led";
   My_Led         : Led_Type (Led_Tag'Size);
   Half_Period_Ms : Unsigned := 500;
...
procedure Ada_Init_Module is
   procedure Ada_Linux_Init with
      Import        => True,
      Convention    => Ada,
      External_Name => "flash_ledinit";
begin
   Ada_Linux_Init;
   My_Led.Init (P => Pin, T => Led_Tag, S => Off);
   ...

   if Wq = K.Null_Wq then -- Ada equal
      Wq := K.Create_Singlethread_Wq ("flash_led_wq");
   end if;

   if Wq /= K.Null_Wq then -- Ada not equal
      K.Queue_Delayed_Work(Wq, 
                           Delayed_Work'Access, -- an Ada pointer
                           K.Msecs_To_Jiffies (Half_Period_Ms));
   end if;
end;

In the callback, instead of printing to the kernel message buffer, we call the Flip_State implementation of our LED object and re-register to the delayed work queue. It now flashes.

procedure Work_Callback (Work : K.Work_Struct_Access) is
begin
   My_Led.Flip_State;
   K.Queue_Delayed_Work (Wq,
                         Delayed_Work'Access, -- An Ada pointer
                         K.Msecs_To_Jiffies (Half_Period_Ms));
end;

Housekeeping

If you search the web for images of “NVIDIA Jetson Development board GPIO header pinout” you will find such diagram.

Right away, you figure there are about 5 data fields describing a single pinout

• Board physical pin number (#).
• Default function (name).
• Alternate function (name).
• Linux GPIO (#).
• Tegra SoC GPIO (name.#).

Looking at this diagram we find hints of the different mapping happening at the Tegra SoC, Linux, and physical pinout level. Each “interface” has its own addressing scheme. The Tegra SoC has logical naming and offers default and alternate functions for a given GPIO line. Linux maintains its own GPIO numbering of the lines so does the physical layout of the board.

From where I stand I want to connect a LED circuit to a board pin and control it without fuss, by using any addressing scheme available. For this we created an array of variant records instantiation, modeling the pin characteristics for the whole header pinouts. Nothing cryptic or ambiguous, just precise and clear structured data.

type Jetson_Nano_Header_Pin is range 1 .. 40; -- Nano Physical Expansion Pinout
type Jetson_Nano_Pin_Data_Array is array (Jetson_Nano_Header_Pin) of Pin_Data;

Jetson_Nano_Header_Pins : constant Jetson_Nano_Pin_Data_Array :=
      (1   => (Default => VDC3_3, Alternate => NIL),
       2   => (Default => VDC5_0, Alternate => NIL),
       3   => (Default       => I2C1_SDA, 
               Alternate     => GPIO, 
               Linux_Nbr     => 75, 
               Port          => PJ, 
               Reg_Bit       => 3, 
               Pinmux_Offset => 16#C8#),
       4   => (Default => VDC5_0, Alternate => NIL),
...
      40   => (Default       => GPIO,      
               Alternate     => I2S_DOUT,  
               Linux_Nbr     => 78,  
               Port          => PJ,  
               Reg_Bit       => 6, 
               Pinmux_Offset => 16#14C#));

Because everything in this Jetson_Nano_Header_Pins data assembly is unique and unrelated it cannot be generalized further, it has to live somewhere, plainly. Let’s check how we model a single pin as Pin_Data.

type Function_Type is (GPIO, VDC3_3, VDC5_0, GND, NIL, ..., I2S_DOUT);
type Gpio_Linux_Nbr is range 0 .. 255;        -- # cat /sys/kernel/debug/gpio
type Gpio_Tegra_Port is (PA, PB, ..., PEE, NIL);
type Gpio_Tegra_Register_Bit is range 0 .. 7;

type Pin_Data (Default : Function_Type := NIL) is record
   Alternate: Function_Type := NIL;
   case Default is
       when VDC3_3 .. GND =>
           Null; -- nothing to add
       when others =>
           Linux_Nbr     : Gpio_Linux_Nbr;
           Port          : Gpio_Tegra_Port;
           Reg_Bit       : Gpio_Tegra_Register_Bit;
           Pinmux_Offset : Storage_Offset;
   end case;
end record;

Pin_Data type is a variant record, meaning, based on a Function_Type, it will contain “variable” data. Notice how we range over the Function_Type values to describe the switch cases. This gives us the capability to model all pins configuration.

When you consult the Technical Reference Manual (TRM) of the Nano board, you find that GPIO register controls are layed out following an arithmetic pattern. Using some hardware entry point constants and the specifics of a pin data held into Jetson_Nano_Header_Pins, one can resolve any register needed.

Gpio_Banks : constant Banks_Array := 
   (To_Address (16#6000_D000#), 
    ...         
    To_Address (16#6000_D700#));

type Register is (GPIO_CNF, GPIO_OE, GPIO_OUT, ..., GPIO_INT_CLR);
type Registers_Offsets_Array is array (Register) of Storage_Offset;
Registers_Offsets : constant Registers_Offsets_Array := 
   (GPIO_CNF     => 16#00#, 
    ... , 
    GPIO_INT_CLR => 16#70#);

function Get_Bank_Phys_Addr (Port : Gpio_Tegra_Port) return System.Address is
   (Gpio_Banks (Gpio_Tegra_Port'Pos (Port) / 4 + 1));

function Get_Register_Phys_Addr (Port : Gpio_Tegra_Port; Reg  : Register) return System.Address is
   (Get_Bank_Phys_Address (Port) + 
    Registers_Offsets (Reg) + 
   (Gpio_Tegra_Port'Pos (Port) mod 4) * 4);

In this experiment, it is mainly used to request the kernel memory mapping of such GPIO register.

-- led.adb (raw io version)
Base_Addr := Ioremap (C.Get_Register_Phys_Address (Pin.Port, C.GPIO_CNF), Control_C'Size);

Form follows function

Now, let’s model a common Pinmux register found in the TRM.

package K renames Kernel;
...
type Bit is mod 2**1;      -- will hold in 1 bit
type Two_Bits is mod 2**2; -- will hold in 2 bits

type Pinmux_Control is record
   Pm         : Two_Bits;
   Pupd       : Two_Bits;
   Tristate   : Bit;
   Park       : Bit;
   E_Input    : Bit;
   Lock       : Bit;
   E_Hsm      : Bit;
   E_Schmt    : Bit;
   Drive_Type : Two_Bits;
end record with Size => K.U32'Size;

for Pinmux_Control use record
   Pm         at 0 range  0 ..  1;  -- At byte 0 range bit 0 to bit 1
   Pupd       at 0 range  2 ..  3;
   Tristate   at 0 range  4 ..  4;
   Park       at 0 range  5 ..  5;
   E_Input    at 0 range  6 ..  6;
   Lock       at 0 range  7 ..  7;
   E_Hsm      at 0 range  9 ..  9;
   E_Schmt    at 0 range 12 .. 12;
   Drive_Type at 0 range 13 .. 14;
end record;

I think the code speaks for itself.

• We specify types Bit and Two_Bits to cover exactly the binary width conveyed by their names.
• We compose the different bitfields over a record size of 32 bits.
• We explicitly layout the bitfields using byte addressing and bit range.

You can now directly address bitfield/s by name and not worry about any bitwise arithmetic mishap. Ok so now what about logically addressing a bitfield/s? You pack inside arrays. We do have an example in the modeling of the GPIO register.

type Gpio_Tegra_Register_Bit is range 0 .. 7;
...
type Bit is mod 2**1;  -- will hold in 1 bit
...
type Gpio_Bit_Array is array (Gpio_Tegra_Register_Bit) of Bit with Pack;

type Gpio_Control is record
   Bits : Gpio_Bit_Array;
   Locks : Gpio_Bit_Array;
end record with Size => K.U32'Size;

for Gpio_Control use record
   Bits  at 0 range 0 .. 7;
   Locks at 1 range 0 .. 7; -- At byte 1 range bit 0 to bit 7
end record;

Now we can do.

procedure Set_Gpio (Pin : C.Pin; S : Led.State) is
   function Bit (S: Led.State) return C.Bit renames Led.State'Enum_Rep;
   -- remember we gave the Led.State Enum a numeric Representation clause.

   Control : C.Gpio_Control := (Bits  => (others => 0),  -- init all to 0
                                Locks => (others => 0));
   ...
begin
   ...
   Control.Bits (Pin.Reg_Bit) := Bit (S); -- Kewl!
   ...
end;

Verbosity

I had to give you a feel of what is to gain by modeling using Ada. To me, it is about semantic clarity, modeling affinity, and structural integrity. Ada offers flexibility through a structured approach to low-level details. Once set foot in Ada, domain modeling becomes easy because as you saw, you are given provisions to incisively specify things using strong user-defined types. The stringent compiler constraints your architecture to fall in place on every iteration. From experience, it is truly amazing how the GNAT toolchain helps you iterate quickly while keeping technical debt in check.

Ada is not too complex, nor too verbose; those are mundane concerns.

Ada demands you to demonstrate that your modeling makes sense for thousands of lines of code; it is code production under continuous streamlining.

What’s next?

In the last entry, we will finally meet the kernel. If I kept your interest and you want to close the loop, move here. Cheers!

I want to thank Quentin Ochem, Nicolas Setton, Fabien Chouteau, Jerome Lambourg, Michael Frank, Derek Schacht, Arnaud Charlet, Pat Bernardi, Leo Germond, and Artium Nihamkin for their different insights and feedback to nail this experiment.

The author, Olivier Henley, is a UX Engineer at AdaCore. His role is exploring new markets through technical stories. Prior to joining AdaCore, Olivier was a consultant software engineer for Autodesk. Prior to that, Olivier worked on AAA game titles such as For Honor and Rainbow Six Siege in addition to many R&D gaming endeavors at Ubisoft Montreal. Olivier graduated from the Electrical Engineering program in Polytechnique Montreal. He is a co-author of patent US8884949B1, describing the invention of a novel temporal filter implicating NI technology. An Ada advocate, Olivier actively curates GitHub’s Awesome-Ada list.