Alive prouve formellement que les optimisations des compilateurs sont correctes

Lorsque l’on développe une application et que l’on rencontre un problème, la source la plus courante est le code que l’on écrit soi-même. Plus rarement, il s’agit d’un défaut dans les bibliothèques utilisées, exceptionnellement dans le compilateur, jamais dans le processeur. Du moins, c’est ce que bon nombre de programmeurs ont fini par intégrer. Il n’empêche que cette hiérarchie est assez optimiste. Par exemple, les processeurs n’exécutent pas toujours correctement les instructions qui leur sont passées : depuis la mauvaise implémentation de FDIV sur les premiers Pentium jusqu’à la technologie HyperThreading de la dernière génération de processeurs Intel Core ou un problème pas encore identifié sur les AMD Ryzen qui causent un bon nombre d’erreurs de segmentation avec GCC.

Les compilateurs ne font pas exception. Comme les fabricants de processeurs, les développeurs de compilateurs sont sous pression. Ils veulent augmenter la performance des applications compilées/exécutées, augmenter l’efficacité énergétique, etc. De plus, la complexité de ces projets ne fait qu’augmenter : il est impossible de dessiner l’entièreté des processeurs à la main pour leur conception depuis belle lurette, les compilateurs modernes font plusieurs millions de lignes de code qui évoluent rapidement. Ainsi, des défauts sont présents, tant au niveau des compilateurs que des processeurs — des défauts qui peuvent mener à des failles de sécurité béantes.

Un exemple : Heartbleed

Par exemple, pour accéder à une cellule d’un tableau en mémoire, il faut s’assurer que l’adresse est bien dans le tableau : sinon, on peut lire des données normalement inaccessibles pour ce morceau de code (c’est notamment le principe de Heartbleed, qui avait fait beaucoup de bruit en 2014). Pour un bon nombre de langages, ces vérifications sont effectuées à chaque accès au tableau, sauf s’il est possible de prouver que l’accès ne pose aucun problème. Si une optimisation du compilateur fait une erreur à ce moment, la sécurité du programme compilé est mise à mal.

Cette preuve peut se faire en déterminant la plage de valeurs possibles pour l’index et en la comparant à la taille du tableau, par exemple. Toutes les optimisations du compilateur doivent ainsi être écrites précisément : si l’une d’entre elles fait une petite erreur dans le calcul de la plage de valeurs possibles, tout le reste du château s’effondre.

Alive

C’est pourquoi une série de chercheurs s’est associée à Microsoft pour développer Alive, un outil de vérification formel des optimisations effectuées par un compilateur. Il faut tout d’abord décrire l’optimisation dans un langage précis ; ensuite, Alive utilise les technologies actuelles de preuve automatique de théorème (plus précisément, le solveur SMT Z3) pour déterminer si l’optimisation est correcte ou non. Les résultats ne se sont pas faits attendre : très rapidement, une dizaine de défauts ont été trouvés dans LLVM ; Alive a aussi empêché l’introduction d’optimisations fausses dans LLVM et le compilateur C++ de Microsoft.

La suite des travaux de ce groupe envisage une intégration dynamique au compilateur : au lieu de vérifier en amont qu’une optimisation est valide (peu importe le programme à compiler), il s’agit de vérifier si l’optimisation d’un programme s’est déroulée sans anicroche. Ce principe s’appelle validation de la traduction et permet de détecter d’autres types de problèmes, dans les cas où l’optimisation effectuée est hors de portée des programmes de vérification. Notamment, Microsoft déclare avoir déjà pu corriger quelques défauts dans son compilateur C++ grâce à cette méthode, malgré les autres analyses effectuées.

Il n’empêche que ces travaux n’ont pas beaucoup d’intérêt si la sémantique de la représentation intermédiaire (utilisée par les compilateurs pour effectuer les optimisations sans dépendre du langage compilé) n’est pas parfaitement définie : c’est là le prochain axe de recherche, déjà entamé en ce qui concerne les comportements indéfinis (notamment en C et C++).

Source : Getting compilers right: a reliable foundation for secure software.

Intel et Huawei s’apprêtent à collaborer dans le domaine du calcul de haute performance

L’annonce a probablement de quoi étonner : Intel et Huawei annoncent un partenariat dans le domaine du calcul de haute performance. En effet, si Intel est un nom très répandu dans le domaine (surtout pour ses processeurs Xeon, moins pour ses coprocesseurs Xeon Phi), Huawei est nettement plus connu pour les télécommunications et téléphones mobiles que pour ses serveurs de calcul. Pourtant, Huawei a développé une large gamme de serveurs à haute densité (exploitant exclusivement des processeurs Intel), sous le nom FusionServer, ainsi que des serveurs bien plus gros dans la gamme KunLun.

Les termes de l’accord portent sur le développement de serveurs fabriqués par Huawei, prévus pour le calcul de haute performance et les services infonuagiques, avec des processeurs Intel (Xeon et Xeon Phi) et sa technologie d’interconnexion entre serveurs Omni-Path. Ainsi, Huawei pourra différentier ses produits par rapport à la concurrence en incluant des composants plus centrés sur le calcul de haute performance.

L’accord prévoit aussi la construction de trois centres d’innovation dans le domaine du calcul de haute performance (deux en Chine, un en Europe, à Munich), où Huawei et Intel lanceront des activités communes, comme des formations, des optimisations d’applications existantes ou encore l’animation de communautés.

Le partenariat avec Huawei se justifie par sa stratégie expansionniste ces dernières années : sa gamme de produits dans le domaine s’étend à vue d’œil, ses profits croissent au même rythme. D’ailleurs, en nombre de serveurs livrés, Huawei est maintenant troisième mondial, juste derrière Dell et HPE (quatrième en termes de revenus). La compagnie compte également seize superordinateurs dans la liste des cinq cents les plus puissants au monde, dont sept en Europe (notamment le Polonais HETMAN, d’une puissance d’un pétaflops).

Au niveau recherche et développement, Intel et Huawei jouent dans la même cour : Huawei a le plus gros budget R&D en Chine, un peu plus de dix milliards de dollars (soit quatorze pour cent de ses revenus) ; Intel monte à vingt-deux pour cent, c’est-à-dire presque treize milliards de dollars. Toute synergie sera donc la bienvenue pour les deux groupes.

Sources : Huawei and Intel Sign Up For HPC Collaboration, Huawei and Intel Sign a MOU to Accelerate HPC Innovation (image).

FUJITSU annonce le développement d’un processeur pour l’apprentissage profond

FUJITSU continue ses développements pour les prochaines générations de superordinateurs. Après le remplacement de l’architecture SPARC64 par ARM, voici l’annonce de processeurs spécifiques pour l’apprentissage profond, des DLU (deep learning unit). L’objectif est de fournir des puces dix fois plus efficaces en termes de puissance de calcul par watt consommé que la concurrence. Ces processeurs sont en développements depuis 2015, mais la première annonce n’a eu lieu qu’à la conférence ISC 2017, centrée autour du calcul de haute performance.

Comme les autres fabricants, FUJITSU mise sur des calculs avec une faible précision pour augmenter la performance et diminuer la consommation d’énergie : en effet, pas besoin d’une très grande précision pour ces réseaux neuronaux (une trop grande précision favoriserait le surapprentissage : le réseau est capable de reproduire les données d’entrée, mais pas d’extrapoler sur de nouvelles données). Ainsi, les DLU ne pourraient gérer que quatre types de données : des nombres à virgule flottante sur trente-deux (précision simple) ou seize bits (demi-précision), ainsi que des entiers de même taille.

Vus de haut, ces processeurs sont constitués d’une série d’unités de calcul spécifiques, des DPU (deep learning processing unit), connectés par des liens à haute performance. Un cœur de calcul distinct gère l’exécution sur les DPU et négocie les accès en mémoire.

Chacun de ces DPU est constitué de seize DPE (deep learning processing element), qui effectuent les calculs. Plus en détail, chaque DPE comporte huit unités de calcul SIMD, avec une banque de registres assez grande : cette dernière n’est pas contrôlée par le matériel comme un cache classique, mais uniquement par du logiciel.

La mémoire est assurée par des puces HBM2, tandis qu’il est possible de rassembler une série de DPU (les processeurs) par une interface Tofu : FUJITSU envisage de créer des systèmes de très grande taille, modulable à l’infini.

Les premiers DLU devraient être disponibles en 2018 en tant que coprocesseurs de calcul : les machines devront disposer d’un autre processeur pour lancer l’apprentissage du réseau neuronal. Cependant, tout comme Intel avec ses Xeon Phi, la deuxième génération de DPU devrait être capable de s’affranchir de ce processeur principal. On ne peut que remarquer des similitudes avec l’approche d’Intel et ses Lake Crest, à venir également l’année prochaine. NVIDIA aurait-il du souci à se faire pour ses processeurs graphiques optimisés pour l’apprentissage profond ?

Source et images : Fujitsu Will Pursue AI with Custom-Built Processor.

Lithographie aux ultraviolets extrêmes : ASML atteint une puissance de 250 W

Pour les prochains processus de fabrication de processeurs (7 nm ou 5 nm), les techniques de lithographie se baseront très probablement sur le rayonnement aux ultraviolets extrêmes (EUV). Cependant, la technologie a longtemps souffert d’une puissance relativement faible : elle était limitée à 185 W l’année dernière, ASML vient de la porter à 250 W (avec quatre ans de retard sur les plans initiaux). Il aura fallu cinq ans à l’entreprise pour dépasser les premiers prototypes, avec une puissance d’à peine 25 W en 2012.

Avec cette augmentation, l’EUV devient intéressant d’un point de vue commercial : il devient possible de produire cent vingt-cinq galettes par heure et par machine (par rapport aux quatre-vingt-cinq de l’année dernière). En effet, plus la puissance est importante, moins une galette doit rester longtemps dans la machine.

D’ailleurs, le succès commercial de la machine d’ASML (seule firme présente sur le marché de l’EUV, Canon poursuivant une voie similaire mais distincte) ne cesse de se démentir : la compagnie a déjà livré vingt-sept machines (notamment, à Intel, TSMC, GlobalFoundries ou encore Samsung), plus trois ces trois derniers mois ; huit autres ont été précommandées. Globalement, ASML annonce un chiffre d’affaires de presque trois milliards d’euros pour ces ventes, à raison de cent millions l’unité.

Les fabricants qui passent à l’EUV avec ce genre de machines n’ont pas uniquement pour objectif de graver plus finement leur silicium : pour une finesse équivalente, l’EUV devrait permettre de limiter la complexité du processus de fabrication. Actuellement, il faut une série d’expositions de la même galette de silicium (trois ou quatre fois) pour atteindre les finesses d’une dizaine de nanomètres ; grâce à l’EUV, il suffirait d’une seule exposition — l’avantage étant aussi en temps de fabrication pour le même nombre de puces.

Sources : Chipmaschinenausrüster: ASML demonstriert 250-Watt-EUV-System, ASML Claims Major EUV Milestone.

Qt Creator 4.4 Beta

La nouvelle mouture de Qt Creator, numérotée 4.4, s’approche : la préversion Beta est maintenant sortie. Au niveau de l’éditeur textuel, elle fournit maintenant des annotations à même le code : des avertissements et des erreurs en provenance du modèle de code Clang, des marque-pages. Ainsi, toutes ces informations sont disponibles sans devoir déplacer la souris sur une ligne mise en évidence ou sur le marqueur du côté gauche.

Au niveau de la refactorisation du code C++, le renommage d’un symbole propose automatiquement de renommer le fichier (s’il porte le même nom), ainsi que les fichiers liés. Le modèle de code Clang (s’il est activé) est maintenant aussi utilisé pour mettre en surbrillance l’identifiant sous le curseur (avant, le modèle de Qt Creator s’en chargeait à tous les coups).

Côté CMake, il devient possible de filtrer les variables lors de la configuration de la compilation. En mode serveur, les fichiers d’en-tête du répertoire racine sont aussi affichés.

Windows CE n’est plus géré par Qt Creator, n’étant plus maintenu depuis belle lurette. L’intégration avec ClearCase est désactivée par défaut.

Voir la liste complète des changements.

Télécharger Qt Creator 4.4 Beta 1.

Le module QtQuick.Shapes fait son apparition avec Qt 5.10

Dessiner des formes arbitraires n’a jamais été chose aisée avec Qt Quick. De base, on ne peut dessiner que des rectangles (avec des bords carrés ou arrondis, au choix). Impossible de dessiner une autre forme, à moins de faire appel à du code JavaScript et l’API Canvas ou de coder soi-même la forme en C++. C’est d’ailleurs l’une des limitations historiques de Qt Quick par rapport à la vue graphique. Avec Qt 5.10, la situation évolue : le module QtQuick.Shapes apporte justement ces éléments manquants… avec une performance inégalée (sauf pour des formes codées en C++).

L’implémentation de ce module a été délicatement pensée. Ainsi, il n’y a aucune pixélisation du rendu : les formes dessinées le sont de manière vectorielles (sans passer par QImage ou un tampon OpenGL), ce qui laisse la possibilité de les afficher avec n’importe quelle résolution, voire de les animer. En effet, l’API est entièrement déclarative et tous les attributs des formes peuvent être animés avec les mécanismes habituels de Qt Quick — sans relancer des calculs inutiles.

Le rendu est implémenté de différentes manières, avec cependant la même API. L’implémentation de base réutilise le moteur de triangulation de QPainter en OpenGL, mais, sur les GPU NVIDIA, il est possible d’utiliser l’extension GL_NV_path_rendering pour accélérer le rendu. Pour le moteur de rendu logiciel de Qt Quick, tout se passe avec QPainter. Dans le futur, il sera ainsi possible d’ajouter un rendu par OpenVG ou Direct3D 12.

Ces formes sont dessinées par un composant Shape, mais la description est effectuée par un ou plusieurs ShapePath. Par exemple, pour dessiner un triangle avec une animation sur la largeur du trait et la couleur de remplissage :

Shape {
    id: tri
    anchors.fill: parent
 
    ShapePath {
        id: tri_sp
        strokeColor: "red"
        strokeWidth: 4
        SequentialAnimation on strokeWidth {
            running: tri.visible
            NumberAnimation { from: 1; to: 20; duration: 2000 }
            NumberAnimation { from: 20; to: 1; duration: 2000 }
        }
        ColorAnimation on fillColor {
            from: "blue"; to: "cyan"; duration: 2000; running: tri.visible
        }
 
        startX: 10; startY: 10
        PathLine { x: tri.width - 10; y: tri.height - 10 }
        PathLine { x: 10; y: tri.height - 10 }
        PathLine { x: 10; y: 10 }
    }
}

Cependant, le module en l’état n’est pas forcément à même de battre la vue graphique en termes de composants à afficher, chaque forme ayant un surcoût en performance à l’affichage — surtout sans accélération graphique, où un trop grand nombre de formes ou d’animations posera rapidement problème. Il est déjà possible de demander le calcul asynchrone de la géométrie, ce qui permet d’afficher rapidement l’interface, les formes Shape venant plus tard, sans retarder le reste de l’interface.

Source : Let There Be Shapes!.

NVIDIA envisage d’intégrer plusieurs puces dans un même boîtier

Les cartes graphiques promettent, de génération en génération, de meilleures performances, de préférence selon une loi géométrique. L’utilité de cette puissance ne se manifeste pas que dans les jeux, là où ces cartes sont les plus utilisées (avec des résolutions qui montent, certains joueurs utilisant plusieurs écrans 4K, sans oublier la réalité virtuelle), mais également dans le calcul de haute performance et l’apprentissage de réseaux neuronaux profonds (pour lesquels les processeurs NVIDIA Volta se spécialise).

Cependant, les procédés de fabrication des processeurs deviennent de plus en plus des obstacles à cette croissance de la performance. Ainsi, un GPU GV100 requiert 815 mm² de silicium, une prouesse technique sur un procédé de fabrication assez récent et aux limites de ce qu’il est possible de faire. Pour continuer à monter en puissance sans devoir utiliser des composants qui nécessitent autant d’étude, un changement de paradigme est requis.

Une exploration de la compagnie, menée avec des utilisateurs de ces accélérateurs (comme le BSC) et des universitaires, tente de quantifier les gains en performance en divisant un GPU monolithique en plusieurs modules, intégrés dans le même boîtier. Par rapport à l’approche traditionnelle, qui est de mettre plusieurs cartes graphiques distinctes dans un même ordinateur, l’idée est de les intégrer au niveau de la puce, avec une structure d’interconnexion de type EMIB, pour former un boîtier MCM (multichip module).

Des approches similaires ont déjà été utilisées dans le passé, notamment pour les Tesla K10 et K80, qui mettent plusieurs processeurs sur une même carte. Cependant, cela pose des problèmes pour répartir la charge entre les différents processeurs : cette communication doit être gérée par le développeur.

Au contraire, la technique proposée fonctionne à un tout autre niveau : les différents modules auraient une taille nettement plus réduite et pourraient communiquer efficacement, étant présents physiquement dans le même boîtier. Chaque module serait nettement plus facile à produire que les GPU de taille déraisonnable comme le GV100 (ces modules auraient une taille réduite approximativement d’un facteur deux). Ainsi, le programmeur pourrait considérer le processeur comme une seule entité, sans devoir gérer des communications entre processeurs.

En termes de chiffres, une telle conception pourrait, d’après des simulations, être 45,5 % plus rapide que le GPU monolithique le plus gros que l’on pourrait envisager de fabriquer, mais aussi 10 % plus rapide qu’un GPU monolithique équivalent (en nombre de cœurs CUDA). Par rapport à une conception utilisant plusieurs processeurs distincts sur la même carte, hypothèse plus réaliste, les gains seraient de 26,8 %.

Les impacts industriels de cette recherche pourraient tomber en même temps que la prochaine feuille de route de NVIDIA (l’actuelle s’arrêtait à Volta), probablement à la prochaine conférence GTC.

NVIDIA n’est pas la seule firme à poursuivre cette direction. AMD a récemment annoncé ses processeurs EPYC, qui utilisent le même mécanisme pour monter en nombre de cœurs. Ils pourraient d’ailleurs l’exploiter également pour la prochaine génération de cartes graphiques, Navi.

Plus de détails : MCM-GPU: Multi-Chip-Module GPUs for Continued Performance Scalability.