En informática , la programación coreográfica es un paradigma de programación para sistemas distribuidos , donde los programas se escriben como composiciones de interacciones entre múltiples participantes concurrentes . [ 1 ] [ 2 ] [ 3 ]
El interbloqueo es un error común que puede ocurrir en sistemas distribuidos. La programación coreográfica garantiza que no se produzca un interbloqueo dentro del ámbito de la coreografía, asegurando que cada vez que se envía un mensaje desde una parte, se reciba uno correspondiente en el otro extremo.
Descripción general
Coreografías
En la programación coreográfica, los desarrolladores utilizan un lenguaje de programación coreográfica para definir el comportamiento de comunicación previsto de los participantes concurrentes. Los programas en este paradigma se denominan coreografías . [ 1 ] Los lenguajes coreográficos se inspiran en la notación de protocolos de seguridad (también conocida como notación "Alice and Bob"). La clave de estos lenguajes es la primitiva de comunicación, por ejemplo
Alice.expr -> Bob.x lee " Alicecomunica el resultado de evaluar la expresión expra Bob, que lo almacena en su variable local x". [ 3 ] Alice, Bob, etc. se denominan típicamente roles o procesos . [ 2 ]
El siguiente ejemplo muestra una coreografía para un protocolo de inicio de sesión único (SSO) simplificado basado en un Servicio de Autenticación Central (CAS) que involucra tres roles:
Client, que desea obtener un token de acceso paraCASinteractuar conService.Service, que necesita saberCASsi seClientle debe dar acceso.CAS, que es el Servicio Central de Autenticación responsable de comprobar lasClientcredenciales del usuario.
La coreografía es:
Cliente.(credenciales, ID de servicio) -> Solicitud de autenticación CAS Si CAS.check(authRequest) entonces CAS.token = genToken(authRequest) CAS.Éxito(token) -> Cliente.resultado CAS.Éxito(token) -> Servicio.resultado demás CAS.Failure -> Cliente.resultado CAS.Failure -> Service.result La coreografía comienza en la Línea 1, donde Clientcomunica un par formado por algunas credenciales y el identificador del servicio al que desea acceder CAS. CASAlmacena este par en su variable local authRequest(para la solicitud de autenticación). En la Línea 2, comprueba CASsi la solicitud es válida para obtener un token de autenticación. Si es así, genera un token y comunica un Successmensaje que contiene el token a ambos Client( ServiceLíneas 3-5). De lo contrario, CASinforma Clienta ambos Serviceque la autenticación falló, enviando un Failuremensaje (Líneas 7-8). Nos referiremos a esta coreografía como la "coreografía SSO" en lo que sigue.
Proyección de punto final
Una característica clave de la programación coreográfica es la capacidad de compilar coreografías en implementaciones distribuidas. Estas implementaciones pueden ser bibliotecas para software que necesita participar en una red informática siguiendo un protocolo, [ 1 ] [ 3 ] [ 4 ] o programas distribuidos independientes. [ 5 ] [ 6 ]
La traducción de una coreografía a programas distribuidos se denomina proyección de punto final (EPP, por sus siglas en inglés). [ 2 ] [ 3 ]
La proyección de punto final devuelve un programa para cada rol descrito en la coreografía de origen. [ 3 ] Por ejemplo, dada la coreografía anterior, la proyección de punto final devolvería tres programas: uno para Client, uno para Servicey uno para CAS. Se muestran a continuación en forma de pseudocódigo, donde sendy recvson primitivas para enviar y recibir mensajes hacia/desde otros roles.
Para cada rol, su código contiene las acciones que debe ejecutar para implementar la coreografía correctamente junto con los demás.
Desarrollo
El paradigma de la programación coreográfica tiene su origen en la tesis doctoral que le da nombre. [ 7 ] [ 8 ] [ 9 ] La inspiración para la sintaxis de los lenguajes de programación coreográfica se remonta a la notación de protocolos de seguridad , también conocida como notación "Alice and Bob". [ 1 ] La programación coreográfica también ha sido fuertemente influenciada por los estándares para la coreografía de servicios y los diagramas de interacción , así como por los desarrollos de la teoría de los cálculos de procesos . [ 1 ] [ 3 ] [ 10 ]
La programación coreográfica es un área de investigación activa. El paradigma se ha utilizado en el estudio del flujo de información , [ 11 ] computación paralela , [ 12 ] sistemas ciberfísicos , [ 13 ] [ 14 ] adaptación en tiempo de ejecución , [ 6 ] e integración de sistemas . [ 15 ]
Idiomas
- AIOCJ ( sitio web ). [ 6 ] Un lenguaje de programación coreográfico para sistemas adaptables que produce código en Jolie .
- Chor. [ 5 ] Un lenguaje de programación coreográfica de tipo sesión que se compilaba en microservicios en Jolie . Mientras tanto, fue reemplazado por Choral.
- Choral ( sitio web ). [ 16 ] [ 17 ] Un lenguaje de programación coreográfica orientado a objetos que se compila en bibliotecas en Java . Choral es el primer lenguaje de programación coreográfica con estructuras de datos descentralizadas y parámetros de orden superior.
- Chorex ( sitio web ). Una biblioteca de Elixir que proporciona un lenguaje de programación coreográfica integrado a través del sistema de macros de Elixir.
- ChoRus ( sitio web ). Programación coreográfica a nivel de biblioteca en Rust .
- Coreografías. [ 18 ] Un modelo teórico central para la programación coreográfica. Una implementación mecanizada está disponible en Rocq . [ 19 ] [ 20 ] [ 21 ]
- HasChor ( sitio web ). [ 22 ] Una biblioteca para programación coreográfica en Haskell .
- Kalas. [ 23 ] Un lenguaje de programación coreográfica con un compilador verificado para CakeML.
- Pirueta. [ 8 ] Una teoría de lenguaje de programación coreográfica mecanizada con procedimientos de orden superior.
- Klor ( sitio web ). Programación coreográfica a nivel de biblioteca en Clojure .
- Tempo ( sitio web ). Un lenguaje de programación coreográfica práctico que se compila en código fuente de biblioteca para múltiples lenguajes de destino.
Véase también
Referencias
- 1 2 3 4 5 Montesi, Fabrizio (2023). Introducción a las coreografías . Cambridge University Press. doi : 10.1017/9781108981491 . ISBN 978-1-108-83376-9. S2CID 102335067 .
- 1 2 3 Yoshida, Nobuko; Vasconcelos, Vasco T.; Padovani, Luca; Bono, Nicolás Ng; Neykova, Rumyana; Montesi, Fabricio; Mascardi, Viviana; Martín, Francisco; Johnsen, Einar Broch; Hu, Raymond; Giachino, Elena; Gesbert, Nils; Gay, Simón J.; Deniélou, Pierre-Malo; Castaña, Giuseppe; Campos, Juana; Bravetti, Mario; Bono, Viviana; Ancona, Davide (2016). "Tipos de comportamiento en lenguajes de programación" . Fundamentos y Tendencias en Lenguajes de Programación . 3 ( 2– 3): 95– 230. doi : 10.1561/2500000031 . hdl : 10044/1/44282 .
- 1 2 3 4 5 6 Giallorenzo, Saverio; Montesi, Fabricio; Peressotti, Marco; Richter, David; Salvaneschi, Guido; Weisenburger, Pascal (2021). Lenguajes multipartidistas: los casos coreográficos y multinivel (Perla) . Procedimientos internacionales de informática de Leibniz (LIPIcs). vol. 194. págs. 22:1–22:27. doi : 10.4230/LIPIcs.ECOOP.2021.22 . ISBN 9783959771900.(Artículo destacado de ECOOP 2021)
- ↑ Lenguaje de programación coral
- 1 2 Carbone, Marco; Montesi, Fabrizio (2013). "Deadlock-freedom-by-design" . Actas del 40.º simposio anual ACM SIGPLAN-SIGACT sobre Principios de los lenguajes de programación - POPL '13 . p. 263. doi : 10.1145/2429069.2429101 . ISBN 9781450318327. S2CID 15627190 .
- 1 2 3 Preda, Mila Dalla; Gabbrielli, Mauricio; Giallorenzo, Saverio; Lanese, Iván; Mauro, Jacopo (2017). «Coreografías Dinámicas: Teoría e Implementación» . Métodos lógicos en informática . 13 (2) 3263. arXiv : 1611.09067 . doi : 10.23638/LMCS-13(2:1)2017 . S2CID 5555662 .
- ↑ Montesi, Fabrizio (2013). Programación coreográfica (PDF) (Tesis doctoral). Universidad de Tecnologías de la Información de Copenhague. ISBN 978-87-7949-299-8.(Premio EAPLS a la mejor tesis doctoral)
- 1 2 Hirsch, Andrew K.; Garg, Deepak (16 de enero de 2022). "Pirouette: coreografías funcionales tipificadas de orden superior" . Actas de la ACM sobre lenguajes de programación . 6 (POPL): 1–27 . arXiv : 2111.03484 . doi : 10.1145/3498684 . S2CID 243833095 . (Artículo destacado de POPL 2022)
- ↑ Arend Rensink (30 de agosto de 2015). "Fabrizio Montesi gana el premio EAPLS a la mejor tesis doctoral de 2014" . Asociación Europea de Lenguajes y Sistemas de Programación.
- ↑ Carbone, Marco; Honda, Kohei; Yoshida, Nobuko (2012). "Programación centrada en la comunicación estructurada para servicios web" . ACM Transactions on Programming Languages and Systems . 34 (2): 1– 78. doi : 10.1145/2220365.2220367 . S2CID 15737118 .
- ↑ Lluch Lafuente, Alberto; Nielson, Flemming; Nielson, Hanne Riis (2015). "Control discrecional del flujo de información para especificaciones orientadas a la interacción" . Lógica, reescritura y concurrencia (PDF) . Notas de clase en informática. Vol. 9200. págs. 427–450 . doi : 10.1007/978-3-319-23165-5_20 . ISBN 978-3-319-23164-8. S2CID 32617923 .
- ↑ Cruz-Filipe, Luís; Montesi, Fabrizio (2016). "Coreografías en la práctica" . Técnicas formales para objetos, componentes y sistemas distribuidos . Lecture Notes in Computer Science. Vol. 9688. pp. 114–123 . arXiv : 1602.08863 . doi : 10.1007/978-3-319-39570-8_8 . ISBN 978-3-319-39569-2. S2CID 18067252 .
- ↑ López, Hugo A.; Heussen, Kai (2017). «Coreografía de sistemas de control distribuido ciberfísicos para el sector energético» . Actas del Simposio sobre Computación Aplicada . págs. 437–443 . doi : 10.1145/3019612.3019656 . ISBN 9781450344869. S2CID 39112346 .
- ↑ López, Hugo A.; Nielson, Flemming; Nielson, Hanne Riis (2016). «Garantizando la disponibilidad en sistemas de comunicación con detección de fallos» . Técnicas formales para objetos, componentes y sistemas distribuidos . Notas de clase en informática. Vol. 9688. pp. 195–211 . doi : 10.1007/978-3-319-39570-8_13 . ISBN 978-3-319-39569-2. S2CID 12872876 .
- ↑ Giallorenzo, Saverio; Lanese, Ivan; Russo, Daniel (2018). "ChIP: Un proceso de integración coreográfica" . En movimiento hacia sistemas de Internet significativos. Conferencias OTM 2018 (PDF) . Lecture Notes in Computer Science. Vol. 11230. pp. 22–40 . doi : 10.1007/978-3-030-02671-4_2 . ISBN 978-3-030-02670-7. S2CID 53015580 .
- ↑ Giallorenzo, Saverio; Montesi, Fabrizio; Peressotti, Marco (2024-01-16). "Choral: Programación coreográfica orientada a objetos" . ACM Trans. Program. Lang. Syst . 46 (1): 1:1–1:59. arXiv : 2005.09520 . doi : 10.1145/3632398 . ISSN 0164-0925 .
- ↑ Giallorenzo, Saverio; Montesi, Fabricio; Peressotti, Marco (19 de octubre de 2023). "Coral: Programación coreográfica orientada a objetos". arXiv : 2005.09520 [ cs.PL ].
- ↑ Cruz-Filipe, Luís; Montesi, Fabrizio (2020). "Un modelo central para la programación coreográfica" . Theoretical Computer Science . 802 : 38–66 . arXiv : 1510.03271 . doi : 10.1016/j.tcs.2019.07.005 . S2CID 199122777 .
- ↑ Cohen, Liron; Kaliszyk, Cezary (2021). Formalización de un lenguaje coreográfico Turing-completo en Coq . Actas Internacionales Leibniz en Informática (LIPIcs). Vol. 193. pp. 15:1–15:18. doi : 10.4230/LIPIcs.ITP.2021.15 . ISBN 9783959771887. S2CID 231802115 .
- ↑ Cruz-Filipe, Luís; Montesi, Fabricio; Peressotti, Marco (27 de mayo de 2023). "Una teoría formal de la programación coreográfica" . Revista de razonamiento automatizado . 67 (2): 21. arXiv : 2209.01886 . doi : 10.1007/s10817-023-09665-3 . ISSN 1573-0670 . S2CID 252090305 .
- ↑ Cruz-Filipe, Luís; Montesi, Fabricio; Peressotti, Marco (2021). Cerón, Antonio; Ölveczky, Peter Csaba (eds.). Certificando Recopilación de Coreografías . Apuntes de conferencias sobre informática. vol. 12819. Cham: Editorial Internacional Springer. págs. 115-133 . arXiv : 2102.10698 . doi : 10.1007/978-3-030-85315-0_8 . ISBN 978-3-030-85314-3. S2CID 231985665 . Consultado el 07-03-2022 .
{{cite book}}:|work=ignorado ( ayuda ) - ↑ Shen, Gan; Kashiwa, Shun; Kuper, Lindsey (31 de agosto de 2023). "HasChor: Programación coreográfica funcional para todos (Functional Pearl)" . Actas de la ACM sobre lenguajes de programación . 7 : 541–565 . arXiv : 2303.00924 . doi : 10.1145/3607849 .
- ↑ Pohjola, Johannes Åman; Gómez-Londoño, Alejandro; Shaker, James; Norrish, Michael (2022). Andronick, June; de Moura, Leonardo (eds.). "Kalas: Un compilador verificado de extremo a extremo para un lenguaje coreográfico" . XIII Conferencia Internacional sobre Demostración Interactiva de Teoremas (ITP 2022) . Actas Internacionales Leibniz en Informática (LIPIcs). 237. Dagstuhl, Alemania: Schloss Dagstuhl – Leibniz-Zentrum für Informatik: 27:1–27:18. doi : 10.4230/LIPIcs.ITP.2022.27 . ISBN 978-3-95977-252-5. S2CID 251322644 .
Enlaces externos
- www.choral-lang.org
- Computación concurrente
- paradigmas de programación