Timetide: Un Modelo de Programación para Sistemas Distribuidos Lógicamente Sincrónicos

Se han logrado grandes avances en modelos deterministas utilizando lenguajes sincrónicos. Se centran principalmente en aplicaciones centralizadas, ya que el enfoque tradicional es compilar la concurrencia. Los lenguajes activados por tiempo, como Giotto y Lingua Franca, son adecuados para la distribución a pesar de que dependen de la sincronización de relojes físicos, lo cual es costoso y puede sufrir problemas de escalabilidad. Por lo tanto, la programación determinista de sistemas distribuidos sigue siendo un desafío. Abordamos los desafíos de la distribución determinista desarrollando una nueva semántica de multiclock de programas sincrónicos. La semántica desarrollada es susceptible a una distribución sin problemas. Además, nuestro modelo de programación, Timetide, alivia la necesidad de sincronización de reloj físico al basarse en el modelo de sincronicidad lógica propuesto recientemente para sistemas distribuidos. Discutimos los aspectos importantes de la distribución de la computación, como los retrasos en la comunicación en red, y exploramos la verificación formal de los programas Timetide. Hasta donde sabemos, Timetide es el primer lenguaje sincrónico de multiclock que es tanto susceptible a la distribución como a la verificación formal sin la necesidad de sincronización de relojes físicos o conmutación de reloj.