Explorateur d’entrelacements de threads

Énumérez les déroulements bornés et séquentiellement cohérents de deux ou trois programmes courts, puis inspectez résultats et témoins réels.

À propos de cet outil

Énumérez tous les déroulements permis de deux ou trois programmes courts, sous cohérence séquentielle. Choisissez un exemple, modifiez les valeurs initiales ou programmes puis Explorer. Une modification efface les anciens résultats. La mise à jour perdue a 20 déroulements : x=1 dans 18, x=2 dans 2. Un mutex rend lecture–incrément–écriture exclusif.

Une instruction par ligne : r1 = x lit une variable partagée, x = r1 écrit un registre local, x = 5 affecte un entier partagé, r1 = r1 + 1 calcule dans un registre local. Addition, soustraction et multiplication acceptent entiers et noms. lock(m) attend un mutex libre ; unlock(m) exige sa possession. wait(x == 1) attend une comparaison vraie sur une variable partagée ; !=, <, >, <= et >= fonctionnent aussi. Les noms ignorent la casse ; r suivi de chiffres est local au thread, les autres sont partagés. Une valeur non initialisée vaut zéro. Valeurs initiales : x = 0, y = 1 ; les doublons sont refusés. // commence un commentaire.

Les résultats comprennent variables partagées et registres locaux. Les proportions comptent les chemins énumérés, jamais des probabilités réelles. Ordre des threads indique un résultat possible en exécutant chaque thread entièrement à son tour ; Entrelacé indique qu’il nécessite l’entrelacement d’instructions. Ces labels ne prouvent ni présence ni absence d’une course de données. Bloqué signifie qu’aucun thread inachevé ne peut avancer : interblocage de mutex ou attente insatisfaite. Déroulement ouvre un témoin réel avec valeurs intermédiaires partagées et locales.

Limites : 18 instructions au total, 80 000 déroulements avant restrictions mutex/attentes, 4 096 caractères par entrée et 64 par nom. Valeurs et calculs restent dans ±9 007 199 254 740 991. Ce modèle pédagogique local exclut boucles, temps réel, réordonnancement du compilateur, atomiques et mémoire faible. Comparez les publications : écrire ready avant data permet de lire 0 ; inverser les écritures ne permet que 42.

La recherche tourne dans un worker local pour garder la page réactive. La barre d’activité n’affiche pas de pourcentage : mutex et attentes peuvent terminer des chemins plus tôt. Le compteur indique les déroulements terminaux explorés ; Annuler arrête le worker en gardant les entrées. Modifier ou quitter arrête aussi le calcul et ignore les réponses tardives. Le filtre cherche les valeurs partagées et registres sans distinction de casse ; tous les termes séparés par espaces doivent correspondre. Les valeurs initiales non référencées figurent une seule fois dans leur section et sont omises des cellules répétées.

Programmes, y compris T3 masqué, nombre de threads, valeurs initiales brutes, erreurs, filtre et témoin choisi/ouvert conservés localement. Structure, sommes et correspondance des entrées sont vérifiées ; le témoin sélectionné est rejoué avant affichage. Ce n’est pas un certificat inviolable. Les résultats importés sont toujours recalculés dans le worker, jamais acceptés sur la foi des compteurs du fichier. Aucun calcul serveur.

Seules les valeurs saisies sont conservées dans ce navigateur. Les résultats calculés et historiques ne sont pas enregistrés.