Explorador de intercalado de hilos

Enumera secuencias acotadas y secuencialmente consistentes de dos o tres programas cortos e inspecciona resultados y testigos reales.

Acerca de esta herramienta

Enumera todas las secuencias permitidas de dos o tres programas cortos con consistencia secuencial. Elige un ejemplo, modifica valores iniciales o programas y pulsa Explorar. Editar borra los resultados anteriores. La actualización perdida tiene 20 secuencias: x=1 en 18, x=2 en 2. Un mutex hace exclusiva la lectura–incremento–escritura.

Una instrucción por línea: r1 = x lee una variable compartida, x = r1 escribe un registro local, x = 5 asigna un entero compartido, r1 = r1 + 1 calcula en un registro local. Suma, resta y multiplicación aceptan enteros y nombres. lock(m) espera un mutex libre; unlock(m) exige poseerlo. wait(x == 1) espera una comparación verdadera de variable compartida; también admite !=, <, >, <= y >=. Los nombres ignoran mayúsculas; r seguido de cifras es local al hilo, los demás compartidos. Los valores sin inicializar son cero. Valores iniciales: x = 0, y = 1; se rechazan duplicados. // inicia un comentario.

Los resultados incluyen valores compartidos y todos los registros locales. Las proporciones cuentan rutas enumeradas, nunca probabilidades reales. Orden de hilos indica un resultado posible completando cada hilo por turno; Intercalado indica que necesita intercalar instrucciones. Estas etiquetas no prueban presencia ni ausencia de carreras de datos. Bloqueado significa que ningún hilo sin terminar puede avanzar: puede ser interbloqueo de mutex o espera no satisfecha. Secuencia abre un testigo real con valores intermedios compartidos y locales.

Límites: 18 instrucciones en total, 80.000 secuencias antes de restricciones mutex/esperas, 4.096 caracteres por entrada y 64 por nombre. Enteros y cálculos dentro de ±9.007.199.254.740.991. Modelo educativo local sin bucles, tiempo real, reordenación del compilador, atómicos ni memoria débil. Compara publicaciones: escribir ready antes de data permite leer 0; invertir el orden solo permite 42.

La búsqueda usa un worker local para mantener la página utilizable. La barra de actividad no muestra porcentaje: mutex y esperas pueden terminar rutas antes. El contador indica secuencias terminales exploradas; Cancelar detiene el worker y conserva las entradas. Editar o salir también detiene e ignora respuestas tardías. El filtro busca valores compartidos y registros sin distinguir mayúsculas; deben coincidir todos los términos separados por espacios. Los valores iniciales no usados aparecen una sola vez en su sección y se omiten de celdas repetidas.

Programas, incluido T3 oculto, número de hilos, valores iniciales originales, errores, filtro y testigo elegido/abierto se conservan localmente. Se comprueban estructura, sumas y correspondencia de entradas, y se reproduce el testigo elegido antes de mostrarlo. No es un certificado contra manipulaciones. Los resultados importados siempre se recalculan en el worker; no se confía en los contadores del archivo. Al superar 100000 caracteres de almacenamiento automático, el estado sigue activo en la aplicación y se conserva la copia anterior; exporta JSON antes de recargar. Sin cálculo de servidor.

Solo se conservan los valores introducidos en este navegador. No se guardan los resultados calculados ni los historiales.