Nicolas Boulay a écrit 15824 commentaires

Un CortexA8 par rapport à un atom peut-être. Pour les autres, c'est sûr que non. (core out of order etc... )

"La première sécurité est la liberté"

euh... l'omap3430 c'est l'équivalent fonctionnelle de atom+chipset avec carte 3D+accélérateur de décompression hardware+accélérateur de crypto.

Le SoC inclue bien plus de chose que l'atom seul.

"La première sécurité est la liberté"

Pour le dsp, c'est moyennement gênant, TI fournit des codecs mpeg4 avec la puce. Pour la carte graphique malheureusement...

Peut-être que la 3D du snapdragon de qualcomm est plus ouverte. La pversion la plus puissante a une puce avec l'équivalent de 2 cortex A8 à 1.5ghz avec une puissance de calcul en SIMD double (Qualcomm a fait sa propre version de l'architecture ARMV7).
http://www.hardmicro-fr.net/news-article.storyid-3422.htm

A priori, le core 3D est en provenance d'ati, donc avec potentiellement un driver libre.
http://www.netbooktech.com/tag/snapdragon-qsd8672/

"La première sécurité est la liberté"

Il y en a avec plus de 5h d'autonomie réel mais il dépasse le kg.

La qualité du clavier va rendre le produit intéressant ou pas, j'aurais aimer un écran 10" en 720p mais si le clavier fait mal au doigts c'est encore pire.

"La première sécurité est la liberté"

C'est juste que je trouve mon eeetop (atom) trop lent à mon gout et que le cpu de l'OMAP est entre 2 et 3 fois plus lent.

"La première sécurité est la liberté"

l'OMAP3430 doit consommer 1 ou 2 W en conso max à 600Mhz. Tu peux même te passer de radiateur.

Le cortex A8 a un double pipeline avec exécution dans l'ordre comme le Pentium I. Cela donne une idée des perfs max.

"La première sécurité est la liberté"

Le cpu est du niveau pentium I à 500 mhz aider par une carte 3D et un dsp pour la decompression de média.

Donc pour regarder un film pas de souci mais pour naviguer sur internet, j'espère que Fennec est bien optimisé.

"La première sécurité est la liberté"

Une liste libriste qui fait la part belle à la compétence de chaque potentiel élue ? (par rapport au autre liste ?)

"La première sécurité est la liberté"

tu ne démontres ni n'explique rien en l'occurrence.

"La première sécurité est la liberté"

Si t'as pas d'OS temps réel, t'as perdu.

Tu as perdu quoi ? Dire que tu compares une méthode formelle (style celle de absint qui utilise un modèle cpu+mémoire) avec la simple mesure de quelques vecteur d'entrés !

Personne n'a dit que les tests offraient de garanties.

Pourquoi tu sous entends que la solution formelle serait moins bonne alors ?

Un valideur formelle ne valide pas les specs, d'où l'intérêt de mon exemple qui n'a strictement rien de fallacieux, et qui au contraire me paraît très réaliste.

Bien sur qu'elle valide les specs ! En rédigeant la spec formelle tu identifies immédiatement tous les manques et précision à demander à ton client !

"La première sécurité est la liberté"

Un outil formel pour le faire permettrait de te trouver le ou les vecteurs d'entrées correspondant à ton pire cas et mesurer ensuite le temps d'exécution. Tout cela pourrait être automatique.

"La première sécurité est la liberté"

Il n'y a pas à tortiller, si la "spec" est "le programme termine sur l'entrée 16 en temps 64", c'est trivial, si c'est "le programme calcule factorielle", c'est indécidable. Les specs que tu veux vérifier, c'est parce qu'elles sont non triviales,

Non, c'est aussi parce que le programme est gros.

Tu veux vérifier que tu ne t'es pas planté dans la copie d'une équation, dans la recopie d'une constante, que tu n'as pas de cas ou tu core dump.

"le programme calcule factorielle"

Sauf que ta spec ne dira pas ça. Il dira factoriel selon l'algo bidule précis à 10^-14 en code double flottant. De toute façon, je vois mal factoriel comme étant une fonction de base de ton logiciel de preuve.

La "preuve" sera l'équivalence à x^-14 prêt entre l'équation mathématique de la spec et ton code (souvent des développements limité).

Mais pour le cas de factoriel, le test tel que définit par la DO-178B demande de couvrir les classes d'équivalences, ce qui va se réduire à tester un nombre négatif, zéro, un nombre positif, voir les nombres max et min du range spécifié, et le range+1 pour voir que cela ne plante pas. 7 tests en tout pour vérifier l'équivalence à 10^-14 prêt et pour avoir la certif de ton avion.

Si tu fais quelques milliers de test en random() en plus, c'est encore mieux (mais la certif s'en fout). Les partitions par classe d'équivalence fonctionnent en test boite blanche quand tu connais la tête du code et que tu voix bien qu'il n'y a pas de branchement. De toute façon, à l'exécution du test, tu vérifies la couverture de code.

Certe tu n'auras pas prouver l'équivalence entre spec et code mais tu auras une grande confiance, ce qui est le principale.

"La première sécurité est la liberté"

Et maintenant que la société est en faillite, vous allez faire comment ?

"La première sécurité est la liberté"

Je rajouterai l'équivalence des programmes, c'est énorme pour l'optimisation.

Je ne pense pas que l'on est besoin que toutes assertions soit prouvable, j'ai peur que cela sois compliqué. Je préfère que des assertions simples (division par zéro) puisse être traité sur le programme en entier. Générer un contre exemple, c'est indispensable tellement, c'est utile.

La génération automatique de pattern de teste pour passer les assertion en dynamique pour faire la couverture de code est très utile (pour avoir le pire cas en timing aussi). Les stratégies de tests pour trouver les vecteurs sont parfaitement automatisable (gestion des classes d'équivalence, branches, valeur singulière, etc..)

"La première sécurité est la liberté"

J'ai du me tromper alors. Je parles évidement de la taille de ce que fournis l'humain pour faire la preuve.

Ensuite, il faut aussi prouver le prouver, ce qui n'est pas gagné.

"La première sécurité est la liberté"

Ma question était de savoir si il existait d'autres méthodes.

J'imagine que écrire le code puis écrire sa preuve devrait aussi suffire.

Mais d'après les exemples de "Why" pour un code de 20 lignes, il y en a 1000 de preuves. On est loin d'être utilisable.

"La première sécurité est la liberté"

Si la propriété est une spécification (totale) alors spec est déjà en quelque sorte le programme en lui-même. Si cette spec était "exécutée", par une machine, son comportement serait le même que celui du programme à vérifier.

Je comprends bien. D'où la recherche de l'écriture de spec exécutable (est ce que tu connais Scade ? c'est l'argument des LLR executable pour le vendre).

Mais il existe toujours un moment il faut spécifier ce que tu mets dans la spec. Il y a toujours une spec de spec en cascade.

Donc, il y a toujours à un moment l'écriture de quelques choses de non ambigüe et l'écriture du code final. Ce qui revient à avoir 2 "modèles", non ?

"La première sécurité est la liberté"

tu travaillais ou avec Esterel ? Chez TI ?

"La première sécurité est la liberté"

Cela revient à écrire 2 fois le même programme dans des paradigmes différents et de vérifier qu'ils produisent les mêmes résultats...

Mais lors d'une recherche de meilleur qualité, il n'y a pas d'autres solutions non ?

"La première sécurité est la liberté"

Tu parles quand même dans un cadre très général bien loin des cas pratiques.

- de déterminer si ce programme fait la même chose qu'un autre programme

Dans le cas général.

Parce que c'est justement dans ce domaine là que les prouveurs formelles sont utilisés industriellement à grande échelle. On appelle cela les "equivalence checker". C'est un outil du domaine de l'EDA qui permet de s'assurer qu'une mer de portes générées par un synthétiseur est équivalent au code source HDL.

- et par extension de déterminer si ce programme est conforme à sa spécification

Il faut encore savoir ce qu'est une spec. Souvent, c'est super flou et pas clair. Le client veut que le produit réponde à son problème et ne plante pas, par contre, il ne sait pas forcément bien le définir. C'est plus un problème d'ingénierie logiciel que de preuves mathématiques.

"La première sécurité est la liberté"

Tu pourrais nous expliquer le genre de code qui est fournis à un assistant de preuve, par exemple, en utilisant du pseudo code ?

Dans le milieu de l'aéronautique, il est souvent question de comparaison de modèles et de confrontation d'interprétation de spec entre 2 équipes utilisant des outils différents. Donc, on a une équipe qui développe le programme et l'autre un modèle sous une autre forme. On compare ensuite les résultats de tests définit par avance par l'équipe de test (mais qui pourrait être généré automatiquement par classe d'équivalence des entrées et couverture de code)

Le but serait ici de facilité la vie de la deuxième équipe.

"La première sécurité est la liberté"

D'ailleurs, y'a ESL Technology qui est à racheter (ex-Esterel EDA), la boite qui a repris le langage Esterel. 10 ans de R&D. Elle est en faillite suite à l'arrêt de la moitié des contrats de prestation du principale client TI.

L'intégration de le preuve est assez sympa. Le langage lui-même fait passer le VHDL pour de l'assembleur par rapport à Java.

"La première sécurité est la liberté"

Dans ce cas là, c'est l'outil qui l'a fait à ta place /o\

"La première sécurité est la liberté"

Ce que tu dis, c'est justement que c'est très précieux, car cela trouve jusqu'au manquement de la spec. Cela repousse le travail idiot du test systématique par une recherche d'une meilleur cohérence de spec et d'un test de haut niveau.

Personne n'a jamais dit qu'un ordinateur ferait tout le boulot à ta place.

Sinon dans les prouveurs "100% automatique", il recherche si il existe les conditions de plantage du code C, comme les "array out of bound", les division par zéro. Le but est ici de prouver que le code ne plante pas, pas qu'il correspond à la spec. C'est déjà pas mal car on ne demande rien aux codeurs "en plus".

D'une manière général, la preuve, c'est génial, sauf que cela passe rarement à l'échelle (pb numero 1) et "les gens" ne font pas confiance à un "toujours vrai" rendu par un outil, par contre, ils aiment bien qu'on trouve leur bug.

"La première sécurité est la liberté"

Vu que DirectFB ne sait que gérer des "layers", cela n'a pas franchement d'intérêt sauf si il sait aussi gérer le reste de l'interface.

"La première sécurité est la liberté"