note : on peut faire du dynamique qui pointe sur du statique ;)
Dans ce cas tu perds énormément en perf.
Pour te donner une idée, bench une page static .html et la même page .php (sans php dedans). La page .php sera bien plus lente (passage dans l'interpréteur php, par rapport à un transfert de fichier par sendfile() en zéro copy ).
Oui et non. Les prédica d'ARM repose sur des valeurs de statut de l'ALU qui fait une dépendance de flot forte (dépendance Read after write). A coté de ça, tu as la prédiction de branchement de l'intel qui est très efficace.
On s'en fout un peu de l'instruction set. Celui-ci a de l'influence sur la taille du cache instruction, un peu sur l'efficacité des instructions mais il n'y a rien de très innovant entre x86 et arm. L'opposition RISC/CISC complexifie l'entrée de pipeline. Mais sa fin est tout aussi dimentionante pour les performances.
Les 2 cpus ont 2 pipelines entier avec exécution dans l'ordre avec une fpu et une unité vectoriel.
- un CPU ARM, alors que la principale critique faite sur les Netbooks est qu'ils ne sont pas assez puissants, et il me semble que les Intel Atom sont bien plus puissant que les ARMs.
C'est vrai pour les applications "génériques" (en gros navigateur web et OOo). Par contre, il dispose de pas mal d'accélérateur dont un DSP pour faire du 720P (est-ce que l'atom peut faire de la HD, j'en doute). Il dispose aussi d'accélérateur de crypto (AES, random,...). Et un core 3D (certe complètement fermé).
donc moins de paquets disponibles
Oui, mais vu la différence de puissance, tu ne peux pas vraiment utiliser les mêmes que sur PC.
Je ne décrit juste que la méthode expérimental [[Méthode_scientifique]]
wikipedia:
La méthode expérimentale est souvent constituée des 8 étapes suivantes :
1. Préciser la question
2. Recueillir des informations et des ressources (observer)
3. Forme des hypothèses
4. Effectuer l'expérience et de recueillir des données
5. Analyser les données
6. Interpréter les données et tirer des conclusions qui serviront pour valider ou infirmer les hypothèses et peut-être aussi comme de point de départ pour de nouvelles hypothèses
7. Publier les résultats
8. Reproduire les expériences (souvent fait par d'autres scientifiques)
Il s'agit évidement de théorie sur le monde réel, pas les mathématiques.
C'est une vue de l'esprit pour ne pas dire que le cortex A8 est un processeur à 2 pipelines in-order avec fpu et unité vectoriel de 64 bits qui tourne à 600 Mhz mais avec peu de cache et une bus mémoire LPDDR de 32 bits qu'il partage avec tous ses périphériques dont la carte 3D.
Même avec un OS, je ne vois pas ce qui empêche de définir des contraintes temps réel mou.
Tu dois pouvoir écrire un modèle d'OS du style, tu as 90 % de chance de te prendre une IT qui dure 10 us, 9% quel dure 100us, 1% 800 µs. Idem pour bon nombre des appels systèmes.
Tu perds beaucoup en précision mais cela reste utile. On peut faire plein de choses avec des probabilités.
Ca me paraît borderline et plus du domaine de la vérification mathématique, on se rapproche du test traditionnel. On arrive également à produire des tests de couverture de code automatiquement sans passer par un vérificateur formel.
Tu fais une différence entre formelle et mathématique ?
Sinon, pour l'augmentation de taux de couverture, il y a aussi des système utilisant de l'aléatoire, mais la plus part sont des systèmes formels.
Oué donc arrache toi pour ton application qui tourne sous Windows ou Ubuntu.
Un futur codeur Scade ;) Je peux te dire que la verif formel de scade débute.
Et je peux te dire que dans la vrai vie, j'ai pas eu vent de comment cela passe; je le fais tous les jours. Je dois respecté la DO178B (celle d'aujourd'hui, en 1970, elle n'existait pas).
Dans ce que tu décris, je ne vois rien de différent avec un test utilisant un "golden model", que l'on utilise en ce moment.
Si tu as une autre méthode moins chiante, je suis preneur.
Si c'est pas prouvé, il te donne un contre exemple immédiatement, donc tu corriges très rapidement ton appli pas besoin de la suite de non régression "overnight". C'est sans doute la partie la plus utile.
Si c'est prouvé bingo. Si l'assertion est correctement exprimé. C'est en fait moins utile que le cas précédent.
Si il n'y arrive pas, le prouveur d'Esterel te donne une profondeur temporel genre 10 coups d'horloges, si on connait la structure de son code (pas de mémoire à plus de 10 coups en arrière), on peut être confiant.
Dans la vérification formel, j'inclus aussi la génération automatique de vecteurs d'entrée pour augmenter le taux de couverture. Il n'y a plus qu'à avoir des sorties de références ou des assertions à vérifier.
Le static timing analyser de temps en pire cas permet de te trouver ton pire cas en timing. (il faut par contre un beau modèle de ton systèm)
Et bossant pour une boite qui vend un "langage formel" pour ce genre d'application, je peux te dire que tout ce qui est vérification formel est loin d'être la règle, et est encore moins reconnu (sauf peut-être dans le ferroviaire et encore).
"La spécialités de mes formateurs en test de logiciels" et ils forment à quel genre de technique ?
J'ai l'impression qu'il y une différence entre les pratiques habituelles pour le développement live critical et ce que tu crois l'être... vu depuis un labo.
Les tests de performance et d'endurance vont te permettre d'obtenir un degré de confiance en mesurant le temps de réponse.
Si tu joues le jeu de la vérification formelle, tu démonteras juste que ce n'est pas prouvable. T'es bien avancé.
Renseignes toi mieux. Ce genre d'outil existe déjà et fonctionne.
En général, tu fais un test pour couvrir un point de spécification. Donc, tu trouves à la main des vecteurs d'entrée, tu évalue ce que doivent être tes sorties et tu compares avec la sortie de ton code.
Dans la preuve formel, tu ajoutes une assertion qui correspond à un point de spécification. La vérification formel balaye toutes les possibilités d'entrée à la recherche d'un contre exemple.
Dans le cas du test, tu es limité par les vecteurs d'entrée que tu trouves à la main alors qu'avec un moteur de preuve, tu as l'exhaustivité.
Tu as perdu la possibilité de prouver quoique ce soit, puisque sur un OS non temps-réel tu n'as strictement aucune garantie sur la disponibilité des ressources.
Quelle différence entre une vérification formelle et un test, ici ?
C'est pas parcque tu as réussi à formaliser les specs que les specs sont valides.
C'est évident ça. mais dans ce cas, on parle de valider la spec par celle au dessus. Au moins on peut trouver les incohérences.
Et là si tu fais pas des tests d'ergonomie...
Cela veut dire que tu codes en suivant une spec mais que tu tests en suivant autre choses ? Je te souhaite bien du courage pour expliquer d'où vient le problème à ton client ! (sa spec et pas ton code)
'est con mais c'est comme ca dans la vraie vie, souvent tu te buttes face à un client qui ne veut pas répondre (pas le temps ou ne sais pas trancher) et tu dois faire des choix.
Je commençais à comprendre que ton client ne faisait pas des avions :)
[^] # Re: Trop beau pour être vrai
Posté par Nicolas Boulay (site web personnel) . En réponse au journal La société Always Innovating porte bien son nom!. Évalué à 1.
"La première sécurité est la liberté"
[^] # Re: merci bcp !
Posté par Nicolas Boulay (site web personnel) . En réponse au message besoin d'un tutoriel Ada pour newbie total de 15 ans. Évalué à 2.
http://www.unixgarden.com/
"La première sécurité est la liberté"
[^] # Re: Trop beau pour être vrai
Posté par Nicolas Boulay (site web personnel) . En réponse au journal La société Always Innovating porte bien son nom!. Évalué à 2.
Dans ce cas tu perds énormément en perf.
Pour te donner une idée, bench une page static .html et la même page .php (sans php dedans). La page .php sera bien plus lente (passage dans l'interpréteur php, par rapport à un transfert de fichier par sendfile() en zéro copy ).
"La première sécurité est la liberté"
[^] # Re: "tueur de netbook ?"
Posté par Nicolas Boulay (site web personnel) . En réponse à la dépêche Touch Book : le tueur de netbook ?. Évalué à 4.
"La première sécurité est la liberté"
[^] # Re: "tueur de netbook ?"
Posté par Nicolas Boulay (site web personnel) . En réponse à la dépêche Touch Book : le tueur de netbook ?. Évalué à 5.
"La première sécurité est la liberté"
[^] # Re: "tueur de netbook ?"
Posté par Nicolas Boulay (site web personnel) . En réponse à la dépêche Touch Book : le tueur de netbook ?. Évalué à 2.
Les 2 cpus ont 2 pipelines entier avec exécution dans l'ordre avec une fpu et une unité vectoriel.
Bref, c'est très comparable.
"La première sécurité est la liberté"
[^] # Re: "tueur de netbook ?"
Posté par Nicolas Boulay (site web personnel) . En réponse à la dépêche Touch Book : le tueur de netbook ?. Évalué à 2.
"La première sécurité est la liberté"
[^] # Re: "tueur de netbook ?"
Posté par Nicolas Boulay (site web personnel) . En réponse à la dépêche Touch Book : le tueur de netbook ?. Évalué à 5.
C'est vrai pour les applications "génériques" (en gros navigateur web et OOo). Par contre, il dispose de pas mal d'accélérateur dont un DSP pour faire du 720P (est-ce que l'atom peut faire de la HD, j'en doute). Il dispose aussi d'accélérateur de crypto (AES, random,...). Et un core 3D (certe complètement fermé).
donc moins de paquets disponibles
Oui, mais vu la différence de puissance, tu ne peux pas vraiment utiliser les mêmes que sur PC.
"La première sécurité est la liberté"
[^] # Re: prouveur automatique/assistant de preuve
Posté par Nicolas Boulay (site web personnel) . En réponse au journal La preuve de programme : où en est-on ?. Évalué à 2.
wikipedia:
La méthode expérimentale est souvent constituée des 8 étapes suivantes :
1. Préciser la question
2. Recueillir des informations et des ressources (observer)
3. Forme des hypothèses
4. Effectuer l'expérience et de recueillir des données
5. Analyser les données
6. Interpréter les données et tirer des conclusions qui serviront pour valider ou infirmer les hypothèses et peut-être aussi comme de point de départ pour de nouvelles hypothèses
7. Publier les résultats
8. Reproduire les expériences (souvent fait par d'autres scientifiques)
Il s'agit évidement de théorie sur le monde réel, pas les mathématiques.
"La première sécurité est la liberté"
[^] # Re: Trop beau pour être vrai
Posté par Nicolas Boulay (site web personnel) . En réponse au journal La société Always Innovating porte bien son nom!. Évalué à 3.
C'était plus court.
"La première sécurité est la liberté"
[^] # Re: Se passer des tests ...
Posté par Nicolas Boulay (site web personnel) . En réponse au journal La preuve de programme : où en est-on ?. Évalué à 2.
"La première sécurité est la liberté"
[^] # Re: prouveur automatique/assistant de preuve
Posté par Nicolas Boulay (site web personnel) . En réponse au journal La preuve de programme : où en est-on ?. Évalué à 2.
"La première sécurité est la liberté"
[^] # Re: Se passer des tests ...
Posté par Nicolas Boulay (site web personnel) . En réponse au journal La preuve de programme : où en est-on ?. Évalué à 2.
Tu dois pouvoir écrire un modèle d'OS du style, tu as 90 % de chance de te prendre une IT qui dure 10 us, 9% quel dure 100us, 1% 800 µs. Idem pour bon nombre des appels systèmes.
Tu perds beaucoup en précision mais cela reste utile. On peut faire plein de choses avec des probabilités.
"La première sécurité est la liberté"
[^] # Re: Se passer des tests ...
Posté par Nicolas Boulay (site web personnel) . En réponse au journal La preuve de programme : où en est-on ?. Évalué à 2.
Tu fais une différence entre formelle et mathématique ?
Sinon, pour l'augmentation de taux de couverture, il y a aussi des système utilisant de l'aléatoire, mais la plus part sont des systèmes formels.
Oué donc arrache toi pour ton application qui tourne sous Windows ou Ubuntu.
Par system, je parlais de HW.
"La première sécurité est la liberté"
[^] # Re: prouveur automatique/assistant de preuve
Posté par Nicolas Boulay (site web personnel) . En réponse au journal La preuve de programme : où en est-on ?. Évalué à 2.
"La première sécurité est la liberté"
[^] # Re: Se passer des tests ...
Posté par Nicolas Boulay (site web personnel) . En réponse au journal La preuve de programme : où en est-on ?. Évalué à 3.
Et je peux te dire que dans la vrai vie, j'ai pas eu vent de comment cela passe; je le fais tous les jours. Je dois respecté la DO178B (celle d'aujourd'hui, en 1970, elle n'existait pas).
Dans ce que tu décris, je ne vois rien de différent avec un test utilisant un "golden model", que l'on utilise en ce moment.
Si tu as une autre méthode moins chiante, je suis preneur.
"La première sécurité est la liberté"
[^] # Re: Se passer des tests ...
Posté par Nicolas Boulay (site web personnel) . En réponse au journal La preuve de programme : où en est-on ?. Évalué à 2.
Ben non. Cela ne marche pas que comme ça.
Si c'est pas prouvé, il te donne un contre exemple immédiatement, donc tu corriges très rapidement ton appli pas besoin de la suite de non régression "overnight". C'est sans doute la partie la plus utile.
Si c'est prouvé bingo. Si l'assertion est correctement exprimé. C'est en fait moins utile que le cas précédent.
Si il n'y arrive pas, le prouveur d'Esterel te donne une profondeur temporel genre 10 coups d'horloges, si on connait la structure de son code (pas de mémoire à plus de 10 coups en arrière), on peut être confiant.
Dans la vérification formel, j'inclus aussi la génération automatique de vecteurs d'entrée pour augmenter le taux de couverture. Il n'y a plus qu'à avoir des sorties de références ou des assertions à vérifier.
Le static timing analyser de temps en pire cas permet de te trouver ton pire cas en timing. (il faut par contre un beau modèle de ton systèm)
J'ai dû oublier d'autres types de vérification.
"La première sécurité est la liberté"
[^] # Re: ça pue c'est pas libre
Posté par Nicolas Boulay (site web personnel) . En réponse au journal La société Always Innovating porte bien son nom!. Évalué à 2.
C'est pas gagné avec un cortex A8, celui-ci dispose d'une fpu et d'instructions SIMD. Je ne suis pas sur qu'il soit moins efficace que le dsp.
Les PowerVR font un carton en ce moment dans l'embarqué
vivement opengraphics :)
"La première sécurité est la liberté"
[^] # Re: Domotique
Posté par Nicolas Boulay (site web personnel) . En réponse au journal La société Always Innovating porte bien son nom!. Évalué à 3.
J'ai toujours voulu un moyen simple (un téléphone portable ?) pour tracer les prix d'un produit entre différent magasin.
"La première sécurité est la liberté"
[^] # Re: Se passer des tests ...
Posté par Nicolas Boulay (site web personnel) . En réponse au journal La preuve de programme : où en est-on ?. Évalué à 2.
Et bossant pour une boite qui vend un "langage formel" pour ce genre d'application, je peux te dire que tout ce qui est vérification formel est loin d'être la règle, et est encore moins reconnu (sauf peut-être dans le ferroviaire et encore).
"La spécialités de mes formateurs en test de logiciels" et ils forment à quel genre de technique ?
"La première sécurité est la liberté"
[^] # Re: Se passer des tests ...
Posté par Nicolas Boulay (site web personnel) . En réponse au journal La preuve de programme : où en est-on ?. Évalué à 1.
"La première sécurité est la liberté"
[^] # Re: Se passer des tests ...
Posté par Nicolas Boulay (site web personnel) . En réponse au journal La preuve de programme : où en est-on ?. Évalué à 2.
Et toi sur quelle planète ?
J'ai l'impression qu'il y une différence entre les pratiques habituelles pour le développement live critical et ce que tu crois l'être... vu depuis un labo.
"La première sécurité est la liberté"
[^] # Re: Se passer des tests ...
Posté par Nicolas Boulay (site web personnel) . En réponse au journal La preuve de programme : où en est-on ?. Évalué à 2.
Si tu joues le jeu de la vérification formelle, tu démonteras juste que ce n'est pas prouvable. T'es bien avancé.
Renseignes toi mieux. Ce genre d'outil existe déjà et fonctionne.
par exemple : http://www.absint.com/ait/
"La première sécurité est la liberté"
[^] # Re: Se passer des tests ...
Posté par Nicolas Boulay (site web personnel) . En réponse au journal La preuve de programme : où en est-on ?. Évalué à 1.
Dans la preuve formel, tu ajoutes une assertion qui correspond à un point de spécification. La vérification formel balaye toutes les possibilités d'entrée à la recherche d'un contre exemple.
Dans le cas du test, tu es limité par les vecteurs d'entrée que tu trouves à la main alors qu'avec un moteur de preuve, tu as l'exhaustivité.
"La première sécurité est la liberté"
[^] # Re: Se passer des tests ...
Posté par Nicolas Boulay (site web personnel) . En réponse au journal La preuve de programme : où en est-on ?. Évalué à 2.
Quelle différence entre une vérification formelle et un test, ici ?
C'est pas parcque tu as réussi à formaliser les specs que les specs sont valides.
C'est évident ça. mais dans ce cas, on parle de valider la spec par celle au dessus. Au moins on peut trouver les incohérences.
Et là si tu fais pas des tests d'ergonomie...
Cela veut dire que tu codes en suivant une spec mais que tu tests en suivant autre choses ? Je te souhaite bien du courage pour expliquer d'où vient le problème à ton client ! (sa spec et pas ton code)
'est con mais c'est comme ca dans la vraie vie, souvent tu te buttes face à un client qui ne veut pas répondre (pas le temps ou ne sais pas trancher) et tu dois faire des choix.
Je commençais à comprendre que ton client ne faisait pas des avions :)
"La première sécurité est la liberté"