Intentaremos escribir un programa que recuerde lo que ha estado haciendo hasta ahora y continúe hacia su objetivo si aborta una repetición. Este es un programa tenaz . Se utilizará una memoria no volátil para almacenar información a través de ejecuciones, como una serie de citas , que son bits con la cuenta de lo que sucede al abortar. Una vez conjeturé que con N cits , cualquier objetivo hasta la longitud 2 (NK) es alcanzable, para algunos pequeños K. fijos Ahora me inclino a pensar que el objetivo no se puede lograr :-(
Se le pide un programa tenaz con objetivo 01
, que ya es un objetivo no trivial ; o una prueba rigurosa de imposibilidad.
Un programa tenaz se define como uno que:
- Siempre que se ejecuta , se ejecuta a partir del mismo punto de entrada, sin entrada, y puede compartir información entre ejecuciones exclusivamente por medio de
N
cits (definidos a continuación); cualquier otra información tiene el mismo contenido al comienzo de cada ejecución, tiene contenido impredecible al inicio de la ejecución, no se puede cambiar (el programa en sí) o no se puede leer ( salida y valor anteriores ). - Es tal que cuando se ejecuta dentro de una sesión se detiene (usando una característica de su lenguaje), dentro de un retraso limitado desde el inicio de la ejecución, a menos que se cancele antes de detenerse; abort ocurre en cualquier instante arbitrario y evita la operación hasta otra ejecución (si la hay).
- Es tal que la concatenación en orden cronológico de los caracteres que genera es la misma cadena finita (el objetivo ) en cualquier sesión de arbitrariamente muchas ejecuciones que comprenden al menos una ejecución donde el programa se dejó en ejecución hasta que se detenga.
- Emite caracteres usando un dispositivo que atómicamente : recibe un valor entre 0 1 2 3 puesto por el programa y emite
0
(resp.1
) Para valores entre 0 o 2 (resp 1 o 3) si y solo si ese valor es diferente del anterior valor puesto, se supone que es 0 para el primer puesto en una sesión.
¡Existen programas tenaces! Cualquier programa que simplemente pone un número fijo de veces un valor fijo válido, luego se detiene, es tenaz con la meta vacía (si el número o el valor es 0), 0
(si el número es positivo y el valor es 2) o 1
(de lo contrario). Cualquier objetivo más largo requiere NVM.
Cada cit modela un bit NVM con la cuenta del efecto de una ejecución anulada durante una escritura en el cit. En cualquier instante un cit está en uno de los tres estados posibles 0
1
o U
. El valor leído de un cit siempre es 0 o 1; también coincide con el estado a menos que U
. Un cit se inicializa al estado 0
antes de la primera ejecución en una sesión y, de lo contrario, cambia de estado solo cuando el programa ordena una escritura , con efecto dependiendo de lo que está escrito, si la ejecución se cancela durante la escritura o no, y desde estado anterior de cit:
Former state 0 1 U Rationale given by hardware guru
Operation
Write 0 completed 0 0 0 Discharging returns cit to 0
Write 0 aborted 0 U U Aborted discharging leaves cit unspecified
Write 1 aborted U 1 U Aborted charging leaves cit unspecified
Write 1 completed 1 1 U Charging a non-discharged cit is inhibited
La HAL para lo anterior se declara en C como:
/* file "hal.h" unspecified parameter values give undefined behavior */
#define N 26 /* number of cits */
void p(unsigned v); /* put value v; v<4 */
unsigned r(unsigned i); /* read from cit at i; returns 0 or 1; i<N. */
void w(unsigned i, unsigned b); /* write b to cit at i; b is 0 or 1; i<N. */
/* all functions return in bounded time unless aborted */
Nuestro primer intento de un programa tenaz con objetivo 01
es:
#include "hal.h" /* discount this line's length */
main(){ /* entry point, no parameters or input */
if (r(3)==0) /* cit 3 read as 0, that is state 0 or U */
w(3,0), /* write 0 to cit 3, to ensure state 0 */
p(2); /* put 2 with output '0' initially */
w(3,1), /* mark we have output '0' (trouble spot!) */
p(1); /* put 1 with output '1' */
} /* halt (but we can be re-run) */
Murphy realiza una primera sesión, deja la primera carrera deteniéndose y finaliza la sesión; la salida de la sesión es la salida de una sola ejecución 01
; Hasta aquí todo bien.
En otra sesión, Murphy aborta una primera carrera w(3,1)
, dejando a cit en estado U
; en una segunda ejecución, Murphy decide que r(3)
es 1 (que cit está en estado U
), y deja el programa paralizado (observe cómo w(3,1)
no cambió el estado de cit); en una tercera carrera, Murphy decide que r(3)
es 0, aborta después p(2)
y termina la sesión.
La salida concatenada de la segunda sesión es 010
(un carácter por ejecución) pero es diferente de 01
la primera sesión, por lo tanto, el programa no es tenaz, ya que la condición 3 no se cumple.
El lenguaje es gratuito, adapte la interfaz C según el lenguaje. Seleccionaré la mejor respuesta según el menor número de citas utilizadas; luego el menor número de escrituras en el peor de los casos desde la ejecución hasta la salida (o se detiene si no hay salida); luego el menor número de escrituras antes de detenerse en una sesión sin abortar; entonces el programa más corto. Cuente solo el código de llamada, no la interfaz o su implementación, que no es necesaria. Una prueba rigurosa de imposibilidad eliminaría cualquier programa (y sería una sorpresa para mí) ; Seleccionaría el más simple de entender.
Verifique tres veces que el programa realmente cumpla con la meta según 3, independientemente de la cantidad y los instantes de abortos; ¡eso es difícil!
Actualización: agregué una respuesta candidata . Siéntase libre de derrotarlo. ¡Oh, Hammar hizo eso en minutos usando un programa sistemático!
Estado : hasta ahora no tenemos solución; sepa con certeza que no hay solución con 1 o 2 cits; pero no tiene prueba de imposibilidad con 3 o más cits. La declaración no se ha encontrado ambigua. El problema tendría una solución si cambiamos la matriz cit ligeramente (por ejemplo, poner 1 en la parte inferior derecha, en cuyo caso el ejemplo anterior es correcto).
fuente
Respuestas:
Si bien no tengo una solución ni una prueba de imposibilidad, pensé que publicaría mi arnés de prueba para cualquiera que quiera jugar con esto, ya que casi me he rendido en este momento.
Es una implementación de los programas de modelado HAL como una mónada Haskell. Comprueba la tenacidad haciendo una búsqueda amplia de las posibles sesiones para comprobar si las sesiones 1. se han detenido una vez sin producir la salida correcta, o 2. han producido una salida que no es un prefijo de la deseada (esto también atrapa programas que producen una salida infinita).
Aquí está el programa de ejemplo dado por el OP convertido a Haskell.
Y aquí está el resultado correspondiente, que muestra que el programa no es tenaz.
fuente
A menos que alguien pueda encontrar un error en este programa, creo que verifica y rechaza todos los programas relevantes de dos cit.
Sostengo que es suficiente considerar los programas que leen todos los cits y activan un número formado por el conjunto. Cada rama del interruptor será una serie de escrituras y puts. Nunca tiene sentido poner el mismo número más de una vez en una rama, o poner el segundo dígito de salida antes del primero. (Estoy moralmente seguro de que no hay ningún punto que muestre el primer dígito que no sea al comienzo de una rama o el segundo dígito que no sea al final, pero por ahora estoy evitando esa simplificación).
Luego, cada rama tiene un conjunto objetivo de cits que quiere establecer, y se mueve hacia él estableciendo los bits que quiere que sean 0 como 0, y los bits que quiere que sean 1 como 0 y luego 1; Estas operaciones de escritura se pueden ordenar de varias maneras. No tiene sentido establecer un bit en 1 a menos que ya lo haya establecido en 0 en esa ejecución, o es probable que sea un nop.
Considera 13680577296 posibles programas; Le tomó a una máquina de 4 núcleos un poco menos de 7 horas verificarlos a todos sin encontrar una sola solución.
fuente
Este
esmi mejor intento de responder a mi propia pregunta.No estoy seguro de que cumpla con el requisito 3, y estoy abierto a la refutación.No es tenaz :-(fuente
01
,: Cits110
. 2. Abortar durante el # 15. Cits:10U
. 3. Leerc = 1
, abortar durante el n. ° 12. Cits:U0U
. 4. Leac = 0
,d = 0
y el programa se imprimirá01
nuevamente.