Version classiqueVersion mobile
OpenEdition Books

L’informatique du temps et des événements

 | 
Gérard Berry

L’informatique du temps et des événements

Leçon inaugurale prononcée le jeudi 28 mars 2013

Gérard Berry

Texte intégral

1Monsieur l’Administrateur,
Chers collègues,
Mesdames, Messieurs,

2C’est un grand honneur pour moi d’inaugurer la première chaire de plein exercice en infor­ma­tique au Collège de France, après y avoir introduit cette science au sein de la chaire annuelle d’Innovation techno­logique Liliane Bettencourt en 2007-2008, puis inauguré la chaire annuelle d’Infor­ma­tique et sciences numériques en 2009-2010. Je remercie tous ceux qui ont contribué à la création de cette chaire, très importante pour toute la communauté infor­ma­tique française. Je remercie en particulier Pierre Corvol, administrateur du Collège de France jusqu’à septembre 2012, Pierre-Louis Lions, qui a promu et porté cette création, la direction d’Inria pour son implication constante, et Monsieur l’Administrateur Serge Haroche pour sa chaleureuse présentation.

Introduction

Informatique et numérique : quel rapport ?

  • 1 Voir ma leçon inaugurale : Pourquoi et comment le monde devient numérique, Paris, Collège de France (...)

3L’informatique est en train de bouleverser littéralement le paysage mondial, à travers ses applications d’une immense variété, allant du calcul scientifique et de la gestion d’entreprises des années pionnières jusqu’à la conception informatisée des objets de tous les jours, la simulation et la conduite de tous les moyens de transports et processus industriels, les bouleversements de la communication, de l’accès à la connaissance et des loisirs, et maintenant ceux de la médecine et de l’ensemble des sciences – tout cela étant coordonné par Internet1. Nous sommes maintenant au début d’une nouvelle étape, tout aussi importante : l’informatisation massive des objets, dotés de systèmes électroniques complexes sur une seule puce, mus par des logiciels élaborés et connectés sur le grand réseau. C’est cette informatique embarquée qui a constitué le cœur de mon travail académique et industriel depuis le milieu des années 1980. J’y consacrerai largement mes cours.

4Étrangement, l’informatique et ses impacts sont restés largement méconnus en France, que ce soit du grand public, des décideurs ou du système d’enseignement. Les choses semblent cependant changer, comme en témoigne récemment la feuille de route du gouvernement sur le numérique2. Je souhaite préciser la différence entre le mot numérique, dont l’utilisation s’est récemment répandue, et le mot informatique. On peut qualifier de numérique toutes les activités reposant sur la numérisation des données : photographie numérique, communication numérique, économie numérique, art numérique, etc. Mais le cœur de toute activité numérique reste la science et la technologie de l’informatique, qui définit, étudie et implémente le calcul automatique sur l’information numérisée. Le beau mot français informatique gagne d’ailleurs le reste du monde, digital et informatics étant de plus en plus utilisés dans le même sens que numérique et informatique. J’emploierai donc toujours ces mots dans les sens précités. Mon enseignement sera consacré à l’informatique, mais toujours en relation avec ses applications dans un monde numérique de plus en plus varié.

L’enseignement de l’informatique

  • 3 Brevet informatique et Internet (B2I) pour les élèves ; certificat informatique et Internet (C2I) p (...)

5Le statut de l’informatique reste précaire dans l’enseignement général, malgré des progrès récents. Alors qu’elle était entrée au lycée au début des années 1980 sous la forme d’un enseignement de la programmation des ordinateurs, elle a été supprimée en 1991, puis de nouveau en 1999 après un bref retour en 1995. Son enseignement a été ensuite remplacé par une formation limitée aux usages des logiciels, réseaux et objets du monde numérique3. Une telle formation, certes utile, n’a en fait que peu à voir avec un vrai enseignement d’informatique. Si l’on regarde les choses en face, son effet est d’apprendre aux gens à se servir des objets et logiciels conçus et fabriqués ailleurs, principalement aux États-Unis et en Asie. Or, les citoyens comme les décideurs se montrent de plus en plus démunis face aux évolutions du monde numérique, qu’ils n’ont pas les moyens de bien comprendre. Étant par essence toujours en retard d’au moins une évolution, un enseignement limité aux usages n’aura aucun effet sur cette situation. Le vrai enjeu pour tout pays est de faire partie des créateurs du monde de demain, donc de ceux qui concevront et fabriqueront les objets matériels et logiciels qui façonneront ce monde. L’objet du système d’éducation doit être d’enseigner le monde de demain, pas celui d’hier – sauf bien sûr en cours d’histoire.

6Pour comprendre quels sont les ressorts de l’évolution du monde numérique et comment en faire partie en tant qu’acteur, il est indispensable de comprendre ce qu’est l’informatique en tant que science et technique autonomes, avec leurs façons spécifiques de penser et de faire. De même que passer le permis de conduire n’apprend rien sur la mécanique et la physique, apprendre à utiliser un ordinateur n’apprend rien sur l’informatique. Cette question a été identifiée et résolue pour la physique, enseignée depuis bien longtemps, ou pour la biologie, intégrée dans l’enseignement des sciences naturelles, mais pas pour l’informatique. Est-ce parce que la France n’a pas fait partie de ses inventeurs, qu’elle a été le seul pays qui n’a pas construit d’ordinateur après la Seconde Guerre mondiale, et qu’elle semble n’avoir jamais vraiment cru à l’essor du domaine depuis cette époque ?

7La situation n’est heureusement pas bloquée, et il existe des progrès récents significatifs. Une collaboration fructueuse entre chercheurs, enseignants et inspecteurs généraux, initiée en 2008 – et à laquelle j’ai eu l’honneur de participer –, a conduit à la mise en place en terminale scientifique d’un enseignement de spécialité intitulé « Informatique et sciences numériques » (ISN). Cet enseignement a été mis en place à la rentrée 2012 pour une dizaine de milliers d’élèves, et la décision a été prise de l’étendre aux autres terminales. Un nouvel enseignement bien conçu de science informatique va également être instauré en classes préparatoires aux grandes écoles scientifiques.

  • 4 L’enseignement de l’informatique en France : il est urgent de ne plus attendre, Académie des scienc (...)
  • 5 Informatics education: Europe cannot afford to miss the boat : http://www.informatics-europe.org/ne (...)
  • 6 Computing in schools: shutdown or restart? : http://royalsociety.org/education/policy/computing-in- (...)

8En parallèle, plusieurs rapports ont dénoncé les carences de l’enseignement de l’informatique dans plusieurs pays européens, dont un rapport que j’ai eu l’honneur de coordonner à l’Académie des sciences4 et un rapport cosigné par des organisations européennes d’enseignants et de chercheurs auquel j’ai également participé5. Tous constatent la trop faible présence de l’Europe dans ce domaine, le manque criant de professionnels formés en informatique pour l’ensemble des métiers de l’avenir et la nécessité de considérer l’informatique comme une nouvelle discipline autonome. Ils recommandent de l’enseigner à tous les élèves dès l’école primaire et de former les professeurs qui l’enseigneront au même niveau et avec les mêmes exigences que dans les autres disciplines scientifiques. À la suite d’un rapport de la Royal Society sobrement intitulé Shutdown or Restart6, la Grande-Bretagne vient de franchir le pas en décidant de remplacer l’enseignement des usages par un vrai enseignement d’informatique, placé à égalité avec les autres enseignements scientifiques au baccalauréat.

9En France, alors qu’une nécessaire réflexion sur l’enseignement de la science informatique était explicitement mentionnée dans la feuille de route du gouvernement sur le numérique, elle a malheureusement disparu dans le texte de la loi sur la refondation de l’école adoptée le 25 juin 2013. La loi ne parle plus que de formation au numérique en termes d’usage et d’utilisation des outils numériques en pédagogie, sans réelle précision sur ce que cela recouvre. Même s’ils reconnaissent désormais l’importance de l’informatique dans le monde numérique, nos dirigeants semblent s’obstiner à croire encore et toujours que son enseignement n’est pas nécessaire et qu’il suffit de savoir l’utiliser servilement.

10Je souhaite relayer ici le message de toute la communauté informatique française et internationale, qui souhaite l’instauration la plus rapide possible d’un vrai enseignement d’informatique non limité aux seuls usages, bien coordonné avec les autres enseignements ainsi qu’avec les usages, assurant à la fois les « littératies numériques » et la vraie compréhension des phénomènes scientifiques et techniques sous-jacents.

L’approche générale et les sujets du cours

Figure 1. Les composantes de l’informatique

Figure 1. Les composantes de l’informatique

11L’informatique peut être résumée par le schéma de la figure 1. Au centre se trouvent les algorithmes. En haut, les données, provenant d’hommes, de capteurs ou d’autres calculs informatiques. En bas, les machines qui effectuent les calculs, actuellement fondées sur l’électronique binaire du silicium – mais d’autres types de machines à information sont à l’étude –, ainsi que les langages qui servent à transcrire la pensée humaine et à la traduire en instructions « machine ». À droite, les interfaces avec le monde extérieur des humains ou des autres systèmes informatiques : capteurs de données physiques, écrans de visualisation, effecteurs mécaniques, etc. Ce système reboucle sur lui-même : puisque les circuits dépassent le milliard de transistors et les logiciels le million de lignes, ils ne peuvent être conçus et fabriqués qu’à l’aide de systèmes informatiques de grande complexité, qui font eux-mêmes appel à une multitude d’algorithmes écrits dans des langages de programmation variés et traitant de grandes masses de données.

  • 7 Ce choix fait, mon ami Jean Vuillemin m’a montré celui de son cours à l’École polytechnique dans le (...)
  • 8 Serge Abiteboul, Science des données : de la logique du premier ordre à la toile, Paris, Collège de (...)
  • 9 Martin Abadi, La sécurité informatique, Paris, Collège de France/Fayard, coll. « Leçons inaugurales (...)

12Mon travail personnel a surtout concerné le bas du schéma, d’où le titre de ma chaire, « Algorithmes, machines et langages7 ». Sans bien sûr les ignorer, je parlerai peu des aspects liés aux données et à la sécurité, déjà développés respectivement par Serge Abiteboul8 et Martin Abadi9 dans le cadre de la chaire annuelle d’Informatique et sciences numériques.

  • 10 G. Berry, Penser, modéliser et maîtriser le calcul informatique, Paris, Collège de France/Fayard, c (...)

13Le fil conducteur de mon enseignement sera le traitement du temps et des événements dans les systèmes informatiques, domaine où notre pays a tenu un rôle particulièrement innovant dans la recherche et dans l’industrie. Dans mon cours de 2009-201010, j’avais insisté sur la nécessité de modéliser mathématiquement calculs, langages et machines pour les comprendre et les maîtriser. Je continuerai dans cette voie, à travers deux champs d’investigation intimement liés à la pratique : d’une part le traitement explicite du temps et des événements dans les circuits et logiciels embarqués, qui les fait différer assez profondément des systèmes informatiques classiques, et d’autre part les méthodes de preuve formelle de correction des applications, indispensables dès que les bogues peuvent avoir des conséquences coûteuses ou dramatiques – que l’on pense aux avions, aux voitures et aux systèmes médicaux implantés dans le corps.

14Enfin, je ne souscrirai pas aux compartimentages traditionnels de la communauté scientifique, qui réunit trop rarement dans les mêmes journaux et conférences matériel et logiciel, programmation d’Internet et programmation de systèmes embarqués, etc. Je m’attacherai au contraire aux similarités et aux complémentarités de ces domaines. En particulier, je ne ferai pas de grande distinction entre matériel et logiciel, ayant personnellement un goût égal pour les deux domaines. Même si les vocabulaires techniques et les objets finaux y sont très différents, les questions de fond ainsi que les solutions conceptuelles et techniques y restent similaires. Et je montrerai que des idées et des façons de faire inventées pour les circuits et les logiciels embarqués sont tout aussi pertinentes dans les domaines inattendus que sont la composition et l’interprétation musicale ou encore l’orchestration et la coordination d’applications web.

Le temps et les événements en informatique

15Le rôle du temps en informatique est souvent vu à travers le seul prisme de la complexité algorithmique : minimisation du temps de cycle d’un circuit, du temps de calcul d’un programme ou du temps de propagation de l’information dans un réseau, échange temps/espace dans les algorithmes et leurs implémentations, etc. Ces questions sont évidemment essentielles, car le coût et le bénéfice final d’une application résultent d’un équilibre subtil entre temps de calcul, taille de la mémoire et énergie dépensée. Mais les algorithmes et les langages de programmation classiques ne parlent pas eux-mêmes du temps, qui reste une considération externe ne faisant pas partie des spécifications fonctionnelles. C’est aussi vrai de la gestion des événements auxquels répondent les programmes ou qu’ils engendrent, souvent traitée ad hoc.

16Pourtant, la gestion du temps et des événements doit être un paramètre explicite et central de la conception et de la spécification de nombreuses applications. Elle constituera l’originalité de mon cours, à travers cinq domaines d’études :

  • La conception des circuits digitaux, dont l’architecture globale et la micro-architecture locale font appel à un combat explicite contre le temps. Un nouveau problème est apparu récemment : pour valider la conception d’un circuit et fabriquer ses logiciels applicatifs avant même que le circuit n’existe physiquement, il devient indispensable de le simuler efficacement par logiciel, ce qui pose des problèmes nouveaux quant à la relation entre temporalité du circuit physique et temporalité de sa simulation.

  • Les systèmes de contrôle en temps réel. Le pilotage informatique d’un avion doit se faire au temps requis par son aérodynamique et non au temps propre de l’ordinateur, les valeurs et événements déclenchés par les capteurs ou par le pilote devant être traités sans délai. L’informatique est ici fortement liée à l’automatique, qui est la science du contrôle. L’informatisation généralisée des transports et objets de toutes sortes donne à ce domaine une importance toujours croissante.

  • La simulation de grands systèmes (automobile, avion, trafic aérien, réseaux informatiques, etc.), indispensable pour leur conception assistée par ordinateur. Elle a souvent le temps et les événements externes pour paramètres principaux. Une difficulté majeure est de coordonner des simulateurs spécifiques aux parties du système qui n’ont pas forcément la même vision du temps et des événements. La même difficulté se retrouve dans les systèmes de réalité virtuelle et dans les jeux vidéo.

  • L’orchestration d’applications web. Au lieu d’afficher une page HTML, beaucoup de sites web proposent des services procéduraux retournant des données formatées. Des applications étonnamment riches peuvent être construites en composant ces services élémentaires. Mais ils peuvent retourner des erreurs ou avoir des temps de réponse imprévisibles. Orchestrer l’interface utilisateur, les questions adressées aux services et la gestion de leurs réponses en traitant toutes les erreurs possibles est un problème de même nature que ceux présentés ci-dessus.

  • L’informatique musicale, où les compositions contemporaines mêlent souvent interprètes humains et sons engendrés par ordinateur. Une question importante est la liaison harmonieuse entre interprètes humains et sons de synthèse, en particulier pour l’harmonie mutuelle du tempo et du phrasé. Une autre question fascinante est la conception de « partitions algorithmiques » utilisables à la fois par les compositeurs, les interprètes et les ordinateurs.

17Ces sujets sont socialement très distincts, voire étanches, mais ils partagent techniquement beaucoup. Nous allons voir qu’il est très utile d’utiliser les idées et façons de faire des uns chez les autres.

18D’autres domaines d’intérêt pourront apparaître au cours des années, en particulier en relation avec les neurosciences et la biologie, où l’étude des phénomènes temporels est centrale.

Parler du temps, mais de manière formelle

19Dans tous les domaines précités, il est nécessaire de parler explicitement du temps et des événements dans les spécifications et les programmes. Or, ni la langue parlée ni les formalisations mathématiques classiques ne sont suffisamment habiles pour nous. Expliquons pourquoi, en étudiant d’abord le grand écart entre la physique du temps et sa perception psychologique.

La mesure du temps

  • 11 À l’exception du sultanat de Jaipur, en Inde, où le sultan avait décrété l’unification du temps dan (...)

20La mesure du temps se fonde sur des phénomènes implacables, comme les mouvements du soleil, de la lune ou des étoiles. L’astronomie étudie depuis toujours leurs régularités et leurs irrégularités, qui sont complexes et ont donné partout naissance à des cosmogonies locales imaginatives. La mesure par les astres a été suivie d’une longue série d’inventions plus maniables, de la clepsydre à l’horloge à balancier, puis de la pendule à ressort aux montres à gousset. La première mesure vraiment précise a été fournie en 1773 par le chronomètre H5 de Harrison, qui ne dérivait que de quelques secondes sur une traversée de l’Atlantique et permettait, pour la première fois, de mesurer précisément la longitude. Pourtant, l’unification des temps locaux des villes d’un même pays est bien postérieure, imposée seulement par les besoins du train et du télégraphe11.

21Les chronomètres mécaniques puis électroniques se sont améliorés avant d’être supplantés par les horloges atomiques, qui définissent actuellement la seconde à 10−10 près et sont à la base du système de positionnement GPS. Les horloges les plus récentes atteignent une précision meilleure que 10−17, soit quelques secondes sur l’âge de l’univers. La seconde est aussi devenue une unité quasi universelle : elle sert à définir le mètre depuis 1983 et pourrait bientôt définir aussi le kilogramme. Je n’irai pas plus loin ici, car il existe de nombreux ouvrages sur la merveilleuse histoire de la mesure du temps et ses conséquences.

Le parler du temps

  • 12 G. Berry, « Manifeste pour la réhabilitation du pavillon des poids et mesures », Viridis Candela, c (...)

22La perception du temps est indépendante de sa mesure physique, comme le montre immédiatement l’étude de la langue parlée du temps12. Elle est très personnelle : « je prends mon temps », « il m’a fait perdre mon temps ». On y trouve des expressions étrangement élastiques comme « de longues années », qui tend curieusement à supplanter « de nombreuses années », « le temps passe vite », voire « le temps passe de plus en plus vite ». Ces expressions que tout le monde emploie n’ont pourtant aucun sens physique : en quelle unité pourrait-on mesurer la vitesse et l’accélération du temps ?

23Le passage du temps est souvent représenté par une flèche, avec le passé à gauche, le futur à droite, et le présent au milieu. Il y a un seul passé et un seul avenir, le nôtre. Un instant est un point de cette flèche, et le présent est l’instant que nous vivons. C’est un instant fugace qui se déplace sans cesse, coincé entre le futur et l’avenir.

  • 13 Surtout dans sa version sud-américaine « mañana por la mañana ».

24Quand on parle du temps, on fait donc généralement un arrêt sur image, en considérant un présent donné. Le passé lointain est appelé la nuit des temps, dont on ne sait jamais vraiment si elle est à l’infini ou pas. Viennent ensuite avec nostalgie le bon vieux temps, le bon temps, etc. Quand on se tourne vers le futur, on prévoit de s’y mettre dès demain, dont la signification est plutôt lâche13, ou alors, à la Saint-Glinglin, synonyme de quand les poules auront des dents.

25Une durée est un morceau de temps d’une certaine longueur. Le nommage des durées est fort joli : le laps de temps, le bout de temps, le bon bout de temps. Dans le Sud, quand on attend longtemps, on a le temps de tuer un âne à coups de figues. Les noms des durées courtes semblent subir un allongement syntaxique inversement proportionnel à la durée exprimée, depuis illico presto jusqu’à en moins de temps qu’il ne faut pour le dire. Et une semaine dure huit jours, alors que deux semaines en font quinze !

26Pour nommer un instant, on le date en qualifiant la durée écoulée avant ou après un événement donné, par exemple la naissance supposée de Jésus-Christ. Mais la numération du temps montre que nous n’avons pas complètement intégré le zéro dans notre vocabulaire : l’année démarre le 01/01 à 00 h 00 ! Quant aux événements, ils représentent quelque chose qui se passe à un instant donné, et qu’on peut donc dater. Les événements sont souvent périodiques : hebdomadaires, mensuels, etc.

La flèche mathématique du temps

27Le langage mathématique du temps est moins poétique. On représente la flèche du temps comme l’ensemble ℜ des nombres réels, avec −∞ pour la nuit des temps et +∞ pour les calendes grecques. Un zéro posé quelque part donne l’origine. Un instant se note toujours t, t’, etc. Un intervalle de temps se note [t,t’] avec t ≤ t’ et peut éventuellement être ouvert à un bout ou à l’autre ; il a pour durée t’t. Une petite différence de temps se note δ, une minuscule Δt. Les objets considérés sont souvent des fonctions du temps, continues, intégrables, différentiables, etc., mais aussi des événements nommés qui adviennent à certaines dates, appelées occurrences de l’événement. Un événement est périodique s’il a des occurrences régulièrement espacées dans le temps, sporadique sinon. Une occurrence d’un événement e à l’instant t précède une occurrence de e’ à t’ si t ≤ t’ et les deux occurrences sont simultanées si t’. Savoir si une occurrence d’un événement e cause une occurrence d’événement e’ est essentiel, mais dépend de chaque système. Si c’est le cas, l’occurrence de e doit précéder celle de e’ ou éventuellement lui être simultanée, sous peine de graves paradoxes temporels.

28Cette représentation brutale est efficace dans des disciplines comme la physique classique, le traitement du signal ou l’automatique (control theory en anglais). Mais elle va s’avérer franchement insuffisante pour nous. Notons déjà que la distinction entre événements et occurrences d’événements est souvent laissée floue, voire absente. Pourtant, elle est essentielle quand on parle de causalité. Par exemple, si chaque occurrence de e cause la suivante, est-il légitime de dire que e cause e ?

La logique temporelle linéaire

29Utiliser systématiquement des dates réelles conduit souvent à des spécifications formelles peu agréables. Considérons par exemple le dicton après la pluie, le beau temps. On peut l’écrire mathématiquement ∀t.t’Pluie(t) ⇒ BeauTemps(t’). Mais pourquoi s’encombrer de t et t’ dont nous nous fichons éperdument ? L’idée des logiques temporelles est d’introduire des modalités pour supprimer les quantificateurs et les variables temporelles, la valeur logique d’une formule modale devenant dépendante de l’instant considéré. En logique temporelle linéaire (LTL), notre dicton s’écrit □(Pluie ⇒ ◊BeauTemps), où □ se lit toujours et ◊ se lit un jour. Reste une question non triviale que nous laisserons aux météorologues : la pluie cause-t-elle le beau temps, ou ne fait-elle que le précéder ? Ni la notation mathématique standard ni la logique LTL ne savent trancher cette question. La causalité est l’essence des systèmes temporels, mais en parler n’est jamais trivial.

30La logique temporelle est moins simple qu’il n’y paraît. Le dicton amour un jour, amour toujours ne s’écrit pas naïvement ◊Amour ⇒ □Amour, car cette formule signifie « si nous devenons amoureux un jour à partir de maintenant, alors nous sommes en fait amoureux toujours à partir de maintenant » ! L’écriture correcte est ◊Amour ⇒ ◊□Amour « un jour amour implique un jour toujours amour » – ce qui n’est pas nécessairement vrai non plus.

Le cône du temps et la logique temporelle arborescente

31Quand on organise son futur ou quand on étudie un système informatique, on essaie souvent d’envisager tous les cas possibles étant donné le passé et le présent. Un raisonnement typique est « à partir de maintenant, si je fais A alors je vais obtenir B au bout d’un temps assez long ; en revanche, comme j’ai eu C dans le passé, faire D me donnera peut-être B mais sûrement E bien plus vite ». Le temps prend alors une forme conique, avec un passé filiforme et un avenir ouvert vers des exécutions multiples. Les logiques temporelles arborescentes permettent d’en parler.

Figure 2. Deux machines à café/thé

Figure 2. Deux machines à café/thé
  • 14 Voir par exemple Z. Manna et A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems: Spec (...)

32Considérons les spécifications des machines à café/thé de la figure 2. La machine anglaise, à gauche, accepte une pièce d’un euro (c’est une importation) et verse du mauvais café ou du bon thé selon qu’on appuie sur le bouton C ou le bouton T. La machine française, à droite, accepte un euro puis choisit elle-même si elle va verser du bon café ou du mauvais thé, ne laissant actif qu’un des deux boutons C ou T. En faisant abstraction du goût du liquide délivré, ces deux machines sont équivalentes si on raisonne linéairement, car seulement capables d’itérer des suites d’actions €.C.Café et €.T.Thé, ce qu’on écrit informatiquement (€.C.Café + €.T.Thé)*. Pourtant, elles ne sont pas équivalentes à l’usage, la machine française ayant un côté frustrant pour l’utilisateur puisqu’elle ne lui laisse pas le choix de sa boisson. On peut distinguer les deux machines par la formule suivante de logique temporelle arborescente : AG(€ ⇒ EF(Café) ∨ EF(Thé)), qui se lit « dans tout état, mettre un euro permet d’obtenir du café par un certain chemin ou du thé par un autre chemin ». Cette propriété est satisfaite par la machine anglaise, mais pas par la machine française. Les modalités AG et EF sont de type différent : AG(F) veut dire « pour tout état, la formule F est vraie » alors que EF(F) veut dire « à partir de l’état courant, il existe un chemin conduisant à un état où F est vraie ». Je ne parlerai pas d’avantage des logiques temporelles, renvoyant le lecteur à la littérature sur le sujet14.

Le double cône du temps

33On peut aussi revisiter son passé. Une personne perpétuellement indécise raisonne ainsi : « si je m’étais débrouillé pour avoir A’ au lieu de A dans le passé, j’aurais eu B plus facilement, mais je ne suis pas sûr que j’aurais eu C ». Ici, le temps prend une forme biconique, avec un cône du passé convergent vers le présent et un cône standard pour le futur.

Élargir la notion de temps

34Nos besoins informatiques vont nous conduire à élargir la notion de temps. Étudions les en général, avant de passer à des exemples plus concrets.

Temps propre, temps coordonné

35La plupart du temps, on ne parle que d’un seul temps, supposé universel. Le meilleur que nous ayons sous la main pour l’instant est donné par le GPS. Son temps est la clef de la mesure de position, dont le principe est simple : les satellites GPS envoient de façon répétitive leur heure courante dans des messages électroniques. Quand le récepteur reçoit un message, il compare l’heure d’émission à l’heure de réception, et en déduit sa distance au satellite puisque la position des satellites et la vitesse de la lumière sont connues. En utilisant plusieurs satellites en en calculant l’intersection des sphères qu’ils déterminent, on sait où on est.

36Mais la réalisation est loin d’être aussi simple. D’abord, contrairement aux satellites, le récepteur GPS ne contient pas d’horloge atomique, ce qui lui impose de calculer en dimension 4 avec au moins quatre satellites pour déterminer à la fois la position et l’heure. Mais, le temps absolu de la mécanique newtonienne n’existe pas : le temps dépend de l’observateur, de sa vitesse, de sa gravité locale, etc. Les physiciens distinguent donc le temps propre d’un observateur et le temps coordonné, engendré par la liaison entre plusieurs observateurs. Il faut fabriquer un « bon » temps coordonné en synchronisant très finement entre elles les horloges des satellites GPS, ce qui fait appel aux relativités restreinte et générale. Le récent exemple d’une subtile erreur de synchronisation d’horloges ayant conduit à une surestimation de la vitesse des neutrinos15 montre bien la difficulté technique de la synchronisation d’horloges. Mais notons que les horloges les plus récentes comme celle de David Wineland, prix Nobel 2012 de physique avec Serge Haroche, est si précise qu’elle permet de mettre en évidence la modification du temps par la gravité, simplement en séparant deux exemplaires identiques de 30 centimètres en hauteur !

37Les problèmes de synchronisation d’horloges et de temps coordonné sont fréquents et essentiels en informatique. Dans une voiture, on cherche à coordonner les freins, la suspension et la direction, par exemple pour maintenir l’assiette quand on freine dans un virage. Ceci demande un alignement temporel précis des différents calculateurs et du réseau informatique qui les connecte. En génie logiciel, pour organiser la compilation des fichiers sources d’un programme, l’utilitaire make provoque la recompilation d’un code source s’il est plus récent que son code objet. Mais pour accélérer la compilation de programmes de grande taille, on utilise souvent plusieurs ordinateurs en parallèle. Dans ce cas, les horloges de ces machines doivent être finement synchronisées pour que des recompilations ne soient pas oubliées. Citons enfin, pour mémoire, les transactions financières à la milliseconde, dont on peut se demander si elles seront vraiment contrôlables et si elles servent vraiment la société autant que leurs auteurs.

Horloges multiples et irrégulières

38Au xxe siècle, les circuits étaient suffisamment petits et suffisamment simples pour être séquencés par une seule horloge, distribuée partout par un arbre d’horloge superbement géométrique. Ce n’est plus le cas. Grâce à l’intégration d’un nombre de plus en plus grand de transistors par unité de surface (selon la loi de Moore, qu’applique l’industrie pour doubler le nombre de transistors par puce tous les deux ans), les systèmes sur puces (systems on chips ou SoCs) modernes incorporent des sous-circuits variés, cadencés par des horloges multiples pas forcément synchronisées : microprocesseur général, processeur de signal numérique (digital signal processor ou DSP), accélérateur graphique, décodeur MPEG, etc. Ces sous-circuits échangent des informations par des systèmes de files d’attente ou des réseaux sur puces, dont certains sont à temps prévisible et d’autres non. De plus, pour économiser l’énergie des appareils autonomes, on cherche à ralentir les calculs autant que possible en baissant le voltage et en ralentissant l’horloge : il ne sert à rien de calculer le son plus vite que la musique. Enfin, les circuits asynchrones ou élastiques fonctionnent dans un mode beaucoup plus dynamique, sans horloge du tout.

39Les systèmes embarqués évoluent aussi vers le multi-horloge, avec de plus en plus d’unités de commande électroniques (electronic control units ou ECUs) connectées par des réseaux à temps contrôlé (TTP, FlexRay) ou non (CAN). Nous avons déjà mentionné le freinage en virage. La synchronisation temporelle est tout aussi essentielle pour les simulateurs de grands systèmes, construits par couplage de simulateurs locaux utilisant leurs horloges de calcul propre.

40Pour tous ces systèmes, il est très important de savoir si les différentes horloges sont synchronisées ou non, et, si elles ne le sont pas, comment se font les transferts d’information entre zones d’horloges distinctes.

Temps logique, temps physique

41Dans un autre registre, remarquons que deux notions de temps sont souvent en compétition dans la vie courante. Pour un paysan, se repérer par rapport au lever du soleil, à son passage au zénith ou à son coucher est souvent plus pertinent que d’utiliser sa montre, sauf bien sûr pour les relations avec l’administration et la ville. Ces événements peuvent être vus comme définissant un temps logique défini par leur répétition reproductible mais irrégulière vis-à-vis du temps physique. Leur précision physique n’est pas forcément grande, comme l’indique l’étymologie du beau mot tintamarre : les ouvriers de la vigne parisienne étaient très organisés dans les temps anciens, et ils revendiquaient une vraie pause de midi. Mais cette heure du passage du soleil à son point le plus haut est difficile à déterminer. Quand il la sentait bien, le chef du syndicat prenait une pierre et faisait tinter le fer de sa houe, appelée marre. Tous les autres vignerons faisaient pareil, ce qui produisait un superbe tintamarre !

42Avec ses blanches, ses noires et ses croches, une partition musicale ne spécifie également qu’un temps logique, dont la transformation en temps physique par l’interprète ne sera pas forcément conforme, voire surtout pas conforme. Vive l’inégalité baroque et le swing du jazz qui jouent avec le temps ; à bas le boum-boum électronique à 120 pulsations du disco !

  • 16 Jordi Cortadella,« Elastic circuits, blending synchronous and asynchronous technologies », séminair (...)

43De même, dans les circuits modernes, l’horloge n’est plus forcément régulière : la ralentir autant que possible est un excellent moyen d’économiser l’énergie. Ceci n’empêche pas de travailler en temps logique lors de la conception du circuit, en faisant comme si le temps était régulier. Un des séminaires du cours 2013-2014 présentera les circuits élastiques16, une merveilleuse façon de coordonner souplement temps logique et temps physique. En programmation de logiciels embarqués, on utilise aussi souvent des temps logiques qu’on ne corrèle finement au temps physique qu’à l’implémentation, voire lors de l’intégration système.

Temps multiforme

44Nous pouvons aller plus loin en appelant temps logique tout quasi-temps défini par la répétition d’un événement donné, et utiliser pour en parler le même vocabulaire et la même logique que pour le temps physique. Quand on marche vers un village, les mètres et les pas se répètent tout autant que les secondes. Il n’y a pas de différence entre dire que le village est à 10 minutes ou dire qu’il est à 10 kilomètres, à 10 000 pas (10 kilopas) ou à 10 000 battements de cœur (10 kilobats). L’ensemble des temps logiques constitue alors un temps multiforme. Le langage de programmation Esterel, que nous décrirons brièvement plus loin, a été conçu pour programmer les applications en jouant avec cette idée de temps multiforme. Il s’applique aussi bien aux applications de contrôle en temps-réel qu’à la spécification et la synthèse de circuits multi-horloges, pour lesquels chaque horloge est vue comme définissant son propre temps logique.

  • 17 Voir les deux derniers séminaires du cours 2012-2013 donnés le 4 juin 2013 : Philippe Manoury, « La (...)

45Notons que le temps de la musique est également multiforme, car des temps logiques indépendants sont introduits par la répétition des motifs et des thèmes, par celle des mouvements, et aussi à un rythme plus rapide par les ornementations interne des notes. Il n’est donc pas étonnant que les musiciens et les chercheurs en informatique musicale de l’Ircam s’intéressent à un langage comme Esterel et en utilisent les notions principales dans des formalismes expérimentaux de partitions algorithmiques17.

Temps continu, temps discret

  • 18 Ce paradoxe n’en est d’ailleurs pas vraiment un : il montre simplement qu’il n’est pas cohérent de (...)

46L’hypothèse de continuité du temps est loin d’être évidente. La physique moderne ne le voit déjà plus forcément comme continu aux échelles élémentaires – ni même comme devant rester un concept primitif, ce qui ne nous concerne pas ici. Plus grave pour nous, la notion de datation par les nombres réels n’est pas naturelle en informatique, car les nombres réels dotés d’une infinité arbitraire de décimales ne sont pas calculables. Nous avons donc aussi besoin d’échelles de temps discrètes, fondées sur des ensembles dénombrables et calculables d’instants et d’événements discrets. Pour rester compatible avec la physique usuelle, on peut continuer à utiliser des nombres réels pour désigner les dates discrètes. Mais il faut alors se méfier du paradoxe de Zénon (ou d’Achille et la tortue), qui se manifeste dès qu’on essaie de placer une infinité d’instants discrets entre deux instants réels successifs18. On peut aussi construire directement une vision linéaire du temps discret en ordonnant totalement tous les événements, par exemple à l’aide d’une date entière ; c’est ce qu’on appelle l’estampillage temporel, fort utile en télécommunications. Mais on peut aussi n’ordonner les événements que partiellement, sans nécessairement définir de relation de précédence entre deux instants. Dans ce cas, la précédence devient un ordre partiel. C’est ce qu’on fait souvent dans les systèmes distribués asynchrones, où les acteurs ne partagent pas de temps commun et où la transmission de messages peut prendre un temps quelconque. L’estampillage est alors en temps logique.

L’épaisseur de l’instant

47Dans le langage courant, la notion d’événement est d’acception très large, et quelque peu différente de la notion mathématique d’instant sans épaisseur. Par exemple, on enseigne que Charlemagne a été couronné en l’an 800. Cette phrase du langage courant peut et doit être vue à plusieurs échelles. À gros grain, l’an 800 est un instant dans l’histoire, et Charlemagne a été couronné à cet instant. Mais l’an 800 s’est composé de 366 jours, eux-mêmes de 24 heures, etc. Et le couronnement de Charlemagne a nécessité une fort longue suite d’opérations élémentaires, donc d’événements distincts à une échelle plus fine. Une très belle expression du langage usuel montre bien l’essence de ce double regard : « l’espace d’un instant ».

48En informatique, et en particulier pour les circuits et les langages synchrones du type d’Esterel, cette dualité événement abstrait/suite d’événements concrets joue un rôle central. Suivant les besoins, un même événement peut être vu comme atomique, donc indécomposable, ou bien comme agrégé, représentant alors l’abstraction d’une suite d’événements plus élémentaires. Nous jonglerons entre ces deux visions d’un événement : dans la vision atomique, nous considérerons que l’événement agrégé se passe en temps nul, ce qui sera redoutablement efficace mathématiquement parlant. Pour l’implémentation, nous devrons détecter ou fabriquer cet événement « pour de vrai », donc en temps non nul. La clef de la correction de ce double mécanisme sera le contrôle précis du vrai déroulement temporel, qui permettra d’assurer que l’abstraction du temps nul est bien raisonnable en pratique pour le domaine considéré.

La question du déterminisme

49La différence entre déterminisme et non-déterminisme est importante pour nos systèmes. Un système est déterministe si ses réactions sont toujours identiques dans des situations identiques, non-déterministe sinon. Les entrées du système ne sont bien sûr pas connues à l’avance ; c’est ce qu’on appelle leur non-déterminisme externe. Mais, si le système doit réagir toujours de la même façon aux mêmes entrées, il ne doit pas contenir de non-déterminisme interne.

50Par exemple, les circuits synchrones sont toujours déterministes, et le freinage d’une voiture doit l’être tout autant. À l’inverse, il est important que la transmission des paquets sur Internet soit globalement non-déterministe, pour qu’elle soit robuste aux pannes et aux reconfigurations. Les deux concepts sont aussi pertinents l’un que l’autre, mais dans des situations différentes. Le déterminisme est le plus souvent requis dans les systèmes embarqués de haute sécurité, dont le comportement doit être parfaitement prévisible : fusées, avions, trains, voitures, etc. À l’inverse, c’est le non-déterminisme intrinsèque d’Internet qui lui a permis de renverser le réseau téléphonique classique, d’une logique quasi déterministe : préserver le déterminisme interne d’un tel réseau demande beaucoup de centralisation d’informations, complique les reconfigurations, et passe mal à l’échelle. Le côté dynamique ou statique des systèmes est également important ici : le nombre de nœuds d’un réseau informatique est en évolution constante, alors que le nombre d’ailes d’un avion déterministe doit rester résolument fixe.

51La distinction déterminisme/non-déterminisme était très sévère au xxe siècle. C’est moins le cas maintenant, à cause du changement d’échelle généralisé des systèmes informatiques, et de nombreux hybrides apparaissent. Les systèmes électroniques sur puce modernes combinent des composants localement synchrones et déterministes de façon asynchrone et non-déterministe, et le contrôle distribué de système embarqué fait la même chose en combinant de façon (faiblement) non-déterministe des logiciels localement déterministes. Mais la formalisation, la réalisation et surtout la vérification de tels systèmes pose des problèmes considérables et loin d’être tous résolus. Ils seront étudiés dans la deuxième année du cours.

La causalité est-elle transitive ?

  • 19 Merci à Jean Krivine pour cet excellent exemple.

52Les relations de causalité qui relient des événements ou leurs occurrences dépendent essentiellement des applications. Mais la causalité doit obéir à une règle générale : « A cause B » implique toujours « A précède B », au sens large car A et B peuvent aussi être simultanés. La question de la transitivité de la causalité est beaucoup moins claire. On considère souvent que « A cause B » et « B cause C » impliquent naturellement « A cause C ». C’est trivial si on interprète « A cause B » comme « A fait partie des causes de B », mais il peut y avoir d’autres acceptions. Par exemple, on peut dire « il pleut, donc j’ouvre mon parapluie » puis « mon parapluie est ouvert, donc je reste sec ». Mais il serait assez étrange de dire « il pleut, donc je reste sec19 » ! Ici, on considère que pour qu’un événement A soit une cause de B dans une séquence d’événements, il faut que la présence de A soit indispensable pour celle de B. Or, il n’est pas indispensable qu’il pleuve pour qu’on reste sec quand on a ouvert son parapluie ! Cette notion de causalité est par exemple utilisée pour l’étude des réseaux de construction de protéines dans la cellule en biologie structurale. Formaliser les différentes sortes de causalité pertinentes reste un problème ouvert de premier intérêt.

Des circuits aux systèmes sur puces

53Les circuits électroniques sont le moteur de l’informatique. Ils illustrent aussi parfaitement plusieurs des questions centrales concernant le temps. Commençons par l’épaisseur de l’instant et l’abstraction associée.

Figure 3. FullAdder, l’additionneur 3 bits

Figure 3. FullAdder, l’additionneur 3 bits

54Le circuit d’addition FullAdder de la figure 3 calcule la somme s et la retenue r des trois bits d’entrée a, b et c. C’est un circuit combinatoire, composé de fils électriques portant des potentiels notés 0/1 et de portes logiques calculant une composition booléenne de leurs entrées. Un tel circuit se voit de deux façons. Dans la vue électrique, le calcul se fait par propagation de voltages dans les fils et les portes, avec des délais déterminés par leur technologie et leur placement physique. Si on maintient les entrées d’une porte à 0 ou 1, ses sorties passent au voltage déterminé par la fonction de la porte au plus tard après son délai. Le système est série/parallèle : les potentiels sont diffusés en parallèle par les connexions et les fils, mais les délais s’additionnent quand les fils et les portes sont connectés en série. Si le graphe du circuit est acyclique, comme pour l’additionneur, les délais s’additionnent donc sur chaque chemin des entrées vers les sorties. Le délai maximal entre une entrée et une sortie quelconques est appelé délai critique ; il est typiquement d’une fraction de nanoseconde pour FullAdder. En fixant les entrées, on est sûr que toutes les sorties restent constantes après le délai critique, et qu’elles ont bien les valeurs booléennes souhaitées ; des transitions intermédiaires peuvent se produire sur le chemin, mais elles sont devenues invisibles. La vision duale est la vision logique abstraite. Les portes sont vues comme de simples opérateurs booléens ; le circuit devient un système d’équations booléennes à résoudre et les équations sont vues comme simultanées et résolues en un instant abstrait sans épaisseur. Le modèle logique est bien plus simple pour concevoir, raisonner et optimiser, car il permet toutes les optimisations et vérifications booléennes. De son côté, le modèle vibratoire fonctionnellement équivalent implémente précisément l’épaisseur de l’instant abstrait. Les concepteurs parlent de fonctions logiques, les électroniciens de fils et de transistors, et l’information-clef qu’ils échangent est le délai critique. Cette coopération bien organisée a permis la fantastique progression des circuits intégrés et le développement de systèmes de synthèse physique des circuits à partir de spécifications de haut niveau.

55Mais l’addition 1-bit ne suffit évidemment pas, et il faut additionner des nombres, représentés par des mots de 32 bits par exemple. Pour cela, il y a deux grandes méthodes : travailler dans l’espace ou travailler dans le temps. Pour additionner dans l’espace, on peut mettre 32 additionneurs 1-bit FullAddern en parallèle, les fils ci propageant les retenues comme à l’école : on pose c0 = 0 et cn = rn−1 pour > 0. C’est simple, mais inefficace car le délai critique est multiplié par le nombre de bits. On peut faire bien mieux en échangeant le temps contre l’espace. Par exemple, l’additionneur de Von Neumann procède par dichotomie et spéculation. On coupe chaque entrée de 2n bits en deux parties de n bits, poids faibles et poids forts. On additionne en parallèle les poids faibles et les poids forts, mais en effectuant spéculativement deux additions pour les poids forts, respectivement avec retenue entrante 0 ou 1. On sort les n premiers bits de la somme des poids faibles comme poids faibles du résultat, et on utilise la retenue des poids faibles pour sélectionner la bonne somme des poids forts, déjà disponible puisque les deux sommes potentielles ont été calculées simultanément. L’autre somme des poids forts est inutilisée. Chaque sous-additionneur est bien sûr construit récursivement de la même manière. Au total, on utilise plus d’espace et plus d’énergie à cause des calculs inutiles, mais on va beaucoup plus vite : l’addition se fait en temps physique log2(n) au lieu de n, ici donc en temps 5 au lieu de 32.

Figure 4. L’additionneur sériel (2-adique), où ++ désigne FullAdder

Figure 4. L’additionneur sériel (2-adique), où ++ désigne FullAdder
  • 20 Voir le cours « Circuits et nombres 2-adiques, une nouvelle vision de l’échange temps-espace », 9 a (...)

56La méthode orthogonale est de faire l’addition dans le temps, en utilisant le circuit synchrone montré dans la figure 4, appelé additionneur sériel. Un seul additionneur élémentaire est couplé à un registre, ou point mémoire élémentaire. Le registre est contrôlé par une horloge, qui émet des signaux carrés dont seul le front montant nous intéresse ici. L’intervalle entre deux fronts montants est appelé cycle, et sa durée doit être supérieure au délai critique de l’additionneur. On présente les nombres un bit par cycle, poids faibles d’abord. À chaque cycle, l’additionneur calcule la somme et la retenue courante. À chaque arrivée du front montant de l’horloge, la retenue courante est stockée dans le registre et devient la retenue entrante pour le cycle suivant. Remarquons qu’il n’y a plus aucune limite au nombre de bits traitables, qui peut sans problème être rendu infini. Or, les nombres écrits en commençant par les poids faibles, mais avec une infinité de chiffres, jouent un rôle fondamental en mathématiques, où ils sont appelés nombres p-adiques, l’entier p étant la base de la numération. Écrits en base 2, les nombres 2-adiques qui nous concernent permettent d’unifier arithmétique et logique booléenne ; dans la figure 4, ils sont caractérisés par l’index initial 2 devant le développement infini. Contrairement aux réels, ils n’ont jamais reçu d’interprétation dans la physique classique, mais Jean Vuillemin a montré qu’ils s’avèrent constituer le modèle naturel des circuits arithmétiques20. Dans cette « physique synthétique » qu’est l’informatique, les nombre réels n’existent pas et les nombre 2-adiques deviennent physiques à leur place.

57Quand tous ses registres sont contrôlés par la même horloge, un circuit est dit synchrone. Le cours étudiera bien d’autres aspects des circuits synchrones impossibles à décrire ici : optimisations par pipeline, spéculation et bien d’autres échanges espace-temps, systèmes de bases redondantes permettant de calculer la multiplication aussi vite que l’addition, ce qui est aussi lumineux que contre-intuitif, etc.

  • 21 J-Y. Girard, Y. Lafont et P. Taylor, Proofs and Types, Cambridge University Press, 1990.

58À travers l’étude du comportement des circuits combinatoires cycliques, nous progresserons aussi dans l’étude de la relation entre modèles de temps en établissant des relations inattendues entre temps discret et temps continu, ainsi qu’entre électricité et logique constructive. Nous montrerons qu’un circuit combinatoire cyclique se stabilise en temps borné pour toutes ses entrées si et seulement si ses équations sont solubles en utilisant seulement la logique constructive, donc sans utiliser le tiers exclu ∨ ¬ = 1. Par exemple, le circuit Hamlet défini par « ToBe = ToBe or not ToBe » oscille électriquement pour certains délais des portes et fils. Ce résultat est en quelque sorte un analogue électrique de la correspondance de Curry-Howard entre calcul et preuve21.

59Si les circuits synchrones restent le paradigme dominant de par leur simplicité, ils ne passent plus à l’échelle des milliards de transistors des systèmes sur puce moderne ou SoCs, comme ceux des téléphones-ordinateurs récents. Ces grands circuits multifonctionnels sont construits par composition de sous-circuits cadencés par des horloges distinctes déterminant des fréquences différentes. Nous étudierons les problèmes fascinants et souvent sous-estimés que pose la communication entre zones d’horloges, dus à d’inévitables occurrences de métastabilité physique des registres qui se produisent quand le signal d’entrée d’un registre change au moment où son front d’horloge arrive. Nous présenterons aussi d’autres paradigmes de circuits sans horloges qui rendent le temps élastique. Et, dans l’avenir, nous verrons apparaître de nouvelles notions de circuits quantiques, probabilistes, neuromimétiques, etc., qu’il convient de suivre avec attention.

Langages synchrones et temps multiforme

  • 22 Safety Critical Application Development Environment.

60Les langages synchrones destinés aux logiciels embarqués ont été conçus au milieu des années 1980 par trois équipes françaises : celle de Paul Caspi et Nicolas Halbwachs pour Lustre à Grenoble, celle d’Albert Benveniste et Paul Le Guernic pour Signal à Rennes, et la mienne pour Esterel à Sophia-Antipolis. Fondés sur une approche résolument scientifique, ces trois langages d’origine académique ont été développés industriellement dans les années 1990 : Esterel avec Dassault Aviation et Thomson pour l’avionique, Bell Labs pour les télécommunications, etc. ; Lustre, sous sa version graphique SCADE22, avec Schneider Electric pour la commande de centrales nucléaires et Airbus pour le pilotage d’avions ; Signal avec SNECMA pour le contrôle de réacteurs et d’autres industriels pour le traitement du signal. D’autres langages synchrones ont été ensuite développés en France et à l’étranger. La société Esterel Technologies, créée en 2001 et dont j’ai été directeur scientifique jusqu’en 2009, a étendu Esterel à la conception, la synthèse et la vérification de circuits électroniques chez divers grands utilisateurs, puis a racheté SCADE et l’a unifié avec Esterel dans sa nouvelle version, qui fait maintenant autorité pour les systèmes embarqués critiques soumis à certification.

Le logiciel synchrone cyclique

  • 23 Les méthodes synchrones ont en fait été développées indépendamment pour les circuits et les logicie (...)

61La logique des langages synchrones est similaire à celle des circuits synchrones, mais avec une syntaxe et des implémentations différentes23. Comme dans la vision abstraite des circuits, ces langages considèrent une suite d’instants sans épaisseur pendant lesquels les calculs et les communications décrits en parallèle ou en séquence se font en temps nul – ce qu’on appelle l’hypothèse de synchronisme parfait. On fait donc comme si on programmait un ordinateur infiniment rapide, qui dort sauf quand il répond en temps nul aux entrées en produisant ses sorties. Cette vision synchrone, longtemps jugée iconoclaste dans la communauté académique, simplifie considérablement la programmation et la sémantique mathématique. Elle autorise un parallélisme déterministe, alors que les visions classiques du parallélisme asynchrone impliquent toujours un non-déterminisme incompatible avec les exigences de la plupart des logiciels embarqués. Elle permet aussi des implémentations optimisées et des vérifications formelles hors de portée des méthodes classiques.

62Deux implémentations à instants épais sont possibles : une traduction directe en circuits, développée surtout pour Esterel, et une implémentation logicielle qui se fonde sur l’approche pragmatique classique de l’exécution cyclique, avec une alternance cyclique de quatre phases comme pour le moteur à explosion : entrées, calcul, sortie, attente. Le cycle peut être déclenché de façon arbitraire, par exemple par des temporisateurs ou des événements externes, et son principe garantit la non-interférence entre entrées, calcul et sorties. Si l’exécution est soumise à des contraintes de temps-réel, il faut calculer le temps d’exécution du pire cas (worst case execution time ou WCET) du code généré et vérifier qu’il est plus court que le temps accordé au cycle par l’application. Pour implémenter le parallélisme et générer un code séquentiel unique, les cycles parallèles sont traités par entrelacement fin de leurs instructions élémentaires tout en respectant les dépendances induites par les communications inter-cycles.

Signaux et programmes en Esterel

63Pour être plus précis, étudions un exemple en Esterel, en montrant comment ce langage rend explicite la vision multiforme du temps.

64Les instructions Esterel communiquent avec l’environnement extérieur et entre elles par des signaux. Un signal S est formé d’un statut booléen présent ou absent, et, optionnellement d’une valeur d’un certain type. Dans la vue abstraite, un programme réagit à ses entrées en produisant instantanément ses sorties ; le statut et la valeur de chaque signal sont uniques à chaque réaction. Un programme est écrit à l’aide d’instructions temporelles, qui peuvent être mises en séquence, en parallèle ou sous préemption, et communiquer instantanément par signaux.

65Voici un programme Esterel décrivant l’entraînement sportif suivant : tous les matins, courir doucement pendant 100 mètres, sauter en soufflant à chaque pas pendant 15 secondes, puis courir à fond jusqu’à la fin du tour, tout cela pendant 4 tours.

every Morning do
   abort
     loop
        abort run slowly when 100 Meter ;
        abort {emit Jump || emit Blow} when 15 Second ;
        run full_speed
    each Lap
  when 4 Lap
end every

  • 24 Pour une description plus complète du langage et de ses possibilités, je renvoie le lecteur aux vid (...)

66Dans ce code manifestement temporel, Morning, Meter, Second et Lap sont des signaux d’entrée, Jump et Blow des signaux de sortie, alors que slowly et full_speed sont des modules non détaillés ici, dont l’exécution temporelle est conduite par l’instruction run. Le caractère « ; » est associé à la mise en séquence, le symbole « || » au parallélisme. Les autres instructions temporelles sont commandées par la présence d’un signal ou la fin du comptage des occurrences d’un signal. Tous les signaux sont traités comme s’ils définissaient des temps indépendants, ce qui conduit à la vision multiforme du temps. Les différents temps sont manipulés par des instructions d’attente, comme « await 5 Second » ou de préemption, comme « abort … when 100 Meter » qui arrête l’exécution de son corps au bout de 100 mètres et « abort … when 15 Second » qui arrête son corps au bout de 15 secondes. Les instructions « every … end » et « loop … each » sont des variantes en boucle de « abort … when ». Un système d’exceptions trap-exit non détaillé ici fournit d’autres modes de préemption et permet un traitement commode de beaucoup de cas d’erreurs, comme par exemple un problème de rythme cardiaque dans la seconde partie d’un tour24.

67Lustre et Signal sont des langages fonctionnels plus simples, dépourvus d’instructions de boucle, de préemption et d’exception. Ils traitent le temps multiforme d’une façon syntaxiquement différente mais équivalente à l’aide d’horloges abstraites, flots de valeurs booléennes qui jouent le rôle du statut de présence des signaux d’Esterel.

Sémantiques formelles et compilation

68Le style de programmation des langages synchrones est clairement différent de celui des langages classiques comme C ou Java. Si l’on savait déjà donner un sens aux programmes des langages classiques, ce qu’on appelle définir leurs sémantiques, la question se posait de façon nouvelle pour les langages synchrones. Nous avons choisi d’être intransigeants et de prendre comme base la sémantique mathématique et pas l’implémentation : nous visions en particulier les systèmes embarqués critiques, qui mettent en jeu la sécurité des biens et des personnes. L’implémentation doit y suivre la sémantique mathématique, et non l’inverse, comme trop souvent.

69Plusieurs types de sémantiques formelles ont été successivement définis pour Esterel, conduisant à des implémentations de plus en plus efficaces. L’histoire a commencé par l’application de techniques d’automates finis, conduisant aux compilateurs Esterel v2 et v3 (industrialisé), qui ont aussi permis d’étudier les problèmes de causalité posés par l’hypothèse de synchronisme. Mais la compilation pouvait exploser exponentiellement en taille, ce qui limitait la taille des applications. Un progrès fondamental a été effectué en collaboration avec l’équipe de Jean Vuillemin au laboratoire parisien de Digital Equipment, quand nous avons compris qu’il était possible et bien plus efficace de traduire directement les programmes Esterel en circuits électroniques puis de simuler ces circuits pour engendrer du logiciel. Cette façon de faire simplifiait la sémantique formelle et faisait définitivement disparaître l’explosion en taille du code généré.

  • 25 D. Potop-Butucaru, S. A. Edwards et G. Berry, Compiling Esterel, Springer, 2007.

70Nous avons ensuite compris comment relier la sémantique d’Esterel d’une part à la logique constructive et d’autre part à l’analyse des circuits combinatoires cycliques, déjà mentionnée ci-dessus à propos du circuit Hamlet. Ce progrès a permis une compréhension bien plus fine des questions de causalité dans le langage et conduit à la sémantique constructive d’Esterel25, qui fait maintenant foi.

Évolution des langages synchrones

  • 26 Il appartient maintenant à la société américaine Synopsys, qui a décidé de geler son exploitation.

71En 2001, j’ai rejoint la société Esterel Technologies, spécialement créée pour le développement d’Esterel et ses applications aux circuits et aux logiciels embarqués. Nous avons défini le langage bien plus complet Esterel v7, en y incorporant des constructions nouvelles et bien définies sémantiquement pour la définition des chemins de données complexes ubiquitaires en électronique. Ce langage a été utilisé en production pour la réalisation de circuits complexes dans de grandes sociétés d’électronique. En 2003, Esterel Technologies a racheté SCADE, utilisé en particulier par Airbus pour les A340 et A380, et a décidé de spécialiser SCADE dans le logiciel et Esterel v7 dans l’électronique. En 2008, les notions principales d’Esterel ont été incorporées dans la nouvelle génération SCADE 6, appliquée maintenant à de nombreux systèmes embarqués de haute sécurité. Malheureusement, Esterel v7 a été anéanti par la grande crise de 2008, en même temps que bien d’autres inventions de jeunes pousses innovantes, et n’est plus accessible même à ses auteurs26. Cela ne m’empêchera pas d’en enseigner la conception et les méthodes de compilation.

Vers de nouvelles applications

72Le cœur synchrone des langages est maintenant bien compris. Mais, comme pour les circuits, les problèmes s’étendent en raison du passage à l’échelle supérieure des applications. Dans le développement logiciel, il s’agit de sortir du cadre des systèmes compacts habituellement traités dans le domaine (pilotage d’avion, freinage de voiture, etc.) pour s’orienter vers des applications davantage distribuées demandant la liaison de plusieurs systèmes. Par exemple, comme cela a déjà été mentionné, la correction d’assiette d’une voiture en cas de freinage en virage demande la coopération des systèmes localement synchrones gérant la direction, la suspension et le freinage. Cela peut se faire à l’aide de réseaux à temps de transmission garantis (TTP, Flexray, etc.), en coordonnant donc précisément plusieurs échelles de temps. La coopération entre voitures circulant sur une même route sera bien plus complexe car les communications à grande échelle ne pourront plus être synchrones. Comme pour les circuits multi-horloges, il faut alors passer à des systèmes de type globalement asynchrones mains localement synchrones (globally asynchronous locally synchronous ou GALS) nettement plus difficiles à programmer et à vérifier.

73Des applications hors du cadre de l’embarqué sont également intéressantes. Les langages réactifs, développés par Frédéric Boussinot et. al., intègrent les concepts synchrones dans les langages de programmation classiques, avec une approche beaucoup plus dynamique que celle des langages synchrones. Le langage HipHop que nous présenterons en 2014 est une version d’Esterel adaptée à l’orchestration d’applications web et rendue dynamique par emprunt de techniques des langages réactifs. Je soupçonne que les concepts originaux des langages synchrones seront incorporés dans bien d’autres travaux où le traitement du temps et des événements s’avère important.

Simulation temps continu/temps discret

Figure 5. Deux boules et un mur

Figure 5. Deux boules et un mur

74Les systèmes de contrôle continu sont le plus souvent décrits par des systèmes d’équations différentielles ordinaires, augmentées de clauses de seuil pour changer d’équations en fonction d’événements discrets endogènes ou exogènes. Considérons le système de la figure 5, en appelant G la boule de gauche, D la boule de droite, et M le mur, de positions respectives g, d et m. Au départ, G est lancée vers la droite avec une vitesse v, alors que D et M sont immobiles. À ce moment, les équations aux positions g, d et vitesse g’, d’ de G et D s’écrivent simplement ainsi :

g : init g0
g’ = v
d : init d0
d’ = 0

75Mais le mouvement uniforme de G ne peut se poursuivre que jusqu’au choc avec D, qui produit un événement endogène au système. À ce moment, les deux boules échangent leur vitesse, G s’arrêtant et D partant vers la droite avec la vitesse v. Les équations deviennent les suivantes :

g : init d0
g’ = 0
d : init d0
d’ = v

76Plutôt que de gérer deux systèmes d’équations, on préfère travailler avec un seul système mêlant le discret et le continu, en introduisant un opérateur temporel cousin de ceux d’Esterel pour détecter le choc :

g : init g0
g’ = v every [ g up d → last(d’) ]
d : init d0
d’ = v every [ g up d → last(g’) ]

77L’opérateur « x up y » compare en permanence x et y et déclenche l’action de l’opérateur « every » dès que x ≥ y, celui-ci modifiant alors l’équation à exécuter. Aux instants de transition, l’opérateur temporel « last » retourne la dernière valeur connue de son argument, c’est-à-dire la limite dans le sens du mouvement de la valeur continue de cet argument.

78Tenons maintenant compte du mur M. Quand m, D touche le mur, ce qui provoque l’inversion de sa vitesse et son retour vers la gauche à la vitesse −v. Il s’ensuit un choc avec G, qui provoque à nouveau l’échange des vitesses : arrêt de D et départ de G vers la gauche avec la vitesse −v. Le système complet s’écrit ainsi, avec maintenant deux clauses pour l’opérateur « every » de l’équation de d’ :

g : init g0
g’ = v every [ g up d → last(d’) ]
d : init d0
d’ = v every [ g up d → last(g’) ,
                     d up m → – last(d’) ]

La simulation classique

  • 27 Les versions flottantes de fonctions d’usage constant comme les fonctions trigonométriques ne sont (...)

79Le fondement de la simulation classique est l’intégration de ces équations selon la variable de temps. Mais ni le continu ni les nombres réels n’existent en informatique (sauf une notion de réel calculable non pertinente ici), et tout doit être discrétisé. Les nombres réels doivent être approximés par des nombres flottants, ce qui est loin d’être simple27. Nous ignorerons les difficultés associées, nous concentrant sur celles qui sont liées à la progression du calcul dans le temps du phénomène simulé.

80L’idée de base est la discrétisation du temps. L’intégration va procéder de façon approximative, par exemple à la Riemann ou avec des méthodes d’interpolation plus sophistiquées, en avançant par pas de temps d’échelle appropriée à l’approximation souhaitée. Pour notre exemple, c’est trivial. À chaque pas de temps ε, la position d’une boule de vitesse v est incrémentée de εν. Après le départ, G bouge donc par pas de εν, avec un test « g up d » à chaque étape. Quand ce test devient vrai, on modifie les équations comme indiqué pour continuer la simulation, faisant progresser D vers le mur, etc.

Les problèmes aux frontières

Figure 6. La seconde boule collée au mur.

Figure 6. La seconde boule collée au mur.

81Regardons maintenant ce qui se passe si D est collée au mur au départ, comme dans la figure 6. Quand G atteint D, celle-ci ne peut partir vers la droite à cause du mur, et G est immédiatement renvoyée vers la gauche. Conceptuellement, on peut dire que G s’arrête en donnant sa vitesse à D, qui touche instantanément le mur sans même bouger, inverse sa vitesse, et retouche G toujours sans bouger, lui communicant sa vitesse vers la gauche et s’arrêtant. Il y a donc trois événements simultanés mais causalement ordonnés : le choc de G sur D, le rebond de D et le choc de D sur G. C’est exactement le phénomène que nous avons décrit pour la propagation synchrone conceptuellement instantanée de la communication dans les circuits et en Esterel.

82Les systèmes classiques ont bien du mal à traiter ce problème car ils ne connaissent pas la notion de propagation synchrone. Selon différents réglages du mécanisme d’intégration et de calcul, le comportement peut être différent, et même conduire à la traversée du mur par la boule D, ce qui est évidemment aberrant ! Quiconque étant concerné par la justesse des comportements et la précision des sémantiques ne peut accepter que le comportement du simulateur dépende de réglages internes difficilement compréhensibles par l’utilisateur.

Sémantique non-standard et temps superdense

  • 28 A. Benveniste, T. Bourke, B. Caillaud et M. Pouzet, « Non-standard semantics of hybrid systems mode (...)

83Une solution théorique très élégante a été proposée récemment28, fondée sur l’idée de s’appuyer non pas sur l’analyse réelle classique mais sur l’analyse non-standard, pour laquelle les ε ne sont pas des réels mais des infiniment petits inférieurs à tout réel et multipliable par des rationnels. On a ainsi 0 < ε < 2ε < x pour tout infiniment petit ε et tout réel x. L’analyse non-standard est une autre façon de parler de synchronisme abstrait : les transitions instantanées peuvent se produire uniquement dans le domaine infinitésimal, sans progression du temps réel comme en simulation classique, mais avec progression des ε. Les paradoxes sont résolus par la contrainte selon laquelle la fonction non-standard calculée par le système doit être standardisable, condition mathématique simple qui permet de rejeter uniformément les comportements non désirés.

84Sur le plan pratique, de nouvelles propositions de langages synchrones continu/discret distinguent le continu et l’instantané par un système de types, appliquant les méthodes d’intégration au continu et les méthodes des langages synchrones au discret. Ces méthodes me semblent promises à un grand avenir pour la simulation des systèmes complexes.

La preuve de programmes

85Une préoccupation constante du cours sera le besoin de prouver formellement que les circuits et programmes considérés répondent bien à leurs spécifications. Quand elle est faisable, la preuve est largement supérieure au simple test, puisqu’elle analyse formellement tous les cas possibles alors que le test ne valide ou invalide que ce qu’on essaie. La preuve formelle a fait récemment des progrès considérables, avec trois types de techniques :

  • Le model-checking, qui a donné le prix Turing 2007 à Joseph Sifakis, Edmund Clarke et E. Allen Emerson.

    • 29 P. Cousot, « Interprétation abstraite », Technique et science informatiques, vol. 19, nos 1-2-3, Pa (...)

    L’interprétation abstraite, développée initialement en France par Patrick Cousot et son équipe, et qui connaît plusieurs industrialisations29.

  • L’assistance à la preuve mathématique, avec des systèmes comme B, HOL, Isabelle, et spécialement Coq.

86Le model-checking vérifie principalement des modèles finis, éventuellement de très grande taille. Il est particulièrement bien adapté à la vérification des programmes synchrones. Il a bénéficié des grands progrès des calculs symboliques booléens ou SMT (booléen modulo théories algébriques). Il est utilisé systématiquement pour la vérification des nombreuses transformations réalisées par les outils de conception de circuits, et, de plus en plus, pour la vérification de leurs propriétés fonctionnelles. Il est aussi utilisé en logiciel embarqué, par exemple pour la signalisation et la gestion des aiguillages ferroviaires. Ses applications ne cessent de s’étendre, y compris à la bio-informatique.

87L’interprétation abstraite travaille par réduction de modèles infinis à des modèles finis en utilisant un cadre formel fondé sur la notion de correspondance de Galois. Elle unifie et simplifie de nombreuses méthodes d’analyse de programmes autrefois disparates. Elle est utilisée dans l’industrie automobile et spatiale, où elle permet de détecter facilement le fameux bug logiciel qui a provoqué l’explosion d’Ariane 501, et en avionique, où elle a permis de prouver que ce type de bug n’existe pas dans le logiciel de pilotage de l’Airbus A380 – exploit scientifique considérable.

88Les assistants de preuve permettent d’automatiser la vérification de preuves logiques et d’aider l’utilisateur dans la conduite de ces preuves. Mentionnons les grands moments du domaine. Dans les applications aux circuits, John Harrison (Intel) a pu prouver avec HOL la correction des opérateurs flottants du Pentium, à la suite du fameux bug de division du Pentium Pro qui a coûté 475 millions de dollars à Intel. Dans le domaine du logiciel, Xavier Leroy (Inria) a pu développer en Coq un compilateur C véritablement prouvé et raisonnablement efficace, ce qui peut avoir des implications importantes dans les systèmes de haute sécurité. Dans le domaine des systèmes d’exploitation, l’équipe de Gernot Heiser (NICTA Sydney) a pu construire un noyau de système efficace dont la plupart des propriétés essentielles ont été prouvées en Isabelle ; ce noyau est réellement utilisé à grande échelle sur des téléphones. En mathématiques, Georges Gonthier et Benjamin Werner ont pu prouver en Coq le fameux théorème des quatre couleurs en 2006. En 2012, Georges Gonthier et son équipe Microsoft/Inria ont terminé la preuve formelle en Coq du fameux Monster Theorem de Feit-Thomson sur la caractérisation des groupes finis d’ordre impair, monument du xxe siècle dont la preuve mathématique n’occupe pas moins de 250 lourdes pages. Pour cela, Gonthier a développé un nouveau génie mathématique dédié à la gestion de grandes preuves, pendant mathématique du génie logiciel dédié à la gestion de grands programmes. L’ampleur phénoménale de ce travail bouleverse littéralement le domaine, et les applications aux circuits et logiciels sont prometteuses.

89Mon intention de recherche est de comprendre comment les techniques de vérification formelle et en particulier celles associées à Coq peuvent s’adapter aux programmes manipulant le temps et les événements.

Conclusion

90Dans ce tour d’horizon, j’ai montré la richesse et l’ouverture des problèmes liés au temps et aux événements en informatique. J’ai présenté de nouvelles visions techniques de la programmation, de la sémantique et de l’implémentation qui permettent d’obtenir des résultats bien supérieurs à ceux qu’on obtiendrait par les méthodes classiques, qui ne savent pas parler du temps et à peine parler des événements. Les cours des prochaines années approfondiront d’abord les concepts, techniques et raisonnements de l’approche synchrone, puis s’intéresseront à deux sujets qui restent à l’heure actuelle largement ouverts : d’une part les difficultés posées par l’explosion en taille des systèmes matériels et logiciels, qui demandent de mieux comprendre la relation entre synchronisme et asynchronisme, et d’autre part les formalismes, les techniques logiques et algorithmiques permettant de prouver des propriétés-clefs de ces systèmes. Il sera également intéressant de voir si les concepts développés dans cette recherche s’avèreront pertinents dans des domaines bien différents comme la biologie et les neurosciences.

Notes

1 Voir ma leçon inaugurale : Pourquoi et comment le monde devient numérique, Paris, Collège de France/Fayard, 2008 ainsi que les vidéos du cours de 2007-2008, disponibles sur le site du Collège de France : http://www.college-de-france.fr/site/gerard-berry.

2 Feuille de route du gouvernement sur le numérique, 28 février 2013 : http://www.gouvernement.fr/sites/default/files/fichiers_joints/feuille_de_route_du_gouvernement_sur_le_numerique.pdf

3 Brevet informatique et Internet (B2I) pour les élèves ; certificat informatique et Internet (C2I) pour les professeurs.

4 L’enseignement de l’informatique en France : il est urgent de ne plus attendre, Académie des sciences, mai 2013 : http://www.academie-sciences.fr/activite/rapport/rads_0513.pdf.

5 Informatics education: Europe cannot afford to miss the boat : http://www.informatics-europe.org/news-and-events/157-joint-informatics-europe-acm-europe-report-on-informatics-education-in-schools.html.

6 Computing in schools: shutdown or restart? : http://royalsociety.org/education/policy/computing-in-schools/report.

7 Ce choix fait, mon ami Jean Vuillemin m’a montré celui de son cours à l’École polytechnique dans les années 1990 : « Algorithmes, nombres, machines et langages ». C’est ce qu’on appelle en ’pataphysique un plagiat par anticipation !

8 Serge Abiteboul, Science des données : de la logique du premier ordre à la toile, Paris, Collège de France/Fayard, coll. « Leçons inaugurales », no 226, 2012 : http://books.openedition.org/cdf/506.

9 Martin Abadi, La sécurité informatique, Paris, Collège de France/Fayard, coll. « Leçons inaugurales », no 219, 2011 : http://books.openedition.org/cdf/421.

10 G. Berry, Penser, modéliser et maîtriser le calcul informatique, Paris, Collège de France/Fayard, coll. « Leçons inaugurales », no 208, 2009. Les vidéos du cours sont disponibles à l’adresse http://www.college-de-france.fr/site/gerard-berry.

11 À l’exception du sultanat de Jaipur, en Inde, où le sultan avait décrété l’unification du temps dans tous les villages. Dans le fabuleux observatoire Yantra Mandir (~ 1730) se trouve un cadran solaire précis à la demi-seconde.

12 G. Berry, « Manifeste pour la réhabilitation du pavillon des poids et mesures », Viridis Candela, correspondancier du Collège de ’pataphysique, no 1, 2007, p. 33-60 : http://www-sop.inria.fr/members/Gerard.Berry/Pataphysique/BerryPoidsEtMesures.pdf.

13 Surtout dans sa version sud-américaine « mañana por la mañana ».

14 Voir par exemple Z. Manna et A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems: Specification, New York, Springer, 1992.

15 « OPERA experiment reports anomaly in flight time of neutrinos from CERN to Gran Sasso », CERN press office, 23 septembre 2011, mise à jour le 8 juin 2012 en raison de l’erreur expérimentale.

16 Jordi Cortadella,« Elastic circuits, blending synchronous and asynchronous technologies », séminaire du 21 mai 2013 (http://www.college-de-france.fr/site/gerard-berry).

17 Voir les deux derniers séminaires du cours 2012-2013 donnés le 4 juin 2013 : Philippe Manoury, « La musique du temps-réel » et Arshia Cont, « Musique informatique : de la synchronisation interprète/électronique à la partition algorithmique » (http://www.college-de-france.fr/site/gerard-berry).

18 Ce paradoxe n’en est d’ailleurs pas vraiment un : il montre simplement qu’il n’est pas cohérent de découper de façon différente le temps et l’espace.

19 Merci à Jean Krivine pour cet excellent exemple.

20 Voir le cours « Circuits et nombres 2-adiques, une nouvelle vision de l’échange temps-espace », 9 avril 2013 (http://www.college-de-france.fr/site/gerard-berry).

21 J-Y. Girard, Y. Lafont et P. Taylor, Proofs and Types, Cambridge University Press, 1990.

22 Safety Critical Application Development Environment.

23 Les méthodes synchrones ont en fait été développées indépendamment pour les circuits et les logiciels embarqués ; nous n’avons constaté leur identité conceptuelle que dans les années 1990.

24 Pour une description plus complète du langage et de ses possibilités, je renvoie le lecteur aux vidéos des cours sur Esterel (16 et 23 avril, 14 et 21 mai 2013) : http://www.college-de-france.fr/site/gerard-berry.

25 D. Potop-Butucaru, S. A. Edwards et G. Berry, Compiling Esterel, Springer, 2007.

26 Il appartient maintenant à la société américaine Synopsys, qui a décidé de geler son exploitation.

27 Les versions flottantes de fonctions d’usage constant comme les fonctions trigonométriques ne sont même pas encore normalisées.

28 A. Benveniste, T. Bourke, B. Caillaud et M. Pouzet, « Non-standard semantics of hybrid systems modelers », Journal of Computer and System Sciences, vol. 78, no 3, 2012 (numéro spécial en l’honneur d’Amir Pnueli), p. 877-910, DOI : 10.1016/j.jcss.2011.08.009.

29 P. Cousot, « Interprétation abstraite », Technique et science informatiques, vol. 19, nos 1-2-3, Paris, Hermès, 2000, p. 155-164.

Table des illustrations

Titre Figure 1. Les composantes de l’informatique
URL http://books.openedition.org/cdf/docannexe/image/3300/img-1.png
Fichier image/png, 53k
Titre Figure 2. Deux machines à café/thé
URL http://books.openedition.org/cdf/docannexe/image/3300/img-2.png
Fichier image/png, 21k
Titre Figure 3. FullAdder, l’additionneur 3 bits
URL http://books.openedition.org/cdf/docannexe/image/3300/img-3.png
Fichier image/png, 23k
Titre Figure 4. L’additionneur sériel (2-adique), où ++ désigne FullAdder
URL http://books.openedition.org/cdf/docannexe/image/3300/img-4.png
Fichier image/png, 44k
Titre Figure 5. Deux boules et un mur
URL http://books.openedition.org/cdf/docannexe/image/3300/img-5.png
Fichier image/png, 18k
Titre Figure 6. La seconde boule collée au mur.
URL http://books.openedition.org/cdf/docannexe/image/3300/img-6.png
Fichier image/png, 18k

Auteur

Professeur au Collège de France, chaire Algorithmes, machines et langages

© Collège de France, 2013

Conditions d’utilisation : http://www.openedition.org/6540

Acheter

Volume papier

Chargement

Unavailable