Principe de Rewind VM

Rewind VM est une machine virtuelle déterministe où chaque exécution d’une construction Nix dépend uniquement de ses entrées, y compris le planificateur de threads. Sur un ordinateur portable à 16 cœurs, le scénario de dépôt concurrent a échoué dans 396 sur 1 000 exécutions, alors qu’en mode monoprocesseur aucun échec n’est observé. La VM expose un seul cœur virtuel, ce qui permet de reproduire exactement le même état jusqu’à l’étape où le planificateur interrompt un thread.

Gestion des entrées via Nix

Le point d’entrée de rewind check est une dérivation Nix, pouvant être référencée par un flake. Nix calcule automatiquement la liste complète des entrées : source du programme, compilateur, bibliothèques, noyau et configuration de la VM. Ces éléments sont empaquetés dans une image erofs en lecture seule. L’identifiant de chaque exécution est un hachage dérivé des mêmes entrées, similaire à un chemin du store Nix. Exemple de commande affichant le hachage :

rewind show 12feb5f8
rewind nix /nix/store/cr8rl40rjb9cmmcd9sxn9mpdrhvp53jj-bank-0.1.0.drv --epoch 1791331200 --clock branches --name bank-0.1.0 # 12feb5f832205a72

Après la construction, la VM renvoie le hachage NAR de chaque sortie, qui est comparé à la copie locale et aux caches binaires Nix, garantissant l’intégrité du build.

Intégration du débogueur et analyse des courses

Grâce à separateDebugInfo, Nix fournit les symboles de débogage et les sources correspondantes, stockés sur cache.nixos.org. Le service debuginfod récupère ces informations à la volée, permettant d’afficher le code source exact au point d’exécution :

rewind where c2f1cfac 3250 process 139 (bank), thread 141, at step 3250 # 4 deposit (bank.c:24)
22 int n = snprintf(line, sizeof line, "teller %d: %ld + %ld\n", teller, seen, amount);
23 > 24 if ( write ( 1, line, n ) != n )
25 return;
26 balance = seen + amount;

Le mode rewind gdb ouvre un fork de l’exécution à l’étape sélectionnée, avec tous les threads actifs. Aucun changement n’est introduit dans l’enregistrement, ce qui permet de placer des points d’arrêt, de surveiller des variables comme balance, puis de reprendre l’exécution ou de revenir à un autre pas.

Comparaison et diagnostics

La fonction rewind compare aligne deux exécutions et signale le premier pas où les traces divergent. Dans l’exemple, le dépôt du deuxième guichet passe de 150 à 200 dans la version réussie, alors que la version échouée conserve 150. En interrogeant le noyau invité à chaque pas, Rewind identifie le thread qui occupait le CPU au moment critique, sans nécessiter d’enregistrement supplémentaire. L’ensemble du processus de vérification sur le portable a duré 11 secondes, démontrant la rapidité du mécanisme.