Il y a quand même des patterns connus pour prouver qu'un calcul distribué termine par exemple. On peut montrer aussi des propriétés d'autostabilisation ou des choses comme ça.
Je pense que tu t'égares :)
Que cela soit en distribué ou pas, on a un système que l'on modélise, une spec, un programme et des outils de preuves pour montrer que le programme est conforme à la spec, étant donné le système considéré.
Pour du code, généralement le système est connu : selon le langage tu as un jeu d'instructions, un système de type (c'est encore plus facile à formaliser/prouver, si ton langage a du typage fort), tu peux éventuellement modéliser la mémoire pour certains langages bas niveau et mettre 2/3 contraintes de QoS (puissance CPU, etc.), mais globalement cela s'arrête là.
Pour un système distribué, en plus d'avoir les contraintes d'implémentations, tu as les contraintes de distributions et de sécurité (cf. fautes byzantines), qui ajoutent des problèmes au niveau spécification. De tels problèmes sont connus, il s'agit par exemple de consensus distribué, de synchronisation en environnement asynchrone, d'authentification forte,...etc
Ce sont deux domaines différents, qui ont tous les deux des cas d'usage difficiles à prouver, mais ce que je veux te montrer c'est que si tu apportes de la distribution, tu apportes de la complexité dans le système, donc tout devient plus difficile à commencer par la spécification.
Pour finir :
Il y a quand même des patterns connus pour prouver qu'un calcul distribué termine par exemple. On peut montrer aussi des propriétés d'autostabilisation ou des choses comme ça.
Avec une modélisation juste d'Internet, c'est-à-dire un système distribué asynchrone dans lequel on ne sait pas distinguer le cas où une machine est lente à répondre ou si elle est en panne, tes propos sont faux. C'est un résultat théorique très connu dans le domaine de l'algorithmique distribué, on le nomme « FLP », pour « Fischer, Lynch, Paterson » et il dit en termes simplifiés :
On ne peut pas réaliser un consensus dans un système distribué asynchrone (modèle message passing) , si on tolère au plus une panne (réseau ou machine).
Ce qui signifie que non : on ne peut pas montrer qu'un consensus se termine ou qu'un système distribué se stabilise, c'est impossible ! Il existe bien entendu des astuces (se reposer sur un serveur centralisé qui fait fois), mais formellement on ne peut pas prouver ce genre de chose si on prend les hypothèses d'un réseau de type WAN.
[^] # Re: On verra
Posté par vlamy . En réponse à la dépêche Core Infrastructure Initiative. Évalué à 6. Dernière modification le 28 avril 2014 à 09:35.
Je pense que tu t'égares :)
Que cela soit en distribué ou pas, on a un système que l'on modélise, une spec, un programme et des outils de preuves pour montrer que le programme est conforme à la spec, étant donné le système considéré.
Pour du code, généralement le système est connu : selon le langage tu as un jeu d'instructions, un système de type (c'est encore plus facile à formaliser/prouver, si ton langage a du typage fort), tu peux éventuellement modéliser la mémoire pour certains langages bas niveau et mettre 2/3 contraintes de QoS (puissance CPU, etc.), mais globalement cela s'arrête là.
Pour un système distribué, en plus d'avoir les contraintes d'implémentations, tu as les contraintes de distributions et de sécurité (cf. fautes byzantines), qui ajoutent des problèmes au niveau spécification. De tels problèmes sont connus, il s'agit par exemple de consensus distribué, de synchronisation en environnement asynchrone, d'authentification forte,...etc
Ce sont deux domaines différents, qui ont tous les deux des cas d'usage difficiles à prouver, mais ce que je veux te montrer c'est que si tu apportes de la distribution, tu apportes de la complexité dans le système, donc tout devient plus difficile à commencer par la spécification.
Pour finir :
Avec une modélisation juste d'Internet, c'est-à-dire un système distribué asynchrone dans lequel on ne sait pas distinguer le cas où une machine est lente à répondre ou si elle est en panne, tes propos sont faux. C'est un résultat théorique très connu dans le domaine de l'algorithmique distribué, on le nomme « FLP », pour « Fischer, Lynch, Paterson » et il dit en termes simplifiés :
Ce qui signifie que non : on ne peut pas montrer qu'un consensus se termine ou qu'un système distribué se stabilise, c'est impossible ! Il existe bien entendu des astuces (se reposer sur un serveur centralisé qui fait fois), mais formellement on ne peut pas prouver ce genre de chose si on prend les hypothèses d'un réseau de type WAN.