Et ne me parle pas de je ne sais quel grade doctoral : j'ai le même grade universitaire qu'un ingénieur, à savoir un bac+5.
Je suis ingénieur, et je n'avais pas entendu parler de Lambda avant de faire un dea d'info. C'est peut être un choix de mon école, mais je n'ai pas cette impression-là.
Autant le code python me parle (je ne connais pas du tout ce langage), autant le DSL ne me parle pas.
déployer de l'analyse statique sérieuse sur les drivers et le code du kernel ne donne pas, à long terme, un avantage clair sur la qualité logicielle.
Cela dépend ce que tu appelles "long terme", car tu peux passer un temps infini sur les faux positifs.
Je ne vois pas pourquoi ce serait incompatible avec "l'Open Source" de travailler avec des universitaire
Je n'ai pas dis ça. J'ai dis qu'il fallait démontrer la supériorité d'une solution avant que celle-ci soit mis en œuvre.
C'est idiot, ce n'est pas réaliste pour des universitaires de développer un produit fini (ce n'est pas leur rôle et leur métier) sans savoir s'il y a une volonté pour l'utiliser derrière.
C'est vrai pour n'importe quel développement. Et c'est exactement pour cette raisons que la plus part des outils libres sont directement utile à leurs auteurs, il est très rare d'avoir de bon outils libre, uniquement utile à d'autres.
Dans le cas du noyau, cela serait bosser dessus, dans le but de faire un outil utile pour vous, comme exemple de passage à l'échelle.
C'est bête de ne pas vouloir entendre qu'il faut de vrais efforts des deux côtés.
Il faut voir le gain de leur coté, qui n'est pas évident à moyen terme. Il faudrait peut être organiser une conférence sur les ponts entre recherche et l'open source, pour que les gens se rencontrent, pour montrer les téchno de recherche, montrer les interactions qui marchent.
Concernant Astrée, j'imagine que c'est le genre d'outil qui peut généré un paquet de faux positif. Par exemple, si il détecte trop "simplement" la division. Sparse ne génère pas de faux positif si je me rappelle bien. Si il ne fonctionne bien qu'avec un code généré par SCADE, il y a une gros soucis (sachant que SCADE génère un C restreint ayant déjà beaucoup de bonnes propriétés).
Coverity propose une analyse de code open source. ( https://www.synopsys.com/software-integrity/resources/analyst-reports/open-source-software-scan-report.html ) Cela a été à la mode pendant un moment, puis les devs en ont eu marre des faux positifs dont la corrections pouvaient entrainée des problèmes subtiles (genre générateur de nombre aléatoire de Debian). Je ne connais pas la différence avec Astrée, mais Sparse a été développé ensuite.
Encore une fois, pour ça il faut une culture volontaire du côté des développeurs, et elle manque pour le noyau Linux (alors qu'elle est présente pour Windows, en partie parce que Microsoft n'a pas laissé le choix à ses développeurs).
Le milieu Open Source ne fonctionne pas comme ça. Celui qui apporte une nouvelle techno doit démontrer sa supériorité pour convaincre. Dire "venez avec moi, cela va être génial", cela fait 20 ans, que les développeurs Kernel l'entendent tous les jours. Et au dernière nouvelles les drivers Windows ne fonctionnent pas mieux que les drivers Linux.
En gros, c'est à la communauté de la recherche de prouver que leur approche est meilleur, si vous considérez que les dev sont bêtes parce qu'ils ne vous écoutent pas, c'est mal barré.
Par exemple le code pour décrire une multiplication matrice/vecteur (GEMV en BLAS) dans ce langage est
L'idée est sympa. J'imagine que les usagers de ce genre de DSL sont docteur en mathématique pour le calcul linéaire. Je ne vois pas qui d'autres pourraient s'en servir vu le formalisme mathématique retenu.
Mes tests remontent à loin, mais typiquement dd était bien plus rapide que cp, je crois que j'avais surtout vu cela avec un raid 0, pour saturer la bande passante, il fallait des gros buffers.
comme le fait le vénérable cp, pourquoi fast-copy serait-il plus rapide ?
Pour avoir déjà fait le teste, j'imagine que c'est à cause de la taille de buffers. Lire puis écrire des morceaux de 16 Mo est beaucoup plus rapide qu'avec des morceaux de 8 Ko, surtout avec un HD.
Si tu veux des références plus précises, peux-tu en dire plus sur ce que tu cherches ? (Quel genre de code ?)
Un langage de haut niveau qui va vite.
En général, les langages "rapides" laissent tout le boulot au codeur (asm, c, c++, fortran). C++ avec les templates proposent un moyen de mettre la complexité en library avec le prix d'une grosse difficulté et des messages d'erreur abscons (et donc des bugs). Ce genre de langage trop bas niveau fournis un code rapide sur une machine, mais qui peut être plus lent sur un autre (intel vs amd ou vs ARM), multicore ou pas, SIMD ou pas.
Les compilateurs C/C++ vont très loin dans les optimisations mais sont bridés par le langage lui-même : gestion mémoire basique et explicite (il faut une grande rigueur pour gérer des pools de mémoires et éviter la fragmentation), layout mémoire fixée dans les structures (optimisation par structures de tableaux au lieu de tableaux de structures impossible), code IEE754 immodifiable (sans changer le résultat final), pointeur trop générique qui nécessite un gros travail "d'analyse de vie" pour éviter l'aliasing. Le SIMD est de mieux en mieux géré, mais le multicore reste complexe sauf avec openMP. Par contre utiliser directement les GPU restent encore très expérimental : il suffit de voir la tronche du code opencl avec des string à envoyer au driver de la carte graphique !
Rust permet une bien meilleur gestion mémoire, mais compile moins bien que gcc. "tensor flow" semble pouvoir décrire du code rapide pour plusieurs architectures très différentes, mais cela n'est pas un langage.
On peut aussi parler des optimisations par propagation de constantes qui se limitent aux littéraux basiques, mais pas au 'string' (utile pour les regexp ou même un code SQL embarqué), et je ne parle pas de container constant (AST, lecture de fichier externe, genre configuration en XML, image embarquées ou même un DSL quelconque).
Je crois que tu te trompes sur les dev kernel. En sécurité, la plus part des bugs sont trouvé avec des fuzzers. Concernant l'analyse statique, il existe https://en.wikipedia.org/wiki/Sparse qui permet de vérifier des propriétés statiques (gestion de mutex, d'espace mémoire, etc…).
(1) il y a peu de moyens "simples" d'utiliser le multi-core
Les goroutines sont déjà un bon exemple. Tout ce qui est bas sur le passage de message simple ou les "grosses" boucles d'openMP.
C'est un peu pareil pour les instructions SIMD, si tu connais une façon simple de les ajouter au langage sans casser les garanties de sûreté du langage, raconte-nous.
Je ne comprends pas trop la question. gcc fait de la vectorisation automatique depuis un bail. Il a aussi proposé simplement des tableaux de 4 flottants ou 8 entiers avec les opérations qui correspondent directement sous forme de fonctions transformés ensuite en assembleur. Qu'est-ce qu'il y a de problématiques de donner accès à des fonctions qui correspondent aux instructions assembleurs ?
De plus, ocaml pourrait faire des map et fold sur des array de nombres, et proposer des versions vectorisés des opérations en question.
LLVM me semble être un exemple, ou alors les travaux sur des DSLs qui se compilent bien vers des GPU par exemple. Si tu veux des références plus précises, peux-tu en dire plus sur ce que tu cherches ? (Quel genre de code ?)
LLVM ? Dans quel domaine ? Je l'ai toujours vu comme un compilateur modulaire, mais qui n'arrive toujours au niveau de GCC en terme de perf. Pour les GPU, c'est openCL ou CUDA qui ressemble à du C pourris. Je n'ai pas vu de DSL. Un moment, j'avais vu la liborc qui proposait un pseudo assembleur qui avait un type de base "tableau" pour générer l'assembleur qui allait bien pour chaque architecture (x86,…).
Il y a pourtant eu pas mal de recherche sur des langages pour la programmation scientifique (X10, Fortress…) dont les aspects que tu mentionnes (à part l'assembleur je pense) étaient des aspects importants.
Forteress a l'air abandonné, je vais regarder X10 qui à l'air d'être un truc HPC pour du multicpu surtout.
Michael Hicks et ses collaborateurs à l'université du Maryland ont travaillé depuis 2001 sur le problème de "Dynamic Software Update"
Je veux dire, une spécification, ce n'est pas juste décrire les limites du programmes ou ce qu'il fait. C'est aussi expliquer des choix de conception.
Je pense qu'il y un problème de vocabulaire. Une spécification vient avant le code, sinon on a un rapport d'architecture, ce qui est souvent plus utile qu'une spécification obsolète, on est d'accord.
Ce qui est vraiment utile, c'est un cahier des charges, justement sans aucune solution technique en tête, à base de scénario d'utilisateurs. C'est aux codeurs de trouver la meilleur technique. Même si les techniques agiles ont rendu l'absence de ce genre de document moins grave, la tache est toujours à faire.
C'est rigolo comme formule quand on pense que c'est dans le ferroviaire, l'aéronautique et le spatiale qu'on cherche le plus à faire du développement piloté par les modèles :D
Oui mais bon, on s'éloigne d'UML qui contient plusieurs centaines de concepts, c'est trop pour comprendre toutes les subtilités.
Du coup, on écrit des spécifications au travers de modèles que l'on transpose ensuite dans le langage cible.
Pas forcément. La mode est de décrire l'architecture, tu as en gros 3 graph : le fonctionnelle (l'ensemble des fonctions de ton code + ou -), le logiciel (en gros les paquets autour des fonctions, qui dialogue avec un Os, et gère la redondance, et les paquets réseau), et le hardware (cpu+réseau).
Une fois que tu as tout ça, tu peux générer tous les stub C de communication pour chacun des ordinateurs de ton architecture (startup code, les différents channels et leur config). Tu peux faire les tables de routages des switch (AFDX). Tu peux faire ta configuration vxworks pour chaque instance de l'OS (du xml). Tu peux générer la doc d'interface (API, …). Et si tu change les entrées/sorties, tu régénères tout d'un clic.
Le contenu des fonctions n'est pas détaillé, et doit être remplit par du "code classique".
C'est une approche puissante, car tu peux jeter l'un des 3 graphs, si tu change de hardware, ou si le hardware est imposé, mais le logiciel est nouveau.
Ils ne seraient pas fâchés que, par exemple, on puisse coder ces règles métier dans les types, je pense.
ça dépend de la complexité conceptuelle.
C’est un peu différent dans l’approche mais la méthode B permet d’en spécifier formellement dans l’invariant.
Je ne sais pas ou en est la méthode B en est mais j'ai entendu parlé dans mes études (y a plus de 15 ans…), et le seul fait d'arme était le code de la ligne 14, avec les preuves écrites à la main. Si on peut vérifier automatiquement la cohérence des invariants, c'est top.
Le truc pour ne pas avoir l’impression d’écrire plusieurs fois la même chose, c’est que la spec soit déclarative et de plus haut niveau que le code.
Oui, la mode est au modèle. Genre SysML qui sert à générer du code ou autre configuration. Écrire un gros méta-modèle cohérent est par contre, vite très compliqué. Les invariants des modèles UML sont codés avec de l'OCL, qui vérifie les propriétés du modèles, mais rien ne permet de tester la cohérence des règles entre elles.
Après avoir bosser quelques années la-dedans, je pense que le centre n'est pas le modèle, mais les transformations entre modèles. Quand tu as un modèle et que tu génères du code, un rapport, une config, ou que tu gères un diff, tu transformes toujours un modèle en un autre. Le Graal est la transformation bidirectionnelle partielle. Cela semble absurde, mais cela arrive tout le temps. En gros, il s'agit du même modèle sous-jacent, mais présenté sous des formes différentes qui suivent un standard précis (AADL, FACE, AUTOSAR,…), avec des outils différents pour travailler dessus. Des gens ont essayés de "mixer" ces modèles, ils ont eu des problèmes…
Ça te laisse complètement le choix de la manière de trier et ça va t’engueuler si t’as commenté l’appel au tri par erreur.
Je crois que les contrats de Smarteffel fonctionne ainsi. Cela reste de la vérification runtime, mais cela a de la valeur (= cela aide vraiment le codeur). Peut être qu'un code exécuté à la compilation pourrait garantir un certain nombre de propriété, mais les méta-compilateurs m'ont l'air bien compliqué à appréhender.
L’exécution à la compilation est une sorte de "propagation de constante" qui fonctionne aussi avec les containers, cela pourrait peut-faire le job. Existe-t-il un langage qui permet de faire ça ? Les templates de C++ ne sont pas une bonne réponse.
Ou alors que le département vente et le département fabrication utilisent pas la même notion de surface et que donc, les règles sont incohérentes et qu’il faut préciser le modèle.
Je suis récemment tombé sur la méthode DDD (https://en.wikipedia.org/wiki/Domain-driven_design), son idée principale est que se mettre d'accord entre service ne passe pas à l'échelle, et est totalement illusoire. L'idée est de créer un "Bounded context" dont l'intérieur est laissé à l’appréciation de chaque équipe, seul les interfaces doivent être spécifiées en commun. Cela rejoint les préoccupations de découpage du code des micro-services, si tu en as entendu parler.
Mais garde à l’esprit que c’est de la recherche en programmation qu’on parle ici. Il s’agit pas forcément d’avoir des choses utilisables dans la seconde.
Bien sur. Disons que j'ai souvent l'impression que la recherche s'intéresse beaucoup à des domaines qui n'intéressent pas les codeurs. Je me rappelle d'un texte d'un codeurs linux qui lisait des papiers de recherche sur un problème précis d'OS qui était majoritairement monocpu, alors que cela n'existe presque plus, et pour des résultats non reproductibles. Je vois la recherche énorme autour du GADT que peu de personnes comprennent, et de l'autre yacc semble abandonné alors que l'on ne peut pas l'utiliser, si il faut générer de vrai messages d'erreur précis et complet. Ocaml semble avoir compris la valeur d'avoir des messages d'erreurs lisible, mais par contre, il n'a toujours pas de moyen simple d'utiliser du multi-core ou les instructions SIMD.
Je n'ai pas vu non plus de recherche sur un langage pour la génération de code performant, c'est pourtant plus écologique d'avoir un code plus rapide. J'ai vu de la recherche sur la compilation du code C (la lib de transformation de boucle utilisé dans gcc), mais pas sur un langage qui permet au compilateur de mieux faire son boulot (unboxing facile, allocation mémoire minime, gestion des instructions assembleurs spécifiques facilités,…).
La recherche semble aussi focaliser sur la recherche du langage ultime. Mais comment fait-on la migration des centaines de millions de lignes de code existantes ? Comment assurer une transition progressive ? Par exemple comment changer "online" le schéma d'une base de données sans perdre de donnée et pouvoir retourner en arrière si besoin ? Le cas général est terriblement complexe. Comment découper un gros code monolithe pour changer la technologie sous-jacente ? C'est un travail d'ingénieur, mais un outil automatique serait un travail de recherche (plus ou moins comme coccinelle). La manipulation du code vu comme une énorme data structurée ne semble pas à la mode.
Dans les faits, la cohérence interne que tu peux vérifier est assez faible. Comme les gens détestent écrire les choses 2 fois, tu te retrouves à faire des calculs avec des données que tu as déjà, plutôt que vérifier que 2 valeurs sont cohérentes.
Pour l'exemple que tu donnes, cela tombe exactement dans ingénierie des modèles et le genre de petites règles que tu peux écrire. C'est très utile, tu peux augmenter très largement la productivité des utilisateurs. Mais tu ne vérifies pas de cohérence en soi, tu écris la règle elle-même. On est très loin d'une "vérification formelle".
La logique peut aussi vérifier la cohérence interne des connaissances des experts sur leur sujet.
Pour ça, il faut un "modèle du monde", ce qui n'existe jamais. C'est le boulot de dingue qui consiste à modéliser toutes les instructions assembleur dans compcert. Donc, non, tu n'as rien de facile sous la main pour confronter ce qu'écrit une personne du métier. Ce qui est typiquement fait, c'est d'utiliser des simulateurs maisons ou pas. Une équipe du métier conçoit un nouveau logiciel de pilote automatique, il va simuler des scénarios pour le valider. Il n'y a pas de règles statiques pour valider qu'il fait n'importe quoi dans certain cas. Dans le cas de ingénierie des modèles, on peut toujours écrire des règles qui permettent de vérifier certaine propriété, c'est forcément limité.
L'autre info c'est de voir le renforcement de alphagoZero en jouant contre lui-même en simulant des parties. Il devrait en théorie être possible de faire une IA qui apprend en utilisant un simulateur. C'est très théorique, je suis d'accord, mais cela serait la porte d'entré de l'IA dans l'ingénierie.
Le "modèle métier" se confronte toujours à une simulation. D'ailleurs, j'imagine qu'un jour les IA s'amuseront directement avec ce genre de simulateur.
Par exemple, le GC de go 1.9 fait maintenant des pauses maximum de 9 ms et utilise des threads. Mais il prends un peu plus de temps cpu pour vérifier la totalité de la RAM. Cela veut dire que pour un serveur chargé qui marche bien actuellement, le nombre de transaction par seconde risque de baisser, même si la latence moyenne pour chaque requête baisse.
Dans l'outil d'ET, il y a un prouveur qui marche assez bien (surtou avec les machines d'état). Je lui est déjà fait trouver des contres-exemples, mais personne ne l'achète ni ne s'en sert.
(si il y a un problème dans le code compilé, il se trouve déjà dans le code C).
Le bug peut être également dans le model. J'imagine que pour vérifier le comportement du C par rapport aux instructions assembleur, il faut modéliser ses instructions, ce qui n'est pas forcément simple.
si le code C est propre et garanti c'est bien, mais si le compilateur introduit un bug c'est un peu couillon, tu ne crois pas ?
J'adore ta condescendance, tu n'a aucune idée de comment le problème est géré actuellement dans de vrai projet, mais tu la ramènes quand même.
T'es sûr ? Tu faisais (ou fais) quoi comme travail chez Esterel ? Tu y appris quoi chez eux pour avoir écrit cela ?
J'ai entre autre appris, que les spécialistes métiers ne sont pas des informaticiens et encore moins des matheux. Et que pour décrire leur système, ils ne veulent surtout pas avoir à faire à ce genre de concept. Ils veulent pouvoir décrire des problème spécifique, les exemples de why3 dont parlait mon commentaire, n'ont aucun rapport avec des problèmes industriels.
T'as pas compris depuis le temps que ce tu qualifies de "industrielles", ce sont aussi des preuves de matheux ? ;-)
Tu n'as compris que la forme était le plus important pour travailler avec un tel outil, pour la compréhension même de ce qu'ils font d'un point de vue métier. C'est le sujet du journal.
Tu devrais tout de même jeter un œil à la vidéo de Xavier Leroy dont j'ai donné le lien au-dessus, il y parle pendant une vingtaine de minutes du milieu de l'avionique et de ses exigences de certification.
C'est sûr, ce n'est pas comme si je n'avais pas déjà certifié 2 ou 3 logiciels.
Dans un vieux journal, je parlais d'un langage que j'ai tenté décrire suivant la mode des langages systèmes, un truc qui ressemble a du xml mais avec une notion de nommage pour faire des graphs acycliques. Le truc est mal définit mais bon. Je me demandais si il n'était pas plus sage d'utiliser un truc costaux comme coq ou pourquoi pas why3 pour vérifier le fichier au lieu de le faire à la main. L'idée est d'avoir un langage structurel très user-friendly, dont la vérification est sous traité. L'idée est qu'un langage structurel est plus facile à vérifier.
compcert a été prouvé avec seulement ce bout de code ? Sans rien de manuel ?
Pour info, j'ai bossé 10 ans dans l'aéronautique, et l'usage des compilos C certifié c'était plutôt : "il faudrait prendre le temps de voir ce que cela donne". De plus la preuve formelle n'est pas encore reconnu dans les certifications aéronautique, en tout cas dans la do178b, je crois que cela bouge un peu dans la DO178C. Et encore, j'imagine que le prouveur lui-même devrait être certifié… Donc, on est pas prêt de voir un avion volé avec un tel code sans certification "papier" à coté. L'outil de ma boite utilisait l'outil de prover, mais c'était peu/aps utilisé car la norme n'en voulait pas.
Pour le reste des échanges, j'arrête là : je pisse dans un violon, tu ne connais pas grand chose aux sujets abordés mais tu parles quand même, ça me saoule.
Je crois que je peux te répondre la même chose, mais pas pour le même domaine.
Après, l'arrêt d'urgence fonctionne dans tous les cas reste assez vague comme contrat. On peut juste dire qu'il ne fera pas d'exception à l'exécution.
Tu crois que cela ressemble à quoi des vrai spec ? :) Je faisais un référence un peu trop subtile à un défaut d'un cruise control de toyota qui s'est fait démonté par un expert aéronautique pour un procès : il ne se désactivait pas si la pédale de frein était enfoncé…
En gros, cela voudrait dire que quelques soit les autres entrés, l'arrivé de l’arrêt d'urgence doit arrêter les moteurs.
Il ne faut pas se voiler la face quand même, il est peut être compliqué d'écrire les contrats de façon à ce qu'ils puissent être prouvés
Je sais bien, c'est d'autant plus difficile que le langage de la preuve est éloigné du langage métier, ou du langage de dev.
Concernant le code du drone, on dirait qu'il a seulement fait attention au overflow de calcul. Il faut que je relise moins en diagonal, je n'ai pas vu de propriété spécifiquement vérifier (genre l’arrêt d'urgence fonctionne dans tous les cas).
Les exemples de preuve sont très matheux. Cela ne ressemble pas à des preuves "industrielles" (à base de bout de spec, de bout d'exemple, de ne "plante jamais", a un temps d'exécution borné).
[^] # Re: Le cerveau n'est pas logique
Posté par Nicolas Boulay (site web personnel) . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 2.
Je suis ingénieur, et je n'avais pas entendu parler de Lambda avant de faire un dea d'info. C'est peut être un choix de mon école, mais je n'ai pas cette impression-là.
Autant le code python me parle (je ne connais pas du tout ce langage), autant le DSL ne me parle pas.
"La première sécurité est la liberté"
[^] # Re: Le cerveau n'est pas logique
Posté par Nicolas Boulay (site web personnel) . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 3.
Oui, mais il y a déjà de gros précédent. cf https://linuxfr.org/news/985-bugs-dans-le-noyau-linux par exemple.
Cela dépend ce que tu appelles "long terme", car tu peux passer un temps infini sur les faux positifs.
Je n'ai pas dis ça. J'ai dis qu'il fallait démontrer la supériorité d'une solution avant que celle-ci soit mis en œuvre.
C'est vrai pour n'importe quel développement. Et c'est exactement pour cette raisons que la plus part des outils libres sont directement utile à leurs auteurs, il est très rare d'avoir de bon outils libre, uniquement utile à d'autres.
Dans le cas du noyau, cela serait bosser dessus, dans le but de faire un outil utile pour vous, comme exemple de passage à l'échelle.
Il faut voir le gain de leur coté, qui n'est pas évident à moyen terme. Il faudrait peut être organiser une conférence sur les ponts entre recherche et l'open source, pour que les gens se rencontrent, pour montrer les téchno de recherche, montrer les interactions qui marchent.
"La première sécurité est la liberté"
[^] # Re: Le cerveau n'est pas logique
Posté par Nicolas Boulay (site web personnel) . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 5.
Concernant Astrée, j'imagine que c'est le genre d'outil qui peut généré un paquet de faux positif. Par exemple, si il détecte trop "simplement" la division. Sparse ne génère pas de faux positif si je me rappelle bien. Si il ne fonctionne bien qu'avec un code généré par SCADE, il y a une gros soucis (sachant que SCADE génère un C restreint ayant déjà beaucoup de bonnes propriétés).
Coverity propose une analyse de code open source. ( https://www.synopsys.com/software-integrity/resources/analyst-reports/open-source-software-scan-report.html ) Cela a été à la mode pendant un moment, puis les devs en ont eu marre des faux positifs dont la corrections pouvaient entrainée des problèmes subtiles (genre générateur de nombre aléatoire de Debian). Je ne connais pas la différence avec Astrée, mais Sparse a été développé ensuite.
Le milieu Open Source ne fonctionne pas comme ça. Celui qui apporte une nouvelle techno doit démontrer sa supériorité pour convaincre. Dire "venez avec moi, cela va être génial", cela fait 20 ans, que les développeurs Kernel l'entendent tous les jours. Et au dernière nouvelles les drivers Windows ne fonctionnent pas mieux que les drivers Linux.
En gros, c'est à la communauté de la recherche de prouver que leur approche est meilleur, si vous considérez que les dev sont bêtes parce qu'ils ne vous écoutent pas, c'est mal barré.
L'idée est sympa. J'imagine que les usagers de ce genre de DSL sont docteur en mathématique pour le calcul linéaire. Je ne vois pas qui d'autres pourraient s'en servir vu le formalisme mathématique retenu.
"La première sécurité est la liberté"
[^] # Re: pas compris
Posté par Nicolas Boulay (site web personnel) . En réponse à la dépêche Sortie de gfast-copy et de fast-copy sur www.open-source-projects.net. Évalué à 3.
Mes tests remontent à loin, mais typiquement dd était bien plus rapide que cp, je crois que j'avais surtout vu cela avec un raid 0, pour saturer la bande passante, il fallait des gros buffers.
"La première sécurité est la liberté"
[^] # Re: pas compris
Posté par Nicolas Boulay (site web personnel) . En réponse à la dépêche Sortie de gfast-copy et de fast-copy sur www.open-source-projects.net. Évalué à 3.
Pour avoir déjà fait le teste, j'imagine que c'est à cause de la taille de buffers. Lire puis écrire des morceaux de 16 Mo est beaucoup plus rapide qu'avec des morceaux de 8 Ko, surtout avec un HD.
"La première sécurité est la liberté"
[^] # Re: Le cerveau n'est pas logique
Posté par Nicolas Boulay (site web personnel) . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 4.
Un langage de haut niveau qui va vite.
En général, les langages "rapides" laissent tout le boulot au codeur (asm, c, c++, fortran). C++ avec les templates proposent un moyen de mettre la complexité en library avec le prix d'une grosse difficulté et des messages d'erreur abscons (et donc des bugs). Ce genre de langage trop bas niveau fournis un code rapide sur une machine, mais qui peut être plus lent sur un autre (intel vs amd ou vs ARM), multicore ou pas, SIMD ou pas.
Les compilateurs C/C++ vont très loin dans les optimisations mais sont bridés par le langage lui-même : gestion mémoire basique et explicite (il faut une grande rigueur pour gérer des pools de mémoires et éviter la fragmentation), layout mémoire fixée dans les structures (optimisation par structures de tableaux au lieu de tableaux de structures impossible), code IEE754 immodifiable (sans changer le résultat final), pointeur trop générique qui nécessite un gros travail "d'analyse de vie" pour éviter l'aliasing. Le SIMD est de mieux en mieux géré, mais le multicore reste complexe sauf avec openMP. Par contre utiliser directement les GPU restent encore très expérimental : il suffit de voir la tronche du code opencl avec des string à envoyer au driver de la carte graphique !
Rust permet une bien meilleur gestion mémoire, mais compile moins bien que gcc. "tensor flow" semble pouvoir décrire du code rapide pour plusieurs architectures très différentes, mais cela n'est pas un langage.
On peut aussi parler des optimisations par propagation de constantes qui se limitent aux littéraux basiques, mais pas au 'string' (utile pour les regexp ou même un code SQL embarqué), et je ne parle pas de container constant (AST, lecture de fichier externe, genre configuration en XML, image embarquées ou même un DSL quelconque).
"La première sécurité est la liberté"
[^] # Re: Le cerveau n'est pas logique
Posté par Nicolas Boulay (site web personnel) . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 4.
Je ne sais pas pourquoi j'avais raté ce message.
Je crois que tu te trompes sur les dev kernel. En sécurité, la plus part des bugs sont trouvé avec des fuzzers. Concernant l'analyse statique, il existe https://en.wikipedia.org/wiki/Sparse qui permet de vérifier des propriétés statiques (gestion de mutex, d'espace mémoire, etc…).
Les goroutines sont déjà un bon exemple. Tout ce qui est bas sur le passage de message simple ou les "grosses" boucles d'openMP.
Je ne comprends pas trop la question. gcc fait de la vectorisation automatique depuis un bail. Il a aussi proposé simplement des tableaux de 4 flottants ou 8 entiers avec les opérations qui correspondent directement sous forme de fonctions transformés ensuite en assembleur. Qu'est-ce qu'il y a de problématiques de donner accès à des fonctions qui correspondent aux instructions assembleurs ?
De plus, ocaml pourrait faire des map et fold sur des array de nombres, et proposer des versions vectorisés des opérations en question.
LLVM ? Dans quel domaine ? Je l'ai toujours vu comme un compilateur modulaire, mais qui n'arrive toujours au niveau de GCC en terme de perf. Pour les GPU, c'est openCL ou CUDA qui ressemble à du C pourris. Je n'ai pas vu de DSL. Un moment, j'avais vu la liborc qui proposait un pseudo assembleur qui avait un type de base "tableau" pour générer l'assembleur qui allait bien pour chaque architecture (x86,…).
Forteress a l'air abandonné, je vais regarder X10 qui à l'air d'être un truc HPC pour du multicpu surtout.
Vivement qu'un outil soit créé alors.
"La première sécurité est la liberté"
[^] # Re: la spec, c'est le code
Posté par Nicolas Boulay (site web personnel) . En réponse à la dépêche Développement très rapide d’applications libres : Extended Man/XML Frames. Évalué à 6.
Je pense qu'il y un problème de vocabulaire. Une spécification vient avant le code, sinon on a un rapport d'architecture, ce qui est souvent plus utile qu'une spécification obsolète, on est d'accord.
Ce qui est vraiment utile, c'est un cahier des charges, justement sans aucune solution technique en tête, à base de scénario d'utilisateurs. C'est aux codeurs de trouver la meilleur technique. Même si les techniques agiles ont rendu l'absence de ce genre de document moins grave, la tache est toujours à faire.
"La première sécurité est la liberté"
[^] # Re: la spec, c'est le code
Posté par Nicolas Boulay (site web personnel) . En réponse à la dépêche Développement très rapide d’applications libres : Extended Man/XML Frames. Évalué à 3.
Oui mais bon, on s'éloigne d'UML qui contient plusieurs centaines de concepts, c'est trop pour comprendre toutes les subtilités.
Pas forcément. La mode est de décrire l'architecture, tu as en gros 3 graph : le fonctionnelle (l'ensemble des fonctions de ton code + ou -), le logiciel (en gros les paquets autour des fonctions, qui dialogue avec un Os, et gère la redondance, et les paquets réseau), et le hardware (cpu+réseau).
Une fois que tu as tout ça, tu peux générer tous les stub C de communication pour chacun des ordinateurs de ton architecture (startup code, les différents channels et leur config). Tu peux faire les tables de routages des switch (AFDX). Tu peux faire ta configuration vxworks pour chaque instance de l'OS (du xml). Tu peux générer la doc d'interface (API, …). Et si tu change les entrées/sorties, tu régénères tout d'un clic.
Le contenu des fonctions n'est pas détaillé, et doit être remplit par du "code classique".
C'est une approche puissante, car tu peux jeter l'un des 3 graphs, si tu change de hardware, ou si le hardware est imposé, mais le logiciel est nouveau.
"La première sécurité est la liberté"
[^] # Re: Le cerveau n'est pas logique
Posté par Nicolas Boulay (site web personnel) . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 3.
ça dépend de la complexité conceptuelle.
Je ne sais pas ou en est la méthode B en est mais j'ai entendu parlé dans mes études (y a plus de 15 ans…), et le seul fait d'arme était le code de la ligne 14, avec les preuves écrites à la main. Si on peut vérifier automatiquement la cohérence des invariants, c'est top.
Oui, la mode est au modèle. Genre SysML qui sert à générer du code ou autre configuration. Écrire un gros méta-modèle cohérent est par contre, vite très compliqué. Les invariants des modèles UML sont codés avec de l'OCL, qui vérifie les propriétés du modèles, mais rien ne permet de tester la cohérence des règles entre elles.
Après avoir bosser quelques années la-dedans, je pense que le centre n'est pas le modèle, mais les transformations entre modèles. Quand tu as un modèle et que tu génères du code, un rapport, une config, ou que tu gères un diff, tu transformes toujours un modèle en un autre. Le Graal est la transformation bidirectionnelle partielle. Cela semble absurde, mais cela arrive tout le temps. En gros, il s'agit du même modèle sous-jacent, mais présenté sous des formes différentes qui suivent un standard précis (AADL, FACE, AUTOSAR,…), avec des outils différents pour travailler dessus. Des gens ont essayés de "mixer" ces modèles, ils ont eu des problèmes…
Je crois que les contrats de Smarteffel fonctionne ainsi. Cela reste de la vérification runtime, mais cela a de la valeur (= cela aide vraiment le codeur). Peut être qu'un code exécuté à la compilation pourrait garantir un certain nombre de propriété, mais les méta-compilateurs m'ont l'air bien compliqué à appréhender.
L’exécution à la compilation est une sorte de "propagation de constante" qui fonctionne aussi avec les containers, cela pourrait peut-faire le job. Existe-t-il un langage qui permet de faire ça ? Les templates de C++ ne sont pas une bonne réponse.
Je suis récemment tombé sur la méthode DDD (https://en.wikipedia.org/wiki/Domain-driven_design), son idée principale est que se mettre d'accord entre service ne passe pas à l'échelle, et est totalement illusoire. L'idée est de créer un "Bounded context" dont l'intérieur est laissé à l’appréciation de chaque équipe, seul les interfaces doivent être spécifiées en commun. Cela rejoint les préoccupations de découpage du code des micro-services, si tu en as entendu parler.
Bien sur. Disons que j'ai souvent l'impression que la recherche s'intéresse beaucoup à des domaines qui n'intéressent pas les codeurs. Je me rappelle d'un texte d'un codeurs linux qui lisait des papiers de recherche sur un problème précis d'OS qui était majoritairement monocpu, alors que cela n'existe presque plus, et pour des résultats non reproductibles. Je vois la recherche énorme autour du GADT que peu de personnes comprennent, et de l'autre yacc semble abandonné alors que l'on ne peut pas l'utiliser, si il faut générer de vrai messages d'erreur précis et complet. Ocaml semble avoir compris la valeur d'avoir des messages d'erreurs lisible, mais par contre, il n'a toujours pas de moyen simple d'utiliser du multi-core ou les instructions SIMD.
Je n'ai pas vu non plus de recherche sur un langage pour la génération de code performant, c'est pourtant plus écologique d'avoir un code plus rapide. J'ai vu de la recherche sur la compilation du code C (la lib de transformation de boucle utilisé dans gcc), mais pas sur un langage qui permet au compilateur de mieux faire son boulot (unboxing facile, allocation mémoire minime, gestion des instructions assembleurs spécifiques facilités,…).
La recherche semble aussi focaliser sur la recherche du langage ultime. Mais comment fait-on la migration des centaines de millions de lignes de code existantes ? Comment assurer une transition progressive ? Par exemple comment changer "online" le schéma d'une base de données sans perdre de donnée et pouvoir retourner en arrière si besoin ? Le cas général est terriblement complexe. Comment découper un gros code monolithe pour changer la technologie sous-jacente ? C'est un travail d'ingénieur, mais un outil automatique serait un travail de recherche (plus ou moins comme coccinelle). La manipulation du code vu comme une énorme data structurée ne semble pas à la mode.
"La première sécurité est la liberté"
[^] # Re: Le cerveau n'est pas logique
Posté par Nicolas Boulay (site web personnel) . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 3.
Dans les faits, la cohérence interne que tu peux vérifier est assez faible. Comme les gens détestent écrire les choses 2 fois, tu te retrouves à faire des calculs avec des données que tu as déjà, plutôt que vérifier que 2 valeurs sont cohérentes.
Pour l'exemple que tu donnes, cela tombe exactement dans ingénierie des modèles et le genre de petites règles que tu peux écrire. C'est très utile, tu peux augmenter très largement la productivité des utilisateurs. Mais tu ne vérifies pas de cohérence en soi, tu écris la règle elle-même. On est très loin d'une "vérification formelle".
"La première sécurité est la liberté"
[^] # Re: Le cerveau n'est pas logique
Posté par Nicolas Boulay (site web personnel) . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 3.
J'ai un peu trop divergé je suis d'accord.
Pour ça, il faut un "modèle du monde", ce qui n'existe jamais. C'est le boulot de dingue qui consiste à modéliser toutes les instructions assembleur dans compcert. Donc, non, tu n'as rien de facile sous la main pour confronter ce qu'écrit une personne du métier. Ce qui est typiquement fait, c'est d'utiliser des simulateurs maisons ou pas. Une équipe du métier conçoit un nouveau logiciel de pilote automatique, il va simuler des scénarios pour le valider. Il n'y a pas de règles statiques pour valider qu'il fait n'importe quoi dans certain cas. Dans le cas de ingénierie des modèles, on peut toujours écrire des règles qui permettent de vérifier certaine propriété, c'est forcément limité.
L'autre info c'est de voir le renforcement de alphagoZero en jouant contre lui-même en simulant des parties. Il devrait en théorie être possible de faire une IA qui apprend en utilisant un simulateur. C'est très théorique, je suis d'accord, mais cela serait la porte d'entré de l'IA dans l'ingénierie.
"La première sécurité est la liberté"
[^] # Re: Le cerveau n'est pas logique
Posté par Nicolas Boulay (site web personnel) . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 4.
Oui, c'est la merde pour ça. Je code avec gokit, et je souffre.
ex: https://github.com/go-kit/kit/blob/master/examples/shipping/routing/proxying.go
Il y a 36 wrappers à écrire pour masquer les interface{}.
"La première sécurité est la liberté"
[^] # Re: go 2.0
Posté par Nicolas Boulay (site web personnel) . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 3.
J'imagine qu'au final, leur GC est 20% plus lent que l'ancien. Je ne retrouve l'article sur le gc 1.9.
Ils en parlent un peu ici : https://golang.org/doc/go1.9
"La première sécurité est la liberté"
[^] # Re: Le cerveau n'est pas logique
Posté par Nicolas Boulay (site web personnel) . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 3.
Le "modèle métier" se confronte toujours à une simulation. D'ailleurs, j'imagine qu'un jour les IA s'amuseront directement avec ce genre de simulateur.
"La première sécurité est la liberté"
[^] # Re: go 2.0
Posté par Nicolas Boulay (site web personnel) . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 3.
Par exemple, le GC de go 1.9 fait maintenant des pauses maximum de 9 ms et utilise des threads. Mais il prends un peu plus de temps cpu pour vérifier la totalité de la RAM. Cela veut dire que pour un serveur chargé qui marche bien actuellement, le nombre de transaction par seconde risque de baisser, même si la latence moyenne pour chaque requête baisse.
"La première sécurité est la liberté"
[^] # Re: Le cerveau n'est pas logique
Posté par Nicolas Boulay (site web personnel) . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 3.
Je pense que pour vraiment se passer de interface{}, il faudrait de l'inférence de type à la place, ce qui n'est pas gagné.
"La première sécurité est la liberté"
[^] # Re: Le cerveau n'est pas logique
Posté par Nicolas Boulay (site web personnel) . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 4.
Dans l'outil d'ET, il y a un prouveur qui marche assez bien (surtou avec les machines d'état). Je lui est déjà fait trouver des contres-exemples, mais personne ne l'achète ni ne s'en sert.
"La première sécurité est la liberté"
# Question bête
Posté par Nicolas Boulay (site web personnel) . En réponse à la dépêche LibraZiK : nouveautés des six derniers mois. Évalué à 9.
Pourquoi faire une Debian dédié plutôt qu'un metapackage qui regroupe tous vos choix ?
"La première sécurité est la liberté"
[^] # Re: Le cerveau n'est pas logique
Posté par Nicolas Boulay (site web personnel) . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 1.
Le bug peut être également dans le model. J'imagine que pour vérifier le comportement du C par rapport aux instructions assembleur, il faut modéliser ses instructions, ce qui n'est pas forcément simple.
J'adore ta condescendance, tu n'a aucune idée de comment le problème est géré actuellement dans de vrai projet, mais tu la ramènes quand même.
J'ai entre autre appris, que les spécialistes métiers ne sont pas des informaticiens et encore moins des matheux. Et que pour décrire leur système, ils ne veulent surtout pas avoir à faire à ce genre de concept. Ils veulent pouvoir décrire des problème spécifique, les exemples de why3 dont parlait mon commentaire, n'ont aucun rapport avec des problèmes industriels.
Tu n'as compris que la forme était le plus important pour travailler avec un tel outil, pour la compréhension même de ce qu'ils font d'un point de vue métier. C'est le sujet du journal.
C'est sûr, ce n'est pas comme si je n'avais pas déjà certifié 2 ou 3 logiciels.
"La première sécurité est la liberté"
[^] # Re: Le cerveau n'est pas logique
Posté par Nicolas Boulay (site web personnel) . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 3.
Dans un vieux journal, je parlais d'un langage que j'ai tenté décrire suivant la mode des langages systèmes, un truc qui ressemble a du xml mais avec une notion de nommage pour faire des graphs acycliques. Le truc est mal définit mais bon. Je me demandais si il n'était pas plus sage d'utiliser un truc costaux comme coq ou pourquoi pas why3 pour vérifier le fichier au lieu de le faire à la main. L'idée est d'avoir un langage structurel très user-friendly, dont la vérification est sous traité. L'idée est qu'un langage structurel est plus facile à vérifier.
"La première sécurité est la liberté"
[^] # Re: Le cerveau n'est pas logique
Posté par Nicolas Boulay (site web personnel) . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 3.
compcert a été prouvé avec seulement ce bout de code ? Sans rien de manuel ?
Pour info, j'ai bossé 10 ans dans l'aéronautique, et l'usage des compilos C certifié c'était plutôt : "il faudrait prendre le temps de voir ce que cela donne". De plus la preuve formelle n'est pas encore reconnu dans les certifications aéronautique, en tout cas dans la do178b, je crois que cela bouge un peu dans la DO178C. Et encore, j'imagine que le prouveur lui-même devrait être certifié… Donc, on est pas prêt de voir un avion volé avec un tel code sans certification "papier" à coté. L'outil de ma boite utilisait l'outil de prover, mais c'était peu/aps utilisé car la norme n'en voulait pas.
Je crois que je peux te répondre la même chose, mais pas pour le même domaine.
"La première sécurité est la liberté"
[^] # Re: Le cerveau n'est pas logique
Posté par Nicolas Boulay (site web personnel) . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 3.
Tu crois que cela ressemble à quoi des vrai spec ? :) Je faisais un référence un peu trop subtile à un défaut d'un cruise control de toyota qui s'est fait démonté par un expert aéronautique pour un procès : il ne se désactivait pas si la pédale de frein était enfoncé…
En gros, cela voudrait dire que quelques soit les autres entrés, l'arrivé de l’arrêt d'urgence doit arrêter les moteurs.
Je sais bien, c'est d'autant plus difficile que le langage de la preuve est éloigné du langage métier, ou du langage de dev.
"La première sécurité est la liberté"
[^] # Re: Le cerveau n'est pas logique
Posté par Nicolas Boulay (site web personnel) . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 3. Dernière modification le 20 octobre 2017 à 15:38.
Je parlais du site web de why3. ( http://toccata.lri.fr/gallery/why3.en.html )
Concernant le code du drone, on dirait qu'il a seulement fait attention au overflow de calcul. Il faut que je relise moins en diagonal, je n'ai pas vu de propriété spécifiquement vérifier (genre l’arrêt d'urgence fonctionne dans tous les cas).
http://blog.adacore.com/how-to-prevent-drone-crashes-using-spark regardes le 2ième commentaires qui signale tout un tas de problème dans les specs du truc.
"La première sécurité est la liberté"
[^] # Re: Le cerveau n'est pas logique
Posté par Nicolas Boulay (site web personnel) . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 3. Dernière modification le 20 octobre 2017 à 14:55.
Les exemples de preuve sont très matheux. Cela ne ressemble pas à des preuves "industrielles" (à base de bout de spec, de bout d'exemple, de ne "plante jamais", a un temps d'exécution borné).
"La première sécurité est la liberté"