Comment la sécurité des threads pourrait-elle être assurée par un langage de programmation similaire à la façon dont la sécurité de la mémoire est assurée par Java et C #?

10

Java et C # assurent la sécurité de la mémoire en vérifiant les limites des tableaux et les déréférences des pointeurs.

Quels mécanismes pourraient être mis en œuvre dans un langage de programmation pour éviter la possibilité de conditions de concurrence et de blocages?

mrpyo
la source
3
Vous pourriez être intéressé par ce que fait Rust: une concurrence sans peur avec Rust
Vincent Savard
2
Rendez tout immuable, ou rendez tout asynchrone avec des canaux sûrs. Vous pourriez également être intéressé par Go et Erlang .
Theraot
@Theraot "rendre tout asynchrone avec des canaux sûrs" - j'aimerais que vous développiez cela.
mrpyo
2
@mrpyo vous n'exposeriez pas les processus ou les threads, chaque appel est une promesse, tout s'exécute simultanément (le runtime planifiant leur exécution et créant / regroupant les threads système en arrière-plan si nécessaire), et la logique qui protège l'état est dans les mécanismes qui transmet des informations ... le runtime peut automatiquement sérialiser par programmation, et il y aurait une bibliothèque standard avec une solution thread-safe pour plus de comportements nuancés, en particulier producteur / consommateur et des agrégations sont nécessaires.
Theraot
2
Soit dit en passant, il existe une autre approche possible: la mémoire transactionnelle .
Theraot

Réponses:

14

Les courses se produisent lorsque vous avez un alias simultané d'un objet et qu'au moins l'un des alias est en mutation.

Donc, pour empêcher les courses, vous devez rendre une ou plusieurs de ces conditions fausses.

Différentes approches abordent différents aspects. La programmation fonctionnelle met l'accent sur l'immuabilité qui supprime la mutabilité. Le verrouillage / atomique supprime la simultanéité. Les types affines suppriment l'aliasing (Rust supprime l'aliasing mutable). Les modèles d'acteurs suppriment généralement l'aliasing.

Vous pouvez restreindre les objets pouvant être aliasés afin qu'il soit plus facile de garantir que les conditions ci-dessus sont évitées. C'est là qu'interviennent les canaux et / ou les styles de passage de messages. Vous ne pouvez pas alias de mémoire arbitraire, juste la fin d'un canal ou d'une file d'attente qui est arrangé pour être sans course. Habituellement, en évitant la simultanéité, c'est-à-dire les verrous ou atomiques.

L'inconvénient de ces différents mécanismes est qu'ils restreignent les programmes que vous pouvez écrire. Plus la restriction est brutale, moins les programmes sont nombreux. Il n'y a donc pas d'alias ou de mutabilité, et ils sont faciles à raisonner, mais sont très limitatifs.

C'est pourquoi la rouille fait autant de bruit. C'est un langage d'ingénierie (par opposition à un langage académique) qui prend en charge l'aliasing et la mutabilité, mais le compilateur vérifie qu'ils ne se produisent pas simultanément. Bien que n'étant pas l'idéal, il permet d'écrire en toute sécurité une plus grande classe de programmes que beaucoup de ses prédécesseurs.

Alex
la source
11

Java et C # assurent la sécurité de la mémoire en vérifiant les limites des tableaux et les déréférences des pointeurs.

Il est important de réfléchir d'abord à la manière dont C # et Java procèdent. Ils le font en convertissant ce qui est un comportement indéfini en C ou C ++ en comportement défini: planter le programme . Les déréférences nulles et les exceptions d'index de tableau ne doivent jamais être interceptées dans un programme C # ou Java correct; ils ne devraient pas se produire en premier lieu parce que le programme ne devrait pas avoir ce bogue.

Mais je pense que ce n'est pas ce que vous entendez par votre question! Nous pourrions assez facilement écrire un runtime "deadlock safe" qui vérifie périodiquement s'il y a n threads qui s'attendent mutuellement et terminent le programme si cela se produit, mais je ne pense pas que cela vous satisfasse.

Quels mécanismes pourraient être mis en œuvre dans un langage de programmation pour éviter la possibilité de conditions de concurrence et de blocages?

Le problème suivant auquel nous sommes confrontés avec votre question est que les "conditions de concurrence", contrairement aux blocages, sont difficiles à détecter. N'oubliez pas que ce que nous recherchons en matière de sécurité des threads n'est pas d' éliminer les courses . Ce que nous voulons, c'est que le programme soit correct, peu importe qui remporte la course ! Le problème avec les conditions de concurrence n'est pas que deux threads s'exécutent dans un ordre indéfini et nous ne savons pas qui va terminer en premier. Le problème avec les conditions de concurrence est que les développeurs oublient que certaines commandes de finition de threads sont possibles et ne tiennent pas compte de cette possibilité.

Donc, votre question se résume essentiellement à "y a-t-il un moyen pour un langage de programmation de s'assurer que mon programme est correct?" et la réponse à cette question est, en pratique, non.

Jusqu'à présent, je n'ai fait que critiquer votre question. Permettez-moi d'essayer de changer de vitesse ici et de répondre à l'esprit de votre question. Existe-t-il des choix que les concepteurs de langage pourraient faire pour atténuer la situation horrible dans laquelle nous nous trouvons avec le multithreading?

La situation est vraiment horrible! Obtenir un code multithread correct, en particulier sur des architectures de modèle de mémoire faible, est très, très difficile. Il est instructif de réfléchir aux raisons de la difficulté:

  • Il est difficile de raisonner sur plusieurs threads de contrôle en un seul processus. Un fil est assez dur!
  • Les abstractions deviennent extrêmement fuyantes dans un monde multithread. Dans le monde à thread unique, nous sommes garantis que les programmes se comportent comme s'ils étaient exécutés dans l'ordre, même s'ils ne sont pas réellement exécutés dans l'ordre. Dans le monde multithread, ce n'est plus le cas; les optimisations qui seraient invisibles sur un seul thread deviennent visibles, et maintenant le développeur doit comprendre ces optimisations possibles.
  • Mais ça empire. La spécification C # indique qu'une implémentation n'est PAS obligée d'avoir un ordre cohérent de lectures et d'écritures qui peut être accepté par tous les threads . L'idée qu'il y a du tout des "courses" et qu'il y a un vainqueur clair, n'est en fait pas vraie! Considérez une situation où il y a deux écritures et deux lectures dans certaines variables sur plusieurs threads. Dans un monde sensé, nous pourrions penser "eh bien, nous ne pouvons pas savoir qui va gagner les courses, mais au moins il y aura une course et quelqu'un gagnera". Nous ne sommes pas dans ce monde sensible. C # permet à plusieurs threads d' être en désaccord sur l'ordre dans lequel les lectures et les écritures se produisent; il n'y a pas nécessairement un monde cohérent que tout le monde observe.

Il existe donc un moyen évident pour les concepteurs de langage d'améliorer les choses. Abandonnez les gains de performances des processeurs modernes . Assurez-vous que tous les programmes, même ceux à plusieurs threads, ont un modèle de mémoire extrêmement solide. Cela rendra les programmes multithread beaucoup, beaucoup plus lents, ce qui va directement à l'encontre de la raison d'avoir des programmes multithread en premier lieu: pour de meilleures performances.

Même en laissant de côté le modèle de mémoire, il existe d'autres raisons pour lesquelles le multithreading est difficile:

  • La prévention des blocages nécessite une analyse de l'ensemble du programme; vous devez connaître l'ordre global dans lequel les verrous peuvent être supprimés et appliquer cet ordre à l'ensemble du programme, même si le programme est composé de composants écrits à différents moments par différentes organisations.
  • Le principal outil que nous vous donnons pour apprivoiser le multithreading est le verrou, mais les verrous ne peuvent pas être composés .

Ce dernier point mérite une explication supplémentaire. Par "composable", j'entends ce qui suit:

Supposons que nous souhaitons calculer un int donné un double. Nous écrivons une implémentation correcte du calcul:

int F(double x) { correct implementation here }

Supposons que nous souhaitons calculer une chaîne avec un int:

string G(int y) { correct implementation here }

Maintenant, si nous voulons calculer une chaîne avec un double:

double d = whatever;
string r = G(F(d));

G et F peuvent être composés en une solution correcte au problème plus complexe.

Mais les serrures n'ont pas cette propriété à cause des blocages. Une méthode correcte M1 qui prend des verrous dans l'ordre L1, L2 et une méthode correcte M2 qui prend des verrous dans l'ordre L2, L1, ne peuvent pas toutes les deux être utilisées dans le même programme sans créer un programme incorrect. Les verrous font en sorte que vous ne pouvez pas dire "chaque méthode individuelle est correcte, donc tout est correct".

Alors, que pouvons-nous faire, en tant que concepteurs linguistiques?

D'abord, n'y allez pas. Plusieurs threads de contrôle dans un programme sont une mauvaise idée, et le partage de mémoire entre les threads est une mauvaise idée, donc ne le mettez pas dans la langue ou le runtime en premier lieu.

Il s'agit apparemment d'un non-démarreur.

Tournons ensuite notre attention vers la question la plus fondamentale: pourquoi avons-nous en premier lieu plusieurs fils? Il y a deux raisons principales, et elles sont souvent confondues dans la même chose, bien qu'elles soient très différentes. Ils sont confondus car ils concernent tous deux la gestion de la latence.

  • Nous créons des threads, à tort, pour gérer la latence des E / S. Besoin d'écrire un gros fichier, d'accéder à une base de données distante, peu importe, de créer un thread de travail plutôt que de verrouiller votre thread d'interface utilisateur.

Mauvaise idée. Au lieu de cela, utilisez une asynchronie à thread unique via les coroutines. C # le fait magnifiquement. Java, pas si bien. Mais c'est le principal moyen que la génération actuelle de concepteurs de langage aide à résoudre le problème de threading. L' awaitopérateur en C # (inspiré des workflows asynchrones F # et autres antériorités) est en cours d'intégration dans de plus en plus de langages.

  • Nous créons des threads, correctement, pour saturer les processeurs inactifs avec un travail de calcul lourd. Fondamentalement, nous utilisons des threads comme processus légers.

Les concepteurs de langage peuvent vous aider en créant des fonctionnalités de langage qui fonctionnent bien avec le parallélisme. Pensez à la façon dont LINQ est étendu si naturellement à PLINQ, par exemple. Si vous êtes une personne sensée et que vous limitez vos opérations TPL à des opérations liées au processeur qui sont très parallèles et ne partagent pas la mémoire, vous pouvez obtenir de gros gains ici.

Que pouvons-nous faire d'autre?

  • Faire en sorte que le compilateur détecte les erreurs les plus osées et les transforme en avertissements ou erreurs.

C # ne vous permet pas d'attendre dans une serrure, car c'est une recette pour les blocages. C # ne vous permet pas de verrouiller un type de valeur car c'est toujours la mauvaise chose à faire; vous verrouillez la boîte, pas la valeur. C # vous avertit si vous alias un volatile, car l'alias n'impose pas de sémantique d'acquisition / libération. Il existe de nombreuses autres façons pour le compilateur de détecter les problèmes courants et de les éviter.

  • Concevez des fonctionnalités «fosse de qualité», où la façon la plus naturelle de le faire est aussi la plus correcte.

C # et Java ont fait une énorme erreur de conception en vous permettant d'utiliser n'importe quel objet de référence comme moniteur. Cela encourage toutes sortes de mauvaises pratiques qui rendent plus difficile le repérage des blocages et plus difficile à éviter statiquement. Et cela gaspille des octets dans chaque en-tête d'objet. Les moniteurs doivent provenir d'une classe de moniteurs.

  • Beaucoup de temps et d'efforts ont été consacrés à la recherche Microsoft pour ajouter de la mémoire transactionnelle logicielle à un langage de type C #, et ils n'ont jamais réussi à le faire fonctionner suffisamment bien pour l'incorporer dans le langage principal.

STM est une belle idée, et j'ai joué avec des implémentations de jouets dans Haskell; il vous permet de composer de manière beaucoup plus élégante des solutions correctes à partir de pièces correctes que les solutions basées sur les verrous. Cependant, je ne connais pas suffisamment les détails pour expliquer pourquoi il n'a pas été possible de travailler à grande échelle; demandez à Joe Duffy la prochaine fois que vous le verrez.

  • Une autre réponse a déjà mentionné l'immuabilité. Si vous avez l'immuabilité combinée à des coroutines efficaces, vous pouvez créer des fonctionnalités comme le modèle d'acteur directement dans votre langage; pense Erlang, par exemple.

Il y a eu beaucoup de recherches sur les langages basés sur le calcul de processus et je ne comprends pas très bien cet espace; essayez de lire vous-même quelques articles et voyez si vous avez des idées.

  • Facilitez la tâche des tiers pour écrire de bons analyseurs

Après avoir travaillé chez Microsoft sur Roslyn, j'ai travaillé chez Coverity, et l'une des choses que j'ai faites a été d'obtenir l'interface utilisateur de l'analyseur en utilisant Roslyn. En ayant une analyse lexicale, syntaxique et sémantique précise fournie par Microsoft, nous pourrions alors nous concentrer sur le dur travail d'écriture des détecteurs qui ont trouvé des problèmes communs de multithreading.

  • Augmenter le niveau d'abstraction

Une raison fondamentale pour laquelle nous avons des races et des blocages et tout ça, c'est parce que nous écrivons des programmes qui disent quoi faire , et il se trouve que nous sommes tous des conneries à écrire des programmes impératifs; l'ordinateur fait ce que vous lui dites et nous lui demandons de faire les mauvaises choses. De nombreux langages de programmation modernes sont de plus en plus sur la programmation déclarative: dites quels résultats vous voulez, et laissez le compilateur trouver la manière efficace, sûre et correcte pour atteindre ce résultat. Encore une fois, pensez à LINQ; nous voulons que vous disiez from c in customers select c.FirstName, qui exprime une intention . Laissez le compilateur comprendre comment écrire le code.

  • Utilisez des ordinateurs pour résoudre des problèmes informatiques.

Les algorithmes d'apprentissage automatique sont bien meilleurs pour certaines tâches que les algorithmes codés à la main, bien qu'il y ait bien sûr de nombreux compromis, notamment la correction, le temps de formation, les biais introduits par une mauvaise formation, etc. Mais il est probable qu'un grand nombre de tâches que nous codons actuellement "à la main" pourront bientôt faire l'objet de solutions générées par machine. Si les humains n'écrivent pas le code, ils n'écrivent pas de bogues.

Désolé, c'était un peu décousu; c'est un sujet énorme et difficile et aucun consensus clair n'a émergé dans la communauté PL au cours des 20 années que j'ai suivies les progrès dans cet espace problématique.

Eric Lippert
la source
"Donc, votre question se résume essentiellement à" y a-t-il un moyen pour un langage de programmation de garantir que mon programme est correct? "Et la réponse à cette question est, en pratique, non." - en fait, c'est tout à fait possible - cela s'appelle la vérification formelle, et bien que ce soit gênant, je suis presque sûr que cela est fait régulièrement sur des logiciels critiques, donc je ne dirais pas que c'est peu pratique. Mais vous, concepteur de langues, savez probablement cela ...
mrpyo
6
@mrpyo: J'en suis bien conscient. Il y a beaucoup de problèmes. Premièrement: j'ai participé à une conférence de vérification formelle au cours de laquelle une équipe de recherche MSFT a présenté un nouveau résultat passionnant: elle a pu étendre sa technique pour vérifier des programmes multithread jusqu'à vingt lignes et faire fonctionner le vérificateur en moins d'une semaine. Ce fut une présentation intéressante, mais inutile pour moi; J'avais un programme de 20 millions de lignes à analyser.
Eric Lippert
@mrpyo: Deuxièmement, comme je l'ai mentionné, un gros problème avec les verrous est qu'un programme fait de méthodes thread-safe n'est pas nécessairement un programme thread-safe. La vérification formelle des méthodes individuelles n'aide pas nécessairement, et l'analyse du programme entier est difficile pour les programmes non triviaux.
Eric Lippert
6
@mrpyo: Troisièmement, le gros problème de l'analyse formelle est que qu'est-ce que nous faisons fondamentalement? Nous présentons une spécification des conditions préalables et postconditions et vérifions ensuite que le programme répond à cette spécification. Génial; en théorie c'est totalement faisable. Dans quelle langue la spécification est-elle écrite? S'il existe un langage de spécification non ambigu et vérifiable, écrivons simplement tous nos programmes dans ce langage et compilons -le . Pourquoi on ne fait pas ça? Parce qu'il s'avère qu'il est vraiment difficile d'écrire des programmes corrects dans le langage de spécifications aussi!
Eric Lippert
2
Il est possible d'analyser l'exactitude d'une demande en utilisant des conditions préalables / postérieures (par exemple, en utilisant des contrats de codage). Cependant, une telle analyse n'est possible qu'à condition que les conditions soient composables, ce qui n'est pas le cas des verrous. Je noterai également que la rédaction d'un programme d'une manière qui permet l'analyse nécessite une discipline rigoureuse. Par exemple, les applications qui ne respectent pas strictement le principe de substitution de Liskov ont tendance à résister à l'analyse.
Brian