Utilisation de Haskell pour les systèmes temps réel de taille importante : comment (si ?)?

Question

J'étais curieux de savoir s'il était possible d'appliquer la puissance de Haskell au monde du temps réel intégré, et en cherchant sur Google, j'ai trouvé l'adresse suivante Atom paquet. Je suppose que dans le cas complexe, le code pourrait présenter tous les bogues C classiques - plantages, corruptions de mémoire, etc. qui les a provoqués. Voici donc la première partie de la question : "Si vous avez eu l'expérience d'Atom, comment avez-vous géré la tâche de déboguer les bugs de bas niveau dans le code C compilé et de les corriger dans le code Haskell original ?".

J'ai cherché d'autres exemples pour Atom, cet article de blog mentionne le code C résultant 22KLOC (et évidemment pas de code :), l'option exemple inclus est un jouet. Ce site y ce ont un code un peu plus pratique, mais cela s'arrête là. Et la raison pour laquelle j'ai mis "sizable" dans le sujet est que je suis très intéressé si vous pouvez partager vos expériences de travail avec le code C généré dans la gamme de 300KLOC+.

Comme je suis un novice en Haskell, il peut évidemment y avoir d'autres moyens que je n'ai pas trouvés en raison de mes inconnues, donc toute autre indication pour l'auto-éducation dans ce domaine serait grandement appréciée - et c'est la deuxième partie de la question - "quelles seraient les autres méthodes pratiques (si) pour faire du développement en temps réel en Haskell ?". Si le multicore est également dans le tableau, c'est un plus supplémentaire :-)

(Concernant l'utilisation de Haskell à cette fin : d'après ce que j'ai lu dans le document cet article de blog Le garbage collection et la paresse en Haskell rendent l'ordonnancement plutôt non déterministe, mais peut-être qu'en deux ans quelque chose a changé. Programmation Haskell dans le monde réel la question sur SO était la plus proche de ce sujet que j'ai pu trouver)

Note : "Je suis curieux de savoir s'il est possible de garantir que le temps de pause lorsque la tâche principale n'est pas exécutée est inférieur à 0,5 ms.

Answer 1

Chez Galois, nous utilisons Haskell pour deux choses :

• Temps réel doux (couches de dispositifs du système d'exploitation, réseaux), où des temps de réponse de 1 à 5 ms sont plausibles. GHC génère du code rapide, et dispose d'un support important pour régler le garbage collector et le scheduler afin d'obtenir les bons timings.
• pour les véritables systèmes en temps réel, les EDSL sont utilisées pour générer du code pour d'autres langages qui fournissent des garanties de timing plus fortes. Par exemple, Cryptol, Atom et Copilot.

Il faut donc faire attention à distinguer l'EDSL (Copilot ou Atom) du langage hôte (Haskell).

---

Quelques exemples de systèmes critiques, et dans certains cas, de systèmes en temps réel, écrits ou générés à partir de Haskell, produits par Galois.

EDSLs

• Copilote : Un moniteur d'exécution en temps réel -- un DSL pour la surveillance en temps réel de l'avionique
• Contrôle d'équivalence et de sécurité en cryptologie -- un DSL pour les composants cryptographiques des systèmes critiques

Systèmes

• HaLVM -- un micro-noyau léger pour les applications embarquées et mobiles
• TSE -- un appareil de réseau inter-domaines (niveau de sécurité)

Answer 2

Andrew,

Oui, il peut être délicat de déboguer les problèmes à travers le code généré pour revenir à la source originale. Atom fournit un moyen de sonder les expressions internes et laisse à l'utilisateur le soin de gérer ces sondes. Pour les tests de véhicules, nous construisons un émetteur (dans Atom) et transmettons les sondes sur un bus CAN. Nous pouvons ensuite capturer ces données, les formater, puis les visualiser avec des outils comme GTKWave, soit en post-traitement, soit en temps réel. Pour la simulation logicielle, les sondes sont traitées différemment. Au lieu d'obtenir les données de la sonde à partir d'un protocole CAN, des crochets sont créés dans le code C pour lever les valeurs de la sonde directement. Les valeurs des sondes sont ensuite utilisées dans le cadre de test unitaire (distribué avec Atom) pour déterminer si un test réussit ou échoue et pour calculer la couverture de la simulation.

Answer 3

Il faudra attendre longtemps avant de trouver un système Haskell qui tienne dans une petite mémoire et puisse garantir des temps de pause inférieurs à la milliseconde. La communauté des implémenteurs Haskell ne semble pas s'intéresser à ce genre d'objectif.

Il existe un intérêt sain pour l'utilisation de Haskell ou de quelque chose de semblable à Haskell pour compiler en quelque chose de très efficace ; par exemple, Bluespec compile vers le matériel.

Je ne pense pas qu'il répondra à vos besoins, mais si vous vous intéressez à la programmation fonctionnelle et aux systèmes embarqués, vous devriez vous renseigner sur les sujets suivants Erlang .

Answer 4

Je ne pense pas que Haskell ou d'autres langages à collecte d'images soient très bien adaptés aux systèmes à temps réel, car les GC ont tendance à amortir leur temps d'exécution en courtes pauses.

Écrire en Atom n'est pas exactement programmer en Haskell, car Haskell peut être considéré comme un simple préprocesseur pour le programme que vous écrivez.

Je pense que Haskell est un génial et l'utilisation de DSEL comme Atom est probablement un excellent moyen de créer des systèmes hard-realtime de taille importante, mais je ne sais pas si Atom correspond ou non à ces critères. Si ce n'est pas le cas, je suis sûr qu'il est possible (et j'encourage tous ceux qui le font !) d'implémenter un DSEL qui le fasse.

Disposer d'un préprocesseur très puissant comme Haskell pour un langage de bas niveau ouvre une énorme fenêtre d'opportunité pour mettre en œuvre des abstractions par le biais de la génération de code qui sont beaucoup plus maladroites lorsqu'elles sont mises en œuvre en tant que générateurs de texte de code C.

Answer 5

Je me suis amusé avec Atom. C'est plutôt cool, mais je pense que c'est mieux pour les petits systèmes. Il est vrai qu'il fonctionne dans des camions et des bus et qu'il met en œuvre des applications critiques du monde réel, mais cela ne signifie pas que ces applications sont nécessairement grandes ou complexes. Il est vraiment destiné aux applications en temps réel et fait tout son possible pour que chaque opération prenne exactement le même temps. Par exemple, au lieu d'une instruction if/else qui exécute conditionnellement l'une des deux branches de code dont le temps d'exécution peut différer, il dispose d'une instruction "mux" qui exécute toujours les deux branches avant de sélectionner conditionnellement l'une des deux valeurs calculées (de sorte que le temps d'exécution total est le même quelle que soit la valeur sélectionnée). Il n'a pas de système de type significatif autre que les types intégrés (comparables à ceux du C) qui sont appliqués par les valeurs GADT passées par la monade Atom. L'auteur travaille sur un outil de vérification statique qui analyse le code C en sortie, ce qui est plutôt cool (il utilise un solveur SMT), mais je pense qu'Atom bénéficierait de plus de fonctionnalités et de vérifications au niveau de la source. Même dans mon application de la taille d'un jouet (contrôleur de lampe de poche à LED), j'ai fait un certain nombre d'erreurs de débutant que quelqu'un de plus expérimenté avec le paquet pourrait éviter, mais qui ont abouti à un code de sortie bogué que j'aurais préféré voir détecté par le compilateur plutôt que par les tests. D'un autre côté, il s'agit toujours de la version 0.1.quelque chose, donc des améliorations sont sans doute à venir.