Hypothèse de la simulation
Simulationsdomaine 12 sur 18

Mathématiques et calcul

Nombres, preuves, graphes et machines, étudiés par le calcul autant que par la déduction.

Les mathématiques et l’informatique testent désormais leurs propres idées par simulation. Elles génèrent des millions de graphes aléatoires pour voir ce qui est typique. Elles font tourner une machine pour voir ce qu’un algorithme fait vraiment. Elles attaquent un chiffrement encore et encore pour apprendre comment il échoue. Rien de tout cela ne décrit le monde physique. Cela explore l’espace des nombres, des structures et des calculs eux-mêmes. La pratique va des mathématiques expérimentales faites à la main pendant des siècles aux outils modernes de vérification qui confrontent une conception à chaque état atteignable avant qu’elle soit construite.

Mathématiques pures par ordinateur

Expériences sur des matrices aléatoires

De grandes matrices remplies de nombres aléatoires, diagonalisées à répétition pour étudier la statistique de leurs valeurs propres.

Question à laquelle elle répond: Quel motif les valeurs propres d’une matrice aléatoire adoptent-elles, et correspond-il à d’autres domaines des mathématiques et de la physique ?

Laisse de côté : N’échantillonne jamais qu’un minuscule recoin d’un espace infini de matrices possibles.

Tourne sur : environ 1012 FLOPS approximatif un cluster universitaire qui génère et diagonalise de nombreuses grandes matricesDepuis : 1955 Les premiers travaux de Wigner sur les statistiques des valeurs propres de matrices aléatoires

Monte Carloplancher : Règles

Expériences sur des graphes aléatoires

Des graphes produits par une règle aléatoire, nœud par nœud ou arête par arête, pour voir quelles propriétés, comme la connexité ou le regroupement, apparaissent typiquement.

Question à laquelle elle répond: À quoi ressemble un réseau « typique » sous cette règle d’ajout de nœuds et d’arêtes ?

Laisse de côté : Les réseaux du monde réel sont rarement aussi nets que la règle qui engendre le modèle.

Tourne sur : environ 1010 FLOPS approximatif tourne sur un ordinateur de bureau pour des graphes jusqu’à des millions de nœudsDepuis : 1959 Le modèle de graphe aléatoire d’Erdős et Rényi

Monte CarloModèles de réseauplancher : Règles

Simulation de percolation

Un réseau dont des sites ou des liens sont ouverts au hasard, observé jusqu’au point où un chemin connecté traverse soudain tout le système.

Question à laquelle elle répond: À partir de quelle densité un réseau aléatoire devient-il soudain connexe de bout en bout ?

Laisse de côté : Les réseaux idéalisés se comportent plus proprement que n’importe quel matériau poreux ou réseau réel.

Tourne sur : environ 1010 FLOPS approximatif une machine de bureau pour de grands balayages de réseauDepuis : 1957 L’introduction de la théorie de la percolation par Broadbent et Hammersley

Estimation de constantes par Monte Carlo

Un échantillonnage aléatoire servant à estimer une constante ou une intégrale mathématique, comme lancer des points pour estimer une aire, comme exercice plutôt que pour un modèle physique.

Question à laquelle elle répond: Avec quelle précision un simple échantillonnage aléatoire aveugle peut-il cerner une quantité mathématique exacte ?

Laisse de côté : Converge bien plus lentement que presque toute méthode numérique plus sophistiquée.

Tourne sur : environ 109 FLOPS approximatif tourne sur un ordinateur portable en quelques secondes à quelques minutesDepuis : 1946 idée d’Ulam de 1946 ; von Neumann proposa une version pour ordinateur électronique en mars 1947, et la méthode fut publiée pour la première fois en 1949 sourceDans l’arbre des simulations: Méthode de Monte Carlo

Lancer le modèle interactif

Monte Carloplancher : Règles

Recherches de théorie des nombres par calcul

De grands nombres testés pour la primalité, factorisés ou examinés à la recherche de propriétés particulières comme les nombres parfaits, avec des algorithmes exécutés à grande échelle plutôt qu’à la main.

Question à laquelle elle répond: Ce très grand nombre a-t-il la propriété recherchée, et jusqu’où la recherche peut-elle repousser le record ?

Laisse de côté : Les recherches qui battent des records disent peu de choses sur les nombres que personne n’a pensé à vérifier.

Tourne sur : environ 1013 FLOPS approximatif un projet de calcul distribué bénévole sur de nombreuses machines donnéesDepuis : 1951 Le test manuel de Lucas pour les nombres premiers de Mersenne, exécuté pour la première fois par ordinateur en 1951

Règles et étatsMonte Carloplancher : Règles

Numérique des attracteurs chaotiques

Un petit ensemble d’équations non linéaires intégré pas à pas pour révéler la dépendance sensible aux conditions initiales et un attracteur fractal.

Question à laquelle elle répond: Pourquoi un système déterministe simple devient-il imprévisible ?

Laisse de côté : L’arrondi numérique fait qu’une longue trajectoire n’est pas une vraie orbite, seulement une trajectoire qui reste proche d’une orbite.

Tourne sur : environ 103 FLOPS approximatif quelques équations, quelques secondes sur un ordinateur portable.Depuis : 1963 L’écoulement déterministe non périodique de Lorenz, un modèle de convection exécuté sur un ordinateur. sourceDans l’arbre des simulations: La convection chaotique de Lorenz

Équations différentiellesplancher : Règles

Expériences non linéaires sur réseau

Une chaîne de masses reliées par des ressorts non linéaires, lancée dans un seul mode et suivie pour voir si l’énergie se répartit uniformément, comme la thermodynamique le laisserait penser.

Question à laquelle elle répond: Une chaîne non linéaire répartit-elle son énergie uniformément entre tous ses mouvements ?

Laisse de côté : Les résultats dépendent de la chaîne choisie et de l’état initial.

Tourne sur : environ 103 FLOPS approximatif minuscule selon les normes actuelles ; l’original utilisait quelques dizaines de masses.Depuis : 1955 Les études de problèmes non linéaires de Fermi, Pasta et Ulam sur un des premiers ordinateurs numériques. source

Expériences numériques sur les solitons

Une équation d’onde non linéaire résolue sur une grille pour voir des impulsions se traverser et conserver leur forme, ce que ne font pas les ondes linéaires.

Question à laquelle elle répond: Pourquoi certaines ondes non linéaires se traversent-elles sans changer ?

Laisse de côté : Il montre une famille d’équations, pas le comportement général des ondes non linéaires.

Tourne sur : environ 104 FLOPS approximatif une grille à une dimension, triviale aujourd’hui.Depuis : 1965 L’interaction de solitons dans un plasma sans collisions et la récurrence des états initiaux de Zabusky et Kruskal. source

Rendu d’ensembles fractals

Une formule itérée simple testée en chaque point du plan complexe pour voir si elle s’échappe, ce qui dessine la frontière de l’ensemble des points stables.

Question à laquelle elle répond: Quelle est la forme de l’ensemble où une itération simple reste bornée ?

Laisse de côté : Les tests d’échappement ne font que suggérer l’appartenance, et l’image est un échantillonnage à résolution finie d’un ensemble infiniment détaillé.

Tourne sur : environ 109 FLOPS approximatif les zooms profonds exigent une itération en précision étendue en des millions de points.Depuis : 1980 Les aspects fractals de l’itération de z vers lambda z(1-z) de Mandelbrot, premières images informatiques de l’ensemble de Mandelbrot. source

Équations différentiellesplancher : Règles

Criticalité auto-organisée du tas de sable

Des grains lâchés sur une grille qui s’effondrent quand la pente est trop forte, ce qui donne des avalanches de toutes tailles sans aucun réglage ; un modèle de la façon dont les systèmes atteignent un état critique.

Question à laquelle elle répond: Pourquoi des avalanches de toutes tailles apparaissent-elles sans aucun réglage ?

Laisse de côté : La question de savoir si les vrais systèmes partagent la même loi d’échelle est contestée.

Tourne sur : environ 109 FLOPS approximatif de longues simulations sur de grandes grilles pour voir le passage à l’échelle.Depuis : 1987 La criticalité auto-organisée de Bak, Tang et Wiesenfeld : une explication du bruit en 1/f. source

Calcul des zéros de la fonction zêta de Riemann

Les valeurs de la fonction zêta le long de sa droite critique sont calculées pour localiser et compter ses zéros, en vérifiant qu’ils se trouvent là où l’hypothèse le dit.

Question à laquelle elle répond: Tous les zéros non triviaux de la fonction zêta se trouvent-ils sur une même droite ?

Laisse de côté : Une vérification finie, aussi longue soit-elle, ne peut pas prouver qu’aucun zéro hors de la droite n’existe au-delà.

Tourne sur : environ 1018 FLOPS approximatif des décennies de temps CPU pour les plus grandes recherches.Depuis : 1953 Les calculs de Turing sur la fonction zêta de Riemann. source

Décimales de pi par ordinateur

Des séries pour pi sont sommées jusqu’à d’énormes nombres de chiffres avec une arithmétique exacte, ce qui teste à la fois le nombre et la machine.

Question à laquelle elle répond: Les décimales de pi ont-elles l’air aléatoires, et peut-on se fier à la machine à cette échelle ?

Laisse de côté : Les décimales ne répondent à aucune question ouverte, et les vérifications ne détectent les erreurs matérielles que si la méthode est indépendante.

Tourne sur : environ 1017 FLOPS approximatif des mois sur un serveur pour des centaines de billions de chiffres.Depuis : 1950 La détermination de pi et de e sur plus de 2000 décimales par Reitwiesner avec l’ENIAC (publiée en 1950, rééditée dans Pi: A Source Book). source

Découverte de conjectures guidée par l’IA

L’apprentissage automatique sur de grands tableaux d’objets mathématiques trouve quelles propriétés sont liées, pour suggérer une conjecture que les mathématiciens essaient ensuite de démontrer.

Question à laquelle elle répond: Quelle relation invisible entre ces grandeurs mathématiques mérite d’être démontrée ?

Laisse de côté : Il ne fait que suggérer des motifs et ne prouve rien par lui-même, et certaines régularités des données peuvent être des artefacts de la façon dont elles ont été produites.

Tourne sur : environ 1015 FLOPS approximatif des jours sur quelques GPU par jeu de données.Depuis : 2021 Davies et ses collègues, faire progresser les mathématiques en guidant l’intuition humaine avec l’IA. source

Émulateurs apprisplancher : Règles

Recherche d’algorithmes et de constructions par apprentissage

Un système de jeu ou de modèle de langage cherche de nouvelles procédures ou de nouveaux objets mathématiques, un ordinateur vérifiant l’exactitude de chaque candidat.

Question à laquelle elle répond: Un programme peut-il découvrir un algorithme plus rapide ou un exemple plus grand que ceux que les gens ont trouvés ?

Laisse de côté : Chaque résultat est un seul nouvel exemple, et la recherche ne couvre que les genres d’objets que ses concepteurs ont formulés comme un jeu.

Tourne sur : environ 1017 FLOPS approximatif de quelques jours à quelques semaines sur des clusters d’accélérateurs.Depuis : 2022 AlphaTensor de Fawzi et ses collègues, qui découvre des algorithmes de multiplication matricielle plus rapides par apprentissage par renforcement. source

Preuve, logique et sécurité

Vérification de modèles

Chaque état atteignable d’un système fini, comme un protocole ou une conception de circuit, énuméré par ordinateur pour vérifier qu’une propriété tient dans tous.

Question à laquelle elle répond: Existe-t-il un état atteignable où cette conception enfreint ses propres règles ?

Laisse de côté : Les espaces d’états explosent au-delà de ce qu’on peut vérifier, si bien que les vrais systèmes sont d’abord simplifiés.

Tourne sur : environ 1012 FLOPS approximatif un cluster universitaire qui épuise un espace d’états vaste mais bornéDepuis : 1981 L’introduction de la vérification de modèles par Clarke et Emerson

Règles et étatsplancher : Règles

Recherche de preuves par démonstration automatique de théorèmes

Une recherche à travers des chaînes d’inférences logiques, produites par ordinateur pas à pas, pour trouver une preuve ou une réfutation d’un énoncé mathématique.

Question à laquelle elle répond: Existe-t-il une chaîne valide d’étapes logiques des axiomes jusqu’à cet énoncé ?

Laisse de côté : Trouve des preuves qu’aucun humain ne choisirait, et parfois aucune à portée.

Tourne sur : environ 1011 FLOPS approximatif un cluster universitaire qui cherche pendant des heures ou des joursDepuis : 1956 le Logic Theorist, un des premiers programmes de recherche automatique de preuves

Règles et étatsMonte Carloplancher : Règles

SAT et résolution de contraintes

Des millions de combinaisons de valeurs vrai ou faux explorées systématiquement pour satisfaire un grand ensemble de contraintes logiques, utilisées pour planifier, acheminer ou vérifier des conceptions.

Question à laquelle elle répond: Existe-t-il une affectation de valeurs qui satisfait toutes ces contraintes à la fois ?

Laisse de côté : Certaines instances sont si difficiles qu’aucun solveur, si bon soit-il, n’en vient à bout à temps.

Tourne sur : environ 1011 FLOPS approximatif un poste de travail ou un cluster, selon la taille du problèmeDepuis : 1962 la procédure de Davis-Putnam pour la recherche de satisfiabilité

Règles et étatsMonte Carloplancher : Règles

Modélisation d’attaques cryptographiques

Un code ou un schéma d’échange de clés attaqué des millions de fois en simulation, par force brute, biais statistique ou faiblesse modélisée, pour mesurer l’effort réellement nécessaire pour le casser.

Question à laquelle elle répond: Combien d’opérations faudrait-il réellement pour casser cela, et ce nombre reste-t-il assez grand pour être sûr ?

Laisse de côté : Ne teste que les attaques que l’analyste a pensé à modéliser, pas celle que personne n’a encore trouvée.

Tourne sur : environ 1014 FLOPS approximatif un cluster distribué de nombreuses machines qui exécutent des essais d’attaqueDepuis : 1976 dès 1976, analyse informatique de la robustesse des chiffrements et des échanges de clés

Monte CarloRègles et étatsplancher : Règles

Simulation des fuites par canaux auxiliaires

La consommation, le timing ou l’émission électromagnétique d’un appareil, modélisés pendant qu’il exécute une opération cryptographique, pour voir ce qu’un espion à l’écoute à l’extérieur pourrait en apprendre.

Question à laquelle elle répond: Quelle part de la clé secrète fuit par le comportement physique de l’appareil, et non par les mathématiques ?

Laisse de côté : Les conditions de laboratoire saisissent des signaux plus nets que ce qu’un appareil réel et bruité en laisse échapper d’habitude.

Tourne sur : environ 1010 FLOPS approximatif un poste de travail qui modélise la trace de consommation ou de timing d’un composantDepuis : 1996 La démonstration par Kocher d’attaques par mesure du temps sur des implémentations cryptographiques

Vérification des protocoles de sécurité

Chaque message qu’un attaquant pourrait envoyer, rejouer ou falsifier dans un protocole de communication, énuméré par ordinateur pour vérifier si l’on peut lui arracher un secret ou une identité.

Question à laquelle elle répond: Une suite de messages peut-elle amener ce protocole à divulguer un secret ou à accepter une fausse identité ?

Laisse de côté : Vérifie le protocole tel qu’il est spécifié, pas les raccourcis que prend une vraie implémentation.

Tourne sur : environ 1011 FLOPS approximatif un poste de travail ou un cluster qui vérifie l’espace des messages d’un protocoleDepuis : 1989 le modèle de Dolev-Yao, une base fondatrice de la vérification de protocoles

Preuve assistée par ordinateur par vérification exhaustive de cas

Un théorème réduit à une liste finie de cas, chacun vérifié par programme, parce qu’aucun humain ne pourrait tous les contrôler.

Question à laquelle elle répond: Une preuve peut-elle être achevée par une machine qui vérifie tous les cas ?

Laisse de côté : La confiance se déplace vers le programme, le matériel et l’argument de réduction des cas.

Tourne sur : environ 109 FLOPS approximatif environ mille heures sur un gros ordinateur (mainframe) pour l’original ; bien moins aujourd’hui.Depuis : 1977 La preuve d’Appel et Haken que toute carte plane se colore avec quatre couleurs, par réductibilité vérifiée par ordinateur. source

Numérique validé

Des calculs menés avec des bornes garanties, si bien qu’un résultat numérique prouve un énoncé mathématique, comme l’existence d’un attracteur chaotique.

Question à laquelle elle répond: Une réponse calculée peut-elle être prouvée correcte, et pas seulement probablement exacte ?

Laisse de côté : Les bornes peuvent exploser sur de longues durées, ce qui limite les preuves à des problèmes courts ou bien comportés.

Tourne sur : environ 109 FLOPS approximatif l’arithmétique d’intervalles multiplie le coût par un facteur modeste.Depuis : 2002 Le solveur rigoureux d’EDO de Tucker et le 14e problème de Smale, qui prouve l’existence de l’attracteur de Lorenz. source

Équations différentiellesplancher : Règles

Énumération de machines de Turing

Chaque petit programme d’une machine minimale exécuté pour voir lesquels s’arrêtent et lesquels tournent indéfiniment, afin de trouver celui qui s’arrête après le plus longtemps pour chaque taille.

Question à laquelle elle répond: Combien de temps un tout petit programme peut-il tourner avant de s’arrêter ?

Laisse de côté : L’indécidabilité signifie que certaines machines ne pourront jamais être classées, quel que soit le temps qu’elles tournent.

Tourne sur : environ 1015 FLOPS approximatif des milliards de machines, avec des preuves pour celles qui ne s’arrêtent pas.Depuis : 1965 Les études informatiques de Lin et Rado sur des problèmes de machines de Turing. source

Vérification statistique de modèles

Un système au comportement aléatoire simulé de nombreuses fois pour estimer avec confiance la probabilité qu’il viole une propriété.

Question à laquelle elle répond: Quelle est la probabilité qu’un système aléatoire enfreigne une règle de sécurité ?

Laisse de côté : Les calculs statistiques donnent une probabilité avec un niveau de confiance, pas une preuve, et les défaillances rares demandent un échantillonnage préférentiel.

Tourne sur : environ 109 FLOPS approximatif des milliers à des millions d’exécutions échantillonnées.Depuis : 2002 La vérification probabiliste de systèmes à événements discrets par échantillonnage d’acceptation de Younes et Simmons. source

Test par fuzzing

Un programme reçoit d’énormes quantités d’entrées aléatoires ou mutées pour trouver celles qui le font planter, ce qui revient à simuler un monde hostile ou négligent.

Question à laquelle elle répond: Quelle entrée fera échouer ce logiciel ?

Laisse de côté : Il ne trouve que les pannes que des entrées aléatoires atteignent, et un programme peut passer pendant des années en cachant un bogue derrière un cas rare.

Tourne sur : environ 1014 FLOPS approximatif des années-machine de temps de processeur pour une grande base de code.Depuis : 1990 L’étude empirique de Miller, Fredriksen et So sur la fiabilité des utilitaires UNIX. source

Exécution symbolique

Un programme exécuté avec des entrées inconnues écrites sous forme de symboles, qui recueille les conditions de chaque chemin, puis un solveur trouve les valeurs qui empruntent chaque branche.

Question à laquelle elle répond: Quelles entrées font exécuter chaque chemin de ce programme, et l’une d’elles mène-t-elle à un bogue ?

Laisse de côté : Le nombre de chemins croît de façon exponentielle avec la taille du programme, si bien que les grands ne sont couverts qu’en partie.

Tourne sur : environ 1012 FLOPS approximatif des heures de temps de solveur par programme, en forte hausse avec le nombre de chemins.Depuis : 1976 L’exécution symbolique et le test de programmes de King. source

Interprétation abstraite

Un programme exécuté sur des ensembles de valeurs possibles, comme des intervalles, plutôt que sur des valeurs uniques, pour prouver des propriétés vraies pour toute entrée.

Question à laquelle elle répond: Ce programme peut-il jamais diviser par zéro ou déborder, pour une entrée quelconque ?

Laisse de côté : L’approximation sûre déclenche de fausses alertes, si bien que les gens doivent quand même vérifier chaque avertissement.

Tourne sur : environ 1011 FLOPS approximatif des heures sur une station de travail pour une grande base de code avionique.Depuis : 1977 L’interprétation abstraite de Cousot et Cousot, un modèle unifié en treillis pour l’analyse statique de programmes. source

Vérification de modèles bornée

Le comportement d’un système sur un nombre fixé d’étapes est écrit sous forme de formule logique et confié à un solveur de satisfiabilité pour trouver tout chemin court vers un bogue.

Question à laquelle elle répond: Ce circuit ou ce programme peut-il atteindre un état d’erreur en un nombre donné de pas ?

Laisse de côté : Il ne prouve rien au-delà de la borne sur le nombre de pas, sauf si un argument séparé montre qu’elle suffit.

Tourne sur : environ 1013 FLOPS approximatif des heures sur un serveur par propriété.Depuis : 1999 La vérification symbolique de modèles sans BDD de Biere, Cimatti, Clarke et Zhu. source

Tests aléatoires fondés sur des propriétés

On énonce une règle qui devrait toujours être vraie, et l’ordinateur génère de nombreux cas aléatoires et réduit tout échec à un petit contre-exemple.

Question à laquelle elle répond: Ce code respecte-t-il sa propre spécification sur un large éventail d’entrées ?

Laisse de côté : Des cas aléatoires peuvent ne jamais atteindre une condition rare, et la propriété écrite n’est peut-être pas celle qui compte.

Tourne sur : environ 109 FLOPS approximatif des minutes sur un ordinateur portable pour des milliers de cas.Depuis : 2000 QuickCheck de Claessen et Hughes, un outil léger de test aléatoire pour les programmes Haskell. source

Monte CarloRègles et étatsplancher : Règles

Vérification de réseaux de neurones

Des solveurs de contraintes prouvent que pour toute entrée dans une région, la sortie d’un réseau de neurones reste dans des bornes, au lieu de tester des échantillons.

Question à laquelle elle répond: Un petit changement d’une entrée peut-il jamais faire donner une mauvaise réponse au réseau ?

Laisse de côté : Les preuves ne passent à l’échelle que pour de petits réseaux, et l’ensemble des perturbations qu’on peut vérifier est étroit.

Tourne sur : environ 1013 FLOPS approximatif de quelques heures à quelques jours sur un serveur pour un petit réseau.Depuis : 2017 Reluplex, de Katz et ses collègues, un solveur SMT pour vérifier des réseaux de neurones profonds. source

Systèmes et machines

Simulation d’architecture d’ordinateur

Le pipeline, les caches et le prédicteur de branchement d’un processeur proposé, modélisés instruction par instruction, pour estimer la vitesse d’une puce avant sa fabrication.

Question à laquelle elle répond: À quelle vitesse ce processeur exécuterait-il de vrais programmes, avant qu’on grave le moindre silicium ?

Laisse de côté : Simplifie assez de la vraie puce pour que le silicium final diffère toujours un peu du modèle.

Tourne sur : environ 1011 FLOPS approximatif un cluster universitaire qui fait passer des programmes d’évaluation dans le modèleDepuis : 1990 dès 1990, simulateurs de processeurs précis au cycle près pour la recherche en architecture

Simulation de systèmes distribués et de consensus

De nombreux ordinateurs modélisés qui s’envoient des messages avec des retards, des pertes et des pannes, pour tester si un algorithme distribué s’accorde encore sur la bonne réponse.

Question à laquelle elle répond: Cet algorithme atteint-il encore le bon accord quand des messages sont perdus, retardés ou que des nœuds plantent ?

Laisse de côté : Les pannes injectées sont celles que le concepteur avait anticipées, pas celles qui surviennent à l’improviste en production.

Tourne sur : environ 1010 FLOPS approximatif un cluster qui simule des centaines de nœuds virtuelsDepuis : 1978 Les premiers travaux de Lamport sur l’ordre et la défaillance dans les systèmes distribués

Simulation de systèmes de stockage

Des disques, des lecteurs et des systèmes de fichiers modélisés pour voir comment ils organisent les données, tombent en panne et se rétablissent, afin de tester une conception de stockage avant d’acheter et de remplir de vrais lecteurs.

Question à laquelle elle répond: Comment cette conception de stockage se comporte-t-elle et survit-elle aux pannes, à une échelle trop coûteuse pour être d’abord testée en vrai ?

Laisse de côté : Les vrais disques tombent en panne de façon plus désordonnée et plus corrélée que le taux de panne aléatoire du modèle.

Tourne sur : environ 1010 FLOPS approximatif un poste de travail ou un petit cluster qui modélise une baie de stockageDepuis : 1988 dès 1988, modèles de simulation de la fiabilité des baies de disques

Simulation d’ordonnanceur de système d’exploitation

Un flux de tâches de calcul modélisé comme arrivant et se disputant un processeur, exécuté avec différentes règles d’ordonnancement pour voir laquelle est la plus équitable ou la plus rapide.

Question à laquelle elle répond: Quelle façon d’ordonner la file de tâches fait avancer le plus de travail, ou est la plus équitable pour chaque tâche ?

Laisse de côté : Les charges de travail synthétiques correspondent rarement au mélange irrégulier de tâches que rencontre une vraie machine.

Tourne sur : environ 109 FLOPS approximatif tourne sur un ordinateur portable ou une station de travail en quelques secondes à quelques minutesDepuis : 1968 dès 1968, études par simulation de politiques d’ordonnancement de processeurs

Événements discretsplancher : Règles

Tests empiriques de performance d’algorithmes

Un algorithme exécuté des milliers de fois sur des entrées générées au hasard ou réelles de taille croissante, pour mesurer comment son temps d’exécution croît vraiment plutôt que de le démontrer sur le papier.

Question à laquelle elle répond: Comment le temps d’exécution de cet algorithme croît-il réellement en pratique, sur les entrées qu’il verra vraiment ?

Laisse de côté : Un pire cas absent des entrées de test reste indétecté jusqu’à ce qu’il se produise.

Tourne sur : environ 109 FLOPS approximatif tourne sur une station de travail sur de nombreuses entrées de test généréesDepuis : 1970 dès 1970, essais empiriques systématiques des temps d’exécution d’algorithmes

Exécution de programmes par des modèles de langage

Un modèle de langage écrit pas à pas les états intermédiaires pour retracer ce qu’un programme calculerait.

Question à laquelle elle répond: Un modèle de langage peut-il émuler l’exécution d’un code ?

Laisse de côté : La justesse du résultat n’est pas garantie, et les longs programmes échouent.

Tourne sur : environ 1014 FLOPS approximatif Inférence par requêteDepuis : 2021 Show your work: scratchpads for intermediate computation with language models (2021) source

Émulateurs apprisplancher : Règles

Simulation de consensus de blockchain

Un réseau de nœuds qui produisent et partagent des blocs avec des délais, pour tester comment la taille des blocs, le calendrier et les attaquants jouent sur la sécurité et le débit.

Question à laquelle elle répond: Quelle est la sécurité et la vitesse d’une blockchain face aux retards du réseau et aux attaques ?

Laisse de côté : Le vrai comportement des nœuds et les topologies de réseau ne sont mesurés qu’en partie.

Tourne sur : environ 108 FLOPS approximatif des exécutions pilotées par événements de milliers de nœuds.Depuis : 2016 L’analyse de sécurité et de performance des blockchains à preuve de travail avec un simulateur de Gervais et ses collègues. source

Simulation parallèle à événements discrets

Une simulation d’événements dans le temps est répartie sur de nombreux processeurs qui avancent chacun leur propre horloge et reviennent en arrière si un message arrive en retard.

Question à laquelle elle répond: Comment une énorme simulation pilotée par événements, comme un réseau ou un champ de bataille, peut-elle tourner vite sur de nombreuses machines ?

Laisse de côté : Les retours en arrière peuvent s’enchaîner en cascade, et le gain de vitesse dépend fortement du degré de couplage des événements.

Tourne sur : environ 1014 FLOPS approximatif des heures sur un supercalculateur pour des milliards d’événements.Depuis : 1985 Le temps virtuel de Jefferson, le mécanisme Time Warp de synchronisation optimiste. source

Événements discretsplancher : Règles

Simulation de l’architecture des processeurs graphiques

Les cœurs, les warps et la mémoire d’un processeur graphique sont modélisés cycle par cycle, avec de vrais programmes, pour évaluer une conception avant de la construire.

Question à laquelle elle répond: Comment une modification de conception affecterait-elle la vitesse de programmes parallèles sur une puce graphique ?

Laisse de côté : Les détails des vraies puces sont secrets ou inconnus, si bien que le modèle ne correspond qu’à peu près aux chiffres des conceptions existantes.

Tourne sur : environ 1012 FLOPS approximatif de quelques heures à quelques jours de temps d’hôte par seconde d’exécution simulée.Depuis : 2009 L’analyse de charges de travail CUDA par Bakhoda et ses collègues à l’aide d’un simulateur de GPU détaillé. source

Simulation de systèmes accélérée par FPGA

Une puce conçue est chargée sur de nombreux circuits reconfigurables qui l’exécutent au cycle près à des vitesses de l’ordre du mégahertz, ce qui permet de simuler des serveurs entiers et leurs réseaux.

Question à laquelle elle répond: Comment ce processeur et son cluster se comporteront-ils avec de vrais logiciels, avant d’être fabriqués ?

Laisse de côté : Il est bien plus lent que la vraie puce, et une conception qui ne tient pas sur les circuits ne peut pas être exécutée.

Tourne sur : environ 1015 FLOPS approximatif des jours sur un nuage de centaines de circuits reconfigurables.Depuis : 2018 FireSim de Karandikar et ses collègues, simulation de systèmes à grande échelle précise au cycle, accélérée par FPGA, dans le cloud public. source

Simulation de système complet

Un ordinateur entier, avec processeurs, mémoire, disques et cartes réseau, simulé assez bien pour démarrer un système d’exploitation non modifié et exécuter ses programmes.

Question à laquelle elle répond: Comment un vrai logiciel se comporte-t-il sur une machine qui n’existe pas encore, ou qu’on peut mettre en pause et rejouer à volonté ?

Laisse de côté : Le timing est approximé pour gagner en vitesse, si bien qu’on n’obtient pas les performances exactes, seulement le comportement fonctionnel.

Tourne sur : environ 1011 FLOPS approximatif presque en temps réel sur un serveur par machine simulée.Depuis : 2002 Simics de Magnusson et ses collègues, une plateforme de simulation de systèmes complets. source

Émulation légère de réseau

Des dizaines ou des centaines d’hôtes et de commutateurs virtuels font tourner de vrais logiciels réseau sur un seul ordinateur portable, reliés par des câbles émulés avec une vitesse et un délai fixés.

Question à laquelle elle répond: Ce programme de contrôle de réseau fonctionnera-t-il sur une topologie entière avant d’être déployé ?

Laisse de côté : Le processeur de l’hôte est partagé par tous les nœuds virtuels, si bien que les liaisons rapides sont ralenties.

Tourne sur : environ 1010 FLOPS approximatif en temps réel sur une seule station de travail.Depuis : 2010 « A network in a laptop » de Lantz, Heller et McKeown, prototypage rapide pour les réseaux définis par logiciel. source

Recuit simulé

Un ordinateur refroidit lentement un modèle d’atomes ou un plan, en acceptant parfois de moins bons arrangements, pour trouver une bonne solution à un problème d’optimisation difficile.

Question à laquelle elle répond: Quel est un agencement ou un calendrier presque optimal parmi un nombre astronomique de possibilités ?

Laisse de côté : Il ne garantit pas la meilleure réponse, et les résultats dépendent du programme de refroidissement.

Tourne sur : environ 1012 FLOPS approximatif des heures sur une station de travail pour un placement de puce.Depuis : 1983 L’optimisation par recuit simulé de Kirkpatrick, Gelatt et Vecchi. source

Calcul bayésien approximatif

On exécute un simulateur avec de nombreuses valeurs d’essai des paramètres, et l’on garde celles qui produisent des données proches des données observées, ce qui donne une idée des valeurs plausibles.

Question à laquelle elle répond: Quels réglages d’un modèle compliqué auraient pu produire les données que nous observons ?

Laisse de côté : Le résultat dépend des résumés de données utilisés et de la proximité requise pour qu’une correspondance compte.

Tourne sur : environ 1013 FLOPS approximatif des millions d’exécutions de simulateur sur un cluster.Depuis : 1997 L’inférence des temps de coalescence à partir de séquences d’ADN par simulation, de Tavaré et ses collègues. source