Accueil Linux Pirater le noyau Linux dans Ada – Partie 2

Pirater le noyau Linux dans Ada – Partie 2

Par

avril 7, 2022

Pour cette série en trois parties, nous avons implémenté un GPIO « pédale au métal », clignotant d’une LED, dans le contexte d’un module de noyau Linux pour la carte de développement NVIDIA Jetson Nano (basée sur le noyau v4.9.294, arm64) dans mon langage de programmation préféré… Ada !

Vous pouvez retrouver l’intégralité du projet publié sur https://github.com/ohenley/adacore_jetson. Il est connu pour se construire et fonctionner correctement. Toutes les instructions pour être opérationnel en 5 minutes sont incluses dans le fichier README.md frontal qui l’accompagne. N’hésitez pas à remplir un ticket Github si vous rencontrez un problème.

Avis de non-responsabilité : ce texte est destiné à plaire aux codeurs Ada et non-Ada. Par conséquent, j’essaie de trouver un équilibre entre la simplicité de l’histoire du code, la traçabilité didactique et la densité des fonctionnalités. Comme je l’ai dit à un collègue, c’est le texte que j’aurais aimé traverser avant de commencer cette expérience.

Table des matières hide

1 Pascal sous stéroïdes vous avez cité ?

2 La traduction du pilote

3 Entretien ménager

4 La forme suit la fonction

5 Verbosité

6 Et après?

Pascal sous stéroïdes vous avez cité ?

led.ads (sfichier de spécification, Ada équivalent au fichier d’en-tête C .h) est l’endroit où nous modélisons une interface simple pour notre 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;

Pour ceux qui découvrent Ada, il se passe beaucoup de choses intéressantes pour un langage opérant au niveau du métal.

Première, taper sont définis par l’utilisateur et solides. Par conséquent, l’analyse au moment de la compilation est extrêmement riche et la vérification extrêmement stricte. De nombreux bogues ne survivent pas à la compilation. Si vous voulez repousser les limites, passez au sous-ensemble SPARK Ada. Vous pouvez alors commencer à prouver l’absence d’erreurs d’exécution dans votre code. C’est cette affaire sérieuse.
Nous avec le package Contrôleurs. Ada avec est une inclusion sémantique sans état au niveau du langage, pas seulement une inclusion de texte de préprocesseur comme #inclure. Par exemple. Plus de contextes de redéfinition, d’accompagnement de passe-partout de garde, et ainsi de suite.
La LED est emballé. Rien à l’intérieur de Led ne peut se heurter à l’extérieur. Il peut alors être avec‘ed, et utiliser‘d à n’importe quelle portée. La portée Ada, l’espacement des noms, la signature, etc. sont puissants et solides dans tous les domaines. Tout expliquer n’a pas sa place ici.
Ici renomme est utilisé comme idiome pour préserver l’espacement de noms absolu, mais l’histoire du code est succincte. Dans les énormes bases de code, la traçabilité reste claire, ce qui est très bienvenu.
Énumération Ada État a une représentation complète de l’image et de la plage. Nous utiliser une clause de représentation numérique, qui servira plus tard.
UNE enregistrement tagué vous permet d’hériter d’un type (comme en POO) et d’utiliser la notation « point ».
Nous sous-typons une balise en tant que chaîne pour plus de clarté sémantique.
en dehors signifie, nous avons besoin d’avoir un objet initialisé avant de retourner « out », en dehors l’objet initialisé « in » passé sera modifié avant de retourner « out ».
Record (vaguement un équivalent de structure C) en spécifiant notre taille de balise.
Nous remplaçons le « ne pas » opérateur pour le État type en tant qu’expression de fonction.
Nous avons public-privé une visibilité de l’information qui nous permet de structurer notre code et de le communiquer aux autres. Un bel exemple, car un emballer est au niveau du langage, vous supprimez tout type dans la partie publique, ajoutez des données dans le fichier corps et vous vous retrouvez avec un Singleton. C’est facile.

La traduction du pilote

l’histoire de code de niveau supérieur réside dans flash_led.adb. Dès que le module est chargé par le noyau, Ada_Init_Module exécute, appelé depuis notre principal c point d’accès. Il importe d’abord la procédure d’élaboration flash_ledinit généré par GNATbind, l’exécute, Init notre objet LED, puis configurez/enregistrez la file d’attente de travail retardée.

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;

Dans le rappel, au lieu d’imprimer dans le tampon de messages du noyau, nous appelons le Flip_State implémentation de notre objet LED et réenregistrement dans la file d’attente des travaux différés. Il clignote maintenant.

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;

Entretien ménager

Si vous recherchez sur le Web des images du « brochage de l’en-tête GPIO de la carte de développement NVIDIA Jetson », vous trouverez ce schéma.

Tout de suite, vous pensez qu’il y a environ 5 champs de données décrivant un seul brochage

Numéro de broche physique de la carte (#).
Fonction par défaut (nom).
Fonction alternative (nom).
GPIO Linux (#).
Tegra SoC GPIO (nom.#).

En regardant ce diagramme, nous trouvons des indices sur les différents mappages qui se produisent au niveau du SoC Tegra, Linux et du brochage physique. Chaque « interface » a son propre schéma d’adressage. Le Tegra SoC a une dénomination logique et offre des fonctions par défaut et alternatives pour une ligne GPIO donnée. Linux maintient sa propre numérotation GPIO des lignes, tout comme la disposition physique de la carte.

D’où je me tiens, je veux connecter un circuit LED à une broche de carte et le contrôler sans problème, en utilisant n’importe quel schéma d’adressage disponible. Pour cela, nous avons créé un tableau d’instanciation d’enregistrements de variantes, modélisant les caractéristiques des broches pour l’ensemble des brochages d’en-tête. Rien de crypté ou d’ambigu, juste des données structurées précises et claires.

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#));

Parce que tout dans ce Jetson_Nano_Header_Pins l’assemblage de données est unique et sans rapport, il ne peut pas être généralisé davantage, il doit vivre quelque part, clairement. Voyons comment nous modélisons une seule broche comme 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_Type de données est un enregistrement de variante, c’est-à-dire basé sur un Function_Type, il contiendra des données « variables ». Remarquez comment nous nous échelonnons sur le Function_Type valeurs pour décrire les cas de commutation. Cela nous donne la possibilité de modéliser toutes les configurations de broches.

Lorsque vous consultez le manuel de référence technique (TRM) du Carte nano, vous constatez que les commandes de registre GPIO sont disposées selon un modèle arithmétique. En utilisant certaines constantes de point d’entrée matérielle et les spécificités d’une donnée de broche conservée dans Jetson_Nano_Header_Pinson peut résoudre n’importe quel registre nécessaire.

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);

Dans cette expérience, il est principalement utilisé pour demander le mappage de la mémoire du noyau d’un tel registre GPIO.

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

La forme suit la fonction

Modélisons maintenant un registre Pinmux commun trouvé dans le 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;

Je pense que le code parle de lui-même.

Nous spécifions les types Bit et Deux_bits pour couvrir exactement la largeur binaire véhiculée par leurs noms.
Nous composons les différents champs de bits sur une taille d’enregistrement de 32 bits.
Nous mettons explicitement en page les champs de bits en utilisant l’adressage d’octets et la plage de bits.

Vous pouvez maintenant adresser directement le(s) champ(s) de bits par leur nom et ne pas vous soucier des problèmes d’arithmétique au niveau du bit. Ok, alors maintenant, qu’en est-il de l’adressage logique d’un ou plusieurs champs de bits ? Vous emballez à l’intérieur des tableaux. Nous avons un exemple dans la modélisation du registre GPIO.

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;

Maintenant, nous pouvons faire.

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;

Verbosité

Je devais vous donner une idée de ce qu’il y a à gagner en modélisant avec Ada. Pour moi, il s’agit de clarté sémantique, d’affinité de modélisation et d’intégrité structurelle. Ada offre de la flexibilité grâce à une approche structurée des détails de bas niveau. Une fois mis les pieds dans Ada, la modélisation de domaine devient facile car, comme vous l’avez vu, vous avez des dispositions pour spécifier de manière incisive les choses en utilisant des types forts définis par l’utilisateur. Le compilateur rigoureux contraint votre architecture à se mettre en place à chaque itération. Par expérience, il est vraiment étonnant de voir comment la chaîne d’outils GNAT vous aide à itérer rapidement tout en maîtrisant la dette technique.

Ada n’est ni trop complexe, ni trop verbeux ; ce sont des préoccupations banales.

Ada vous demande de démontrer que votre modélisation a du sens pour des milliers de lignes de code ; c’est la production de code sous rationalisation continue.

Et après?

Dans la dernière entrée, nous rencontrerons enfin le noyau. Si j’ai gardé ton intérêt et que tu veux boucler la boucle, bouge ici. Acclamations!

Je tiens à remercier Quentin Ochem, Nicolas Setton, Fabien Chouteau, Jérôme Lambourg, Michael Frank, Derek Schacht, Arnaud Charlet, Pat Bernardi, Leo Germond et Artium Nihamkin pour leurs différentes idées et commentaires pour réussir cette expérience.

L’auteur, Olivier Henleyest ingénieur UX chez AdaCoreComment. Son rôle consiste à explorer de nouveaux marchés à travers des histoires techniques. Avant de rejoindre AdaCore, Olivier était ingénieur logiciel consultant pour Autodesk. Avant cela, Olivier a travaillé sur des titres de jeux AAA tels que For Honor et Rainbow Six Siege en plus de nombreux efforts de R&D en matière de jeux chez Ubisoft Montréal. Olivier est diplômé du programme de génie électrique de Polytechnique Montréal. Il est co-auteur du brevet US8884949B1, décrivant l’invention d’un nouveau filtre temporel impliquant la technologie NI. Défenseur d’Ada, Olivier organise activement Liste Awesome-Ada de GitHub.

Rate this post