Aller au contenu
learn
Menu global

Réseaux de Petri — Mission

Pourquoi j’apprends ça

Section intitulée « Pourquoi j’apprends ça »

Je sais dessiner une machine à états. J’en ai écrit en C# avec un enum et un switch, en Java avec un patron état, et elles fonctionnent tant que le système ne fait qu’une chose à la fois. Puis deux choses arrivent en même temps. Deux fils d’exécution prennent deux verrous dans deux ordres. Un Channel<T> se remplit et le producteur se bloque pour toujours. Un workflow a trois branches et personne ne sait dire si toutes peuvent se terminer.

Une machine à états ne peut rien dire de tout cela, parce qu’elle a un état courant, et que la chose que je modélise en a plusieurs. Ce que je veux, c’est un modèle dont l’état est une distribution : tant de requêtes dans la file, tant de travailleurs occupés, un verrou tenu. Un réseau de Petri est exactement cela, et il vient avec un petit corpus de mathématiques qui répond à des questions auxquelles je réponds aujourd’hui par des tests de charge et de l’espoir :

  • cette file peut-elle déborder ? Pas « a-t-elle débordé mardi dernier » — peut-elle, un jour, sous n’importe quel entrelacement ;
  • ce système peut-il s’interbloquer ? Et si oui, quelle est la séquence la plus courte qui y mène ;
  • ce workflow va-t-il se terminer ? Depuis tous les états où il peut se retrouver, pas seulement le chemin heureux.

Ces trois questions sont tranchées par un programme dans ce cours, sur des réseaux qui modélisent des choses réelles : un tampon borné, une exclusion mutuelle, deux verrous pris dans des ordres opposés.

À qui s’adresse ce cours

Section intitulée « À qui s’adresse ce cours »

Vous êtes développeur C# ou Java. Vous avez écrit du code concurrent et modélisé des processus avec des machines à états. Vous n’avez besoin d’aucune mathématique au-delà de l’addition de vecteurs et de la multiplication d’une matrice par un vecteur ; le cours introduit ce qu’il utilise, et la première matrice n’apparaît qu’à la leçon 2, parce qu’elle rend quelque chose de concret plus facile.

Les leçons sur la concurrence s’appuient sur ce que vous savez déjà. La leçon 7 reprend la contre-pression des leçons 6 à 9 du cours C# avancé — channels, TPL Dataflow, Rx — et la modélise au lieu de la mesurer. La leçon 14 commence le dogfooding du dépôt par un cycle de vie C# borné et un verrou de lane d’agents ; RabbitMQ et Kubernetes restent des expériences suivantes explicites.

L’exemple fil rouge

Section intitulée « L’exemple fil rouge »

Un producteur, un consommateur, et un tampon de deux emplacements. Trois places tiennent l’état du producteur, du consommateur et du tampon ; quatre transitions sont les événements. Rien n’est un « état courant » : le marquage dit où se trouve chaque jeton, tous à la fois.

flowchart LR
    ready(("ready<br/>●"))
    produced(("produced"))
    free(("free<br/>● ●"))
    full(("full"))
    waiting(("waiting<br/>●"))
    taken(("taken"))
    produce["produce"]
    deposit["deposit"]
    take["take"]
    consume["consume"]
    ready --> produce
    produce --> produced
    produced --> deposit
    free --> deposit
    deposit --> full
    deposit --> ready
    full --> take
    waiting --> take
    take --> taken
    take --> free
    taken --> consume
    consume --> waiting

Les noms des places et des transitions restent en anglais dans les trois langues : ils font partie de la sortie du programme, comparée par check.sh, et les traduire ferait diverger les listings.

Ce réseau a douze marquages accessibles, il ne s’interbloque jamais, et la place free est toute la raison pour laquelle le tampon ne peut pas déborder — retirez-la, et l’ensemble des marquages accessibles devient infini. Les leçons 1 à 4 prouvent ces trois affirmations, et la leçon 5 prouve la première à nouveau sans regarder un seul marquage.

À la fin de ce cours, je saurai

Section intitulée « À la fin de ce cours, je saurai »
  • lire et dessiner un réseau de Petri, et dire ce que son marquage signifie dans le système qu’il modélise ;
  • écrire la matrice d’incidence d’un réseau, et savoir ce que l’équation d’état décide et ne décide pas ;
  • construire un graphe d’accessibilité, et un arbre de couverture quand le graphe est infini ;
  • décider la bornitude, la sûreté, la vivacité, l’absence d’interblocage, la réversibilité et la persistance, et dire lesquelles un système donné exige réellement ;
  • calculer les invariants de places et de transitions, et utiliser un invariant comme une preuve valable pour tous les marquages accessibles ;
  • reconnaître les machines à états, les graphes marqués et les réseaux à choix libre, et utiliser les théorèmes qui viennent avec ces classes ;
  • modéliser l’exclusion mutuelle, le producteur-consommateur, les lecteurs-rédacteurs et les philosophes, et comparer ces modèles aux constructions C# et Java qu’ils représentent ;
  • utiliser les réseaux colorés, temporisés et stochastiques, et savoir ce que chaque extension coûte à l’analyse ;
  • vérifier la soundness d’un workflow, et traduire entre BPMN et réseaux de workflow ;
  • échanger des réseaux avec TINA, LoLA, CPN Tools, GreatSPN et TAPAAL via PNML ;
  • modéliser des morceaux des systèmes de ce dépôt, et dire honnêtement ce que le modèle a trouvé et ce qu’il a manqué ;
  • savoir où le formalisme s’arrête : ce qui est indécidable, ce qui est décidable mais désespéré, et ce qu’il faut prendre à la place.

Plan

Section intitulée « Plan »
# Leçon Ce que vous connaissez peut-être déjà
1 Pourquoi les réseaux de Petri les machines à états, enum plus switch, une file bornée
2 La définition formelle et la matrice d’incidence les vecteurs, un produit matriciel
3 Le graphe d’accessibilité un parcours en largeur, l’explosion d’une matrice de tests
4 Propriétés interblocage, famine, livelock
5 Invariants un invariant de boucle, une quantité conservée
6 Classes structurelles : machines à états, graphes marqués, réseaux à choix libre
7 Modéliser la concurrence : exclusion mutuelle, producteur-consommateur, lecteurs-rédacteurs, philosophes lock, SemaphoreSlim, Channel<T>, synchronized, ReentrantLock
8 Réseaux colorés les génériques, un message typé
9 Temps et probabilités : réseaux temporisés, stochastiques, GSPN les percentiles, un modèle de files d’attente
10 Workflows : réseaux de workflow, soundness, BPMN, process mining BPMN, un moteur de workflow
11 Outils et interopérabilité : PNML, TINA, LoLA, Snoopy, PIPE, CPN Tools, GreatSPN, TAPAAL un format d’échange XML
12 Applications industrielles : ateliers flexibles, protocoles, matériel, biochimie, sécurité un banc d’essai public, un espace d’états
13 Face aux autres formalismes : TLA+, statecharts, algèbres de processus, automates temporisés un second espace d’états, calculé ailleurs
14 Sur nos systèmes : pipelines C# et lanes d’agents C# avancé ; RabbitMQ et Kubernetes sont des expériences suivantes
15 Limites et suite : indécidabilité, dépliages, réduction d’ordre partiel, extensions une réponse fausse d’un algorithme correct
16 Interopérabilité : préserver le comportement, pas seulement le dessin un test d’aller-retour, un fichier qui se valide et perd quand même des données

Journal : ce que j’ai essayé, ce qui m’a surpris, ce qu’il me reste à vérifier.

Ressources

Section intitulée « Ressources »