kantien a écrit 1239 commentaires

Alors quelques précisions: […]

C'est globalement ce que j'en avais compris des deux articles du membre de l'équipe chargée du compilateur. L'idée étant de pouvoir rajouter un smart pointer Gc<T> dont l'intention serait similaire à Rc<T>. Si la gestion automatique est basée sur du comptage de références, je comprends pourquoi la politique de gestion est drastique via le borrow checker (comme éviter des cycles dans le graphe des pointeurs qui sont gérés par des éphémérons dans le cas du GC d'OCaml).

La différence peut être mince, comme tu le soulignes avec les unikernels, mais je dirais qu'un langage système permet de maîtriser suffisamment parfaitement le comportement du code pour pouvoir écrire du code temps-réel (au sens temps réel dur, pas au sens globalement performant).

Mais dans ce cas ne faut-il pas une gestion totalement manuelle de la mémoire pour faire ce genre de chose ? Un langage tel que Rust peut-il s'attaquer à ce genre de problématique avec son mode de gestion automatique ?

Mais justement le lien que j'ai donné explique bien que Haskell va donner de très bon débit, mais va avoir des problèmes de latences ; ton benchmarck au final est équivalent à tester un débit moyen, mais ne va pas du tout tester les problèmes de latences, parce que 1) c'est pénible à tester 2) ce n'est pas ton problème.

Effectivement mon benchmark ne montre que le débit moyen, j'utilise time, mais parce que n'étant pas programmeur je ne connais pas les outils pour faire de la mesure de latence. En réalité, la modification que j'ai apporté au code OCaml de départ est plus un sketch of proof pour régler des problèmes de latence liés au GC. Ce qui fait que je suis passé de 25 s à 5.5 s est que j'ai fait disparaître une action du GC qui est responsable de la latence observée dans l'article que tu as cité sur le GC de Haskell : un parcours de la major heap.

Le tas est composé de deux memory pool : une minor heap et une major heap. La première sert pour les objets à courte durée de vie et est très efficace pour ce qui concerne les temps d'allocation et de désallocation mémoire. Lorsqu'elle est pleine le GC nettoie et transfert les structures encore en vie vers la major heap, puis à chaque fois qu'il fait cela, il nettoie par tranche cette major heap (de manière incrémentale) : c'est ce processus en mode stop the world qui prend plus du temps et génère de la latence. Dans mon code, j'ai adapté la gestion de la mémoire pour ne pas y avoir recours. Cela se passe en trois temps :

(* le memory pool de la minor heap est définie avec une taille
 * suffisante pour les besoins du calcul : un gros malloc une
 * bonne fois pour toute *)
let () = set_minor_heap (8 lsl max_depth)

(* c'est la partie proprement calculatoire du code *)
let worker (niter, d) =
  let c = ref 0 in
  for i = 1 to niter do
    (* je nettoie la minor heap pour éviter des transferts
     * vers la major heap *)
    Gc.minor();
    c := !c + check(make  i d) + check(make (-i) d)
  done;
  !c

(* le bout de code qui enchaîne les calculs
 * ne subit plus de latence *)
compute ~worker ~master tasks;

Sans cela j'avais un grand nombre de major collection, qui sont responsables des latences observées dans le fonctionnement du GC, là où maintenant je n'en ai plus aucune. ;-)

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Je vois un peu mieux le principe du borrow checker, je regarderai peu être plus en détail la façon dont Rust gère les références. Cela étant, au début de Rust il y avait un GC qu'ils ont abandonné, mais l'idée de remettre de la gestion automatique est toujours présente, cela semble être néanmoins compliqué. Il y a deux articles sur le sujet sur le blog d'un des membres de l'équipe du compilateur :

• GC and Rust Part 1: Specifying the Problem
• GC and Rust Part 2: The Roots of the Problem

Sinon quelle différence fais-tu entre un langage qui peut faire de la programmation système et un langage système ? Il y a des personnes qui écrivent des noyaux, sous la forme d'unikernel, en OCaml :

MirageOS is a library operating system that constructs unikernels for secure, high-performance network applications across a variety of cloud computing and mobile platforms. Code can be developed on a normal OS such as Linux or MacOS X, and then compiled into a fully-standalone, specialised unikernel that runs under the Xen hypervisor.

MirageOs

Il y a bien des problèmes de latence liés au GC qui peuvent apparaître (contrairement à la gestion totalement manuelle du C par exemple) mais cela se gère aussi en adaptant son fonctionnement à l'application. Je ne connais pas le fonctionnement du GC de Haskell (mais d'après l'article c'est similaire à celui de OCaml), mais pour celui de OCaml ce chapitre de Real World OCaml en détail bien le fonctionnement.

Le premier commentaire de l'article que tu cites renvoie sur un benchmark (dont je n'ai pas estimé la pertinence) qui mesure la latence d'un serveur web qui stocke une hashtable (pour le serveur web en OCaml, il utilise d'ailleurs une bibliothèque développée par l'équipe de MirageOS) :

J'ai eu une polémique récemment sur le coup de la latence du GC de OCaml en rapport à ce benchmark du benchmarkgame de chez Debian. J'avais mal estimé le rôle du GC dans les mauvais résultats : comme pour le cas de ton article, il y a des objets trop gros qui restent vivants trop longtemps. En adaptant la taille de la minor heap on obtient de meilleurs résultats (j'utilise aussi la bibliothèque functory, qui fait une sorte de MapReduce, pour le parallélisme ) :

open Functory.Cores
let () = set_number_of_cores 4

let set_minor_heap size = Gc.set {(Gc.get()) with Gc.minor_heap_size=size}

type tree = Empty | Node of tree * int * tree

let rec make i d =
  if d = 0 then Node(Empty, i, Empty)
  else let i2 = 2 * i and d = d - 1 in Node(make (i2 - 1) d, i, make i2 d)

let rec check = function Empty -> 0 | Node(l, i, r) -> i + check l - check r

let min_depth = 4
let max_depth = 
  let n = try int_of_string(Array.get Sys.argv 1) with _ -> 10 in
  max (min_depth + 2) n

(*
* c'est ici que j'adapte la taille de la minor heap 
* ce qui évite de nombreuse copie entre la minor et la major heap
* et réduit grandement la latence due au GC 
*)
let () = set_minor_heap (8 lsl max_depth)

let stretch_depth = max_depth + 1

let () =
  let c = check (make 0 stretch_depth) in
  Printf.printf "stretch tree of depth %i\t check: %i\n" stretch_depth c

let long_lived_tree = make 0 max_depth

let worker (niter, d) =
  let c = ref 0 in
  for i = 1 to niter do 
    Gc.minor();
    c := !c + check(make  i d) + check(make (-i) d)
  done;
  !c

let () =
  flush stdout;
  let tasks =
    let l = ref [] in
    for i = ((max_depth - min_depth) / 2 + 1) - 1 downto 0 do
      let d = min_depth + i * 2 in
      let niter = 1 lsl (max_depth - d + min_depth) in
      l := ((niter, d), None) :: !l
    done;
    !l
  in
  let res = ref [] in
  let master ((niter, d), _) c =
    res := (2*niter, d, c) :: !res;
    []
  in
  (* il n'y a plus de major collection pendant ce calcul *)
  compute ~worker ~master tasks;
  let log (niter, d, c) =
    let s = Printf.sprintf "%i\t trees of depth %i\t check: %i" niter d c in
    print_endline s;
  in
  List.iter log (List.sort (fun (_, d, _) (_, d', _) -> compare d d') !res);
  Printf.printf "long lived tree of depth %i\t check: %i\n"
    max_depth (check long_lived_tree)

avec ce code, sur ma machine à 4 cœurs, j'obtiens comme résultat standard avec un time btree 20 :

real    0m5.411s
user    0m16.320s
sys     0m0.492s

là où avec le code C le plus performant je suis dans cet ordre de grandeur :

real    0m3.721s
user    0m13.144s
sys     0m0.204s

c'est pas si mal et bien mieux que le 25.82 s du meilleur code OCaml du test. D'autant que, n'étant pas moi même programmeur (je suis mathématicien et logicien, pas informaticien), il est fort probable qu'un spécialiste du langage puisse encore améliorer cela.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Oui c'est ce que je disais dans mon commentaire avec "si les objets contenus sont mutable ils pourraient être modifiés de l'extérieur malgré ça"

J'avais bien compris, mais je préférais illustrer par un exemple pour que ceux qui se demandent comment éviter ces effets de bords puissent avoir une illustration du problème. Résultat cela m'a amené à regarder s'il n'y avait pas une fonction de copie profonde d'une structure en Python, et voilà : copy.deepcopy() :-)

>>> class Test:
...     def __init__(self, items=()):
...       from copy import deepcopy
...       self.items = list(deepcopy(items))
... 
>>> l = [1, [2, 3], 4]
>>> a = Test(l)
>>> l.append(5)
>>> l[1].append(6)
>>> l
[1, [2, 3, 6], 4, 5]
>>> a.items
[1, [2, 3], 4]

La décorrélation est totale ! \o/

Et le système d'emprunt de références va tout de même garantir qu'un seul endroit du code a la responsabilité de modification à un instant T.

C'est un système de lock pour les problèmes d'accès concurrents ? Ou si plusieurs structures se partagent une référence, seule une peut la modifier jusqu'à ce qu'elle soit désallouée et une autre en prend le contrôle, et ainsi de suite ? (j'essaye de traduire les notions de propriétaire/temps de vie).

le système de typage est moins puissant qu'en Haskell/OCaml

Il y a des travaux pour améliorer encore celui d'OCaml pour pouvoir faire du polymorphisme ad-hoc et de la surcharge d'opérateur en utilisant son système de module et les foncteurs. Et on peut aussi manipuler des références (mais là c'est sans garde-fou) et faire de la programmation système en OCaml (la seule limite actuelle, c'est le GC qui ne gère pas les accès concurrents sur la major heap ce qui pose problème pour le parallélisme, cf multicore OCaml).

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

C'est même plus propre par rapport à ma solution et au problème initial : si on passe une liste dans l'appel au constructeur, on peut se retrouver au même désagrément sur les effets de bords.

>>> class Test:
...    def __init__(self, items=None):
...      self.items = [] if items is None else items
...    
...    def add(self, item):
...      self.items.append(item)
... 
>>> l = [1, 2, 3]
>>> a = Test(l)
>>> l.append(4)
>>> a.items
[1, 2, 3, 4]

Là où avec ta solution, en plus d'accepter plus de type comme paramètre du constructeur, l'attribut est un peu mieux décorrélé (mais pas totalement) de l'argument.

>>> class Test:
...     def __init__(self, items=()):
...         self.items = list(items)
... 
>>> l = [1, [2, 3], 4]
>>> a = Test(l)
>>> l.append(5)
>>> a.items
[1, [2, 3], 4]
>>> l[1].append(6)
>>> a.items
[1, [2, 3, 6], 4]
>>>

Je ne sais pas ce que sont les notions de propriétaires/temps de vie en Rust, mais je dirais pour ma part : comme quoi le fonctionnel pur (ou l'observationnellement immuable) ça a son intérêt ! :-)

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Heu, le gestionnaire d'openSUSE, construit autour de libsolv?

Je ne connaissais pas. Quel est l'ordre de grandeur du temps de résolution ?

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Je suis entrain de me former à Python. Comment expliquer ce comportement, et comment faudrait-il modifier le code pour avoir un bon fonctionnement ?

Le comportement observé est du au fait que les arguments optionnels ne sont évalués qu'une seule fois lors de la définition de la fonction. S'ils sont mutables, et qu'on les affecte comme attribut aux objets de la classe, ils ne sont alors pas propre aux objets mais deviennent des variables de classe. Pour éviter cela, si ce n'est pas ce que l'on souhaite, il faut utiliser la solution de flan et utiliser la valeur None comme paramètre par défaut, puis tester dessus pour avoir des listes vides différentes pour chaque objet de la classe.

>>> class Test:
...   def __init__(self, items=None):
...     self.items = [] if items is None else items
...   
...   def add(self, item):
...     self.items.append(item)
... 
>>> a = Test()
>>> a.add('foo')
>>> b = Test()
>>> b.add('bar')
>>> a.items
['foo']
>>> b.items
['bar']

En OCaml, par exemple, les arguments optionnels sont implicitement représentés par le type polymorphe 'a option :

let foo ?x () =
  match x with
  | None -> print_endline "pas d'argument optionnel"
  | Some i -> Printf.printf "l'entier %i\n" i
;;
val foo : ?x:int -> unit -> unit = <fun>

foo ~x:2 ();;
l'entier 2
- : unit = ()

foo ();;
pas d'argument optionnel
- : unit = ()

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

C'est ce qui m'a séduit dans Haskell.

Je peux comprendre, les effets de bords et les valeurs mutables ça peut avoir des comportements surprenants :

>>> class Test:
...   def __init__(self, items=[]):
...     self.items = items
...   
...   def add(self, item):
...     self.items.append(item)
... 
>>> a = Test()
>>> a.add("foo")
>>> b = Test()
>>> b.add("bar")
>>> a.items
['foo', 'bar']
>>> b.items
['foo', 'bar']

La valeur optionnelle, qui est mutable, est initialisée une fois et partagée par toutes les instances ! \o/

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Tous les travaux universitaires existants montrent que le réel scandale de l'impôt français, c'est qu'il n'est pas assez progressif, et que les pauvres payent parfois plus que les riches.

J'aurais plutôt dit que le réel scandale de l'impôt français (il n'est pas le seul), c'est qu'il soit progressif. Le problème c'est l'assiette pas le taux : à taux fixe, celui qui a plus, paye plus.

Art. 13. Pour l'entretien de la force publique, et pour les dépenses d'administration, une contribution commune est indispensable : elle doit être également répartie entre tous les citoyens, en raison de leurs facultés.

Art. 14. Tous les Citoyens ont le droit de constater, par eux-mêmes ou par leurs représentants, la nécessité de la contribution publique, de la consentir librement, d'en suivre l'emploi, et d'en déterminer la quotité, l'assiette, le recouvrement et la durée.

Déclaration des Droits de l'Homme et du Citoyen de 1789

J'ai tendance à penser que dans la langue du XVIII^e l'expression « en raison de » est synonyme de « au prorata ».

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Haskell est énorme mais fait peur. Ocaml c'est sympa.

Honnêtement, pour ce qui est de leur système de types, c'est du pareil au même entre les deux; en dehors de l'absence de typeclasses en OCaml mais plus pour longtemps (modular implicits). Leur système prend leur inspiration dans la correspondance de Curry-Howard (ou correspondance preuve-programme, correspondance formule-type), ce qui en fait un système très expressif mais très exigeant : quand le compilateur gueule, c'est comme un mathématicien qui se plaint que la preuve d'une énoncé n'est pas correcte.

Là où Haskell peut faire peur, c'est que comme il fait du fonctionnel pur il faut recourir à des monades pour les effets de bords : ça peut effrayer au premier abord. OCaml de son côté permet de mélanger les paradigmes impératif, fonctionnel et objet; et faire de la réutilisation de code (comme pour le paradigme objet) via les variants polymorphes (je ne sais pas s'il y a un équivalent en Haskell).

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Pas du tout. Ça permet de se rendre compte de beaucoup d'erreurs à la compilation.

Effectivement, quel est l'intérêt de laisser compiler un code qui de toute façon ne pourra que planter à l'exécution ?¹ et cela, tout en refusant de le compiler parce qu'il est mal indenté… Il y a vraiment des choix de design que je ne comprends pas dans ce langage. :-/

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Jsais pas fais le test toi même.

Par curiosité j'ai installé une debian testing hier avec juste le destkop de base et le groupe de packages multimedia + les paquets apt-cusd et aspcud. J'ai voulu dist-upgrader en SID et avec le solver aspcud il a refusé de faire quoique ce soit me signalant une liste de paquets broken. Avec le solveur de base j'ai pas compté mais il a upgradé un bon nombre de packages sans forcément interrompre tout.

J'étais étonné alors hier soir j'ai installé une jessie 8.3-amd64 dans une VM avec Gnome. Une fois l'installation finie, j'installe apscud et apt-cudf. Je modifie mon source.list pour le faire ressembler à cela :

deb http://ftp.fr.debian.org/debian/ jessie main contrib non-free
deb-src http://ftp.fr.debian.org/debian/ jessie main contrib non-free

deb http://security.debian.org/ jessie/updates main
deb-src http://security.debian.org/ jessie/updates main

# jessie-updates, previously known as 'volatile'
deb http://ftp.fr.debian.org/debian/ jessie-updates main
deb-src http://ftp.fr.debian.org/debian/ jessie-updates main

# testing
deb http://ftp.fr.debian.org/debian/ testing main

# sid
deb http://ftp.fr.debian.org/debian/ sid main

Je lance un apt-get update puis apt-get dist-upgrade et apt-get dist-upgrade --solver aspcud. Les deux me proposent bien une procédure de mise à jour, la différence : le premier voulait me supprimer, entre autre, gdm3, gnome et gnome-shell. :-/

Pour ce qui est de la stratégie de aspcud c'est celle par défaut dans le fichier /etc/apt-cudf.conf :

solver: mccs-cbc , mccs-lpsolve
upgrade: -lex[-new,-removed,-notuptodate]
dist-upgrade: -lex[-notuptodate,-new]
install: -lex[-removed,-changed]
remove: -lex[-removed,-changed]
trendy: -lex[-removed,-notuptodate,-unsat_recommends,-new]
paranoid: -lex[-removed,-changed]

solver: *
upgrade: -new,-removed,-notuptodate
dist-upgrade: -notuptodate,-new
install: -removed,-changed
remove: -removed,-changed
trendy: -removed,-notuptodate,-unsat_recommends,-new
paranoid: -removed,-changed

c'est-à-dire qu'il va chercher à minimiser le nombre de nouveaux paquets -new et ceux qui ne sont pas à jour -notuptodate.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Mais que se passe-t-il si je donne à la fonction pgcd sans annotations des objets pour lesquels sont définis les opérations mod et comparaison à 0 (une classe polynôme par exemple) ? Est ce que le systême d'inférence va me mettre des bâtons dans les roues parce qu'il a fait de mauvaise hypothèses ?

En OCaml il n'y as pas de typeclasses comme en Haskell (il y a des travaux pour rajouter cela au langage) et on ne peut pas surcharger les opérateurs. Les opération mod et la comparaison à 0 ne fonctionnent que sur les types int et donc le système d'inférence identifie que les paramètres de la fonction sont nécessairement de type int.

( mod );;
- : int -> int -> int = <fun>

0;;
- : int = 0

Néanmoins on peut définir une module qui implémente le type polynôme avec sa propre fonction mod et sa valeur zero.

Pour reprendre le cas du pgcd si je compare la valeur à un float comme 0.0 le système se plaindra :

let rec pgdc a b =
  match a mod b with
  | 0. -> b
  | r -> pgcd b r
;;
Error: This pattern matches values of type float 
       but a pattern was expected which matches values of type int

Pour comparer avec python :

>>> def f(i):
...   print("l'entier %i" % i)
... 
>>> f(2)
l'entier 2
>>> def g():
...   f("a")
... 
>>> g()
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
  File "<stdin>", line 2, in g
  File "<stdin>", line 2, in f
TypeError: %i format: a number is required, not str

là où avec l'inférence de type l'erreur sur g est determiné statiquement à la compilation

let f i = Printf.printf "l'entier %i" i;;
val f : int -> unit = <fun>

f 2;;
l'entier 2- : unit = ()
let g () = f "a";;
Error: This expression has type string but an expression was expected of type int

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

D'après ce que wikipédia dit des systèmes structurels de types cela a l'air de correspondre.

En tout cas, moi je trouve la syntaxe concrète plus esthétique. Je ne trouve pas que le recours aux accolades pour délimiter les blocs et l'usage du point-virgule a tout bout de champ soit particulièrement joli. De plus, mettre un objet de type int dans une expression booléenne est surprenant sur le plan du typage (la transtypage 0 = false et true pour les entiers non nuls a son charme pour certain, moi je n'aime pas le mélange des genres). Le code qui s'approche de la manipulation des registres dans sa forme, c'est assez bas niveau : je préfère celui qui mime le principe même de l'algorithme d'Euclide pour le calcul du pgcd (on calcul le reste de la division euclidienne des opérandes, s'il est nul on renvoie le diviseur, sinon on poursuit avec le calcul du pgcd du diviseur et du reste : la traduction c'est l'affaire du compilateur). Enfin niveau performance, si l'on compile en natif, on se retrouve proche du C/C++.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Ou alors ils pourraient implémenter un système d'inférence de type à la Hindley-Milner ce qui leur permettrait de faire du duck-typing avec un typage statique et fort. :-)

(* définition avec annotations *)
let rec pgcd (a:int) (b:int):int =
  match a mod b with
  | 0 -> b
  | r -> pgcd b r
;;
val pgcd : int -> int -> int = <fun>

(* la même sans les annotations *)
let rec pgcd' a b =
  match a mod b with
  | 0 -> b
  | r -> pgcd' b r
;;
val pgcd' : int -> int -> int = <fun>
(* le système d'inférence s'en est sorti tout seul et a su typer correctement la fonction *)

(* je ne sais plus le type de la fonction, je demande à la boucle REPL *)
pgcd;;
- : int -> int -> int = <fun>

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Tu n'as pas graissé les bons mots : « quand ça devient tendu ». ;-)

Comme je l'ai écrit dans un autre message, j'utilise rarement apt-cudf, les réponses d'apt-get me conviennent presque toujours.

Pour ce qui est des réponses qu'il fournit, tout dépend des critères d'optimisation que tu lui passes. Son utilisation, pour un contrôle fin, est sans doute plus compliquée que pour apt-get; ce qui doit expliquer la raison pour laquelle ce n'est pas le gestionnaire par défaut, outre son temps de calcul plus long. Et je ne connais pas de tutoriel pour expliquer, pas à pas, son fonctionnement de base. Pour les critères de base, il y a bien cette page sur le projet Mancoosi : MISC-2012 optimization criteria mais pour un utilisateur lambda cela doit paraître assez abscons.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Donc les tests montrent que ce nouveau solveur est vraiment mieux que tous les autres.
En plus l'un des auteurs a été DPL plusieurs années de suite et a donc une grande aura dans le projet Debian.
Question : pourquoi est-ce que apt ne passe pas en deprecated au profit d'aspcud et apt-cudf qui seraient installés par défaut ?

C'est une question que l'on peut légitimement se poser d'autant qu'un autre ancien DPL, en la personne de Lucas Nussbaum, a participé au projet Mancoosi. N'étant pas développeur Debian, je ne sais rien des discussions qu'ils ont pu avoir sur le sujet, mais je suppose qu'ils doivent avoir leur raison pour avoir laisser les choses en l'état. Personnellement j'utilise apt-get et ne bascule sur apt-cudf que lorsque la solution proposée par le premier ne me convient pas. Pour une administration quotidienne et « standard », apt-get fait bien son job et le temps de calcul est bien moins long (il ne s'attaque pas au même problème).

En revanche, les projets Edos et Mancoosi ont eu une incidence sur les processus d'assurance qualité chez Debian. L'étude du graphe de dépendance entre les paquets permet d'identifier les paquets qui ne sont pas installables, périmés ou critiques pour la distribution :

• Strong dependencies between software components
• Mining Component Repositories for Installability Issues
• Learning from the Future of Component Repositories
• Dependency Hell sur le wiki Debian.

Cela étant, en dehors du gestionnaire de paquets OPAM (Ocaml PAckage Manager) qui est un gestionnaire de paquets sources à la mode Gentoo, je ne connais pas de gestionnaires dont l'architecture est nativement construite autour d'un solveur SAT pour la gestion des dépendances.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

En même temps, si tu n'utilises pas les bons outils pour ce genre de pratique free-style, il ne faut pas s'étonner si ça pose problème au niveau du gestionnaire de paquets.

Le solveur interne d'apt-get est une vrai bouse quand ça devient tendu (constat qui n'est pas propre au solveur d'apt-get, c'est le cas de la quasi-totalité des gestionnaires de paquets et pas seulement chez Debian), ce n'est pas un nouveauté, mais le problème de la gestion des dépendances est un problème ardu.

Lors du projet Edos qui se concentrait sur le problème spécifique de la construction de distribution linux, il a été montré en 2006 que le problème de la gestion des dépendances est un problème NP-complet par réduction à un problème de type 3-SAT (voir cet article].

S'en est suivi le projet Mancoosi étalé sur quatre années (de 2008 à 20011) qui a, entre autre, prolongé l'étude de cette problématique. Le projet a donné lieu a un concours de solveur SAT dont est sorti vainqueur le solveur aspcud. Le DPL de l'époque, Stefano Zacchiroli, a même mis au point un DSL pour les échanges entre les solveurs et les gestionnaires de paquets : CUDF.

Dans un article coécrit avec Pietro Abate, Roberto Di Cosmo et Ralf Treinen, ils proposaient une nouvelle architecture pour les gestionnaires de paquets : MPM, a modular package manager. Pour l'occasion ils ont juste développé un prototype en python qu'ils comparaient à apt, aptitude, cupt et smart dans des configurations constituées à l'époque de : sarge, etch , lenny, squeeze et sid (ils testent les 5 configurations en ajoutant progressivement chacun de ces dépôts dans le source.list). Pour ce qui est de trouver un scénario d'upgrade qui ne casse pas le système, le prototype a mis à l'amende tous ses concurrents ! :-)

Aujourd'hui, comment faire ? Installer aspcud et apt-cudf ! Pour se faire une idée de leur utilisation, on pourra se référer à ces articles sur le blog de Roberto Di Cosmo.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Effectivement, le livre n'explique pas le lien entre CPS et élimination des coupures : celui-ci est plutôt le fruit d'une réflexion personnelle en faisant un raisonnement par analogie via la correspondance de Curry-Howard. Cela étant, c'est plus une réflexion informelle qu'autre chose et il se peut que je pousse l'analogie au-delà de ses limites acceptables (ce n'est pas mon domaine de spécialisation, je ne suis pas informaticien théoricien).

Je vais détailler le schéma de pensée qui m'a amené à cette conclusion. Que dit la règle des coupures en théorie de la démonstration ? Elle généralise le principe du modus ponens : si A alors B, or A donc B. La forme générale de la règle des coupures est donné en bas de la page 11 dans le livre sus-cité : si j'ai deux séquents dans lesquels une même proposition A se trouve dans les prémisses de l'un et dans les conclusions de l'autre, alors je peux produire un séquent dans lequel celle-ci a disparue en fusionnant les prémisses et les conclusions. En haut de la page 12, cette règle est exprimée sous la forme particulière du modus ponens : si j'ai une preuve P1 qui a pour conclusion la proposition A, puis une preuve P2 dont la conclusion est la proposition B et dont A fait partie des prémisses, alors je peux produire une preuve P3 de la proposition B dans laquelle A ne fait plus partie des prémisses. Ensuite, la règle d'élimination des coupures affirme qu'il est également possible de produire une preuve P4 de la proposition B directement sans faire intervenir la preuve P1 qui produit la conclusion A ni la preuve P2 qui produit la proposition B lorsqu'elle a la proposition A dans ses prémisses.

Maintenant passons dans le monde des programmes via la correspondance de Curry-Howard. Cette dernière nous dit que chacune des preuves Pi correspond à un programme et les formules qu'elles manipulent sont les types des objets des programmes. Ainsi la preuve P1 produit un objet de type A qui est consommé par la preuve P2 pour produire un objet de type B ce qui, par coupure, fournit un programme P3 qui produit un objet de type B mais qui dans son exécution (par son recours à P1) doit allouer sur le tas un objet de type A (qui sera à terme désallouer par le ramasse-miette) : le modus ponens est la règle de typage de l'application de fonction :

let app (f:'a->'b) (x:'a):'b = f x;;
val app : ('a -> 'b) -> 'a -> 'b = <fun>

Mais, la règle d'élimination des coupures nous dit qu'il est possible d'écrire un programme P4 qui se passe totalement de cette allocation. Prenons maintenant l'exemple donné par Pierre Chambart dans l'article de blog chez OCamlPro pour calculer le minimum et le maximum d'une liste :

let rec fold_left f init l =
  match l with
  | [] -> init
  | h :: t ->
    let acc = f init h in
    fold_left f acc t

let keep_min_max (min, max) v =
  let min = if v < min then v else min in
  let max = if v > max then v else max in
  min, max

let find_min_max l =
  match l with
  | [] -> invalid_arg "find_min_max"
  | h :: t ->
    fold_left keep_min_max (h, h) t

Les types de ces trois fonctions sont :

val fold_left : ('a -> 'b -> 'a) -> 'a -> 'b list -> 'a = <fun>
val keep_min_max : 'a * 'a -> 'a -> 'a * 'a = <fun>
val find_min_max : 'a list -> 'a * 'a = <fun>

Icikeep_min_max joue le rôle de la preuve P1 (c'est un lemme qui est responsable d'allocation) et fold_left joue le rôle de la coupure qui produit la preuve P3 à savoir find_min_max. Puis dans la suite de l'article, en transformant son code via CPS, il produit la preuve P4 sans coupure find_min_max_k2 qui se passe d'allocation et qui aura la même fonction que la fonction find_min_max initiale si on lui passe comme continuation la fonction identité fun x -> x.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

L'avantage d'utiliser un tableau est en fait celui de la Réification, on ne traite plus une méthode de calcul mais des valeurs. Par exemple si on veut tracer les courbes qui correspondent à la suite pour un n fixé, un nombre énorme de calculs seront refait plusieurs fois, alors qu'en ayant enregistré toutes les étapes intermédiaires, on ne refait jamais deux fois le même calcul, et le tableau se calcule en temps linéaire par rapport à sa taille.

Oui, c'est une manière comme une autre d'allouer sur le tas (en l'occurrence ici dans une matrice) ce qui autrement resterait dans la pile d'appel à chaque calcul de la fonction, ce qui revient à faire de la mémoïsation.

À l'inverse, dans certain cas, on peut vouloir éviter ce genre d'allocation pour gagner du temps de calcul lorsque l'on n'a pas besoin de réutiliser ultérieurement les données produites (traitement en flux) :
transformation CPS et réification de la pile d'appel
éviter les allocations en utilisant le paradigme Continuation Passing Style

Pour le rapport avec la preuve de la correction d'algorithme et la théorie de la démonstration, voir par exemple le livre Categorical semantics of linear logic aux pages 11-13 sur l'élimination des coupures.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

C'est si gentiment demandé. :-) Bruno Michel t'as en partie donnée une réponse satisfaisante.

D'abord la citation que je donnais provient du site du benchmarck à la page why measure toy benchmark programms ?. Je la remets pour que ce soit clair, et le graissage n'est pas de moi mais se trouve dans la page original :

Non-motivation: We are profoundly uninterested in claims that these measurements, of a few tiny programs, somehow define the relative performance of programming languages.

Leur objectif, clairement affiché (« we are porofoundly unintersted »), n'est pas de se servir des résultats comme base pour determiner les performances relatives des différents langages. Visiblement, tu ne lui donnes pas le même objectif que ses auteurs.

Ensuite, passons à l'analyse d'un des tests, celui qui semble te préoccuper le plus : la gestion de la mémoire. Pour mettre à l'épreuve les GC, il y a le test binary trees

The work

The work is to create binary trees - composed only of tree nodes all the way down-to depth 0, before any of those nodes are GC'd - using at-minimum the number of allocations of Jeremy Zerfas's C program. Don't optimize away the work.

Le programme de Jeremy Zefra's, écrit en C donc avec gestion manuelle de la mémoire, est celui qui sert de référence et qui réalise le meilleur score du test

Maintenant, comparons ses performances face à deux langages avec GC :

Code source	temps	charge cpu
C gcc #3	3.26	59% 76% 78% 99%
Haskell GHC	25.62	36% 88% 49% 36%
OCaml #2	25.82	89% 95% 54% 64%
OCaml #5	41.55	1% 100% 1% 1%

Et là, on peut se dire : ces deux langages, avec leur gestion automatique, se prennent une valise ! M'enfin, OCaml a deux codes pour le test et avec un grande différence de temps entre le deux, pourquoi ? Alors, on regarde la charge CPU : le second est mono thread et pas le premier, donc déjà il y a une optimisation faite qui ne change rien au coût du GC et qui consiste dans la parallélisation des calculs. Mais au fait, n'y aurait-il pas d'autres code en C qui ont passé le test ? Et bien si, et voilà le résultat :

Code source	temps	charge cpu
C gcc #5	21.20	96% 89% 97% 97%

Tiens, on se rapproche déjà plus des performances de OCaml et Haskell ! Mais que ce passe-t-il donc dans ce code C par rapport au super code de la mort qui tue en 3.26 secondes ? Tout simplement il optimise bien moins le parallélisme. Il utilise pthread là où le plus rapide utilise apr-1.0.

Au final, les résultats du test (qui était sensé mettre à l'épreuve les GC) mais surtout en avant des optimisations de parallélisme. On trouvera les différents codes à ces adresses :

• code C gcc #3
• code C gcc #5
• code Haskell GHC
• code OCaml #2
• code OCaml #5

On pourra également noté que pour le code OCaml le plus rapide le parallélisme est fait à l'arrache (voir dans les commentaires : « Rough parallelization by Mauricio Fernandez »), que le code Haskell n'a pas le droit (c'est la règle du jeu) de profiter de son évaluation paresseuse (ce qu'aucun développeur ne fera dans du code réel) :

--
-- an artificially strict tree. 
--
-- normally you would ensure the branches are lazy, but this benchmark
-- requires strict allocation.
--
data Tree = Nil | Node !Int !Tree !Tree

et enfin que le code compilé OCaml ne profite pas de dernières optimisations apportées dans le compilateur par Flambda, contrairement au code C qui est compilé avec l'option -O3 de gcc.

Cela étant pour répondre à ta proposition de soumettre mon propre au code au test (qui devrait uniquement consister en une optimisation du parallélisme pour se rapprocher du haut du panier), j'ai autre chose à faire de mon temps que de jouer à « qui à la plus grosse ? ». Je suppose qu'il en est de même pour Fabrice Le Fessant, le fondateur de OCaml Pro, vu que c'est lui qui a soumis le code le plus lent (enfin, il a apporté des modifications sur le code d'un autre) : il sait pertinemment optimiser du calcul parallèle en OCaml, mais il doit avoir d'autres chats à fouetter.

Les benchmarks, c'est bien, encore faut-il en analyser correctement les résultats. ;-)

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

D'autant que sur un tel code, la définition de la fonction suit le schéma de la preuve par récurrence qui justifie son bon fonctionnement (c'est le principe même des langages fonctionnels, et des structures récursives).

Exemple en OCaml sur le calcul de la hauteur d'un arbre binaire :

type 'a btree = Empty | Btree of'a tree * a * 'a tree

let rec depth t = 
  match t with
  (* arbre vide, ou preuve de P(0) i.e on initialise la récurrence *)
  | Empty -> 0
  (* arbre à deux branches, ou preuve de P(n) => P(n+1) *)
  | Btree(left, _, right) -> (max_int (depth left) (depth right)) + 1

depth (Btree(Empty, 1, Btree(Empty, 0, Empty)))
- : int = 2

Dans ton cas, c'était une récurrence double et à la lecture du code il n'est pas difficile de se convaincre qu'il est correct. Sur des cas plus complexes, cela demande plus de réflexion, mais en fonctionnel cela reste plus simple.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

C'est considéré comme une clause léonine ?

La clause d'un contrat est dite "léonine" lorsque les charges en sont supportées par une seule des parties alors que l'autre en tire tous les avantages. (Voir dans le domaine du droit des sociétés, le second alinéa de l'article 1844-1 du Code civil).

L'existence d'une telle clause dans un contrat ne le rend pas nul, la clause est seulement réputée non écrite.

Cela ne me choquerai pas, mais y a-t-il déjà eu des jugements allant dans ce sens ?

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Il y avait de l'exagération volontaire dans mon propos. Je peux même comprendre, qu'en dehors du niveau A, SCADE puisse apparaître comme un char d'assaut (cela étant, en prenant en compte la nécessité d'avoir des développeurs formés à l'outil, le coût serait-il supérieur pour du niveau B ?).

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Comparatif intéressant et sans doute plus impartial. L'article aurait pu s'intituler : « Quand la pratique peine à rejoindre la théorie ». :-)

En même temps, il y a peut être de la mauvaise foi non assumée chez une personne qui considère le benchmarkgame de chez Debian comme une « référence en terme d'optimisation » pour comparer les langages, là où pour les auteurs du comparatif ce n'est même pas le cas :

Non-motivation: We are profoundly uninterested in claims that these measurements, of a few tiny programs, somehow define the relative performance of programming languages.

source

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Si j'étais cynique, je dirais que cela me fait penser à la scène de Fight Club dans laquelle Edward Norton explique son travail à son « amie à usage unique » au début du film : « Une voiture construite par ma société roule aux alentours de 90 km/h, le différentiel arrière se bloque. La voiture se crache est prend feu avec toute la famille à bord. Question : faut-il déclencher un rappel de ce modèle ? Prendre le nombre de véhicules concernés : A; le multiplier par le taux probable de défaillances : B; puis multiplier le résultat par la moyenne des sommes que l'on a été condamné à verser : C. A * B * C = X, si cet X est inférieur au coût d'un rappel : on ne fait rien. » :-/

Transposer le principe aux coûts de développements…

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.