Pour faire du calcul concurrent distribué, il y a les formalismes basés sur le pi-calcul. Si tu parles de SMP (Symmetric Multiprocessing) en parlant spécifiquement de la mémoire partagée, il y a peu de formalismes spécialisés (enfin les travaux sur les modèles mémoire faibles s'en approchent le plus), mais de toute façon les gens ne sont pas convaincus qu'il y a de bons modèles de programmation qui exploitent la mémoire partagée. Ce qu'on sait faire c'est utiliser des types linéaires pour garder trace de "qui possède" les données, et donc permettre des passages de message zéro-copie dans un cadre SMP (en très gros c'est ce que vise Rust, et il y a aussi des langages de recherche plus formalisés sur le sujet). Enfin tu as les logiques de séparation (en) concurrentes, qui sont des extensions de la logique de Hoare à des raisonnements avec accès concurrent à des ressources partagées qui garantissent l'absence de race.
Si tu parles spécifiquement des spécificités des programmes bas-niveau faisant de la concurrence par mémoire partagée, la situation est en fait "meilleure" qu'avec les langages fonctionnels: la seule façon de coder un truc correct sans se tirer une balle est de comprendre ces sémantiques formelles et de prouver la correction du programme avec. À côté le lambda-calcul est délicieusement haut niveau et explicite, on n'a presque pas besoin de savoir comment ça marche pour coder correctement dans un langage fonctionnel… lambda.
[^] # Re: Mouais
Posté par gasche . En réponse au journal The Future of Functional Programming Languages. Évalué à 3.
Pour faire du calcul concurrent distribué, il y a les formalismes basés sur le pi-calcul. Si tu parles de SMP (Symmetric Multiprocessing) en parlant spécifiquement de la mémoire partagée, il y a peu de formalismes spécialisés (enfin les travaux sur les modèles mémoire faibles s'en approchent le plus), mais de toute façon les gens ne sont pas convaincus qu'il y a de bons modèles de programmation qui exploitent la mémoire partagée. Ce qu'on sait faire c'est utiliser des types linéaires pour garder trace de "qui possède" les données, et donc permettre des passages de message zéro-copie dans un cadre SMP (en très gros c'est ce que vise Rust, et il y a aussi des langages de recherche plus formalisés sur le sujet). Enfin tu as les logiques de séparation (en) concurrentes, qui sont des extensions de la logique de Hoare à des raisonnements avec accès concurrent à des ressources partagées qui garantissent l'absence de race.
Si tu parles spécifiquement des spécificités des programmes bas-niveau faisant de la concurrence par mémoire partagée, la situation est en fait "meilleure" qu'avec les langages fonctionnels: la seule façon de coder un truc correct sans se tirer une balle est de comprendre ces sémantiques formelles et de prouver la correction du programme avec. À côté le lambda-calcul est délicieusement haut niveau et explicite, on n'a presque pas besoin de savoir comment ça marche pour coder correctement dans un langage fonctionnel… lambda.