Tallulah: Gestione Assiomatica di Modelli Reversibili

Riuscire ad annullare un’azione in un programma comporta numerosi vantaggi: uno dei quali è la maggiore semplicità nel rilevare problemi in fase di debugging. Mentre nei programmi sequenziali è sufficiente annullare ricorsivamente le ultime istruzioni eseguite, ciò non è possibile in un ambiente concorrente. Tra i diversi approcci proposti per i modelli da utilizzare in questo caso ne esiste uno chiamato Causal-Consistent Reversibility. La Causal Consistent Reversibility sostituisce il concetto di temporalità con quello di causalità. In letteratura è stato studiato un sistema assiomatico per dimostrare le proprietà della CausalConsistent Reversibility tramite assiomi più semplici da verificare. Nonostante ciò risulta comunque complicato verificare queste proprietà manualmente. In questo documento si espone Tallulah: uno strumento per la gestione di questi assiomi e proprietà.