Ce que je reproche à la communauté Linux n'est pas un manque de compétences techniques, mais un manque d'intérêt pour les méthodes formelles pour le logiciel. C'est une culture qui s'acquiert, qui est présente dans certains environnement (par exemple Mozilla a fait des choses très louables dans cette direction, et surtout Microsoft a su intégrer ça étonnamment bien en production, y-compris pour le développement kernel), mais absente en grande majorité du milieu du libre—qui aurait pourtant aujourd'hui la "puissance", en terme d'argents et de ressource, pour faire des choses très intéressantes dans ce domaine.
Il y a beaucoup de choses intéressantes à faire avant d'essayer de faire des preuves de correction complètes. Par exemple, garantir l'absence de comportements indéfinis dans une partie la plus grande possible du code serait déjà un très bon pas en avant; et ACSL par exemple peut servir à spécifier ce genre de propriétés de sûreté (un pointeur reste dans la bonne région mémoire).
Les gens de Microsoft ont développé des annotations formelles pour les drivers et le code noyau, qui peuvent être vérifiées par des outils d'analyse statique. Ça demande que les développeurs acceptent de s'en servir—et il y a sans doute des faux négatifs qui sont parfois casse-pieds—mais ça marche bien et ça a eu de bons effets. Ça existe depuis une décennie environ maintenant.
Je ne comprends pas trop le sens de ta (deuxième) remarque sur le multi-cœur dans SeL4. C'est vrai que la mémoire partagée est très difficile à gérer (formellement, mais aussi quand on programme) et que l'état de l'art ne gère pas bien cet aspect là. Est-ce une bonne raison de ne pas faire d'efforts pour intégrer les outils existants dans nos pratiques de développement, là où ils peuvent apporter quelque chose ?
[^] # Re: Virtualisation par défaut
Posté par gasche . En réponse à la dépêche Capsicum dans Linux : ça bouge !. Évalué à 4.
Ce que je reproche à la communauté Linux n'est pas un manque de compétences techniques, mais un manque d'intérêt pour les méthodes formelles pour le logiciel. C'est une culture qui s'acquiert, qui est présente dans certains environnement (par exemple Mozilla a fait des choses très louables dans cette direction, et surtout Microsoft a su intégrer ça étonnamment bien en production, y-compris pour le développement kernel), mais absente en grande majorité du milieu du libre—qui aurait pourtant aujourd'hui la "puissance", en terme d'argents et de ressource, pour faire des choses très intéressantes dans ce domaine.
Il y a beaucoup de choses intéressantes à faire avant d'essayer de faire des preuves de correction complètes. Par exemple, garantir l'absence de comportements indéfinis dans une partie la plus grande possible du code serait déjà un très bon pas en avant; et ACSL par exemple peut servir à spécifier ce genre de propriétés de sûreté (un pointeur reste dans la bonne région mémoire).
Les gens de Microsoft ont développé des annotations formelles pour les drivers et le code noyau, qui peuvent être vérifiées par des outils d'analyse statique. Ça demande que les développeurs acceptent de s'en servir—et il y a sans doute des faux négatifs qui sont parfois casse-pieds—mais ça marche bien et ça a eu de bons effets. Ça existe depuis une décennie environ maintenant.
Je ne comprends pas trop le sens de ta (deuxième) remarque sur le multi-cœur dans SeL4. C'est vrai que la mémoire partagée est très difficile à gérer (formellement, mais aussi quand on programme) et que l'état de l'art ne gère pas bien cet aspect là. Est-ce une bonne raison de ne pas faire d'efforts pour intégrer les outils existants dans nos pratiques de développement, là où ils peuvent apporter quelque chose ?